--- a/Nominal/Ex/CoreHaskell.thy Sat Aug 21 20:07:52 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy Sun Aug 22 11:00:53 2010 +0800
@@ -106,49 +106,82 @@
*}
ML {*
- val thms_d = map (lift_thm qtys @{context}) @{thms distinct}
-*}
-
-ML {*
- val thms_i = map (lift_thm qtys @{context}) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts}
+fun lifted ctxt qtys rthm =
+let
+ (* When the theorem is atomized, eta redexes are contracted,
+ so we do it both in the original theorem *)
+ val rthm' = Drule.eta_contraction_rule rthm
+ val ((_, [rthm'']), ctxt') = Variable.import false [rthm'] ctxt
+ val goal = Quotient_Term.derive_qtrm ctxt' qtys (prop_of rthm'')
+in
+ Goal.prove ctxt' [] [] goal (K (Quotient_Tacs.lift_tac ctxt' [rthm'] 1))
+ |> singleton (ProofContext.export ctxt' ctxt)
+end
*}
ML {*
- val thms_f = map (lift_thm qtys @{context}) @{thms fv_defs}
+fun lifted2 ctxt qtys rthms =
+let
+ (* When the theorem is atomized, eta redexes are contracted,
+ so we do it both in the original theorem *)
+ val rthms' = map Drule.eta_contraction_rule rthms
+ val ((_, rthms''), ctxt') = Variable.import false rthms' ctxt
+ val goals = map (Quotient_Term.derive_qtrm ctxt' qtys o prop_of) rthms''
+in
+ Goal.prove_multi ctxt' [] [] goals (K (Quotient_Tacs.lift_tac ctxt' rthms' 1))
+ |> ProofContext.export ctxt' ctxt
+end
+*}
+
+ML {*
+ val _ = timeit (fn () => map (lifted @{context} qtys) @{thms distinct})
+*}
+
+ML {*
+ val _ = timeit (fn () => lifted2 @{context} qtys @{thms distinct})
+*}
+
+
+ML {*
+ val thms_i = map (lift_thm @{context} qtys) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts}
+*}
+
+ML {*
+ val thms_f = map (lift_thm @{context} qtys) @{thms fv_defs}
*}
ML {*
- val thms_i = map (lift_thm qtys @{context}) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98)}
+ val thms_i = map (lift_thm @{context} qtys) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98)}
*}
ML {*
- val thms_p = map (lift_thm qtys @{context}) @{thms perm_simps}
+ val thms_p = map (lift_thm @{context} qtys) @{thms perm_simps}
*}
ML {*
- val thms_f = map (lift_thm qtys @{context}) @{thms perm_laws}
+ val thms_f = map (lift_thm @{context} qtys) @{thms perm_laws}
*}
ML {*
- val thms_e = map (lift_thm qtys @{context})
+ val thms_e = map (lift_thm @{context} qtys)
@{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
prod.cases]}
*}
ML {*
- val thms_f = map (lift_thm qtys @{context}) @{thms bn_defs}
+ val thms_f = map (lift_thm @{context} qtys) @{thms bn_defs}
*}
ML {*
- val thms_f = map (lift_thm qtys @{context}) @{thms bn_eqvt}
+ val thms_f = map (lift_thm @{context} qtys) @{thms bn_eqvt}
*}
ML {*
- val thms_f = map (lift_thm qtys @{context}) @{thms fv_eqvt}
+ val thms_f = map (lift_thm @{context} qtys) @{thms fv_eqvt}
*}
ML {*
- val thms_f = map (lift_thm qtys @{context}) @{thms size_eqvt}
+ val thms_f = map (lift_thm @{context} qtys) @{thms size_eqvt}
*}
--- a/Nominal/Ex/SingleLet.thy Sat Aug 21 20:07:52 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy Sun Aug 22 11:00:53 2010 +0800
@@ -23,8 +23,6 @@
"bn (As x y t) = {atom x}"
-
-
ML {* Function.prove_termination *}
text {* can lift *}
@@ -44,65 +42,78 @@
thm bn_eqvt
thm size_eqvt
-
ML {*
- val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct}
-*}
-
-ML {*
- val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.inducts}
-*}
-
-ML {*
- val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw.exhaust}
-*}
-
-ML {*
- val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms assg_raw.exhaust}
+fun lifted ctxt qtys rthm =
+let
+ (* When the theorem is atomized, eta redexes are contracted,
+ so we do it both in the original theorem *)
+ val rthm' = Drule.eta_contraction_rule rthm
+ val ((_, [rthm'']), ctxt') = Variable.import false [rthm'] ctxt
+ val goal = Quotient_Term.derive_qtrm ctxt' qtys (prop_of rthm'')
+in
+ Goal.prove ctxt' [] [] goal (K (Quotient_Tacs.lift_tac ctxt' [rthm'] 1))
+ |> singleton (ProofContext.export ctxt' ctxt)
+end
*}
ML {*
- val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs}
+ val _ = timeit (fn () => map (lifted @{context} [@{typ trm}, @{typ assg}]) @{thms distinct})
*}
ML {*
- val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)}
+ val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms trm_raw_assg_raw.inducts}
+*}
+
+ML {*
+ val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms trm_raw.exhaust}
+*}
+
+ML {*
+ val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms assg_raw.exhaust}
*}
ML {*
- val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps}
+ val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms fv_defs}
+*}
+
+ML {*
+ val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms trm_raw_assg_raw.size(9 - 16)}
*}
ML {*
- val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws}
+ val thms_p = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms perm_simps}
*}
ML {*
- val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context})
+ val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms perm_laws}
+*}
+
+ML {*
+ val thms_e = map (lift_thm @{context} [@{typ trm}, @{typ assg}])
@{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
prod.cases]}
*}
ML {*
- val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context})
+ val thms_e = map (lift_thm @{context} [@{typ trm}, @{typ assg}])
@{thms eq_iff_simps[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
prod.cases]}
*}
ML {*
- val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms bn_defs}
+ val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms bn_defs}
*}
ML {*
- val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms bn_eqvt}
+ val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms bn_eqvt}
*}
ML {*
- val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_eqvt}
+ val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms fv_eqvt}
*}
ML {*
- val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms size_eqvt}
+ val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms size_eqvt}
*}
--- a/Nominal/NewParser.thy Sat Aug 21 20:07:52 2010 +0800
+++ b/Nominal/NewParser.thy Sun Aug 22 11:00:53 2010 +0800
@@ -566,7 +566,7 @@
fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
val _ = warning "Lifting induction";
val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs;
- val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 raw_induct_thm);
+ val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 qtys raw_induct_thm);
fun note_suffix s th ctxt =
snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
fun note_simp_suffix s th ctxt =
@@ -576,24 +576,24 @@
[Rule_Cases.name constr_names q_induct]) lthy13;
val q_inducts = Project_Rule.projects lthy13 (1 upto (length raw_fvs)) q_induct
val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
- val q_perm = map (lift_thm qtys lthy14) raw_perm_simps;
+ val q_perm = map (lift_thm lthy14 qtys) raw_perm_simps;
val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
- val q_fv = map (lift_thm qtys lthy15) raw_fv_defs;
+ val q_fv = map (lift_thm lthy15 qtys) raw_fv_defs;
val lthy16 = note_simp_suffix "fv" q_fv lthy15;
- val q_bn = map (lift_thm qtys lthy16) raw_bn_defs;
+ val q_bn = map (lift_thm lthy16 qtys) raw_bn_defs;
val lthy17 = note_simp_suffix "bn" q_bn lthy16;
val _ = warning "Lifting eq-iff";
(*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff
val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0
- val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded1;
+ val q_eq_iff_pre0 = map (lift_thm lthy17 qtys) eq_iff_unfolded1;
val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms Pair_eqvt}) q_eq_iff_pre0
val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1
val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2
val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
- val q_dis = map (lift_thm qtys lthy18) alpha_distincts;
+ val q_dis = map (lift_thm lthy18 qtys) alpha_distincts;
val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
- val q_eqvt = map (lift_thm qtys lthy19) (raw_bn_eqvt @ raw_fv_eqvt);
+ val q_eqvt = map (lift_thm lthy19 qtys) (raw_bn_eqvt @ raw_fv_eqvt);
val (_, lthy20) = Local_Theory.note ((Binding.empty,
[Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
val _ = warning "Supports";
--- a/Nominal/Rsp.thy Sat Aug 21 20:07:52 2010 +0800
+++ b/Nominal/Rsp.thy Sun Aug 22 11:00:53 2010 +0800
@@ -5,7 +5,7 @@
ML {*
fun const_rsp qtys lthy const =
let
- val nty = Quotient_Term.derive_qtyp qtys (fastype_of const) lthy
+ val nty = Quotient_Term.derive_qtyp lthy qtys (fastype_of const)
val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty);
in
HOLogic.mk_Trueprop (rel $ const $ const)
--- a/Nominal/nominal_dt_quot.ML Sat Aug 21 20:07:52 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML Sun Aug 22 11:00:53 2010 +0800
@@ -19,7 +19,7 @@
val define_qsizes: typ list -> string list -> (string * term * mixfix) list ->
local_theory -> local_theory
- val lift_thm: typ list -> Proof.context -> thm -> thm
+ val lift_thm: Proof.context -> typ list -> thm -> thm
end
structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
@@ -56,7 +56,7 @@
val (_, lthy'') = define_qconsts qtys perm_specs lthy'
- val lifted_perm_laws = map (Quotient_Tacs.lifted qtys lthy'') raw_perm_laws
+ val lifted_perm_laws = map (Quotient_Tacs.lifted lthy'' qtys) raw_perm_laws
fun tac _ =
Class.intro_classes_tac [] THEN
@@ -106,8 +106,8 @@
Thm.rename_boundvars trm trm' th
end
-fun lift_thm qtys ctxt thm =
- Quotient_Tacs.lifted qtys ctxt thm
+fun lift_thm ctxt qtys thm =
+ Quotient_Tacs.lifted ctxt qtys thm
|> unraw_bounds_thm
|> unraw_vars_thm