# HG changeset patch # User Christian Urban # Date 1282451813 -28800 # Node ID b29eb13d3f9df114445cc835c28b266b83b8a013 # Parent 58e60df1ff79a8bda067196c6b08cb987f42d282# Parent f5cbf74d4ec5894d833c9049e13404ea26a74bb3 merged diff -r f5cbf74d4ec5 -r b29eb13d3f9d Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Fri Aug 20 16:55:58 2010 +0900 +++ b/Nominal/Ex/CoreHaskell.thy Sun Aug 22 12:36:53 2010 +0800 @@ -20,7 +20,7 @@ | TC "string" | TApp "ty" "ty" | TFun "string" "ty_lst" -| TAll tv::"tvar" "tkind" T::"ty" bind_set tv in T +| TAll tv::"tvar" "tkind" T::"ty" bind (set) tv in T | TEq "ckind" "ty" and ty_lst = TsNil @@ -30,7 +30,7 @@ | CConst "string" | CApp "co" "co" | CFun "string" "co_lst" -| CAll cv::"cvar" "ckind" C::"co" bind_set cv in C +| CAll cv::"cvar" "ckind" C::"co" bind (set) cv in C | CEq "ckind" "co" | CRefl "ty" | CSym "co" @@ -48,13 +48,13 @@ and trm = Var "var" | K "string" -| LAMT tv::"tvar" "tkind" t::"trm" bind_set tv in t -| LAMC cv::"cvar" "ckind" t::"trm" bind_set cv in t +| LAMT tv::"tvar" "tkind" t::"trm" bind (set) tv in t +| LAMC cv::"cvar" "ckind" t::"trm" bind (set) cv in t | AppT "trm" "ty" | AppC "trm" "co" -| Lam v::"var" "ty" t::"trm" bind_set v in t +| Lam v::"var" "ty" t::"trm" bind (set) v in t | App "trm" "trm" -| Let x::"var" "ty" "trm" t::"trm" bind_set x in t +| Let x::"var" "ty" "trm" t::"trm" bind (set) x in t | Case "trm" "assoc_lst" | Cast "trm" "ty" --"ty is supposed to be a coercion type only" and assoc_lst = @@ -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} *} diff -r f5cbf74d4ec5 -r b29eb13d3f9d Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Fri Aug 20 16:55:58 2010 +0900 +++ b/Nominal/Ex/Lambda.thy Sun Aug 22 12:36:53 2010 +0800 @@ -1,14 +1,19 @@ theory Lambda -imports "../NewParser" Quotient_Option +imports "../NewParser" begin atom_decl name -declare [[STEPS = 9]] +declare [[STEPS = 2]] -nominal_datatype lam = +nominal_datatype 'a lam = Var "name" -| App "lam" "lam" -| Lam x::"name" l::"lam" bind x in l +| App "'a lam" "'a lam" +| Lam x::"name" l::"'a lam" bind x in l + +ML {* Datatype.read_typ *} + + +thm eq_iff thm lam.fv thm lam.supp diff -r f5cbf74d4ec5 -r b29eb13d3f9d Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Fri Aug 20 16:55:58 2010 +0900 +++ b/Nominal/Ex/SingleLet.thy Sun Aug 22 12:36:53 2010 +0800 @@ -10,9 +10,9 @@ nominal_datatype trm = Var "name" | App "trm" "trm" -| Lam x::"name" t::"trm" bind_set x in t -| Let a::"assg" t::"trm" bind_set "bn a" in t -| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind_set x in y t t1 t2 +| Lam x::"name" t::"trm" bind x in t +| Let a::"assg" t::"trm" bind (set) "bn a" in t +| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2 | Bar x::"name" y::"name" t::"trm" bind y x in t x y | Baz x::"name" t1::"trm" t2::"trm" bind x in t1, bind x in t2 and assg = @@ -23,7 +23,6 @@ "bn (As x y t) = {atom x}" - ML {* Function.prove_termination *} text {* can lift *} @@ -32,78 +31,90 @@ thm trm_raw_assg_raw.inducts thm trm_raw.exhaust thm assg_raw.exhaust -thm FV_defs +thm fv_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 fv_eqvt thm bn_eqvt thm size_eqvt - ML {* - val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} +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_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 _ = timeit (fn () => map (lifted @{context} [@{typ trm}, @{typ assg}]) @{thms distinct}) *} ML {* - val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms assg_raw.exhaust} + val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms trm_raw_assg_raw.inducts} *} -ML {* - val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs} +ML {* + val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms trm_raw.exhaust} *} 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 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} -*} - -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_defs} *} 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 bn_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 fv_eqvt} *} +ML {* + val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}]) @{thms size_eqvt} +*} diff -r f5cbf74d4ec5 -r b29eb13d3f9d Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Fri Aug 20 16:55:58 2010 +0900 +++ b/Nominal/Ex/TypeSchemes.thy Sun Aug 22 12:36:53 2010 +0800 @@ -6,7 +6,7 @@ atom_decl name -declare [[STEPS = 15]] +declare [[STEPS = 20]] nominal_datatype ty = Var "name" diff -r f5cbf74d4ec5 -r b29eb13d3f9d Nominal/Lift.thy --- a/Nominal/Lift.thy Fri Aug 20 16:55:58 2010 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,66 +0,0 @@ -theory Lift -imports "../Nominal-General/Nominal2_Atoms" - "../Nominal-General/Nominal2_Eqvt" - "../Nominal-General/Nominal2_Supp" - "Abs" "Perm" "Rsp" -begin - -ML {* -fun define_quotient_types binds tys alphas equivps ctxt = -let - fun def_ty ((b, ty), (alpha, equivp)) ctxt = - Quotient_Type.add_quotient_type ((([], b, NoSyn), (ty, alpha, false)), equivp) ctxt; - val alpha_equivps = List.take (equivps, length alphas) - val (qinfo, ctxt') = fold_map def_ty ((binds ~~ tys) ~~ (alphas ~~ alpha_equivps)) ctxt; - val qtys = map #qtyp qinfo; -in - (qtys, ctxt') -end -*} - -(* Renames schematic variables in a theorem *) -ML {* -fun rename_vars fnctn thm = -let - val vars = Term.add_vars (prop_of thm) [] - val nvars = map (Var o ((apfst o apfst) fnctn)) vars -in - Thm.certify_instantiate ([], (vars ~~ nvars)) thm -end -*} - -ML {* -fun un_raws name = -let - fun un_raw name = unprefix "_raw" name handle Fail _ => name - fun add_under names = hd names :: (map (prefix "_") (tl names)) -in - implode (map un_raw (add_under (space_explode "_" name))) -end -*} - -(* Similar to Tools/IsaPlanner/rw_tools.ML *) -ML {* -fun rename_term_bvars (Abs(s, ty, t)) = (Abs(un_raws s, ty, rename_term_bvars t)) - | rename_term_bvars (a $ b) = (rename_term_bvars a) $ (rename_term_bvars b) - | rename_term_bvars x = x; - -fun rename_thm_bvars th = -let - val t = Thm.prop_of th -in - Thm.rename_boundvars t (rename_term_bvars t) th -end; -*} - -ML {* -fun lift_thm qtys ctxt thm = -let - val un_raw_names = rename_vars un_raws -in - rename_thm_bvars (un_raw_names (Quotient_Tacs.lifted qtys ctxt thm)) -end -*} - -end - diff -r f5cbf74d4ec5 -r b29eb13d3f9d Nominal/NewParser.thy --- a/Nominal/NewParser.thy Fri Aug 20 16:55:58 2010 +0900 +++ b/Nominal/NewParser.thy Sun Aug 22 12:36:53 2010 +0800 @@ -2,7 +2,7 @@ imports "../Nominal-General/Nominal2_Base" "../Nominal-General/Nominal2_Eqvt" "../Nominal-General/Nominal2_Supp" - "Perm" "Tacs" "Lift" "Equivp" + "Perm" "Tacs" "Equivp" begin (* TODO @@ -20,48 +20,7 @@ *} - -ML {* -(* nominal datatype parser *) -local - structure P = Parse; - structure S = Scan - - fun triple1 ((x, y), z) = (x, y, z) - fun triple2 (x, (y, z)) = (x, y, z) - fun tuple ((x, y, z), u) = (x, y, z, u) - fun tswap (((x, y), z), u) = (x, y, u, z) -in - -val _ = Keyword.keyword "bind" -val _ = Keyword.keyword "bind_set" -val _ = Keyword.keyword "bind_res" - -val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ - -val bind_mode = P.$$$ "bind" || P.$$$ "bind_set" || P.$$$ "bind_res" - -val bind_clauses = - P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1) - -val cnstr_parser = - P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tswap - -(* datatype parser *) -val dt_parser = - (P.type_args -- P.binding -- P.opt_mixfix >> triple1) -- - (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple - -(* binding function parser *) -val bnfun_parser = - S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], []) - -(* main parser *) -val main_parser = - P.and_list1 dt_parser -- bnfun_parser >> triple2 - -end -*} +ML {* print_depth 50 *} ML {* fun get_cnstrs dts = @@ -288,7 +247,7 @@ (* for testing porposes - to exit the procedure early *) exception TEST of Proof.context -val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 10); +val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 0); fun get_STEPS ctxt = Config.get ctxt STEPS *} @@ -607,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 = @@ -617,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"; @@ -667,7 +626,7 @@ val thy = ProofContext.theory_of lthy fun mk_type full_tname tvrs = - Type (full_tname, map (fn a => TVar ((a, 0), [])) tvrs) + Type (full_tname, map (fn a => TFree (a, @{sort "{pt, fs}"})) tvrs) fun prep_cnstr full_tname tvs (cname, anno_tys, mx, _) = let @@ -687,6 +646,8 @@ end val (cnstrs, dts) = split_list (map prep_dt dt_strs) + + val _ = tracing ("Contructors:\n" ^ cat_lines (map @{make_string} cnstrs)) in lthy |> Local_Theory.theory (Sign.add_consts_i (flat cnstrs)) @@ -744,16 +705,12 @@ fun prep_body env bn_str = index_lookup env bn_str - fun prep_mode "bind" = Lst - | prep_mode "bind_set" = Set - | prep_mode "bind_res" = Res - fun prep_bclause env (mode, binders, bodies) = let val binders' = map (prep_binder env) binders val bodies' = map (prep_body env) bodies in - BC (prep_mode mode, binders', bodies') + BC (mode, binders', bodies') end fun prep_bclauses (annos, bclause_strs) = @@ -812,7 +769,51 @@ in timeit (fn () => nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd) end +*} +ML {* +(* nominal datatype parser *) +local + structure P = Parse; + structure S = Scan + + fun triple1 ((x, y), z) = (x, y, z) + fun triple2 (x, (y, z)) = (x, y, z) + fun tuple ((x, y, z), u) = (x, y, z, u) + fun tswap (((x, y), z), u) = (x, y, u, z) +in + +val _ = Keyword.keyword "bind" +val _ = Keyword.keyword "set" +val _ = Keyword.keyword "res" +val _ = Keyword.keyword "list" + +val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ + +val bind_mode = P.$$$ "bind" |-- + S.optional (Args.parens + (P.$$$ "list" >> K Lst || P.$$$ "set" >> K Set || P.$$$ "res" >> K Res)) Lst + +val bind_clauses = + P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1) + +val cnstr_parser = + P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tswap + +(* datatype parser *) +val dt_parser = + (P.type_args -- P.binding -- P.opt_mixfix >> triple1) -- + (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple + +(* binding function parser *) +val bnfun_parser = + S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], []) + +(* main parser *) +val main_parser = + P.and_list1 dt_parser -- bnfun_parser >> triple2 + +end (* Command Keyword *) diff -r f5cbf74d4ec5 -r b29eb13d3f9d Nominal/Rsp.thy --- a/Nominal/Rsp.thy Fri Aug 20 16:55:58 2010 +0900 +++ b/Nominal/Rsp.thy Sun Aug 22 12:36: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) diff -r f5cbf74d4ec5 -r b29eb13d3f9d Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Fri Aug 20 16:55:58 2010 +0900 +++ b/Nominal/nominal_dt_quot.ML Sun Aug 22 12:36:53 2010 +0800 @@ -2,7 +2,7 @@ Author: Christian Urban Author: Cezary Kaliszyk - Performing quotient constructions + Performing quotient constructions and lifting theorems *) signature NOMINAL_DT_QUOT = @@ -18,6 +18,8 @@ val define_qsizes: typ list -> string list -> (string * term * mixfix) list -> local_theory -> local_theory + + val lift_thm: Proof.context -> typ list -> thm -> thm end structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = @@ -54,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 @@ -79,5 +81,36 @@ |> Named_Target.theory_init end + +(* lifts a theorem and deletes all "_raw" suffixes *) + +fun unraw_str s = + unsuffix "_raw" s + handle Fail _ => s + +fun unraw_vars_thm thm = +let + fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T) + + val vars = Term.add_vars (prop_of thm) [] + val vars' = map (Var o unraw_var_str) vars +in + Thm.certify_instantiate ([], (vars ~~ vars')) thm +end + +fun unraw_bounds_thm th = +let + val trm = Thm.prop_of th + val trm' = Term.map_abs_vars unraw_str trm +in + Thm.rename_boundvars trm trm' th +end + +fun lift_thm ctxt qtys thm = + Quotient_Tacs.lifted ctxt qtys thm + |> unraw_bounds_thm + |> unraw_vars_thm + + end (* structure *)