Theory Mono_Nits

theory Mono_Nits
imports Main
(*  Title:      HOL/Nitpick_Examples/Mono_Nits.thy
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2009-2011

Examples featuring Nitpick's monotonicity check.
*)

header {* Examples Featuring Nitpick's Monotonicity Check *}

theory Mono_Nits
imports Main
        (* "~/afp/thys/DPT-SAT-Solver/DPT_SAT_Solver" *)
        (* "~/afp/thys/AVL-Trees/AVL2" "~/afp/thys/Huffman/Huffman" *)
begin

ML {*
open Nitpick_Util
open Nitpick_HOL
open Nitpick_Preproc

exception BUG

val thy = @{theory}
val ctxt = @{context}
val subst = []
val tac_timeout = seconds 1.0
val case_names = case_const_names ctxt
val defs = all_defs_of thy subst
val nondefs = all_nondefs_of ctxt subst
val def_tables = const_def_tables ctxt subst defs
val nondef_table = const_nondef_table nondefs
val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
val psimp_table = const_psimp_table ctxt subst
val choice_spec_table = const_choice_spec_table ctxt subst
val intro_table = inductive_intro_table ctxt subst def_tables
val ground_thm_table = ground_theorem_table thy
val ersatz_table = ersatz_table ctxt
val hol_ctxt as {thy, ...} : hol_context =
  {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [], wfs = [],
   user_axioms = NONE, debug = false, whacks = [], binary_ints = SOME false,
   destroy_constrs = true, specialize = false, star_linear_preds = false,
   total_consts = NONE, needs = NONE, tac_timeout = tac_timeout, evals = [],
   case_names = case_names, def_tables = def_tables,
   nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table,
   psimp_table = psimp_table, choice_spec_table = choice_spec_table,
   intro_table = intro_table, ground_thm_table = ground_thm_table,
   ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
   special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
   wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
val binarize = false

fun is_mono t =
  Nitpick_Mono.formulas_monotonic hol_ctxt binarize @{typ 'a} ([t], [])

fun is_const t =
  let val T = fastype_of t in
    Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t), @{const False})
    |> is_mono
  end

fun mono t = is_mono t orelse raise BUG
fun nonmono t = not (is_mono t) orelse raise BUG
fun const t = is_const t orelse raise BUG
fun nonconst t = not (is_const t) orelse raise BUG
*}

ML {* Nitpick_Mono.trace := false *}

ML_val {* const @{term "A::('a=>'b)"} *}
ML_val {* const @{term "(A::'a set) = A"} *}
ML_val {* const @{term "(A::'a set set) = A"} *}
ML_val {* const @{term "(λx::'a set. a ∈ x)"} *}
ML_val {* const @{term "{{a::'a}} = C"} *}
ML_val {* const @{term "{f::'a=>nat} = {g::'a=>nat}"} *}
ML_val {* const @{term "A ∪ (B::'a set)"} *}
ML_val {* const @{term "λA B x::'a. A x ∨ B x"} *}
ML_val {* const @{term "P (a::'a)"} *}
ML_val {* const @{term "λa::'a. b (c (d::'a)) (e::'a) (f::'a)"} *}
ML_val {* const @{term "∀A::'a set. a ∈ A"} *}
ML_val {* const @{term "∀A::'a set. P A"} *}
ML_val {* const @{term "P ∨ Q"} *}
ML_val {* const @{term "A ∪ B = (C::'a set)"} *}
ML_val {* const @{term "(λA B x::'a. A x ∨ B x) A B = C"} *}
ML_val {* const @{term "(if P then (A::'a set) else B) = C"} *}
ML_val {* const @{term "let A = (C::'a set) in A ∪ B"} *}
ML_val {* const @{term "THE x::'b. P x"} *}
ML_val {* const @{term "(λx::'a. False)"} *}
ML_val {* const @{term "(λx::'a. True)"} *}
ML_val {* const @{term "(λx::'a. False) = (λx::'a. False)"} *}
ML_val {* const @{term "(λx::'a. True) = (λx::'a. True)"} *}
ML_val {* const @{term "Let (a::'a) A"} *}
ML_val {* const @{term "A (a::'a)"} *}
ML_val {* const @{term "insert (a::'a) A = B"} *}
ML_val {* const @{term "- (A::'a set)"} *}
ML_val {* const @{term "finite (A::'a set)"} *}
ML_val {* const @{term "¬ finite (A::'a set)"} *}
ML_val {* const @{term "finite (A::'a set set)"} *}
ML_val {* const @{term "λa::'a. A a ∧ ¬ B a"} *}
ML_val {* const @{term "A < (B::'a set)"} *}
ML_val {* const @{term "A ≤ (B::'a set)"} *}
ML_val {* const @{term "[a::'a]"} *}
ML_val {* const @{term "[a::'a set]"} *}
ML_val {* const @{term "[A ∪ (B::'a set)]"} *}
ML_val {* const @{term "[A ∪ (B::'a set)] = [C]"} *}
ML_val {* const @{term "{(λx::'a. x = a)} = C"} *}
ML_val {* const @{term "(λa::'a. ¬ A a) = B"} *}
ML_val {* const @{prop "∀F f g (h::'a set). F f ∧ F g ∧ ¬ f a ∧ g a --> ¬ f a"} *}
ML_val {* const @{term "λA B x::'a. A x ∧ B x ∧ A = B"} *}
ML_val {* const @{term "p = (λ(x::'a) (y::'a). P x ∨ ¬ Q y)"} *}
ML_val {* const @{term "p = (λ(x::'a) (y::'a). p x y :: bool)"} *}
ML_val {* const @{term "p = (λA B x. A x ∧ ¬ B x) (λx. True) (λy. x ≠ y)"} *}
ML_val {* const @{term "p = (λy. x ≠ y)"} *}
ML_val {* const @{term "(λx. (p::'a=>bool=>bool) x False)"} *}
ML_val {* const @{term "(λx y. (p::'a=>'a=>bool=>bool) x y False)"} *}
ML_val {* const @{term "f = (λx::'a. P x --> Q x)"} *}
ML_val {* const @{term "∀a::'a. P a"} *}

ML_val {* nonconst @{term "∀P (a::'a). P a"} *}
ML_val {* nonconst @{term "THE x::'a. P x"} *}
ML_val {* nonconst @{term "SOME x::'a. P x"} *}
ML_val {* nonconst @{term "(λA B x::'a. A x ∨ B x) = myunion"} *}
ML_val {* nonconst @{term "(λx::'a. False) = (λx::'a. True)"} *}
ML_val {* nonconst @{prop "∀F f g (h::'a set). F f ∧ F g ∧ ¬ a ∈ f ∧ a ∈ g --> F h"} *}

ML_val {* mono @{prop "Q (∀x::'a set. P x)"} *}
ML_val {* mono @{prop "P (a::'a)"} *}
ML_val {* mono @{prop "{a} = {b::'a}"} *}
ML_val {* mono @{prop "(λx. x = a) = (λy. y = (b::'a))"} *}
ML_val {* mono @{prop "(a::'a) ∈ P ∧ P ∪ P = P"} *}
ML_val {* mono @{prop "∀F::'a set set. P"} *}
ML_val {* mono @{prop "¬ (∀F f g (h::'a set). F f ∧ F g ∧ ¬ a ∈ f ∧ a ∈ g --> F h)"} *}
ML_val {* mono @{prop "¬ Q (∀x::'a set. P x)"} *}
ML_val {* mono @{prop "¬ (∀x::'a. P x)"} *}
ML_val {* mono @{prop "myall P = (P = (λx::'a. True))"} *}
ML_val {* mono @{prop "myall P = (P = (λx::'a. False))"} *}
ML_val {* mono @{prop "∀x::'a. P x"} *}
ML_val {* mono @{term "(λA B x::'a. A x ∨ B x) ≠ myunion"} *}

ML_val {* nonmono @{prop "A = (λx::'a. True) ∧ A = (λx. False)"} *}
ML_val {* nonmono @{prop "∀F f g (h::'a set). F f ∧ F g ∧ ¬ a ∈ f ∧ a ∈ g --> F h"} *}

ML {*
val preproc_timeout = seconds 5.0
val mono_timeout = seconds 1.0

fun is_forbidden_theorem name =
  length (Long_Name.explode name) <> 2 orelse
  String.isPrefix "type_definition" (List.last (Long_Name.explode name)) orelse
  String.isPrefix "arity_" (List.last (Long_Name.explode name)) orelse
  String.isSuffix "_def" name orelse
  String.isSuffix "_raw" name

fun theorems_of thy =
  filter (fn (name, th) =>
             not (is_forbidden_theorem name) andalso
             (theory_of_thm th, thy) |> pairself Context.theory_name |> op =)
         (Global_Theory.all_thms_of thy true)

fun check_formulas tsp =
  let
    fun is_type_actually_monotonic T =
      Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp
    val free_Ts = fold Term.add_tfrees (op @ tsp) [] |> map TFree
    val (mono_free_Ts, nonmono_free_Ts) =
      TimeLimit.timeLimit mono_timeout
          (List.partition is_type_actually_monotonic) free_Ts
  in
    if not (null mono_free_Ts) then "MONO"
    else if not (null nonmono_free_Ts) then "NONMONO"
    else "NIX"
  end
  handle TimeLimit.TimeOut => "TIMEOUT"
       | NOT_SUPPORTED _ => "UNSUP"
       | exn => if Exn.is_interrupt exn then reraise exn else "UNKNOWN"

fun check_theory thy =
  let
    val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode)
    val _ = File.write path ""
    fun check_theorem (name, th) =
      let
        val t = th |> prop_of |> Type.legacy_freeze |> close_form
        val neg_t = Logic.mk_implies (t, @{prop False})
        val (nondef_ts, def_ts, _, _, _, _) =
          TimeLimit.timeLimit preproc_timeout (preprocess_formulas hol_ctxt [])
                              neg_t
        val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
      in File.append path (res ^ "\n"); writeln res end
      handle TimeLimit.TimeOut => ()
  in thy |> theorems_of |> List.app check_theorem end
*}

(*
ML_val {* check_theory @{theory AVL2} *}
ML_val {* check_theory @{theory Fun} *}
ML_val {* check_theory @{theory Huffman} *}
ML_val {* check_theory @{theory List} *}
ML_val {* check_theory @{theory Map} *}
ML_val {* check_theory @{theory Relation} *}
*)

ML {* getenv "ISABELLE_TMP" *}

end