122 apply(simp add: pt_name1) |
122 apply(simp add: pt_name1) |
123 apply(assumption) |
123 apply(assumption) |
124 apply(simp add: abs_fresh) |
124 apply(simp add: abs_fresh) |
125 done |
125 done |
126 |
126 |
|
127 |
|
128 ML {* val qty = @{typ "lam"} *} |
|
129 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
127 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def} *} |
130 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def} *} |
128 ML {* val consts = [@{const_name "rVar"}, @{const_name "rApp"}, @{const_name "rLam"}, @{const_name "perm"}]; *} |
131 ML {* val consts = lookup_quot_consts defs *} |
129 |
132 ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "lam" *} |
130 ML {* val rty = @{typ "rlam"} *} |
|
131 ML {* val qty = @{typ "lam"} *} |
|
132 ML {* val rel = @{term "alpha"} *} |
|
133 ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *} |
|
134 ML {* val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv] *} |
|
135 ML {* val quot = @{thm QUOTIENT_lam} *} |
|
136 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
133 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
137 ML {* val trans2 = @{thm QUOT_TYPE_I_lam.R_trans2} *} |
134 ML {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *} |
138 ML {* val reps_same = @{thm QUOT_TYPE_I_lam.REPS_same} *} |
|
139 |
|
140 ML {* add_lower_defs @{context} @{thms perm_lam_def} *} |
|
141 ML {* val rr = @{thm eq_reflection} OF [hd (rev (add_lower_defs @{context} @{thms perm_lam_def}))] *} |
|
142 |
|
143 ML {* val rrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rr *} |
|
144 ML {* |
|
145 fun lift_thm_lam lthy t = |
|
146 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t |
|
147 *} |
|
148 |
135 |
149 ML {* lift_thm_lam @{context} @{thm pi_var_com} *} |
136 ML {* lift_thm_lam @{context} @{thm pi_var_com} *} |
150 ML {* lift_thm_lam @{context} @{thm pi_app_com} *} |
137 ML {* lift_thm_lam @{context} @{thm pi_app_com} *} |
151 ML {* lift_thm_lam @{context} @{thm pi_lam_com} *} |
138 ML {* lift_thm_lam @{context} @{thm pi_lam_com} *} |
152 |
|
153 thm supp_def |
|
154 |
139 |
155 fun |
140 fun |
156 option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)" |
141 option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)" |
157 where |
142 where |
158 "option_map f (nSome x) = nSome (f x)" |
143 "option_map f (nSome x) = nSome (f x)" |
180 apply (simp only: option_map.simps) |
165 apply (simp only: option_map.simps) |
181 apply (subst option_rel.simps) |
166 apply (subst option_rel.simps) |
182 (* Simp starts hanging so don't know how to continue *) |
167 (* Simp starts hanging so don't know how to continue *) |
183 sorry |
168 sorry |
184 |
169 |
185 (* Christian: Does it make sense? *) |
170 (* Not sure if it make sense or if it will be needed *) |
186 lemma abs_fun_rsp: "(op = ===> alpha ===> op = ===> op =) abs_fun abs_fun" |
171 lemma abs_fun_rsp: "(op = ===> alpha ===> op = ===> op =) abs_fun abs_fun" |
187 sorry |
172 sorry |
188 |
173 |
189 (* Should not be needed *) |
174 (* Should not be needed *) |
190 lemma eq_rsp2: "((op = ===> op =) ===> (op = ===> op =) ===> op =) op = op =" |
175 lemma eq_rsp2: "((op = ===> op =) ===> (op = ===> op =) ===> op =) op = op =" |
214 (* It is just a test, it doesn't seem true... *) |
199 (* It is just a test, it doesn't seem true... *) |
215 lemma quotient_cheat: "QUOTIENT op = (option_map ABS_lam) (option_map REP_lam)" |
200 lemma quotient_cheat: "QUOTIENT op = (option_map ABS_lam) (option_map REP_lam)" |
216 sorry |
201 sorry |
217 |
202 |
218 ML {* val rsp_thms = @{thms abs_fun_rsp OPT_QUOTIENT eq_rsp2 quotient_cheat perm_rsp_eq fresh_rsp_eq} @ rsp_thms *} |
203 ML {* val rsp_thms = @{thms abs_fun_rsp OPT_QUOTIENT eq_rsp2 quotient_cheat perm_rsp_eq fresh_rsp_eq} @ rsp_thms *} |
219 ML {* |
204 ML {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *} |
220 fun lift_thm_lam lthy t = |
|
221 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t |
|
222 *} |
|
223 |
205 |
224 thm a3 |
206 thm a3 |
225 ML {* Toplevel.program (fn () => lift_thm_lam @{context} @{thm a3}) *} |
207 ML {* Toplevel.program (fn () => lift_thm_lam @{context} @{thm a3}) *} |
226 thm a3 |
208 thm a3 |
227 ML {* val t_u1 = eqsubst_thm @{context} @{thms abs_fresh(1)} (atomize_thm @{thm a3}) *} |
209 ML {* val t_u1 = eqsubst_thm @{context} @{thms abs_fresh(1)} (atomize_thm @{thm a3}) *} |