equal
deleted
inserted
replaced
73 apply(simp add: fresh_star_permute_iff) |
73 apply(simp add: fresh_star_permute_iff) |
74 apply(clarsimp) |
74 apply(clarsimp) |
75 done |
75 done |
76 |
76 |
77 lemma alpha_gen_compose_sym: |
77 lemma alpha_gen_compose_sym: |
78 assumes b: "\<exists>pi. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
78 fixes pi |
|
79 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
79 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
80 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
80 shows "\<exists>pi. (ab, s) \<approx>gen R f pi (aa, t)" |
81 shows "(ab, s) \<approx>gen R f (- pi) (aa, t)" |
81 using b apply - |
82 using b apply - |
82 apply(erule exE) |
|
83 apply(rule_tac x="- pi" in exI) |
|
84 apply(simp add: alpha_gen.simps) |
83 apply(simp add: alpha_gen.simps) |
85 apply(erule conjE)+ |
84 apply(erule conjE)+ |
86 apply(rule conjI) |
85 apply(rule conjI) |
87 apply(simp add: fresh_star_def fresh_minus_perm) |
86 apply(simp add: fresh_star_def fresh_minus_perm) |
88 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
87 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
90 apply(rule a) |
89 apply(rule a) |
91 apply assumption |
90 apply assumption |
92 done |
91 done |
93 |
92 |
94 lemma alpha_gen_compose_trans: |
93 lemma alpha_gen_compose_trans: |
95 assumes b: "\<exists>pi\<Colon>perm. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)" |
94 fixes pi pia |
96 and c: "\<exists>pi\<Colon>perm. (ab, ta) \<approx>gen R f pi (ac, sa)" |
95 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)" |
|
96 and c: "(ab, ta) \<approx>gen R f pia (ac, sa)" |
97 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
97 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
98 shows "\<exists>pi\<Colon>perm. (aa, t) \<approx>gen R f pi (ac, sa)" |
98 shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)" |
99 using b c apply - |
99 using b c apply - |
100 apply(simp add: alpha_gen.simps) |
100 apply(simp add: alpha_gen.simps) |
101 apply(erule conjE)+ |
101 apply(erule conjE)+ |
102 apply(erule exE)+ |
|
103 apply(erule conjE)+ |
|
104 apply(rule_tac x="pia + pi" in exI) |
|
105 apply(simp add: fresh_star_plus) |
102 apply(simp add: fresh_star_plus) |
106 apply(drule_tac x="- pia \<bullet> sa" in spec) |
103 apply(drule_tac x="- pia \<bullet> sa" in spec) |
107 apply(drule mp) |
104 apply(drule mp) |
108 apply(rotate_tac 4) |
105 apply(rotate_tac 4) |
109 apply(drule_tac pi="- pia" in a) |
106 apply(drule_tac pi="- pia" in a) |