Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/Metis_Examples/Proxies.thy
author blanchet
Mon, 06 Jun 2011 20:36:35 +0200
changeset 44046 23b81469499f
parent 44043 6ce09f69657c
child 44053 050a03afe024
permissions -rw-r--r--
more preparations towards hijacking Metis 
     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 (new_metis_exhaust inc_def plus_1_not_0)

    28 

    29 lemma "inc = (\<lambda>y. y + 1)"

    30 sledgehammer [expect = some] (inc_def)

    31 by (new_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 (new_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 (new_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_sys = poly_args, max_relevant = 200, expect = some]

    54 by (new_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_sys = erased, expect = none] (id_apply)

    61 sledgehammer [type_sys = poly_tags?, expect = none] (id_apply) (* unfortunate *)

    62 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)

    63 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)

    64 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)

    65 sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)

    66 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)

    67 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)

    68 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)

    69 by (metisFT id_apply)

    70 

    71 lemma "id True"

    72 sledgehammer [type_sys = erased, expect = some] (id_apply)

    73 sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)

    74 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)

    75 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)

    76 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)

    77 sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)

    78 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)

    79 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)

    80 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)

    81 by (new_metis_exhaust id_apply)

    82 

    83 lemma "\<not> id False"

    84 sledgehammer [type_sys = erased, expect = some] (id_apply)

    85 sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)

    86 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)

    87 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)

    88 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)

    89 sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)

    90 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)

    91 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)

    92 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)

    93 by (new_metis_exhaust id_apply)

    94 

    95 lemma "x = id True \<or> x = id False"

    96 sledgehammer [type_sys = erased, expect = some] (id_apply)

    97 sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)

    98 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)

    99 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)

   100 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)

   101 sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)

   102 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)

   103 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)

   104 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)

   105 by (new_metis_exhaust id_apply)

   106 

   107 lemma "id x = id True \<or> id x = id False"

   108 sledgehammer [type_sys = erased, expect = some] (id_apply)

   109 sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)

   110 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)

   111 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)

   112 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)

   113 sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)

   114 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)

   115 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)

   116 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)

   117 by (new_metis_exhaust id_apply)

   118 

   119 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"

   120 sledgehammer [type_sys = erased, expect = none] ()

   121 sledgehammer [type_sys = poly_args, expect = none] ()

   122 sledgehammer [type_sys = poly_tags?, expect = some] ()

   123 sledgehammer [type_sys = poly_tags, expect = some] ()

   124 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)

   125 sledgehammer [type_sys = poly_preds, expect = some] ()

   126 sledgehammer [type_sys = mangled_tags?, expect = some] ()

   127 sledgehammer [type_sys = mangled_tags, expect = some] ()

   128 sledgehammer [type_sys = mangled_preds?, expect = some] ()

   129 sledgehammer [type_sys = mangled_preds, expect = some] ()

   130 by metisFT

   131 

   132 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"

   133 sledgehammer [type_sys = erased, expect = some] (id_apply)

   134 sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)

   135 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)

   136 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)

   137 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)

   138 sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)

   139 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)

   140 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)

   141 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)

   142 by (new_metis_exhaust id_apply)

   143 

   144 lemma "id (\<not> \<not> a) \<Longrightarrow> id a"

   145 sledgehammer [type_sys = erased, expect = some] (id_apply)

   146 sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)

   147 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)

   148 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)

   149 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)

   150 sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)

   151 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)

   152 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)

   153 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)

   154 by (new_metis_exhaust id_apply)

   155 

   156 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"

   157 sledgehammer [type_sys = erased, expect = some] (id_apply)

   158 sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)

   159 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)

   160 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)

   161 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)

   162 sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)

   163 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)

   164 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)

   165 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)

   166 by (new_metis_exhaust id_apply)

   167 

   168 lemma "id (a \<and> b) \<Longrightarrow> id a"

   169 sledgehammer [type_sys = erased, expect = some] (id_apply)

   170 sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)

   171 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)

   172 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)

   173 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)

   174 sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)

   175 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)

   176 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)

   177 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)

   178 by (new_metis_exhaust id_apply)

   179 

   180 lemma "id (a \<and> b) \<Longrightarrow> id b"

   181 sledgehammer [type_sys = erased, expect = some] (id_apply)

   182 sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)

   183 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)

   184 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)

   185 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)

   186 sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)

   187 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)

   188 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)

   189 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)

   190 by (new_metis_exhaust id_apply)

   191 

   192 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"

   193 sledgehammer [type_sys = erased, expect = some] (id_apply)

   194 sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)

   195 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)

   196 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)

   197 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)

   198 sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)

   199 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)

   200 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)

   201 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)

   202 by (new_metis_exhaust id_apply)

   203 

   204 lemma "id a \<Longrightarrow> id (a \<or> b)"

   205 sledgehammer [type_sys = erased, expect = some] (id_apply)

   206 sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)

   207 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)

   208 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)

   209 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)

   210 sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)

   211 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)

   212 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)

   213 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)

   214 by (new_metis_exhaust id_apply)

   215 

   216 lemma "id b \<Longrightarrow> id (a \<or> b)"

   217 sledgehammer [type_sys = erased, expect = some] (id_apply)

   218 sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)

   219 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)

   220 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)

   221 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)

   222 sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)

   223 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)

   224 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)

   225 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)

   226 by (new_metis_exhaust id_apply)

   227 

   228 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"

   229 sledgehammer [type_sys = erased, expect = some] (id_apply)

   230 sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)

   231 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)

   232 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)

   233 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)

   234 sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)

   235 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)

   236 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)

   237 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)

   238 by (new_metis_exhaust id_apply)

   239 

   240 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"

   241 sledgehammer [type_sys = erased, expect = some] (id_apply)

   242 sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)

   243 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)

   244 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)

   245 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)

   246 sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)

   247 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)

   248 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)

   249 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)

   250 by (new_metis_exhaust id_apply)

   251 

   252 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"

   253 sledgehammer [type_sys = erased, expect = some] (id_apply)

   254 sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)

   255 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)

   256 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)

   257 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)

   258 sledgehammer [type_sys = mangled_tags?, expect = some] (id_apply)

   259 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)

   260 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)

   261 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)

   262 by (new_metis_exhaust id_apply)

   263 

   264 end
wneuper/isa