# HG changeset patch # User Christian Urban # Date 1281951556 -28800 # Node ID 7645e18e8b1970df84bc258583105ab05d0dbe3e # Parent c6d30d5f5ba19dd9ecd69610f200dad0e3145689 modified the code for class instantiations (with help from Florian) diff -r c6d30d5f5ba1 -r 7645e18e8b19 Nominal/Ex/SingleLet.thy --- 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 \ 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 diff -r c6d30d5f5ba1 -r 7645e18e8b19 Nominal/NewParser.thy --- 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); diff -r c6d30d5f5ba1 -r 7645e18e8b19 Nominal/nominal_dt_quot.ML --- 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 *) diff -r c6d30d5f5ba1 -r 7645e18e8b19 Nominal/nominal_dt_rawperm.ML --- 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