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.
Removed Inl and Inr
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 28 Jun 2011 14:01:15 +0900
changeset 2918 aaaed6367b8f
parent 2917 6ad2f1c296a7
child 2919 13ae668bdb15
Removed Inl and Inr
Nominal/Ex/LetRecB.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Ex/LetRecB.thy	Tue Jun 28 14:49:48 2011 +0100
+++ b/Nominal/Ex/LetRecB.thy	Tue Jun 28 14:01:15 2011 +0900
@@ -143,9 +143,25 @@
   apply(perm_simp)
   apply(simp)
   apply(simp add: inj_on_def)
-  --"HERE"
-  thm Abs_lst_fcb Abs_lst_fcb2
-  apply (drule_tac c="()" and ba="bn" in Abs_lst_fcb2)
+  --"The following could be done by nominal"
+  apply (simp add: meta_eq_to_obj_eq[OF height_trm_def, symmetric, unfolded fun_eq_iff])
+  apply (simp add: meta_eq_to_obj_eq[OF height_bp_def, symmetric, unfolded fun_eq_iff])
+  apply (subgoal_tac "eqvt_at height_bp bp")
+  apply (subgoal_tac "eqvt_at height_bp bpa")
+  apply (subgoal_tac "eqvt_at height_trm b")
+  apply (subgoal_tac "eqvt_at height_trm ba")
+  apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inr bp)")
+  apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inr bpa)")
+  apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inl b)")
+  apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inl ba)")
+  defer
+  apply (simp add: eqvt_at_def height_trm_def)
+  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 (erule_tac c="()" and ba="bn" in Abs_lst_fcb2)
+
   prefer 8
   apply(assumption)
   apply (drule_tac c="()" in Abs_lst_fcb2)
nominal2