author blanchet Mon, 06 Dec 2010 13:33:09 +0100 changeset 41012 e5a23ffb5524 parent 41011 5c2f16eae066 child 41013 117345744f44
improve precision of forall in constancy part of the monotonicity calculus
```--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Dec 06 13:33:09 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Dec 06 13:33:09 2010 +0100
@@ -113,9 +113,9 @@
ML {* const @{term "(\<lambda>x. (p\<Colon>'a\<Rightarrow>bool\<Rightarrow>bool) x False)"} *}
ML {* const @{term "(\<lambda>x y. (p\<Colon>'a\<Rightarrow>'a\<Rightarrow>bool\<Rightarrow>bool) x y False)"} *}
ML {* const @{term "f = (\<lambda>x\<Colon>'a. P x \<longrightarrow> Q x)"} *}
+ML {* const @{term "\<forall>a\<Colon>'a. P a"} *}

ML {* nonconst @{term "\<forall>P (a\<Colon>'a). P a"} *}
-ML {* nonconst @{term "\<forall>a\<Colon>'a. P a"} *}
ML {* nonconst @{term "THE x\<Colon>'a. P x"} *}
ML {* nonconst @{term "SOME x\<Colon>'a. P x"} *}
ML {* nonconst @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) = myunion"} *}
@@ -199,9 +199,9 @@
in thy |> theorems_of |> List.app check_theorem end
*}

-(*
ML {* getenv "ISABELLE_TMP" *}

+(*
(* ML {* check_theory @{theory AVL2} *} *)
ML {* check_theory @{theory Fun} *}
(* ML {* check_theory @{theory Huffman} *} *)```
```--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
@@ -790,10 +790,11 @@
fun do_all T (gamma, cset) =
let
val abs_M = mtype_for (domain_type (domain_type T))
+        val x = Unsynchronized.inc max_fresh
val body_M = mtype_for (body_type T)
in
-        (MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M),
-         (gamma, cset |> add_mtype_is_complete [] abs_M))
+        (MFun (MFun (abs_M, V x, body_M), A Gen, body_M),
+         (gamma, cset |> add_mtype_is_complete [(x, (Plus, Tru))] abs_M))
end
fun do_equals T (gamma, cset) =
let```