Quelle  Mono_Nits.thy

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

Examples featuring Nitpick's monotonicity check.
*)

section ‹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 ‹
  Nitpick_Util
  Nitpick_HOL
  Nitpick_Preproc

  BUG

  thy = 🍋
  ctxt = 🍋
  subst = []
  tac_timeout = seconds 1.0
  case_names = case_const_names ctxt
  defs = all_defs_of thy subst
  nondefs = all_nondefs_of ctxt subst
  def_tables = const_def_tables ctxt subst defs
  nondef_table = const_nondef_table nondefs
  simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
  psimp_table = const_psimp_table ctxt subst
  choice_spec_table = const_choice_spec_table ctxt subst
  intro_table = inductive_intro_table ctxt subst def_tables
  ground_thm_table = ground_theorem_table thy
  ersatz_table = ersatz_table ctxt
  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 []}
  binarize = false

  is_mono t =
 Nitpick_Mono.formulas_monotonic hol_ctxt binarize 🍋‹'a› ([t], [])

  is_const t =
 let val T = fastype_of t in
 Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t), 🍋‹False›)
 |> is_mono
 end

  mono t = is_mono t orelse raise BUG
  nonmono t = not (is_mono t) orelse raise BUG
  const t = is_const t orelse raise BUG
  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 ‹
  preproc_timeout = seconds 5.0
  mono_timeout = seconds 1.0

  is_forbidden_theorem name =
 Long_Name.count 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

  theorems_of thy =
 filter (fn ((name, _), th) =>
 not (is_forbidden_theorem name) andalso
 Thm.theory_long_name th = Context.theory_long_name thy)
 (Global_Theory.all_thms_of thy true)

  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) =
 Timeout.apply 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
 catch Timeout.TIMEOUT _ => "TIMEOUT"
 | NOT_SUPPORTED _ => "UNSUP"
 | _ => "UNKNOWN"
 ›

  check_theory thy =
 let
 val path = File.tmp_path (Context.theory_base_name thy ^ ".out" |> Path.explode)
 val _ = File.write path ""
 fun check_theorem (name, th) =
 let
 val t = th |> Thm.prop_of |> Type.legacy_freeze |> close_form
 val neg_t = Logic.mk_implies (t, prop‹False›)
 val (nondef_ts, def_ts, _, _, _, _) =
 Timeout.apply preproc_timeout (preprocess_formulas hol_ctxt [])
 neg_t
 val res = Thm_Name.print name ^ ": " ^ check_formulas (nondef_ts, def_ts)
 in File.append path (res ^ "\n"); writeln res end
 handle Timeout.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} *}
*)

end