src/HOL/Metis_Examples/Proxies.thy
author huffman
Thu Aug 11 09:11:15 2011 -0700 (2011-08-11)
changeset 44165 d26a45f3c835
parent 43989 eb763b3ff9ed
child 44494 a77901b3774e
permissions -rw-r--r--
remove lemma stupid_ext
     1 (*  Title:      HOL/Metis_Examples/Proxies.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3 
     4 Example that exercises Metis's and Sledgehammer's logical symbol proxies for
     5 rudimentary higher-order reasoning.
     6 *)
     7 
     8 header {*
     9 Example that Exercises Metis's and Sledgehammer's Logical Symbol Proxies for
    10 Rudimentary Higher-Order Reasoning.
    11 *}
    12 
    13 theory Proxies
    14 imports Type_Encodings
    15 begin
    16 
    17 text {* Extensionality and set constants *}
    18 
    19 lemma plus_1_not_0: "n + (1\<Colon>nat) \<noteq> 0"
    20 by simp
    21 
    22 definition inc :: "nat \<Rightarrow> nat" where
    23 "inc x = x + 1"
    24 
    25 lemma "inc \<noteq> (\<lambda>y. 0)"
    26 sledgehammer [expect = some] (inc_def plus_1_not_0)
    27 by (metis_exhaust inc_def plus_1_not_0)
    28 
    29 lemma "inc = (\<lambda>y. y + 1)"
    30 sledgehammer [expect = some] (inc_def)
    31 by (metis_exhaust inc_def)
    32 
    33 definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
    34 "add_swap = (\<lambda>x y. y + x)"
    35 
    36 lemma "add_swap m n = n + m"
    37 sledgehammer [expect = some] (add_swap_def)
    38 by (metis_exhaust add_swap_def)
    39 
    40 definition "A = {xs\<Colon>'a list. True}"
    41 
    42 lemma "xs \<in> A"
    43 sledgehammer [expect = some]
    44 by (metis_exhaust A_def Collect_def mem_def)
    45 
    46 definition "B (y::int) \<equiv> y \<le> 0"
    47 definition "C (y::int) \<equiv> y \<le> 1"
    48 
    49 lemma int_le_0_imp_le_1: "x \<le> (0::int) \<Longrightarrow> x \<le> 1"
    50 by linarith
    51 
    52 lemma "B \<subseteq> C"
    53 sledgehammer [type_enc = poly_args, max_relevant = 100, expect = some]
    54 by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
    55 
    56 
    57 text {* Proxies for logical constants *}
    58 
    59 lemma "id (op =) x x"
    60 sledgehammer [type_enc = erased, expect = none] (id_apply)
    61 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
    62 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
    63 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
    64 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
    65 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
    66 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
    67 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
    68 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
    69 by (metis (full_types) id_apply)
    70 
    71 lemma "id True"
    72 sledgehammer [type_enc = erased, expect = some] (id_apply)
    73 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
    74 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
    75 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
    76 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
    77 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
    78 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
    79 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
    80 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
    81 by (metis_exhaust id_apply)
    82 
    83 lemma "\<not> id False"
    84 sledgehammer [type_enc = erased, expect = some] (id_apply)
    85 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
    86 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
    87 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
    88 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
    89 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
    90 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
    91 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
    92 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
    93 by (metis_exhaust id_apply)
    94 
    95 lemma "x = id True \<or> x = id False"
    96 sledgehammer [type_enc = erased, expect = some] (id_apply)
    97 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
    98 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
    99 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
   100 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   101 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
   102 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
   103 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
   104 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
   105 by (metis_exhaust id_apply)
   106 
   107 lemma "id x = id True \<or> id x = id False"
   108 sledgehammer [type_enc = erased, expect = some] (id_apply)
   109 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
   110 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   111 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
   112 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   113 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
   114 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
   115 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
   116 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
   117 by (metis_exhaust id_apply)
   118 
   119 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
   120 sledgehammer [type_enc = erased, expect = none] ()
   121 sledgehammer [type_enc = poly_args, expect = none] ()
   122 sledgehammer [type_enc = poly_tags?, expect = some] ()
   123 sledgehammer [type_enc = poly_tags, expect = some] ()
   124 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
   125 sledgehammer [type_enc = poly_guards, expect = some] ()
   126 sledgehammer [type_enc = mangled_tags?, expect = some] ()
   127 sledgehammer [type_enc = mangled_tags, expect = some] ()
   128 sledgehammer [type_enc = mangled_guards?, expect = some] ()
   129 sledgehammer [type_enc = mangled_guards, expect = some] ()
   130 by (metis (full_types))
   131 
   132 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
   133 sledgehammer [type_enc = erased, expect = some] (id_apply)
   134 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
   135 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   136 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
   137 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   138 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
   139 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
   140 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
   141 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
   142 by (metis_exhaust id_apply)
   143 
   144 lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
   145 sledgehammer [type_enc = erased, expect = some] (id_apply)
   146 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
   147 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   148 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
   149 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   150 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
   151 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
   152 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
   153 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
   154 by (metis_exhaust id_apply)
   155 
   156 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
   157 sledgehammer [type_enc = erased, expect = some] (id_apply)
   158 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
   159 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   160 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
   161 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   162 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
   163 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
   164 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
   165 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
   166 by (metis_exhaust id_apply)
   167 
   168 lemma "id (a \<and> b) \<Longrightarrow> id a"
   169 sledgehammer [type_enc = erased, expect = some] (id_apply)
   170 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
   171 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   172 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
   173 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   174 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
   175 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
   176 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
   177 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
   178 by (metis_exhaust id_apply)
   179 
   180 lemma "id (a \<and> b) \<Longrightarrow> id b"
   181 sledgehammer [type_enc = erased, expect = some] (id_apply)
   182 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
   183 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   184 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
   185 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   186 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
   187 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
   188 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
   189 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
   190 by (metis_exhaust id_apply)
   191 
   192 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
   193 sledgehammer [type_enc = erased, expect = some] (id_apply)
   194 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
   195 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   196 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
   197 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   198 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
   199 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
   200 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
   201 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
   202 by (metis_exhaust id_apply)
   203 
   204 lemma "id a \<Longrightarrow> id (a \<or> b)"
   205 sledgehammer [type_enc = erased, expect = some] (id_apply)
   206 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
   207 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   208 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
   209 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   210 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
   211 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
   212 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
   213 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
   214 by (metis_exhaust id_apply)
   215 
   216 lemma "id b \<Longrightarrow> id (a \<or> b)"
   217 sledgehammer [type_enc = erased, expect = some] (id_apply)
   218 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
   219 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   220 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
   221 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   222 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
   223 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
   224 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
   225 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
   226 by (metis_exhaust id_apply)
   227 
   228 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
   229 sledgehammer [type_enc = erased, expect = some] (id_apply)
   230 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
   231 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   232 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
   233 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   234 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
   235 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
   236 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
   237 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
   238 by (metis_exhaust id_apply)
   239 
   240 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
   241 sledgehammer [type_enc = erased, expect = some] (id_apply)
   242 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
   243 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   244 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
   245 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   246 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
   247 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
   248 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
   249 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
   250 by (metis_exhaust id_apply)
   251 
   252 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
   253 sledgehammer [type_enc = erased, expect = some] (id_apply)
   254 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply)
   255 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   256 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply)
   257 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   258 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply)
   259 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply)
   260 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply)
   261 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply)
   262 by (metis_exhaust id_apply)
   263 
   264 end