author blanchet Mon, 06 Dec 2010 13:33:09 +0100 changeset 41014 e538a4f9dd86 parent 41013 117345744f44 child 41015 3eeb25d953d2
add more flexibility to the monotonicity calculus: instead of hardcoding F-arrows, also allow G-arrows, simulating applications of the Sub rule
```--- 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
@@ -8,9 +8,24 @@
header {* Examples Featuring Nitpick's Monotonicity Check *}

theory Mono_Nits
-imports Main
+imports Nitpick2d(*###*) "~/afp/thys/AVL-Trees/AVL2" "~/afp/thys/Huffman/Huffman"
begin

+(* ML {* Nitpick_Mono.first_calculus := false *} *)
+ML {* Nitpick_Mono.trace := true *}
+
+thm alphabet.simps
+
+fun alphabetx where
+"alphabetx (Leaf w a) = {a}" |
+"alphabetx (InnerNode w t\<^isub>1 t\<^isub>2) = alphabetx t\<^isub>1 \<union> alphabetx t\<^isub>2"
+
+lemma "\<exists>a. alphabetx (t::'a tree) (a::'a)"
+nitpick [debug, card = 1-2, dont_box, dont_finitize, dont_destroy_constrs]
+
+lemma "consistent t \<Longrightarrow> \<exists>a\<in>alphabet t. depth t a = Huffman.height t"
+nitpick [debug, card = 1-2, dont_box, dont_finitize]
+
ML {*
open Nitpick_Util
open Nitpick_HOL
@@ -67,6 +82,7 @@
ML {* Nitpick_Mono.trace := false *}

ML {* const @{term "A\<Colon>('a\<Rightarrow>'b)"} *}
+(*
ML {* const @{term "(A\<Colon>'a set) = A"} *}
ML {* const @{term "(A\<Colon>'a set set) = A"} *}
ML {* const @{term "(\<lambda>x\<Colon>'a set. x a)"} *}
@@ -137,6 +153,7 @@

ML {* nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"} *}
ML {* nonmono @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h"} *}
+*)

ML {*
val preproc_timeout = SOME (seconds 5.0)
@@ -182,8 +199,8 @@

fun check_theory thy =
let
-    val finitizes = [(NONE, NONE)]
-    val monos = [(NONE, NONE)]
+    val finitizes = [(NONE, SOME false)]
+    val monos = [(NONE, SOME false)]
val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode)
val _ = File.write path ""
fun check_theorem (name, th) =
@@ -201,13 +218,11 @@

ML {* getenv "ISABELLE_TMP" *}

-(*
-(* ML {* check_theory @{theory AVL2} *} *)
+ML {* check_theory @{theory AVL2} *}
ML {* check_theory @{theory Fun} *}
-(* ML {* check_theory @{theory Huffman} *} *)
+ML {* check_theory @{theory Huffman} *}
ML {* check_theory @{theory List} *}
ML {* check_theory @{theory Map} *}
ML {* check_theory @{theory Relation} *}
-*)

end```
```--- 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
@@ -800,11 +800,11 @@
fun do_equals T (gamma, cset) =
let
val M = mtype_for (domain_type T)
-        val aa = V (Unsynchronized.inc max_fresh)
+        val x = Unsynchronized.inc max_fresh
in
-        (MFun (M, A Gen, MFun (M, aa, mtype_for (nth_range_type 2 T))),
+        (MFun (M, A Gen, MFun (M, V x, mtype_for (nth_range_type 2 T))),
(gamma, cset |> add_mtype_is_concrete [] M
-                      |> add_annotation_atom_comp Leq [] (A Fls) aa))
+                      |> add_annotation_atom_comp Leq [] (A Fls) (V x)))
end
fun do_robust_set_operation T (gamma, cset) =
let
@@ -980,8 +980,13 @@
SOME t' =>
let
val M = mtype_for T
-                val (m', accum) = do_term t' (accum |>> push_bound (A Fls) T M)
-              in (MAbs (s, T, M, A Fls, m'), accum |>> pop_bound) end
+                val x = Unsynchronized.inc max_fresh
+                val (m', accum) = do_term t' (accum |>> push_bound (V x) T M)
+              in
+                (MAbs (s, T, M, V x, m'),
+                 accum |>> pop_bound
+                       ||> add_annotation_atom_comp Leq [] (A Fls) (V x))
+              end
| NONE =>
((case t' of
t1' \$ Bound 0 =>
@@ -999,10 +1004,10 @@
handle SAME () =>
let
val M = mtype_for T
-                        val aa = V (Unsynchronized.inc max_fresh)
+                        val x = Unsynchronized.inc max_fresh
val (m', accum) =
-                          do_term t' (accum |>> push_bound aa T M)
-                      in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end))
+                          do_term t' (accum |>> push_bound (V x) T M)
+                      in (MAbs (s, T, M, V x, m'), accum |>> pop_bound) end))
| @{const Not} \$ t1 => do_connect imp_triple t1 @{const False} accum
| @{const conj} \$ t1 \$ t2 => do_connect conj_triple t1 t2 accum
| @{const disj} \$ t1 \$ t2 => do_connect disj_triple t1 t2 accum
@@ -1051,14 +1056,14 @@
val accum = accum ||> add_mtypes_equal M1 M2
val body_M = fresh_mtype_for_type mdata false (nth_range_type 2 T)
val m = MApp (MApp (MRaw (Const x,
-                           MFun (M1, A Gen, MFun (M2, A Fls, body_M))), m1), m2)
+                           MFun (M1, A Gen, MFun (M2, A Gen, body_M))), m1), m2)
in
-    (m, if def then
-          let val (head_m, arg_ms) = strip_mcomb m1 in
-            accum ||> force_gen_funs (length arg_ms) (mtype_of_mterm head_m)
-          end
-        else
-          accum)
+    (m, (if def then
+           let val (head_m, arg_ms) = strip_mcomb m1 in
+             accum ||> force_gen_funs (length arg_ms) (mtype_of_mterm head_m)
+           end
+         else
+           accum))
end

fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, max_fresh,```