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.
Proper compose_sym2
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 17 Mar 2010 17:40:14 +0100
changeset 1487 b55b78e63913
parent 1482 a98c15866300
child 1488 44e68ab6841e
Proper compose_sym2
Nominal/Abs.thy file | annotate | diff | comparison | revisions
Nominal/Fv.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Abs.thy	Wed Mar 17 17:09:01 2010 +0100
+++ b/Nominal/Abs.thy	Wed Mar 17 17:40:14 2010 +0100
@@ -87,33 +87,25 @@
   done
 
 lemma alpha_gen_compose_sym2:
-  assumes a: "(aa, (t1, t2)) \<approx>gen (\<lambda>(x11, x12) (x21, x22). R1 x11 x21 \<and> R1 x21 x11 \<and> R2 x12 x22 \<and> R2 x22 x12)
-  (\<lambda>(b, a). fb b \<union> fa a) pi (ab, (s1, s2))"
+  assumes a: "(aa, t1, t2) \<approx>gen (\<lambda>(x11, x12) (x21, x22).
+  (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
   and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
   and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
-  shows "(ab, (s1, s2)) \<approx>gen
- (\<lambda>x1 x2. (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) x1 x2 \<and> (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) x2 x1)
- (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, (t1, t2))"
- using a
-apply(simp add: alpha_gen)
-apply clarify
-apply (rule conjI)
+  shows "(ab, s1, s2) \<approx>gen (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
+  using a
+  apply(simp add: alpha_gen)
+  apply clarify
+  apply (rule conjI)
   apply(simp add: fresh_star_def fresh_minus_perm)
-apply (rule conjI)
-apply (rotate_tac 3)
-apply (drule_tac pi="- pi" in r1)
-apply simp
-apply (rule conjI)
-apply (rotate_tac -1)
-apply (drule_tac pi="- pi" in r2)
-apply simp
-apply (rule conjI)
-apply (drule_tac pi="- pi" in r1)
-apply simp
-apply (rule conjI)
-apply (drule_tac pi="- pi" in r2)
-apply simp_all
-done
+  apply (rule conjI)
+  apply (rotate_tac 3)
+  apply (drule_tac pi="- pi" in r1)
+  apply simp
+  apply (rule conjI)
+  apply (rotate_tac -1)
+  apply (drule_tac pi="- pi" in r2)
+  apply simp_all
+  done
 
 lemma alpha_gen_compose_trans:
   fixes pi pia
--- a/Nominal/Fv.thy	Wed Mar 17 17:09:01 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 17 17:40:14 2010 +0100
@@ -609,10 +609,8 @@
   THEN_ALL_NEW
   split_conjs THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
-  (rtac @{thm alpha_gen_compose_sym} THEN' RANGE [
-    (asm_full_simp_tac (HOL_ss addsimps @{thms plus_perm_eq})),
-    (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
-  ])
+  TRY o (rtac @{thm alpha_gen_compose_sym2} ORELSE' rtac @{thm alpha_gen_compose_sym}) THEN_ALL_NEW
+  (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
 *}
 
 ML {*
nominal2