# HG changeset patch # User Christian Urban # Date 1282748142 -28800 # Node ID 92dc6cfa3a95d4592107343fd9302db3ca430ee5 # Parent ff887850d83c48caa1cb3a4aa36a6119b89f0de4 automatic lifting diff -r ff887850d83c -r 92dc6cfa3a95 Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Wed Aug 25 20:19:10 2010 +0800 +++ b/Nominal/Ex/Classical.thy Wed Aug 25 22:55:42 2010 +0800 @@ -7,7 +7,7 @@ atom_decl name atom_decl coname -declare [[STEPS = 9]] +declare [[STEPS = 21]] nominal_datatype trm = Ax "name" "coname" @@ -18,17 +18,17 @@ | ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2 | ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t -thm alpha_trm_raw.intros[no_vars] +thm distinct +thm induct +thm exhaust +thm fv_defs +thm bn_defs +thm perm_simps +thm eq_iff +thm fv_bn_eqvt +thm size_eqvt -(* -thm trm.fv -thm trm.eq_iff -thm trm.bn -thm trm.perm -thm trm.induct -thm trm.distinct -thm trm.fv[simplified trm.supp] -*) + end diff -r ff887850d83c -r 92dc6cfa3a95 Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Wed Aug 25 20:19:10 2010 +0800 +++ b/Nominal/Ex/CoreHaskell.thy Wed Aug 25 22:55:42 2010 +0800 @@ -8,7 +8,7 @@ atom_decl cvar atom_decl tvar -declare [[STEPS = 20]] +declare [[STEPS = 21]] nominal_datatype tkind = KStar @@ -88,72 +88,15 @@ (* can lift *) thm distinct +thm induct +thm exhaust thm fv_defs -thm alpha_bn_imps alpha_equivp - -thm 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 +thm bn_defs thm perm_simps -thm perm_laws -thm 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) - thm eq_iff -thm eq_iff_simps - -ML {* - val qtys = [@{typ tkind}, @{typ ckind}, @{typ ty}, @{typ ty_lst}, @{typ co}, - @{typ co_lst}, @{typ trm}, @{typ assoc_lst}, @{typ pat}, @{typ vars}, - @{typ tvars}, @{typ cvars}] -*} - - -ML {* - val _ = timeit (fn () => map (lift_thm @{context} qtys []) @{thms distinct}) -*} - -ML {* - val _ = timeit (fn () => 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.induct}) -*} - -ML {* - val thms_f = map (lift_thm @{context} qtys []) @{thms fv_defs} -*} +thm fv_bn_eqvt +thm size_eqvt -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.size(50 - 98)} -*} - -ML {* - val thms_p = map (lift_thm @{context} qtys []) @{thms perm_simps} -*} - -ML {* - val thms_f = map (lift_thm @{context} qtys []) @{thms perm_laws} -*} - -ML {* - val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps - prod.cases} -*} - -ML {* - val thms_e = map (lift_thm @{context} qtys simps) @{thms eq_iff} -*} - -ML {* - val thms_f = map (lift_thm @{context} qtys []) @{thms bn_defs} -*} - -ML {* - val thms_f = map (lift_thm @{context} qtys []) @{thms bn_eqvt} -*} - -ML {* - val thms_f = map (lift_thm @{context} qtys []) @{thms fv_eqvt} -*} - -ML {* - val thms_f = map (lift_thm @{context} qtys []) @{thms size_eqvt} -*} diff -r ff887850d83c -r 92dc6cfa3a95 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Wed Aug 25 20:19:10 2010 +0800 +++ b/Nominal/Ex/Lambda.thy Wed Aug 25 22:55:42 2010 +0800 @@ -3,7 +3,7 @@ begin atom_decl name -declare [[STEPS = 20]] +declare [[STEPS = 21]] class s1 class s2 @@ -14,88 +14,16 @@ | App "('a::s1, 'b::s2) lam" "('a, 'b) lam" | Lam x::"name" l::"('a, 'b) lam" bind x in l -term Var_raw -term Var -term App_raw -term App -thm Var_def App_def Lam_def -term abs_lam - thm distinct -thm lam_raw.inducts -thm lam_raw.exhaust +thm induct +thm exhaust thm fv_defs thm bn_defs thm perm_simps -thm perm_laws -thm lam_raw.size thm eq_iff -thm eq_iff_simps -thm fv_eqvt -thm bn_eqvt +thm fv_bn_eqvt thm size_eqvt -ML {* - val qtys = [@{typ "('a::{s1, fs}, 'b::{s2,fs}) lam"}] -*} - -ML {* - val thm_a = timeit (fn () => map (lift_thm @{context} qtys []) @{thms distinct}) -*} - -ML {* - val thms_i = map (lift_thm @{context} qtys []) @{thms lam_raw.induct} -*} - -ML {* - val thms_i = map (lift_thm @{context} qtys []) @{thms lam_raw.exhaust} -*} - -ML {* - val thms_f = map (lift_thm @{context} qtys []) @{thms fv_defs} -*} - -ML {* - val thms_p = map (lift_thm @{context} qtys []) @{thms perm_simps} -*} - -ML {* - val thms_f = map (lift_thm @{context} qtys []) @{thms perm_laws} -*} - -ML {* - val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps - prod.cases} -*} - -ML {* - val thms_e = map (lift_thm @{context} qtys simps) @{thms eq_iff} -*} - -ML {* - val thms_e = map (lift_thm @{context} qtys simps) @{thms eq_iff_simps} -*} - - -ML {* - val thms_f = map (lift_thm @{context} qtys []) @{thms bn_defs} -*} - -ML {* - val thms_f = map (lift_thm @{context} qtys []) @{thms bn_eqvt} -*} - -ML {* - val thms_f = map (lift_thm @{context} qtys []) @{thms fv_eqvt} -*} - -ML {* - val thms_f = map (lift_thm @{context} qtys []) @{thms size_eqvt} -*} - - - -thm eq_iff thm lam.fv thm lam.supp diff -r ff887850d83c -r 92dc6cfa3a95 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Wed Aug 25 20:19:10 2010 +0800 +++ b/Nominal/Ex/SingleLet.thy Wed Aug 25 22:55:42 2010 +0800 @@ -4,7 +4,7 @@ atom_decl name -declare [[STEPS = 20]] +declare [[STEPS = 21]] nominal_datatype singlelet: trm = Var "name" @@ -22,86 +22,17 @@ "bn (As x y t) = {atom x}" -text {* can lift *} - thm distinct -thm trm_raw_assg_raw.inducts -thm trm_raw.exhaust -thm assg_raw.exhaust +thm induct +thm exhaust thm fv_defs thm bn_defs thm perm_simps -thm perm_laws -thm trm_raw_assg_raw.size(9 - 16) thm eq_iff -thm eq_iff_simps -thm bn_defs -thm fv_eqvt -thm bn_eqvt +thm fv_bn_eqvt thm size_eqvt -ML {* - val _ = timeit (fn () => map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms distinct}) -*} - -ML {* - 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_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_p = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms perm_simps} -*} - -ML {* - val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms perm_laws} -*} - -ML {* - val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps - prod.cases} -*} - -ML {* - val thms_e = map (lift_thm @{context} [@{typ trm}, @{typ assg}] simps) @{thms eq_iff} -*} - -ML {* - val thms_e = map (lift_thm @{context} [@{typ trm}, @{typ assg}] simps) @{thms eq_iff_simps} -*} - -ML {* - val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms bn_defs} -*} - -ML {* - val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms bn_eqvt} -*} - -ML {* - val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms fv_eqvt} -*} - -ML {* - val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms size_eqvt} -*} - diff -r ff887850d83c -r 92dc6cfa3a95 Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Wed Aug 25 20:19:10 2010 +0800 +++ b/Nominal/Ex/TypeSchemes.thy Wed Aug 25 22:55:42 2010 +0800 @@ -6,22 +6,22 @@ atom_decl name -declare [[STEPS = 20]] +declare [[STEPS = 21]] nominal_datatype ty = Var "name" | Fun "ty" "ty" and tys = - All xs::"name fset" ty::"ty" bind_res xs in ty + All xs::"name fset" ty::"ty" bind (res) xs in ty + nominal_datatype ty2 = Var2 "name" | Fun2 "ty2" "ty2" -instance ty2 :: pt sorry nominal_datatype tys2 = - All2 xs::"name fset" ty::"ty2" bind_res xs in ty + All2 xs::"name fset" ty::"ty2" bind (res) xs in ty lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp] diff -r ff887850d83c -r 92dc6cfa3a95 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Wed Aug 25 20:19:10 2010 +0800 +++ b/Nominal/NewParser.thy Wed Aug 25 22:55:42 2010 +0800 @@ -471,24 +471,50 @@ val qfvs = map #qconst qfvs_info val qfv_bns = map #qconst qfv_bns_info val qalpha_bns = map #qconst qalpha_bns_info + + (* lifting of the theorems *) + val _ = warning "Lifting of Theorems" + + val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps + prod.cases} + + val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = + if get_STEPS lthy > 20 + then + lthy9a + |> lift_thms qtys [] alpha_distincts + ||>> lift_thms qtys eq_iff_simps alpha_eq_iff + ||>> lift_thms qtys [] raw_fv_defs + ||>> lift_thms qtys [] raw_bn_defs + ||>> lift_thms qtys [] raw_perm_simps + ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) + else raise TEST lthy9a + + val (((qsize_eqvt, [qinduct]), qexhausts), lthyB) = + if get_STEPS lthy > 20 + then + lthyA + |> lift_thms qtys [] raw_size_eqvt + ||>> lift_thms qtys [] [raw_induct_thm] + ||>> lift_thms qtys [] raw_exhaust_thms + else raise TEST lthyA + (* temporary theorem bindings *) - val (_, lthy9') = lthy9a - |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) - ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) - ||>> Local_Theory.note ((@{binding "eq_iff_simps"}, []), alpha_eq_iff_simps) - ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) - ||>> Local_Theory.note ((@{binding "bn_defs"}, []), raw_bn_defs) - ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) - ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) - ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) - ||>> Local_Theory.note ((@{binding "alpha_equivp"}, []), alpha_equivp_thms) - ||>> Local_Theory.note ((@{binding "fv_eqvt"}, []), raw_fv_eqvt) - ||>> Local_Theory.note ((@{binding "bn_eqvt"}, []), raw_bn_eqvt) - ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt) + val (_, lthy9') = lthyB + |> Local_Theory.note ((@{binding "distinct"}, []), qdistincts) + ||>> Local_Theory.note ((@{binding "eq_iff"}, []), qeq_iffs) + ||>> Local_Theory.note ((@{binding "fv_defs"}, []), qfv_defs) + ||>> Local_Theory.note ((@{binding "bn_defs"}, []), qbn_defs) + ||>> Local_Theory.note ((@{binding "perm_simps"}, []), qperm_simps) + ||>> Local_Theory.note ((@{binding "fv_bn_eqvt"}, []), qfv_qbn_eqvts) + ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), qsize_eqvt) + ||>> Local_Theory.note ((@{binding "induct"}, []), [qinduct]) + ||>> Local_Theory.note ((@{binding "exhaust"}, []), qexhausts) + val _ = - if get_STEPS lthy > 20 + if get_STEPS lthy > 21 then true else raise TEST lthy9' (* old stuff *) @@ -553,7 +579,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) []; - val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 qtys [] raw_induct_thm); + val q_induct = Rule_Cases.name constr_names (the_single (fst (lift_thms qtys [] [raw_induct_thm] lthy13))); fun note_suffix s th ctxt = snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); fun note_simp_suffix s th ctxt = @@ -563,24 +589,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 lthy14 qtys []) raw_perm_simps; + val q_perm = fst (lift_thms qtys [] raw_perm_simps lthy14); val lthy15 = note_simp_suffix "perm" q_perm lthy14a; - val q_fv = map (lift_thm lthy15 qtys []) raw_fv_defs; + val q_fv = fst (lift_thms qtys [] raw_fv_defs lthy15); val lthy16 = note_simp_suffix "fv" q_fv lthy15; - val q_bn = map (lift_thm lthy16 qtys []) raw_bn_defs; + val q_bn = fst (lift_thms qtys [] raw_bn_defs lthy16); 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 lthy17 qtys []) eq_iff_unfolded1; + val q_eq_iff_pre0 = fst (lift_thms qtys [] eq_iff_unfolded1 lthy17); 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 lthy18 qtys []) alpha_distincts; + val q_dis = fst (lift_thms qtys [] alpha_distincts lthy18); val lthy19 = note_simp_suffix "distinct" q_dis lthy18; - val q_eqvt = map (lift_thm lthy19 qtys []) (raw_bn_eqvt @ raw_fv_eqvt); + val q_eqvt = fst (lift_thms qtys [] (raw_bn_eqvt @ raw_fv_eqvt) lthy19); val (_, lthy20) = Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; val _ = warning "Supports"; diff -r ff887850d83c -r 92dc6cfa3a95 Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Wed Aug 25 20:19:10 2010 +0800 +++ b/Nominal/nominal_dt_quot.ML Wed Aug 25 22:55:42 2010 +0800 @@ -19,7 +19,7 @@ val define_qsizes: typ list -> string list -> (string * sort) list -> (string * term * mixfix) list -> local_theory -> local_theory - val lift_thm: Proof.context -> typ list -> thm list -> thm -> thm + val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context end structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = @@ -49,8 +49,6 @@ (* defines the quotient permutations and proves pt-class *) fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy = let - val _ = tracing ("qtys:\n" ^ cat_lines (map @{make_string} qtys)) - val lthy1 = lthy |> Local_Theory.exit_global @@ -122,12 +120,12 @@ Thm.rename_boundvars trm trm' th end -fun lift_thm ctxt qtys simps thm = - thm - |> Quotient_Tacs.lifted ctxt qtys simps - |> unraw_bounds_thm - |> unraw_vars_thm - |> Drule.zero_var_indexes +fun lift_thms qtys simps thms ctxt = + (map (Quotient_Tacs.lifted ctxt qtys simps + #> unraw_bounds_thm + #> unraw_vars_thm + #> Drule.zero_var_indexes) thms, ctxt) + end (* structure *)