# HG changeset patch
# User blanchet
# Date 1291638789 -3600
# Node ID e538a4f9dd86fe6e89d7cce490a65c35670eab88
# Parent  117345744f44e0363cd311aafe925fa149760d90
add more flexibility to the monotonicity calculus: instead of hardcoding F-arrows, also allow G-arrows, simulating applications of the Sub rule

diff -r 117345744f44 -r e538a4f9dd86 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- 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
diff -r 117345744f44 -r e538a4f9dd86 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- 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,