--- 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}
*}
--- 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
--- 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}
+*}
--- 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"
--- 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
-
--- 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 *)
--- 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)
--- 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 *)