--- a/Nominal/Ex/SingleLet.thy Sun Aug 15 14:00:28 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy Mon Aug 16 17:39:16 2010 +0800
@@ -22,6 +22,7 @@
"bn (As x y t) = {atom x}"
(* can lift *)
+
thm distinct
thm trm_raw_assg_raw.inducts
thm fv_defs
@@ -57,7 +58,18 @@
val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws}
*}
-
+ML {*
+ Local_Theory.exit_global;
+ Class.instantiation;
+ Class.prove_instantiation_exit_result;
+ Named_Target.theory_init;
+ op |->
+*}
+
+done
+|> ...
+ |-> (fn x => Class.prove_instantiation_exit_result phi tac x)
+ |-> (fn y => ...)
@@ -87,35 +99,6 @@
val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolding alphas]}
*}
-section {* NOT *}
-
-ML {*
- val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps(1)}
-*}
-
-instance trm :: pt sorry
-instance assg :: pt sorry
-
-
-
-
-
-
-
-
-
-
-thm eq_iff[no_vars]
-
-ML {*
- val q1 = lift_thm [@{typ trm}, @{typ assg}] @{context} @{thm "eq_iff"(1)}
-*}
-
-local_setup {* Local_Theory.note ((@{binding d1}, []), thms_d) #> snd *}
-local_setup {* Local_Theory.note ((@{binding i1}, []), thms_i) #> snd *}
-local_setup {* Local_Theory.note ((@{binding f1}, []), thms_f) #> snd *}
-local_setup {* Local_Theory.note ((@{binding q1}, []), [q1]) #> snd *}
-
thm perm_defs
thm perm_simps
@@ -139,27 +122,6 @@
-ML {*
- map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff}
-*}
-
-
-
-
-
-lemma "Var x \<noteq> App y1 y2"
-apply(descending)
-apply(simp add: trm_raw.distinct)
-
-
-
-ML {*
- map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw.distinct(1)}
-*}
-
-
-
-
typ trm
typ assg
--- a/Nominal/NewParser.thy Sun Aug 15 14:00:28 2010 +0800
+++ b/Nominal/NewParser.thy Mon Aug 16 17:39:16 2010 +0800
@@ -331,12 +331,10 @@
(* definitions of raw permutations *)
val _ = warning "Definition of raw permutations";
- val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) =
+ val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) =
if get_STEPS lthy0 > 1
- then Local_Theory.theory_result
- (define_raw_perms raw_full_ty_names raw_tys raw_constrs raw_induct_thm) lthy0
+ then define_raw_perms raw_full_ty_names raw_tys raw_constrs raw_induct_thm lthy0
else raise TEST lthy0
- val lthy2a = Named_Target.reinit lthy2 lthy2
(* noting the raw permutations as eqvt theorems *)
val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2a
@@ -511,18 +509,14 @@
(* definition of the quotient permfunctions and pt-class *)
val lthy9 =
if get_STEPS lthy > 18
- then Local_Theory.theory
- (define_qperms qtys qty_full_names qperm_descr raw_perm_laws) lthy8
+ then define_qperms qtys qty_full_names qperm_descr raw_perm_laws lthy8
else raise TEST lthy8
- val lthy9' =
+ val lthy9a =
if get_STEPS lthy > 19
- then Local_Theory.theory
- (define_qsizes qtys qty_full_names qsize_descr) lthy9
+ then define_qsizes qtys qty_full_names qsize_descr lthy9
else raise TEST lthy9
- val lthy9a = Named_Target.reinit lthy9' lthy9'
-
val qconstrs = map #qconst qconstrs_info
val qbns = map #qconst qbns_info
val qfvs = map #qconst qfvs_info
@@ -602,12 +596,9 @@
val qalphabn_defs = map #def qalpha_info
val _ = warning "Lifting permutations";
- val thy = Local_Theory.exit_global lthy12c;
val perm_names = map (fn x => "permute_" ^ x) qty_names
val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs
- (* use Local_Theory.theory_result *)
- val thy' = define_qperms qtys qty_full_names dd raw_perm_laws thy;
- val lthy13 = Named_Target.init "" thy';
+ val lthy13 = define_qperms qtys qty_full_names dd raw_perm_laws lthy12c
val q_name = space_implode "_" qty_names;
fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
--- a/Nominal/nominal_dt_quot.ML Sun Aug 15 14:00:28 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML Mon Aug 16 17:39:16 2010 +0800
@@ -14,10 +14,10 @@
Quotient_Info.qconsts_info list * local_theory
val define_qperms: typ list -> string list -> (string * term * mixfix) list ->
- thm list -> theory -> theory
+ thm list -> local_theory -> local_theory
val define_qsizes: typ list -> string list -> (string * term * mixfix) list ->
- theory -> theory
+ local_theory -> local_theory
end
structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
@@ -45,34 +45,38 @@
(* defines the quotient permutations and proves pt-class *)
-fun define_qperms qtys qfull_ty_names perm_specs raw_perm_laws thy =
+fun define_qperms qtys qfull_ty_names perm_specs raw_perm_laws lthy =
let
- val lthy = Class.instantiation (qfull_ty_names, [], @{sort pt}) thy
+ val lthy' =
+ lthy
+ |> Local_Theory.exit_global
+ |> Class.instantiation (qfull_ty_names, [], @{sort pt})
- val (_, lthy') = define_qconsts qtys perm_specs lthy
+ 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 qtys lthy'') raw_perm_laws
fun tac _ =
Class.intro_classes_tac [] THEN
(ALLGOALS (resolve_tac lifted_perm_laws))
in
- lthy'
+ lthy''
|> Class.prove_instantiation_exit tac
+ |> Named_Target.theory_init
end
(* defines the size functions and proves size-class *)
-fun define_qsizes qtys qfull_ty_names size_specs thy =
+fun define_qsizes qtys qfull_ty_names size_specs lthy =
let
- val lthy = Class.instantiation (qfull_ty_names, [], @{sort size}) thy
-
- val (_, lthy') = define_qconsts qtys size_specs lthy
-
fun tac _ = Class.intro_classes_tac []
in
- lthy'
+ lthy
+ |> Local_Theory.exit_global
+ |> Class.instantiation (qfull_ty_names, [], @{sort size})
+ |> snd o (define_qconsts qtys size_specs)
|> Class.prove_instantiation_exit tac
+ |> Named_Target.theory_init
end
end (* structure *)
--- a/Nominal/nominal_dt_rawperm.ML Sun Aug 15 14:00:28 2010 +0800
+++ b/Nominal/nominal_dt_rawperm.ML Mon Aug 16 17:39:16 2010 +0800
@@ -9,8 +9,8 @@
signature NOMINAL_DT_RAWPERM =
sig
- val define_raw_perms: string list -> typ list -> term list -> thm -> theory ->
- (term list * thm list * thm list) * theory
+ val define_raw_perms: string list -> typ list -> term list -> thm -> local_theory ->
+ (term list * thm list * thm list) * local_theory
end
@@ -20,7 +20,7 @@
(** proves the two pt-type class properties **)
-fun prove_permute_zero lthy induct perm_defs perm_fns =
+fun prove_permute_zero induct perm_defs perm_fns lthy =
let
val perm_types = map (body_type o fastype_of) perm_fns
val perm_indnames = Datatype_Prop.make_tnames perm_types
@@ -42,7 +42,7 @@
end
-fun prove_permute_plus lthy induct perm_defs perm_fns =
+fun prove_permute_plus induct perm_defs perm_fns lthy =
let
val p = Free ("p", @{typ perm})
val q = Free ("q", @{typ perm})
@@ -90,7 +90,7 @@
end
-fun define_raw_perms full_ty_names tys constrs induct_thm thy =
+fun define_raw_perms full_ty_names tys constrs induct_thm lthy =
let
val perm_fn_names = full_ty_names
|> map Long_Name.base_name
@@ -102,15 +102,6 @@
val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs
- val lthy =
- Class.instantiation (full_ty_names, [], @{sort pt}) thy
-
- val ((perm_funs, perm_eq_thms), lthy') =
- Primrec.add_primrec perm_fn_binds perm_eqs lthy;
-
- val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs
- val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs
-
fun tac _ (_, _, simps) =
Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
@@ -118,10 +109,20 @@
(map (Morphism.term phi) fvs,
map (Morphism.thm phi) dfs,
map (Morphism.thm phi) simps);
+
+ val ((perm_funs, perm_eq_thms), lthy') =
+ lthy
+ |> Local_Theory.exit_global
+ |> Class.instantiation (full_ty_names, [], @{sort pt})
+ |> Primrec.add_primrec perm_fn_binds perm_eqs
+
+ val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy'
+ val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy'
in
lthy'
|> Class.prove_instantiation_exit_result morphism tac
(perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms)
+ ||> Named_Target.theory_init
end