# HG changeset patch # User haftmann # Date 1134720011 -3600 # Node ID bf448d999b7e5a02501057250d60a383ef4ad64d # Parent 149cc4126997ed9f4670ab3234482a4658d06c47 re-arranged tuples (theory * 'a) to ('a * theory) in Pure diff -r 149cc4126997 -r bf448d999b7e src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Thu Dec 15 21:51:31 2005 +0100 +++ b/src/HOL/Tools/datatype_package.ML Fri Dec 16 09:00:11 2005 +0100 @@ -766,13 +766,11 @@ let val _ = Theory.requires thy0 "Inductive" "datatype representations"; - fun app_thmss srcs thy = foldl_map (fn (thy, x) => apply_theorems x thy) (thy, srcs); - fun app_thm src thy = apsnd hd (apply_theorems [src] thy); - - val (((thy1, induction), inject), distinct) = thy0 - |> app_thmss raw_distinct - |> apfst (app_thmss raw_inject) - |> apfst (apfst (app_thm raw_induction)); + val (((distinct, inject), [induction]), thy1) = + thy0 + |> fold_map apply_theorems raw_distinct + ||>> fold_map apply_theorems raw_inject + ||>> apply_theorems [raw_induction]; val sign = Theory.sign_of thy1; val induction' = freezeT induction; diff -r 149cc4126997 -r bf448d999b7e src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Thu Dec 15 21:51:31 2005 +0100 +++ b/src/HOL/Tools/inductive_package.ML Fri Dec 16 09:00:11 2005 +0100 @@ -583,7 +583,7 @@ val facts = args |> map (fn ((a, atts), props) => ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props)); - in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end; + in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end; val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop; val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop; @@ -864,7 +864,7 @@ val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs; val (cs', intr_ts') = unify_consts thy cs intr_ts; - val (thy', monos) = thy |> IsarThy.apply_theorems raw_monos; + val (monos, thy') = thy |> IsarThy.apply_theorems raw_monos; in add_inductive_i verbose false "" coind false false cs' ((intr_names ~~ intr_ts') ~~ intr_atts) monos thy' diff -r 149cc4126997 -r bf448d999b7e src/HOL/Tools/recdef_package.ML --- a/src/HOL/Tools/recdef_package.ML Thu Dec 15 21:51:31 2005 +0100 +++ b/src/HOL/Tools/recdef_package.ML Fri Dec 16 09:00:11 2005 +0100 @@ -272,7 +272,7 @@ val _ = requires_recdef thy; val _ = message ("Deferred recursive function " ^ quote name ^ " ..."); - val (thy1, congs) = thy |> app_thms raw_congs; + val (congs, thy1) = thy |> app_thms raw_congs; val (thy2, induct_rules) = tfl_fn thy1 congs name eqs; val ([induct_rules'], thy3) = thy2 diff -r 149cc4126997 -r bf448d999b7e src/HOL/Tools/specification_package.ML --- a/src/HOL/Tools/specification_package.ML Thu Dec 15 21:51:31 2005 +0100 +++ b/src/HOL/Tools/specification_package.ML Fri Dec 16 09:00:11 2005 +0100 @@ -191,7 +191,6 @@ fun undo_imps thm = equal_elim (symmetric rew_imp) thm - fun apply_atts arg = Thm.apply_attributes (arg, map (Attrib.global_attribute thy) atts) fun add_final (arg as (thy, thm)) = if name = "" then arg |> Library.swap @@ -201,7 +200,7 @@ args |> apsnd (remove_alls frees) |> apsnd undo_imps |> apsnd standard - |> apply_atts + |> Thm.apply_attributes (map (Attrib.global_attribute thy) atts) |> add_final |> Library.swap end diff -r 149cc4126997 -r bf448d999b7e src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Thu Dec 15 21:51:31 2005 +0100 +++ b/src/Pure/Isar/attrib.ML Fri Dec 16 09:00:11 2005 +0100 @@ -180,7 +180,7 @@ let val ths = PureThy.select_thm thmref fact; val atts = map (attrib (theory_of st)) srcs; - val (st', ths') = Thm.applys_attributes ((st, ths), atts); + val (st', ths') = Thm.applys_attributes atts (st, ths); in (st', pick name ths') end)); val global_thm = gen_thm I global_attribute_i PureThy.get_thms PureThy.single_thm; diff -r 149cc4126997 -r bf448d999b7e src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Thu Dec 15 21:51:31 2005 +0100 +++ b/src/Pure/Isar/context_rules.ML Fri Dec 16 09:00:11 2005 +0100 @@ -258,7 +258,7 @@ (* low-level modifiers *) fun modifier att (x, ths) = - #1 (Thm.applys_attributes ((x, rev ths), [att])); + fst (Thm.applys_attributes [att] (x, rev ths)); val addXIs_global = modifier (intro_query_global NONE); val addXEs_global = modifier (elim_query_global NONE); diff -r 149cc4126997 -r bf448d999b7e src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Thu Dec 15 21:51:31 2005 +0100 +++ b/src/Pure/Isar/isar_thy.ML Fri Dec 16 09:00:11 2005 +0100 @@ -11,14 +11,14 @@ val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory val add_defs: bool * ((bstring * string) * Attrib.src list) list -> theory -> theory val add_defs_i: bool * ((bstring * term) * theory attribute list) list -> theory -> theory - val apply_theorems: (thmref * Attrib.src list) list -> theory -> theory * thm list - val apply_theorems_i: (thm list * theory attribute list) list -> theory -> theory * thm list + val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory + val apply_theorems_i: (thm list * theory attribute list) list -> theory -> thm list * theory val theorems: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list - -> theory -> theory * (string * thm list) list + -> theory -> (string * thm list) list * theory val theorems_i: string -> ((bstring * theory attribute list) * (thm list * theory attribute list) list) list - -> theory -> theory * (string * thm list) list + -> theory -> (string * thm list) list * theory val smart_theorems: string -> xstring option -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list -> theory -> theory * Proof.context @@ -75,21 +75,19 @@ fun theorems kind args thy = thy |> PureThy.note_thmss (Drule.kind kind) (Attrib.map_facts (Attrib.global_attribute thy) args) - |> tap (present_theorems kind) - |> swap; + |> tap (present_theorems kind); fun theorems_i kind args = PureThy.note_thmss_i (Drule.kind kind) args - #> tap (present_theorems kind) - #> swap; + #> tap (present_theorems kind); -fun apply_theorems args = apsnd (List.concat o map snd) o theorems "" [(("", []), args)]; -fun apply_theorems_i args = apsnd (List.concat o map snd) o theorems_i "" [(("", []), args)]; +fun apply_theorems args = apfst (List.concat o map snd) o theorems "" [(("", []), args)]; +fun apply_theorems_i args = apfst (List.concat o map snd) o theorems_i "" [(("", []), args)]; fun smart_theorems kind NONE args thy = thy |> theorems kind args - |> tap (present_theorems kind o swap) - |> (fn (thy, _) => (thy, ProofContext.init thy)) + |> tap (present_theorems kind) + |> (fn (_, thy) => (thy, ProofContext.init thy)) | smart_theorems kind (SOME loc) args thy = thy |> Locale.note_thmss kind loc args |> tap (present_theorems kind o swap o apfst #1) diff -r 149cc4126997 -r bf448d999b7e src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Thu Dec 15 21:51:31 2005 +0100 +++ b/src/Pure/Isar/method.ML Fri Dec 16 09:00:11 2005 +0100 @@ -624,7 +624,7 @@ fun thms ss = Scan.unless (sect ss) Attrib.local_thms; fun thmss ss = Scan.repeat (thms ss) >> List.concat; -fun apply (f, att) (ctxt, ths) = Thm.applys_attributes ((f ctxt, ths), [att]); +fun apply (f, att) (ctxt, ths) = Thm.applys_attributes [att] (f ctxt, ths); fun section ss = (sect ss -- thmss ss) :-- (fn (m, ths) => Scan.depend (fn ctxt => Scan.succeed (apply m (ctxt, ths)))) >> #2; diff -r 149cc4126997 -r bf448d999b7e src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Dec 15 21:51:31 2005 +0100 +++ b/src/Pure/Isar/proof_context.ML Fri Dec 16 09:00:11 2005 +0100 @@ -1018,7 +1018,7 @@ fun gen_note_thmss get = fold_map (fn ((name, more_attrs), ths_attrs) => fn ctxt => let fun app (th, attrs) (ct, ths) = - let val (ct', th') = Thm.applys_attributes ((ct, get ctxt th), attrs @ more_attrs) + let val (ct', th') = Thm.applys_attributes (attrs @ more_attrs) (ct, get ctxt th) in (ct', th' :: ths) end; val (ctxt', rev_thms) = fold app ths_attrs (ctxt, []); val thms = List.concat (rev rev_thms); diff -r 149cc4126997 -r bf448d999b7e src/Pure/axclass.ML --- a/src/Pure/axclass.ML Thu Dec 15 21:51:31 2005 +0100 +++ b/src/Pure/axclass.ML Fri Dec 16 09:00:11 2005 +0100 @@ -11,9 +11,9 @@ val print_axclasses: theory -> unit val get_info: theory -> string -> {super_classes: class list, intro: thm, axioms: thm list} val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list -> - theory -> theory * {intro: thm, axioms: thm list} + theory -> {intro: thm, axioms: thm list} * theory val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list -> - theory -> theory * {intro: thm, axioms: thm list} + theory -> {intro: thm, axioms: thm list} * theory val add_classrel_thms: thm list -> theory -> theory val add_arity_thms: thm list -> theory -> theory val add_inst_subclass: xstring * xstring -> tactic -> theory -> theory @@ -210,7 +210,7 @@ |> PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts) ||> Theory.restore_naming class_thy ||> AxclassesData.map (Symtab.update (class, info)); - in (final_thy, {intro = intro, axioms = axioms}) end; + in ({intro = intro, axioms = axioms}, final_thy) end; in @@ -347,7 +347,7 @@ OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl ((P.name -- Scan.optional ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name - >> (Toplevel.theory o (#1 oo uncurry add_axclass))); + >> (Toplevel.theory o (snd oo uncurry add_axclass))); val instanceP = OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal diff -r 149cc4126997 -r bf448d999b7e src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Thu Dec 15 21:51:31 2005 +0100 +++ b/src/Pure/pure_thy.ML Fri Dec 16 09:00:11 2005 +0100 @@ -308,8 +308,8 @@ fun name_thmss name xs = (case filter_out (null o fst) xs of [([x], z)] => [([name_thm true (name, x)], z)] - | _ => snd (foldl_map (fn (i, (ys, z)) => - (i + length ys, (map (name_thm true) (gen_names i (length ys) name ~~ ys), z))) (0, xs))); + | _ => fst (fold_map (fn (ys, z) => fn i => + ((map (name_thm true) (gen_names i (length ys) name ~~ ys), z), i + length ys)) xs 0)); (* enter_thms *) @@ -317,7 +317,7 @@ fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name); fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name); -fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms) +fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms) |> swap | enter_thms pre_name post_name app_att (bname, thms) thy = let val name = Sign.full_name thy bname; @@ -333,15 +333,15 @@ if Thm.eq_thms (thms', thms'') then warn_same name else warn_overwrite name); r := {theorems = (space', theorems'), index = index'}; - (thy', thms') + (thms', thy') end; (* add_thms(s) *) fun add_thms_atts pre_name ((bname, thms), atts) = - swap o enter_thms pre_name (name_thms false) - (Thm.applys_attributes o rpair atts) (bname, thms); + enter_thms pre_name (name_thms false) + (Thm.applys_attributes atts) (bname, thms); fun gen_add_thmss pre_name = fold_map (add_thms_atts pre_name); @@ -357,21 +357,21 @@ local -fun gen_note_thss get kind_att (thy, ((bname, more_atts), ths_atts)) = +fun gen_note_thss get kind_att ((bname, more_atts), ths_atts) thy = let - fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts); - val (thy', thms) = thy |> enter_thms + fun app (x, (ths, atts)) = Thm.applys_attributes atts (x, ths); + val (thms, thy') = thy |> enter_thms name_thmss (name_thms false) (apsnd List.concat o foldl_map app) (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind_att])) ths_atts); - in (thy', (bname, thms)) end; + in ((bname, thms), thy') end; -fun gen_note_thmss get kind_att args thy = - foldl_map (gen_note_thss get kind_att) (thy, args); +fun gen_note_thmss get kind_att = + fold_map (gen_note_thss get kind_att); in -val note_thmss = swap ooo gen_note_thmss get_thms; -val note_thmss_i = swap ooo gen_note_thmss (K I); +val note_thmss = gen_note_thmss get_thms; +val note_thmss_i = gen_note_thmss (K I); end; @@ -390,12 +390,12 @@ fun smart_store _ (name, []) = error ("Cannot store empty list of theorems: " ^ quote name) | smart_store name_thm (name, [thm]) = - #2 (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm)) + fst (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm)) | smart_store name_thm (name, thms) = let fun merge (thy, th) = Theory.merge (thy, Thm.theory_of_thm th); val thy = Library.foldl merge (Thm.theory_of_thm (hd thms), tl thms); - in #2 (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end; + in fst (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end; in diff -r 149cc4126997 -r bf448d999b7e src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Dec 15 21:51:31 2005 +0100 +++ b/src/Pure/thm.ML Fri Dec 16 09:00:11 2005 +0100 @@ -142,8 +142,8 @@ val no_prems: thm -> bool val no_attributes: 'a -> 'a * 'b list val simple_fact: 'a -> ('a * 'b list) list - val apply_attributes: ('a * thm) * 'a attribute list -> 'a * thm - val applys_attributes: ('a * thm list) * 'a attribute list -> 'a * thm list + val apply_attributes: 'a attribute list -> 'a * thm -> 'a * thm + val applys_attributes: 'a attribute list -> 'a * thm list -> 'a * thm list val terms_of_tpairs: (term * term) list -> term list val full_prop_of: thm -> term val get_name_tags: thm -> string * tag list @@ -400,8 +400,8 @@ fun no_attributes x = (x, []); fun simple_fact x = [(x, [])]; -fun apply_attributes (x_th, atts) = Library.apply atts x_th; -fun applys_attributes (x_ths, atts) = foldl_map (Library.apply atts) x_ths; +val apply_attributes = Library.apply; +fun applys_attributes atts = foldl_map (Library.apply atts); (* hyps *) diff -r 149cc4126997 -r bf448d999b7e src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Thu Dec 15 21:51:31 2005 +0100 +++ b/src/ZF/Tools/datatype_package.ML Fri Dec 16 09:00:11 2005 +0100 @@ -394,13 +394,14 @@ val dom_sum = if sdom = "" then Ind_Syntax.data_domain coind (rec_tms, con_ty_lists) else read_i sdom; - - val (thy', ((monos, type_intrs), type_elims)) = thy - |> IsarThy.apply_theorems raw_monos - |>>> IsarThy.apply_theorems raw_type_intrs - |>>> IsarThy.apply_theorems raw_type_elims; - in add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy' end; - + in + thy + |> IsarThy.apply_theorems raw_monos + ||>> IsarThy.apply_theorems raw_type_intrs + ||>> IsarThy.apply_theorems raw_type_elims + |-> (fn ((monos, type_intrs), type_elims) => + add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims)) + end; (* outer syntax *) diff -r 149cc4126997 -r bf448d999b7e src/ZF/Tools/ind_cases.ML --- a/src/ZF/Tools/ind_cases.ML Thu Dec 15 21:51:31 2005 +0100 +++ b/src/ZF/Tools/ind_cases.ML Fri Dec 16 09:00:11 2005 +0100 @@ -55,7 +55,7 @@ val facts = args |> map (fn ((name, srcs), props) => ((name, map (Attrib.global_attribute thy) srcs), map (Thm.no_attributes o single o mk_cases) props)); - in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end; + in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end; (* ind_cases method *) diff -r 149cc4126997 -r bf448d999b7e src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Thu Dec 15 21:51:31 2005 +0100 +++ b/src/ZF/Tools/induct_tacs.ML Fri Dec 16 09:00:11 2005 +0100 @@ -172,16 +172,14 @@ end; fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy = - let - val (thy', (((elims, inducts), case_eqns), recursor_eqns)) = thy - |> IsarThy.apply_theorems [raw_elim] - |>>> IsarThy.apply_theorems [raw_induct] - |>>> IsarThy.apply_theorems raw_case_eqns - |>>> IsarThy.apply_theorems raw_recursor_eqns; - in - thy' |> rep_datatype_i (PureThy.single_thm "elimination" elims) - (PureThy.single_thm "induction" inducts) case_eqns recursor_eqns - end; + thy + |> IsarThy.apply_theorems [raw_elim] + ||>> IsarThy.apply_theorems [raw_induct] + ||>> IsarThy.apply_theorems raw_case_eqns + ||>> IsarThy.apply_theorems raw_recursor_eqns + |-> (fn (((elims, inducts), case_eqns), recursor_eqns) => + rep_datatype_i (PureThy.single_thm "elimination" elims) + (PureThy.single_thm "induction" inducts) case_eqns recursor_eqns); (* theory setup *) diff -r 149cc4126997 -r bf448d999b7e src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Thu Dec 15 21:51:31 2005 +0100 +++ b/src/ZF/Tools/inductive_package.ML Fri Dec 16 09:00:11 2005 +0100 @@ -567,16 +567,16 @@ val dom_sum = read Ind_Syntax.iT sdom_sum; val intr_tms = map (read propT o snd o fst) sintrs; val intr_specs = (map (fst o fst) sintrs ~~ intr_tms) ~~ map snd sintrs; - - val (thy', (((monos, con_defs), type_intrs), type_elims)) = thy - |> IsarThy.apply_theorems raw_monos - |>>> IsarThy.apply_theorems raw_con_defs - |>>> IsarThy.apply_theorems raw_type_intrs - |>>> IsarThy.apply_theorems raw_type_elims; in - add_inductive_i true (rec_tms, dom_sum) intr_specs - (monos, con_defs, type_intrs, type_elims) thy' - end + thy + |> IsarThy.apply_theorems raw_monos + ||>> IsarThy.apply_theorems raw_con_defs + ||>> IsarThy.apply_theorems raw_type_intrs + ||>> IsarThy.apply_theorems raw_type_elims + |-> (fn (((monos, con_defs), type_intrs), type_elims) => + add_inductive_i true (rec_tms, dom_sum) intr_specs + (monos, con_defs, type_intrs, type_elims)) + end; (* outer syntax *)