Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tweak Metis example to avoid glitch in proof reconstruction with a few guard-based, type-argument-less encodings
authorblanchet
Wed, 06 Jun 2012 10:35:05 +0200
changeset 48098 dd611ab202a8
parent 48097 7618e1d9322c
child 48099 e7e647949c95
tweak Metis example to avoid glitch in proof reconstruction with a few guard-based, type-argument-less encodings
src/HOL/Metis_Examples/Type_Encodings.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Wed Jun 06 10:35:05 2012 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Wed Jun 06 10:35:05 2012 +0200
@@ -27,7 +27,7 @@
    "poly_guards",
    "poly_guards?",
    "poly_guards??",
-   (* "poly_guards@?", *)
+   "poly_guards@?",
    "poly_tags",
    "poly_tags?",
    "poly_tags??",
@@ -73,8 +73,8 @@
 lemma "x = y \<Longrightarrow> y = x"
 by metis_exhaust
 
-lemma "[a] = [1 + 1] \<Longrightarrow> a = 1 + (1::int)"
-by (metis_exhaust last.simps)
+lemma "[a] = [Suc 0] \<Longrightarrow> a = 1"
+by (metis_exhaust last.simps One_nat_def)
 
 lemma "map Suc [0] = [Suc 0]"
 by (metis_exhaust map.simps)
@@ -90,7 +90,7 @@
 lemma "P (null xs) \<Longrightarrow> null xs \<Longrightarrow> xs = []"
 by (metis_exhaust null_def)
 
-lemma "(0::nat) + 0 = 0"
+lemma "(0\<Colon>nat) + 0 = 0"
 by (metis_exhaust add_0_left)
 
 end
isabelle