# HG changeset patch # User paulson # Date 824466952 -3600 # Node ID 7b7d20e89b1bb7f44a68f82b55e77c045671a0bb # Parent 41a1b0426b2eab4b114011c0ec17a2edec735d53 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted. diff -r 41a1b0426b2e -r 7b7d20e89b1b src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Feb 15 10:51:22 1996 +0100 +++ b/src/Pure/ROOT.ML Fri Feb 16 11:35:52 1996 +0100 @@ -40,47 +40,9 @@ use "goals.ML"; use "axclass.ML"; -(*Will be visible to all object-logics.*) -structure Type = TypeFun(structure Symtab=Symtab and Syntax=Syntax); -structure Sign = SignFun(structure Type=Type and Syntax=Syntax); -structure Sequence = SequenceFun(); -structure Envir = EnvirFun(); -structure Pattern = PatternFun(structure Sign=Sign and Envir=Envir); -structure Unify = UnifyFun(structure Sign=Sign and Envir=Envir - and Sequence=Sequence and Pattern=Pattern); -structure Net = NetFun(); -structure Logic = LogicFun(structure Unify=Unify and Net=Net); -structure Thm = ThmFun(structure Logic=Logic and Unify=Unify and Net=Net - and Pattern=Pattern); -structure Drule = DruleFun(structure Logic=Logic and Thm=Thm); -structure Tactical = TacticalFun(structure Logic=Logic and Drule=Drule); -structure Tactic = TacticFun(structure Logic=Logic and Drule=Drule - and Tactical=Tactical and Net=Net); -structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule - and Tactic=Tactic and Pattern=Pattern); -structure AxClass = AxClassFun(structure Logic = Logic - and Goals = Goals and Tactic = Tactic); -open BasicSyntax Thm Drule Tactical Tactic Goals; - structure Pure = struct val thy = pure_thy end; structure CPure = struct val thy = cpure_thy end; -(* hide functors; saves space in PolyML *) -functor TypeFun() = struct end; -functor SignFun() = struct end; -functor SequenceFun() = struct end; -functor EnvirFun() = struct end; -functor PatternFun() = struct end; -functor UnifyFun() = struct end; -functor NetFun() = struct end; -functor LogicFun() = struct end; -functor ThmFun() = struct end; -functor DruleFun() = struct end; -functor TacticalFun() = struct end; -functor TacticFun() = struct end; -functor GoalsFun() = struct end; -functor AxClassFun() = struct end; - (*Theory parser and loader*) cd "Thy"; use "ROOT.ML"; diff -r 41a1b0426b2e -r 7b7d20e89b1b src/Pure/axclass.ML --- a/src/Pure/axclass.ML Thu Feb 15 10:51:22 1996 +0100 +++ b/src/Pure/axclass.ML Fri Feb 16 11:35:52 1996 +0100 @@ -6,43 +6,30 @@ *) signature AX_CLASS = -sig - structure Tactical: TACTICAL - local open Tactical Tactical.Thm in - val add_thms_as_axms: (string * thm) list -> theory -> theory - val add_classrel_thms: thm list -> theory -> theory - val add_arity_thms: thm list -> theory -> theory - val add_axclass: class * class list -> (string * string) list - -> theory -> theory - val add_axclass_i: class * class list -> (string * term) list - -> theory -> theory - val add_inst_subclass: class * class -> string list -> thm list - -> tactic option -> theory -> theory - val add_inst_arity: string * sort list * class list -> string list - -> thm list -> tactic option -> theory -> theory - val axclass_tac: theory -> thm list -> tactic - val prove_subclass: theory -> class * class -> thm list - -> tactic option -> thm - val prove_arity: theory -> string * sort list * class -> thm list - -> tactic option -> thm - val goal_subclass: theory -> class * class -> thm list - val goal_arity: theory -> string * sort list * class -> thm list - end -end; + sig + val add_thms_as_axms: (string * thm) list -> theory -> theory + val add_classrel_thms: thm list -> theory -> theory + val add_arity_thms: thm list -> theory -> theory + val add_axclass: class * class list -> (string * string) list + -> theory -> theory + val add_axclass_i: class * class list -> (string * term) list + -> theory -> theory + val add_inst_subclass: class * class -> string list -> thm list + -> tactic option -> theory -> theory + val add_inst_arity: string * sort list * class list -> string list + -> thm list -> tactic option -> theory -> theory + val axclass_tac: theory -> thm list -> tactic + val prove_subclass: theory -> class * class -> thm list + -> tactic option -> thm + val prove_arity: theory -> string * sort list * class -> thm list + -> tactic option -> thm + val goal_subclass: theory -> class * class -> thm list + val goal_arity: theory -> string * sort list * class -> thm list + end; -functor AxClassFun(structure Logic: LOGIC and Goals: GOALS and Tactic: TACTIC - sharing Goals.Tactical = Tactic.Tactical): AX_CLASS = +structure AxClass : AX_CLASS = struct -structure Tactical = Goals.Tactical; -structure Thm = Tactical.Thm; -structure Sign = Thm.Sign; -structure Type = Sign.Type; -structure Pretty = Sign.Syntax.Pretty; - -open Logic Thm Tactical Tactic Goals; - - (** utilities **) (* type vars *) @@ -63,7 +50,7 @@ val get_axioms = mapfilter o get_ax; -val is_def = is_equals o #prop o rep_thm; +val is_def = Logic.is_equals o #prop o rep_thm; fun witnesses thy axms thms = map (get_axiom thy) axms @ thms @ filter is_def (map snd (axioms_of thy)); @@ -74,13 +61,14 @@ (* subclass relations as terms *) -fun mk_classrel (c1, c2) = mk_inclass (aT [c1], c2); +fun mk_classrel (c1, c2) = Logic.mk_inclass (aT [c1], c2); fun dest_classrel tm = let fun err () = raise_term "dest_classrel" [tm]; - val (ty, c2) = dest_inclass (freeze_vars tm) handle TERM _ => err (); + val (ty, c2) = Logic.dest_inclass (Logic.freeze_vars tm) + handle TERM _ => err (); val c1 = (case ty of TFree (_, [c]) => c | _ => err ()); in (c1, c2) @@ -94,14 +82,15 @@ val names = tl (variantlist (replicate (length ss + 1) "'", [])); val tfrees = map TFree (names ~~ ss); in - mk_inclass (Type (t, tfrees), c) + Logic.mk_inclass (Type (t, tfrees), c) end; fun dest_arity tm = let fun err () = raise_term "dest_arity" [tm]; - val (ty, c) = dest_inclass (freeze_vars tm) handle TERM _ => err (); + val (ty, c) = Logic.dest_inclass (Logic.freeze_vars tm) + handle TERM _ => err (); val (t, tfrees) = (case ty of Type (t, tys) => (t, map (fn TFree x => x | _ => err ()) tys) @@ -189,7 +178,7 @@ fun abs_axm ax = if null (term_tfrees ax) then - mk_implies (mk_inclass (aT logicS, class), ax) + Logic.mk_implies (Logic.mk_inclass (aT logicS, class), ax) else map_term_tfrees (K (aT [class])) ax; @@ -212,10 +201,10 @@ val axS = Sign.norm_sort sign (logicC :: flat (map axm_sort axioms)); - val int_axm = close_form o map_term_tfrees (K (aT axS)); - fun inclass c = mk_inclass (aT axS, c); + val int_axm = Logic.close_form o map_term_tfrees (K (aT axS)); + fun inclass c = Logic.mk_inclass (aT axS, c); - val intro_axm = list_implies + val intro_axm = Logic.list_implies (map inclass super_classes @ map (int_axm o snd) axioms, inclass class); in add_axioms_i ((class ^ "I", intro_axm) :: abs_axioms) thy