Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nitpick_Examples/Mono_Nits.thy
changeset 63167 0909deb8059b
parent 62519 a564458f94db
child 65458 cf504b7a7aa7
equal deleted inserted replaced
63166:143f58bb34f9 63167:0909deb8059b 
     3     Copyright   2009-2011
 
     3     Copyright   2009-2011
 
     4 
     4 
     5 Examples featuring Nitpick's monotonicity check.
 
     5 Examples featuring Nitpick's monotonicity check.
 
     6 *)
 
     6 *)
 
     7 
     7 
     8 section {* Examples Featuring Nitpick's Monotonicity Check *}
 
     8 section \<open>Examples Featuring Nitpick's Monotonicity Check\<close>
 
     9 
     9 
    10 theory Mono_Nits
 
    10 theory Mono_Nits
 
    11 imports Main
 
    11 imports Main
 
    12         (* "~/afp/thys/DPT-SAT-Solver/DPT_SAT_Solver" *)
 
    12         (* "~/afp/thys/DPT-SAT-Solver/DPT_SAT_Solver" *)
 
    13         (* "~/afp/thys/AVL-Trees/AVL2" "~/afp/thys/Huffman/Huffman" *)
 
    13         (* "~/afp/thys/AVL-Trees/AVL2" "~/afp/thys/Huffman/Huffman" *)
 
    14 begin
 
    14 begin
 
    15 
    15 
    16 ML {*
 
    16 ML \<open>
 
    17 open Nitpick_Util
 
    17 open Nitpick_Util
 
    18 open Nitpick_HOL
 
    18 open Nitpick_HOL
 
    19 open Nitpick_Preproc
 
    19 open Nitpick_Preproc
 
    20 
    20 
    21 exception BUG
 
    21 exception BUG
 
    60 
    60 
    61 fun mono t = is_mono t orelse raise BUG
 
    61 fun mono t = is_mono t orelse raise BUG
 
    62 fun nonmono t = not (is_mono t) orelse raise BUG
 
    62 fun nonmono t = not (is_mono t) orelse raise BUG
 
    63 fun const t = is_const t orelse raise BUG
 
    63 fun const t = is_const t orelse raise BUG
 
    64 fun nonconst t = not (is_const t) orelse raise BUG
 
    64 fun nonconst t = not (is_const t) orelse raise BUG
 
    65 *}
 
    65 \<close>
 
    66 
    66 
    67 ML {* Nitpick_Mono.trace := false *}
 
    67 ML \<open>Nitpick_Mono.trace := false\<close>
 
    68 
    68 
    69 ML_val {* const @{term "A::('a\<Rightarrow>'b)"} *}
 
    69 ML_val \<open>const @{term "A::('a\<Rightarrow>'b)"}\<close>
 
    70 ML_val {* const @{term "(A::'a set) = A"} *}
 
    70 ML_val \<open>const @{term "(A::'a set) = A"}\<close>
 
    71 ML_val {* const @{term "(A::'a set set) = A"} *}
 
    71 ML_val \<open>const @{term "(A::'a set set) = A"}\<close>
 
    72 ML_val {* const @{term "(\<lambda>x::'a set. a \<in> x)"} *}
 
    72 ML_val \<open>const @{term "(\<lambda>x::'a set. a \<in> x)"}\<close>
 
    73 ML_val {* const @{term "{{a::'a}} = C"} *}
 
    73 ML_val \<open>const @{term "{{a::'a}} = C"}\<close>
 
    74 ML_val {* const @{term "{f::'a\<Rightarrow>nat} = {g::'a\<Rightarrow>nat}"} *}
 
    74 ML_val \<open>const @{term "{f::'a\<Rightarrow>nat} = {g::'a\<Rightarrow>nat}"}\<close>
 
    75 ML_val {* const @{term "A \<union> (B::'a set)"} *}
 
    75 ML_val \<open>const @{term "A \<union> (B::'a set)"}\<close>
 
    76 ML_val {* const @{term "\<lambda>A B x::'a. A x \<or> B x"} *}
 
    76 ML_val \<open>const @{term "\<lambda>A B x::'a. A x \<or> B x"}\<close>
 
    77 ML_val {* const @{term "P (a::'a)"} *}
 
    77 ML_val \<open>const @{term "P (a::'a)"}\<close>
 
    78 ML_val {* const @{term "\<lambda>a::'a. b (c (d::'a)) (e::'a) (f::'a)"} *}
 
    78 ML_val \<open>const @{term "\<lambda>a::'a. b (c (d::'a)) (e::'a) (f::'a)"}\<close>
 
    79 ML_val {* const @{term "\<forall>A::'a set. a \<in> A"} *}
 
    79 ML_val \<open>const @{term "\<forall>A::'a set. a \<in> A"}\<close>
 
    80 ML_val {* const @{term "\<forall>A::'a set. P A"} *}
 
    80 ML_val \<open>const @{term "\<forall>A::'a set. P A"}\<close>
 
    81 ML_val {* const @{term "P \<or> Q"} *}
 
    81 ML_val \<open>const @{term "P \<or> Q"}\<close>
 
    82 ML_val {* const @{term "A \<union> B = (C::'a set)"} *}
 
    82 ML_val \<open>const @{term "A \<union> B = (C::'a set)"}\<close>
 
    83 ML_val {* const @{term "(\<lambda>A B x::'a. A x \<or> B x) A B = C"} *}
 
    83 ML_val \<open>const @{term "(\<lambda>A B x::'a. A x \<or> B x) A B = C"}\<close>
 
    84 ML_val {* const @{term "(if P then (A::'a set) else B) = C"} *}
 
    84 ML_val \<open>const @{term "(if P then (A::'a set) else B) = C"}\<close>
 
    85 ML_val {* const @{term "let A = (C::'a set) in A \<union> B"} *}
 
    85 ML_val \<open>const @{term "let A = (C::'a set) in A \<union> B"}\<close>
 
    86 ML_val {* const @{term "THE x::'b. P x"} *}
 
    86 ML_val \<open>const @{term "THE x::'b. P x"}\<close>
 
    87 ML_val {* const @{term "(\<lambda>x::'a. False)"} *}
 
    87 ML_val \<open>const @{term "(\<lambda>x::'a. False)"}\<close>
 
    88 ML_val {* const @{term "(\<lambda>x::'a. True)"} *}
 
    88 ML_val \<open>const @{term "(\<lambda>x::'a. True)"}\<close>
 
    89 ML_val {* const @{term "(\<lambda>x::'a. False) = (\<lambda>x::'a. False)"} *}
 
    89 ML_val \<open>const @{term "(\<lambda>x::'a. False) = (\<lambda>x::'a. False)"}\<close>
 
    90 ML_val {* const @{term "(\<lambda>x::'a. True) = (\<lambda>x::'a. True)"} *}
 
    90 ML_val \<open>const @{term "(\<lambda>x::'a. True) = (\<lambda>x::'a. True)"}\<close>
 
    91 ML_val {* const @{term "Let (a::'a) A"} *}
 
    91 ML_val \<open>const @{term "Let (a::'a) A"}\<close>
 
    92 ML_val {* const @{term "A (a::'a)"} *}
 
    92 ML_val \<open>const @{term "A (a::'a)"}\<close>
 
    93 ML_val {* const @{term "insert (a::'a) A = B"} *}
 
    93 ML_val \<open>const @{term "insert (a::'a) A = B"}\<close>
 
    94 ML_val {* const @{term "- (A::'a set)"} *}
 
    94 ML_val \<open>const @{term "- (A::'a set)"}\<close>
 
    95 ML_val {* const @{term "finite (A::'a set)"} *}
 
    95 ML_val \<open>const @{term "finite (A::'a set)"}\<close>
 
    96 ML_val {* const @{term "\<not> finite (A::'a set)"} *}
 
    96 ML_val \<open>const @{term "\<not> finite (A::'a set)"}\<close>
 
    97 ML_val {* const @{term "finite (A::'a set set)"} *}
 
    97 ML_val \<open>const @{term "finite (A::'a set set)"}\<close>
 
    98 ML_val {* const @{term "\<lambda>a::'a. A a \<and> \<not> B a"} *}
 
    98 ML_val \<open>const @{term "\<lambda>a::'a. A a \<and> \<not> B a"}\<close>
 
    99 ML_val {* const @{term "A < (B::'a set)"} *}
 
    99 ML_val \<open>const @{term "A < (B::'a set)"}\<close>
 
   100 ML_val {* const @{term "A \<le> (B::'a set)"} *}
 
   100 ML_val \<open>const @{term "A \<le> (B::'a set)"}\<close>
 
   101 ML_val {* const @{term "[a::'a]"} *}
 
   101 ML_val \<open>const @{term "[a::'a]"}\<close>
 
   102 ML_val {* const @{term "[a::'a set]"} *}
 
   102 ML_val \<open>const @{term "[a::'a set]"}\<close>
 
   103 ML_val {* const @{term "[A \<union> (B::'a set)]"} *}
 
   103 ML_val \<open>const @{term "[A \<union> (B::'a set)]"}\<close>
 
   104 ML_val {* const @{term "[A \<union> (B::'a set)] = [C]"} *}
 
   104 ML_val \<open>const @{term "[A \<union> (B::'a set)] = [C]"}\<close>
 
   105 ML_val {* const @{term "{(\<lambda>x::'a. x = a)} = C"} *}
 
   105 ML_val \<open>const @{term "{(\<lambda>x::'a. x = a)} = C"}\<close>
 
   106 ML_val {* const @{term "(\<lambda>a::'a. \<not> A a) = B"} *}
 
   106 ML_val \<open>const @{term "(\<lambda>a::'a. \<not> A a) = B"}\<close>
 
   107 ML_val {* const @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> \<not> f a"} *}
 
   107 ML_val \<open>const @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> \<not> f a"}\<close>
 
   108 ML_val {* const @{term "\<lambda>A B x::'a. A x \<and> B x \<and> A = B"} *}
 
   108 ML_val \<open>const @{term "\<lambda>A B x::'a. A x \<and> B x \<and> A = B"}\<close>
 
   109 ML_val {* const @{term "p = (\<lambda>(x::'a) (y::'a). P x \<or> \<not> Q y)"} *}
 
   109 ML_val \<open>const @{term "p = (\<lambda>(x::'a) (y::'a). P x \<or> \<not> Q y)"}\<close>
 
   110 ML_val {* const @{term "p = (\<lambda>(x::'a) (y::'a). p x y :: bool)"} *}
 
   110 ML_val \<open>const @{term "p = (\<lambda>(x::'a) (y::'a). p x y :: bool)"}\<close>
 
   111 ML_val {* const @{term "p = (\<lambda>A B x. A x \<and> \<not> B x) (\<lambda>x. True) (\<lambda>y. x \<noteq> y)"} *}
 
   111 ML_val \<open>const @{term "p = (\<lambda>A B x. A x \<and> \<not> B x) (\<lambda>x. True) (\<lambda>y. x \<noteq> y)"}\<close>
 
   112 ML_val {* const @{term "p = (\<lambda>y. x \<noteq> y)"} *}
 
   112 ML_val \<open>const @{term "p = (\<lambda>y. x \<noteq> y)"}\<close>
 
   113 ML_val {* const @{term "(\<lambda>x. (p::'a\<Rightarrow>bool\<Rightarrow>bool) x False)"} *}
 
   113 ML_val \<open>const @{term "(\<lambda>x. (p::'a\<Rightarrow>bool\<Rightarrow>bool) x False)"}\<close>
 
   114 ML_val {* const @{term "(\<lambda>x y. (p::'a\<Rightarrow>'a\<Rightarrow>bool\<Rightarrow>bool) x y False)"} *}
 
   114 ML_val \<open>const @{term "(\<lambda>x y. (p::'a\<Rightarrow>'a\<Rightarrow>bool\<Rightarrow>bool) x y False)"}\<close>
 
   115 ML_val {* const @{term "f = (\<lambda>x::'a. P x \<longrightarrow> Q x)"} *}
 
   115 ML_val \<open>const @{term "f = (\<lambda>x::'a. P x \<longrightarrow> Q x)"}\<close>
 
   116 ML_val {* const @{term "\<forall>a::'a. P a"} *}
 
   116 ML_val \<open>const @{term "\<forall>a::'a. P a"}\<close>
 
   117 
   117 
   118 ML_val {* nonconst @{term "\<forall>P (a::'a). P a"} *}
 
   118 ML_val \<open>nonconst @{term "\<forall>P (a::'a). P a"}\<close>
 
   119 ML_val {* nonconst @{term "THE x::'a. P x"} *}
 
   119 ML_val \<open>nonconst @{term "THE x::'a. P x"}\<close>
 
   120 ML_val {* nonconst @{term "SOME x::'a. P x"} *}
 
   120 ML_val \<open>nonconst @{term "SOME x::'a. P x"}\<close>
 
   121 ML_val {* nonconst @{term "(\<lambda>A B x::'a. A x \<or> B x) = myunion"} *}
 
   121 ML_val \<open>nonconst @{term "(\<lambda>A B x::'a. A x \<or> B x) = myunion"}\<close>
 
   122 ML_val {* nonconst @{term "(\<lambda>x::'a. False) = (\<lambda>x::'a. True)"} *}
 
   122 ML_val \<open>nonconst @{term "(\<lambda>x::'a. False) = (\<lambda>x::'a. True)"}\<close>
 
   123 ML_val {* nonconst @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"} *}
 
   123 ML_val \<open>nonconst @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"}\<close>
 
   124 
   124 
   125 ML_val {* mono @{prop "Q (\<forall>x::'a set. P x)"} *}
 
   125 ML_val \<open>mono @{prop "Q (\<forall>x::'a set. P x)"}\<close>
 
   126 ML_val {* mono @{prop "P (a::'a)"} *}
 
   126 ML_val \<open>mono @{prop "P (a::'a)"}\<close>
 
   127 ML_val {* mono @{prop "{a} = {b::'a}"} *}
 
   127 ML_val \<open>mono @{prop "{a} = {b::'a}"}\<close>
 
   128 ML_val {* mono @{prop "(\<lambda>x. x = a) = (\<lambda>y. y = (b::'a))"} *}
 
   128 ML_val \<open>mono @{prop "(\<lambda>x. x = a) = (\<lambda>y. y = (b::'a))"}\<close>
 
   129 ML_val {* mono @{prop "(a::'a) \<in> P \<and> P \<union> P = P"} *}
 
   129 ML_val \<open>mono @{prop "(a::'a) \<in> P \<and> P \<union> P = P"}\<close>
 
   130 ML_val {* mono @{prop "\<forall>F::'a set set. P"} *}
 
   130 ML_val \<open>mono @{prop "\<forall>F::'a set set. P"}\<close>
 
   131 ML_val {* mono @{prop "\<not> (\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h)"} *}
 
   131 ML_val \<open>mono @{prop "\<not> (\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h)"}\<close>
 
   132 ML_val {* mono @{prop "\<not> Q (\<forall>x::'a set. P x)"} *}
 
   132 ML_val \<open>mono @{prop "\<not> Q (\<forall>x::'a set. P x)"}\<close>
 
   133 ML_val {* mono @{prop "\<not> (\<forall>x::'a. P x)"} *}
 
   133 ML_val \<open>mono @{prop "\<not> (\<forall>x::'a. P x)"}\<close>
 
   134 ML_val {* mono @{prop "myall P = (P = (\<lambda>x::'a. True))"} *}
 
   134 ML_val \<open>mono @{prop "myall P = (P = (\<lambda>x::'a. True))"}\<close>
 
   135 ML_val {* mono @{prop "myall P = (P = (\<lambda>x::'a. False))"} *}
 
   135 ML_val \<open>mono @{prop "myall P = (P = (\<lambda>x::'a. False))"}\<close>
 
   136 ML_val {* mono @{prop "\<forall>x::'a. P x"} *}
 
   136 ML_val \<open>mono @{prop "\<forall>x::'a. P x"}\<close>
 
   137 ML_val {* mono @{term "(\<lambda>A B x::'a. A x \<or> B x) \<noteq> myunion"} *}
 
   137 ML_val \<open>mono @{term "(\<lambda>A B x::'a. A x \<or> B x) \<noteq> myunion"}\<close>
 
   138 
   138 
   139 ML_val {* nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"} *}
 
   139 ML_val \<open>nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"}\<close>
 
   140 ML_val {* nonmono @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"} *}
 
   140 ML_val \<open>nonmono @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"}\<close>
 
   141 
   141 
   142 ML {*
 
   142 ML \<open>
 
   143 val preproc_timeout = seconds 5.0
 
   143 val preproc_timeout = seconds 5.0
 
   144 val mono_timeout = seconds 1.0
 
   144 val mono_timeout = seconds 1.0
 
   145 
   145 
   146 fun is_forbidden_theorem name =
 
   146 fun is_forbidden_theorem name =
 
   147   length (Long_Name.explode name) <> 2 orelse
 
   147   length (Long_Name.explode name) <> 2 orelse
 
   186                               neg_t
 
   186                               neg_t
 
   187         val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
 
   187         val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
 
   188       in File.append path (res ^ "\n"); writeln res end
 
   188       in File.append path (res ^ "\n"); writeln res end
 
   189       handle Timeout.TIMEOUT _ => ()
 
   189       handle Timeout.TIMEOUT _ => ()
 
   190   in thy |> theorems_of |> List.app check_theorem end
 
   190   in thy |> theorems_of |> List.app check_theorem end
 
   191 *}
 
   191 \<close>
 
   192 
   192 
   193 (*
 
   193 (*
 
   194 ML_val {* check_theory @{theory AVL2} *}
 
   194 ML_val {* check_theory @{theory AVL2} *}
 
   195 ML_val {* check_theory @{theory Fun} *}
 
   195 ML_val {* check_theory @{theory Fun} *}
 
   196 ML_val {* check_theory @{theory Huffman} *}
 
   196 ML_val {* check_theory @{theory Huffman} *}
 
   197 ML_val {* check_theory @{theory List} *}
 
   197 ML_val {* check_theory @{theory List} *}
 
   198 ML_val {* check_theory @{theory Map} *}
 
   198 ML_val {* check_theory @{theory Map} *}
 
   199 ML_val {* check_theory @{theory Relation} *}
 
   199 ML_val {* check_theory @{theory Relation} *}
 
   200 *)
 
   200 *)
 
   201 
   201 
   202 ML {* getenv "ISABELLE_TMP" *}
 
   202 ML \<open>getenv "ISABELLE_TMP"\<close>
 
   203 
   203 
   204 end
 
   204 end
isabelle