133 val (const_rsps, lthy9) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
135 val (const_rsps, lthy9) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
134 (fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bvs_rsp) alpha_equivp 1)) consts lthy8 |
136 (fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bvs_rsp) alpha_equivp 1)) consts lthy8 |
135 val (perms_rsp, lthy10) = prove_const_rsp Binding.empty perms |
137 val (perms_rsp, lthy10) = prove_const_rsp Binding.empty perms |
136 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy9; |
138 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy9; |
137 val thy3 = Local_Theory.exit_global lthy10; |
139 val thy3 = Local_Theory.exit_global lthy10; |
|
140 (* TODO: fix this hack... *) |
|
141 val tinfo = #abs_type (Typedef.the_info thy3 "Lift.trm5"); |
|
142 (*val thy4 = define_lifted_perms ["Term1.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})] |
|
143 @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append}*) |
138 val lthy11 = Theory_Target.init NONE thy3; |
144 val lthy11 = Theory_Target.init NONE thy3; |
139 val lift_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy11, induct)); |
145 val lift_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy11, induct)); |
140 val lthy12 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy11) |
146 val lthy12 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy11); |
141 *} |
147 *} |
142 |
148 |
143 setup {* fn _ => Local_Theory.exit_global lthy12 *} |
149 setup {* fn _ => Local_Theory.exit_global lthy12 *} |
144 thm lift_induct |
150 thm lift_induct |
145 |
151 |