add more flexibility to the monotonicity calculus: instead of hardcoding F-arrows, also allow G-arrows, simulating applications of the Sub rule
authorblanchet
Mon Dec 06 13:33:09 2010 +0100 (2010-12-06)
changeset 41014e538a4f9dd86
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
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 @@ -8,9 +8,24 @@
     1.4  header {* Examples Featuring Nitpick's Monotonicity Check *}
     1.5  
     1.6  theory Mono_Nits
     1.7 -imports Main
     1.8 +imports Nitpick2d(*###*) "~/afp/thys/AVL-Trees/AVL2" "~/afp/thys/Huffman/Huffman"
     1.9  begin
    1.10  
    1.11 +(* ML {* Nitpick_Mono.first_calculus := false *} *)
    1.12 +ML {* Nitpick_Mono.trace := true *}
    1.13 +
    1.14 +thm alphabet.simps
    1.15 +
    1.16 +fun alphabetx where
    1.17 +"alphabetx (Leaf w a) = {a}" |
    1.18 +"alphabetx (InnerNode w t\<^isub>1 t\<^isub>2) = alphabetx t\<^isub>1 \<union> alphabetx t\<^isub>2"
    1.19 +
    1.20 +lemma "\<exists>a. alphabetx (t::'a tree) (a::'a)"
    1.21 +nitpick [debug, card = 1-2, dont_box, dont_finitize, dont_destroy_constrs]
    1.22 +
    1.23 +lemma "consistent t \<Longrightarrow> \<exists>a\<in>alphabet t. depth t a = Huffman.height t"
    1.24 +nitpick [debug, card = 1-2, dont_box, dont_finitize]
    1.25 +
    1.26  ML {*
    1.27  open Nitpick_Util
    1.28  open Nitpick_HOL
    1.29 @@ -67,6 +82,7 @@
    1.30  ML {* Nitpick_Mono.trace := false *}
    1.31  
    1.32  ML {* const @{term "A\<Colon>('a\<Rightarrow>'b)"} *}
    1.33 +(*
    1.34  ML {* const @{term "(A\<Colon>'a set) = A"} *}
    1.35  ML {* const @{term "(A\<Colon>'a set set) = A"} *}
    1.36  ML {* const @{term "(\<lambda>x\<Colon>'a set. x a)"} *}
    1.37 @@ -137,6 +153,7 @@
    1.38  
    1.39  ML {* nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"} *}
    1.40  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"} *}
    1.41 +*)
    1.42  
    1.43  ML {*
    1.44  val preproc_timeout = SOME (seconds 5.0)
    1.45 @@ -182,8 +199,8 @@
    1.46  
    1.47  fun check_theory thy =
    1.48    let
    1.49 -    val finitizes = [(NONE, NONE)]
    1.50 -    val monos = [(NONE, NONE)]
    1.51 +    val finitizes = [(NONE, SOME false)]
    1.52 +    val monos = [(NONE, SOME false)]
    1.53      val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode)
    1.54      val _ = File.write path ""
    1.55      fun check_theorem (name, th) =
    1.56 @@ -201,13 +218,11 @@
    1.57  
    1.58  ML {* getenv "ISABELLE_TMP" *}
    1.59  
    1.60 -(*
    1.61 -(* ML {* check_theory @{theory AVL2} *} *)
    1.62 +ML {* check_theory @{theory AVL2} *}
    1.63  ML {* check_theory @{theory Fun} *}
    1.64 -(* ML {* check_theory @{theory Huffman} *} *)
    1.65 +ML {* check_theory @{theory Huffman} *}
    1.66  ML {* check_theory @{theory List} *}
    1.67  ML {* check_theory @{theory Map} *}
    1.68  ML {* check_theory @{theory Relation} *}
    1.69 -*)
    1.70  
    1.71  end
     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 @@ -800,11 +800,11 @@
     2.4      fun do_equals T (gamma, cset) =
     2.5        let
     2.6          val M = mtype_for (domain_type T)
     2.7 -        val aa = V (Unsynchronized.inc max_fresh)
     2.8 +        val x = Unsynchronized.inc max_fresh
     2.9        in
    2.10 -        (MFun (M, A Gen, MFun (M, aa, mtype_for (nth_range_type 2 T))),
    2.11 +        (MFun (M, A Gen, MFun (M, V x, mtype_for (nth_range_type 2 T))),
    2.12           (gamma, cset |> add_mtype_is_concrete [] M
    2.13 -                      |> add_annotation_atom_comp Leq [] (A Fls) aa))
    2.14 +                      |> add_annotation_atom_comp Leq [] (A Fls) (V x)))
    2.15        end
    2.16      fun do_robust_set_operation T (gamma, cset) =
    2.17        let
    2.18 @@ -980,8 +980,13 @@
    2.19                SOME t' =>
    2.20                let
    2.21                  val M = mtype_for T
    2.22 -                val (m', accum) = do_term t' (accum |>> push_bound (A Fls) T M)
    2.23 -              in (MAbs (s, T, M, A Fls, m'), accum |>> pop_bound) end
    2.24 +                val x = Unsynchronized.inc max_fresh
    2.25 +                val (m', accum) = do_term t' (accum |>> push_bound (V x) T M)
    2.26 +              in
    2.27 +                (MAbs (s, T, M, V x, m'),
    2.28 +                 accum |>> pop_bound
    2.29 +                       ||> add_annotation_atom_comp Leq [] (A Fls) (V x))
    2.30 +              end
    2.31              | NONE =>
    2.32                ((case t' of
    2.33                    t1' $ Bound 0 =>
    2.34 @@ -999,10 +1004,10 @@
    2.35                 handle SAME () =>
    2.36                        let
    2.37                          val M = mtype_for T
    2.38 -                        val aa = V (Unsynchronized.inc max_fresh)
    2.39 +                        val x = Unsynchronized.inc max_fresh
    2.40                          val (m', accum) =
    2.41 -                          do_term t' (accum |>> push_bound aa T M)
    2.42 -                      in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end))
    2.43 +                          do_term t' (accum |>> push_bound (V x) T M)
    2.44 +                      in (MAbs (s, T, M, V x, m'), accum |>> pop_bound) end))
    2.45           | @{const Not} $ t1 => do_connect imp_triple t1 @{const False} accum
    2.46           | @{const conj} $ t1 $ t2 => do_connect conj_triple t1 t2 accum
    2.47           | @{const disj} $ t1 $ t2 => do_connect disj_triple t1 t2 accum
    2.48 @@ -1051,14 +1056,14 @@
    2.49      val accum = accum ||> add_mtypes_equal M1 M2
    2.50      val body_M = fresh_mtype_for_type mdata false (nth_range_type 2 T)
    2.51      val m = MApp (MApp (MRaw (Const x,
    2.52 -                           MFun (M1, A Gen, MFun (M2, A Fls, body_M))), m1), m2)
    2.53 +                           MFun (M1, A Gen, MFun (M2, A Gen, body_M))), m1), m2)
    2.54    in
    2.55 -    (m, if def then
    2.56 -          let val (head_m, arg_ms) = strip_mcomb m1 in
    2.57 -            accum ||> force_gen_funs (length arg_ms) (mtype_of_mterm head_m)
    2.58 -          end
    2.59 -        else
    2.60 -          accum)
    2.61 +    (m, (if def then
    2.62 +           let val (head_m, arg_ms) = strip_mcomb m1 in
    2.63 +             accum ||> force_gen_funs (length arg_ms) (mtype_of_mterm head_m)
    2.64 +           end
    2.65 +         else
    2.66 +           accum))
    2.67    end
    2.68  
    2.69  fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, max_fresh,