88 |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5}))) |
88 |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5}))) |
89 *} |
89 *} |
90 print_theorems |
90 print_theorems |
91 |
91 |
92 lemma alpha5_rfv: |
92 lemma alpha5_rfv: |
93 "(t \<approx>5 s \<longrightarrow> fv_rtrm5 t = fv_rtrm5 s) \<and> (l \<approx>l m \<longrightarrow> fv_rlts l = fv_rlts m) \<and> (alpha_rbv5 a b c \<longrightarrow> True)" |
93 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)" |
94 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
94 "(l \<approx>l m \<Longrightarrow> (fv_rlts l = fv_rlts m))" |
|
95 "(alpha_rbv5 a b c \<Longrightarrow> True)" |
|
96 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
95 apply(simp_all) |
97 apply(simp_all) |
96 apply(simp add: alpha_gen) |
98 apply(simp add: alpha_gen) |
97 apply(erule conjE)+ |
99 apply(clarify) |
98 apply(erule exE) |
|
99 apply(erule conjE)+ |
|
100 apply(simp_all) |
100 apply(simp_all) |
101 sorry |
101 sorry (* works for non-rec *) |
102 |
102 |
103 lemma bv_list_rsp: |
103 lemma bv_list_rsp: |
104 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
104 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
105 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
105 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
106 apply(simp_all) |
106 apply(simp_all) |
120 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
120 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
121 "(op = ===> alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" |
121 "(op = ===> alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" |
122 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
122 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
123 apply (clarify) |
123 apply (clarify) |
124 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
124 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
125 defer |
125 apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
|
126 apply (simp_all add: alpha5_inj) |
126 apply clarify |
127 apply clarify |
127 apply (erule alpha_rlts.cases) |
128 apply clarify |
128 apply (erule alpha_rlts.cases) |
129 apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
129 apply (simp_all) |
130 apply simp_all |
130 defer |
131 apply (erule_tac[!] alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) |
131 apply (erule alpha_rlts.cases) |
132 apply simp_all |
132 apply (simp_all) |
133 defer defer (* Both sides false, so equal when we have distinct *) |
133 defer |
134 apply (erule conjE)+ |
134 apply clarify |
135 apply clarify |
135 apply (simp add: alpha5_inj) |
136 apply (simp add: alpha5_inj) |
136 sorry (* may be true? *) |
137 sorry (* may be true? *) |
|
138 |
137 lemma |
139 lemma |
138 shows "(alpha_rlts ===> op =) rbv5 rbv5" |
140 shows "(alpha_rlts ===> op =) rbv5 rbv5" |
139 by (simp add: bv_list_rsp) |
141 by (simp add: bv_list_rsp) |
140 |
142 |
141 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] |
143 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] |