src/HOL/Metis_Examples/Proxies.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 53989 729700091556
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
     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 sledgehammer_params [prover = spass, blocking, fact_filter = mepo, timeout = 30,
    18                      preplay_timeout = 0, dont_minimize]
    19 
    20 text {* Extensionality and set constants *}
    21 
    22 lemma plus_1_not_0: "n + (1\<Colon>nat) \<noteq> 0"
    23 by simp
    24 
    25 definition inc :: "nat \<Rightarrow> nat" where
    26 "inc x = x + 1"
    27 
    28 lemma "inc \<noteq> (\<lambda>y. 0)"
    29 sledgehammer [expect = some] (inc_def plus_1_not_0)
    30 by (metis_exhaust inc_def plus_1_not_0)
    31 
    32 lemma "inc = (\<lambda>y. y + 1)"
    33 sledgehammer [expect = some]
    34 by (metis_exhaust inc_def)
    35 
    36 definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
    37 "add_swap = (\<lambda>x y. y + x)"
    38 
    39 lemma "add_swap m n = n + m"
    40 sledgehammer [expect = some] (add_swap_def)
    41 by (metis_exhaust add_swap_def)
    42 
    43 definition "A = {xs\<Colon>'a list. True}"
    44 
    45 lemma "xs \<in> A"
    46 (* The "add:" argument is unfortunate. *)
    47 sledgehammer [expect = some] (add: A_def mem_Collect_eq)
    48 by (metis_exhaust A_def mem_Collect_eq)
    49 
    50 definition "B (y::int) \<equiv> y \<le> 0"
    51 definition "C (y::int) \<equiv> y \<le> 1"
    52 
    53 lemma int_le_0_imp_le_1: "x \<le> (0::int) \<Longrightarrow> x \<le> 1"
    54 by linarith
    55 
    56 lemma "B \<le> C"
    57 sledgehammer [expect = some]
    58 by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
    59 
    60 text {* Proxies for logical constants *}
    61 
    62 lemma "id (op =) x x"
    63 sledgehammer [type_enc = erased, expect = none] (id_apply)
    64 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
    65 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
    66 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
    67 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
    68 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
    69 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
    70 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
    71 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
    72 by (metis (full_types) id_apply)
    73 
    74 lemma "id True"
    75 sledgehammer [type_enc = erased, expect = some] (id_apply)
    76 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
    77 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
    78 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
    79 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
    80 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
    81 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
    82 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
    83 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
    84 by (metis_exhaust id_apply)
    85 
    86 lemma "\<not> id False"
    87 sledgehammer [type_enc = erased, expect = some] (id_apply)
    88 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
    89 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
    90 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
    91 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
    92 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
    93 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
    94 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
    95 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
    96 by (metis_exhaust id_apply)
    97 
    98 lemma "x = id True \<or> x = id False"
    99 sledgehammer [type_enc = erased, expect = some] (id_apply)
   100 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
   101 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   102 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
   103 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   104 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
   105 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
   106 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
   107 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
   108 by (metis_exhaust id_apply)
   109 
   110 lemma "id x = id True \<or> id x = id False"
   111 sledgehammer [type_enc = erased, expect = some] (id_apply)
   112 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
   113 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   114 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
   115 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   116 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
   117 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
   118 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
   119 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
   120 by (metis_exhaust id_apply)
   121 
   122 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
   123 sledgehammer [type_enc = erased, expect = none] ()
   124 sledgehammer [type_enc = poly_args, expect = none] ()
   125 sledgehammer [type_enc = poly_tags??, expect = some] ()
   126 sledgehammer [type_enc = poly_tags, expect = some] ()
   127 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
   128 sledgehammer [type_enc = poly_guards, expect = some] ()
   129 sledgehammer [type_enc = mono_tags??, expect = some] ()
   130 sledgehammer [type_enc = mono_tags, expect = some] ()
   131 sledgehammer [type_enc = mono_guards??, expect = some] ()
   132 sledgehammer [type_enc = mono_guards, expect = some] ()
   133 by (metis (full_types))
   134 
   135 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
   136 sledgehammer [type_enc = erased, expect = some] (id_apply)
   137 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
   138 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   139 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
   140 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   141 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
   142 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
   143 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
   144 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
   145 by (metis_exhaust id_apply)
   146 
   147 lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
   148 sledgehammer [type_enc = erased, expect = some] (id_apply)
   149 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
   150 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   151 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
   152 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   153 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
   154 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
   155 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
   156 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
   157 by metis_exhaust
   158 
   159 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
   160 sledgehammer [type_enc = erased, expect = some] (id_apply)
   161 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
   162 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   163 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
   164 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   165 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
   166 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
   167 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
   168 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
   169 by (metis_exhaust id_apply)
   170 
   171 lemma "id (a \<and> b) \<Longrightarrow> id a"
   172 sledgehammer [type_enc = erased, expect = some] (id_apply)
   173 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
   174 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   175 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
   176 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   177 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
   178 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
   179 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
   180 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
   181 by (metis_exhaust id_apply)
   182 
   183 lemma "id (a \<and> b) \<Longrightarrow> id b"
   184 sledgehammer [type_enc = erased, expect = some] (id_apply)
   185 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
   186 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   187 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
   188 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   189 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
   190 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
   191 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
   192 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
   193 by (metis_exhaust id_apply)
   194 
   195 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
   196 sledgehammer [type_enc = erased, expect = some] (id_apply)
   197 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
   198 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   199 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
   200 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   201 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
   202 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
   203 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
   204 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
   205 by (metis_exhaust id_apply)
   206 
   207 lemma "id a \<Longrightarrow> id (a \<or> b)"
   208 sledgehammer [type_enc = erased, expect = some] (id_apply)
   209 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
   210 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   211 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
   212 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   213 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
   214 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
   215 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
   216 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
   217 by (metis_exhaust id_apply)
   218 
   219 lemma "id b \<Longrightarrow> id (a \<or> b)"
   220 sledgehammer [type_enc = erased, expect = some] (id_apply)
   221 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
   222 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   223 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
   224 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   225 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
   226 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
   227 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
   228 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
   229 by (metis_exhaust id_apply)
   230 
   231 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
   232 sledgehammer [type_enc = erased, expect = some] (id_apply)
   233 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
   234 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   235 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
   236 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   237 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
   238 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
   239 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
   240 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
   241 by (metis_exhaust id_apply)
   242 
   243 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
   244 sledgehammer [type_enc = erased, expect = some] (id_apply)
   245 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
   246 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   247 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
   248 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   249 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
   250 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
   251 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
   252 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
   253 by (metis_exhaust id_apply)
   254 
   255 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
   256 sledgehammer [type_enc = erased, expect = some] (id_apply)
   257 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
   258 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
   259 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
   260 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
   261 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
   262 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
   263 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
   264 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
   265 by (metis_exhaust id_apply)
   266 
   267 end