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.
Leftover only inj and eqvt
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 28 Jun 2011 14:30:30 +0900
changeset 2920 99069744ad74
parent 2919 13ae668bdb15
child 2921 6b496f69f76c
Leftover only inj and eqvt
Nominal/Ex/LetRecB.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Ex/LetRecB.thy	Tue Jun 28 14:18:26 2011 +0900
+++ b/Nominal/Ex/LetRecB.thy	Tue Jun 28 14:30:30 2011 +0900
@@ -159,14 +159,28 @@
   apply (simp add: eqvt_at_def height_trm_def)
   apply (simp add: eqvt_at_def height_bp_def)
   apply (simp add: eqvt_at_def height_bp_def)
-  --"I'd like to apply FCB here, but the following fails"
   apply (subgoal_tac "height_bp bp = height_bp bpa")
   apply (subgoal_tac "height_trm b = height_trm ba")
   apply simp
   apply (subgoal_tac "(\<lambda>as x c. height_trm (snd (bp, b))) as x c = (\<lambda>as x c. height_trm (snd (bpa, ba))) as x c")
   apply simp
-  apply (erule_tac c="()" and ba="bn" and f="\<lambda>as x c. height_trm (snd x)" in Abs_lst_fcb2)
-  ...
+  apply (erule_tac c="()" in Abs_lst_fcb2)
+  apply (simp add: fresh_star_def pure_fresh)
+  apply (simp add: fresh_star_def pure_fresh)
+  apply (simp add: fresh_star_def pure_fresh)
+  apply (simp add: eqvt_at_def)
+  apply (simp add: eqvt_at_def)
+  defer defer
+  apply (subgoal_tac "(\<lambda>as x c. height_bp (fst (bp, b))) as x c = (\<lambda>as x c. height_bp (fst (bpa, ba))) as x c")
+  apply simp
+  apply (erule_tac c="()" in Abs_lst_fcb2)
+  apply (simp add: fresh_star_def pure_fresh)
+  apply (simp add: fresh_star_def pure_fresh)
+  apply (simp add: fresh_star_def pure_fresh)
+  apply (simp add: fresh_star_def pure_fresh)
+  apply (simp add: eqvt_at_def)
+  apply (simp add: eqvt_at_def)
+--""
   done
 
 termination by lexicographic_order
nominal2