Mercurial Mercurial > hg > nominal2 / 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.
attempt to manual prove eqvt for alpha
authorChristian Urban <urbanc@in.tum.de>
Fri, 16 Apr 2010 10:46:50 +0200
changeset 1863 457bf371c91a
parent 1861 226b797868dc
child 1864 3d68573e46d3
attempt to manual prove eqvt for alpha
Nominal/Ex/Lambda.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Ex/Lambda.thy	Fri Apr 16 10:18:16 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Fri Apr 16 10:46:50 2010 +0200
@@ -194,6 +194,18 @@
 lemma
   assumes a: "alpha_lam_raw' t1 t2"
   shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)"
+using a
+apply(induct)
+apply(perm_simp)
+apply(rule a1)
+apply(simp)
+apply(perm_simp)
+apply(rule a2)
+apply(simp)
+apply(simp)
+apply(perm_simp)
+apply(rule a3)
+apply(unfold alpha_gen)
 oops
 
 lemma
nominal2