improve precision of forall in constancy part of the monotonicity calculus
authorblanchet
Mon Dec 06 13:33:09 2010 +0100 (2010-12-06)
changeset 41012e5a23ffb5524
parent 41011 5c2f16eae066
child 41013 117345744f44
improve precision of forall in constancy part of the monotonicity calculus
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/Tools/Nitpick/nitpick_mono.ML
     1.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Dec 06 13:33:09 2010 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Dec 06 13:33:09 2010 +0100
     1.3 @@ -113,9 +113,9 @@
     1.4  ML {* const @{term "(\<lambda>x. (p\<Colon>'a\<Rightarrow>bool\<Rightarrow>bool) x False)"} *}
     1.5  ML {* const @{term "(\<lambda>x y. (p\<Colon>'a\<Rightarrow>'a\<Rightarrow>bool\<Rightarrow>bool) x y False)"} *}
     1.6  ML {* const @{term "f = (\<lambda>x\<Colon>'a. P x \<longrightarrow> Q x)"} *}
     1.7 +ML {* const @{term "\<forall>a\<Colon>'a. P a"} *}
     1.8  
     1.9  ML {* nonconst @{term "\<forall>P (a\<Colon>'a). P a"} *}
    1.10 -ML {* nonconst @{term "\<forall>a\<Colon>'a. P a"} *}
    1.11  ML {* nonconst @{term "THE x\<Colon>'a. P x"} *}
    1.12  ML {* nonconst @{term "SOME x\<Colon>'a. P x"} *}
    1.13  ML {* nonconst @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) = myunion"} *}
    1.14 @@ -199,9 +199,9 @@
    1.15    in thy |> theorems_of |> List.app check_theorem end
    1.16  *}
    1.17  
    1.18 -(*
    1.19  ML {* getenv "ISABELLE_TMP" *}
    1.20  
    1.21 +(*
    1.22  (* ML {* check_theory @{theory AVL2} *} *)
    1.23  ML {* check_theory @{theory Fun} *}
    1.24  (* ML {* check_theory @{theory Huffman} *} *)
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     2.3 @@ -790,10 +790,11 @@
     2.4      fun do_all T (gamma, cset) =
     2.5        let
     2.6          val abs_M = mtype_for (domain_type (domain_type T))
     2.7 +        val x = Unsynchronized.inc max_fresh
     2.8          val body_M = mtype_for (body_type T)
     2.9        in
    2.10 -        (MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M),
    2.11 -         (gamma, cset |> add_mtype_is_complete [] abs_M))
    2.12 +        (MFun (MFun (abs_M, V x, body_M), A Gen, body_M),
    2.13 +         (gamma, cset |> add_mtype_is_complete [(x, (Plus, Tru))] abs_M))
    2.14        end
    2.15      fun do_equals T (gamma, cset) =
    2.16        let