41 done |
41 done |
42 |
42 |
43 lemma fv_rtrm5_rlts_eqvt[eqvt]: |
43 lemma fv_rtrm5_rlts_eqvt[eqvt]: |
44 "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)" |
44 "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)" |
45 "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)" |
45 "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)" |
|
46 "pi \<bullet> (fv_rbv5 l) = fv_rbv5 (pi \<bullet> l)" |
46 apply (induct x and l) |
47 apply (induct x and l) |
47 apply (simp_all add: eqvts atom_eqvt) |
48 apply (simp_all add: eqvts atom_eqvt) |
48 done |
49 done |
49 |
50 |
50 lemma alpha5_eqvt: |
51 lemma alpha5_eqvt: |
55 done |
56 done |
56 |
57 |
57 lemma alpha5_reflp: |
58 lemma alpha5_reflp: |
58 "y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 0 x x)" |
59 "y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 0 x x)" |
59 apply (rule rtrm5_rlts.induct) |
60 apply (rule rtrm5_rlts.induct) |
60 thm rtrm5_rlts.induct |
|
61 alpha_rtrm5_alpha_rlts_alpha_rbv5.induct |
|
62 apply (simp_all add: alpha5_inj) |
61 apply (simp_all add: alpha5_inj) |
63 apply (rule_tac x="0::perm" in exI) |
62 apply (rule_tac x="0::perm" in exI) |
64 apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm) |
63 apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm) |
65 done |
64 done |
66 |
65 |
67 lemma alpha5_symp: |
66 lemma alpha5_symp: |
68 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
67 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
69 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
68 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
70 (alpha_rbv5 p x y \<longrightarrow> alpha_rbv5 (-p) y x)" |
69 (alpha_rbv5 p x y \<longrightarrow> alpha_rbv5 (-p) y x)" |
71 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
70 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
72 thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct |
|
73 thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros |
|
74 apply (simp_all add: alpha5_inj) |
71 apply (simp_all add: alpha5_inj) |
75 sorry |
72 sorry |
76 |
73 |
77 lemma alpha5_equivp: |
74 lemma alpha5_equivp: |
78 "equivp alpha_rtrm5" |
75 "equivp alpha_rtrm5" |
93 |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) |
90 |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) |
94 |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) |
91 |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) |
95 |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) |
92 |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) |
96 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) |
93 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) |
97 |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) |
94 |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) |
|
95 |> snd o (Quotient_Def.quotient_lift_const ("fv_bv5", @{term fv_rbv5})) |
98 |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})) |
96 |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})) |
99 |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5}))) |
97 |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5}))) |
100 *} |
98 *} |
101 print_theorems |
99 print_theorems |
102 |
100 |
103 lemma alpha5_rfv: |
101 lemma alpha5_rfv: |
104 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)" |
102 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)" |
105 "(l \<approx>l m \<Longrightarrow> (fv_rlts l = fv_rlts m))" |
103 "(l \<approx>l m \<Longrightarrow> (fv_rlts l = fv_rlts m \<and> fv_rbv5 l = fv_rbv5 m))" |
106 "(alpha_rbv5 a b c \<Longrightarrow> True)" |
104 "(alpha_rbv5 0 b c \<Longrightarrow> fv_rbv5 b = fv_rbv5 c)" |
107 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
105 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
108 apply(simp_all) |
106 apply(simp_all add: eqvts) |
109 apply(simp add: alpha_gen) |
107 apply(simp add: alpha_gen) |
110 apply(clarify) |
108 apply(clarify) |
111 apply(simp_all) |
109 apply(simp) |
112 sorry (* works for non-rec *) |
110 sorry |
113 |
111 |
114 lemma bv_list_rsp: |
112 lemma bv_list_rsp: |
115 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
113 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
116 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
114 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
117 apply(simp_all) |
115 apply(simp_all) |
119 apply simp |
117 apply simp |
120 done |
118 done |
121 |
119 |
122 lemma [quot_respect]: |
120 lemma [quot_respect]: |
123 "(alpha_rlts ===> op =) fv_rlts fv_rlts" |
121 "(alpha_rlts ===> op =) fv_rlts fv_rlts" |
|
122 "(alpha_rlts ===> op =) fv_rbv5 fv_rbv5" |
124 "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" |
123 "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" |
125 "(alpha_rlts ===> op =) rbv5 rbv5" |
124 "(alpha_rlts ===> op =) rbv5 rbv5" |
126 "(op = ===> alpha_rtrm5) rVr5 rVr5" |
125 "(op = ===> alpha_rtrm5) rVr5 rVr5" |
127 "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" |
126 "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" |
128 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
127 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
171 |
170 |
172 end |
171 end |
173 |
172 |
174 lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] |
173 lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] |
175 lemmas bv5[simp] = rbv5.simps[quot_lifted] |
174 lemmas bv5[simp] = rbv5.simps[quot_lifted] |
176 lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] |
175 lemmas fv_trm5_bv5[simp] = fv_rtrm5_fv_rbv5.simps[quot_lifted] |
|
176 lemmas fv_lts[simp] = fv_rlts.simps[quot_lifted] |
177 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
177 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
178 |
178 |
179 lemma lets_ok: |
179 lemma lets_ok: |
180 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
180 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
181 apply (simp add: alpha5_INJ) |
181 thm alpha5_INJ |
|
182 apply (simp only: alpha5_INJ) |
182 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
183 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
183 apply (simp_all add: alpha_gen) |
184 apply (simp_all add: alpha_gen) |
184 apply (simp add: permute_trm5_lts fresh_star_def) |
185 apply (simp add: permute_trm5_lts fresh_star_def) |
185 apply (metis flip_at_simps(1) supp_at_base supp_eqvt) |
186 apply (metis flip_at_simps(1) supp_at_base supp_eqvt) |
186 done |
187 done |