Elimination of fully-functorial style.
authorpaulson
Fri Feb 16 11:35:52 1996 +0100 (1996-02-16)
changeset 14987b7d20e89b1b
parent 1497 41a1b0426b2e
child 1499 01fdd1ea6324
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
src/Pure/ROOT.ML
src/Pure/axclass.ML
     1.1 --- a/src/Pure/ROOT.ML	Thu Feb 15 10:51:22 1996 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Fri Feb 16 11:35:52 1996 +0100
     1.3 @@ -40,47 +40,9 @@
     1.4  use "goals.ML";
     1.5  use "axclass.ML";
     1.6  
     1.7 -(*Will be visible to all object-logics.*)
     1.8 -structure Type = TypeFun(structure Symtab=Symtab and Syntax=Syntax);
     1.9 -structure Sign = SignFun(structure Type=Type and Syntax=Syntax);
    1.10 -structure Sequence = SequenceFun();
    1.11 -structure Envir = EnvirFun();
    1.12 -structure Pattern = PatternFun(structure Sign=Sign and Envir=Envir);
    1.13 -structure Unify = UnifyFun(structure Sign=Sign and Envir=Envir
    1.14 -                           and Sequence=Sequence and Pattern=Pattern);
    1.15 -structure Net = NetFun();
    1.16 -structure Logic = LogicFun(structure Unify=Unify and Net=Net);
    1.17 -structure Thm = ThmFun(structure Logic=Logic and Unify=Unify and Net=Net
    1.18 -                             and Pattern=Pattern);
    1.19 -structure Drule = DruleFun(structure Logic=Logic and Thm=Thm);
    1.20 -structure Tactical = TacticalFun(structure Logic=Logic and Drule=Drule);
    1.21 -structure Tactic = TacticFun(structure Logic=Logic and Drule=Drule
    1.22 -                             and Tactical=Tactical and Net=Net);
    1.23 -structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule
    1.24 -                           and Tactic=Tactic and Pattern=Pattern);
    1.25 -structure AxClass = AxClassFun(structure Logic = Logic
    1.26 -  and Goals = Goals and Tactic = Tactic);
    1.27 -open BasicSyntax Thm Drule Tactical Tactic Goals;
    1.28 -
    1.29  structure Pure = struct val thy = pure_thy end;
    1.30  structure CPure = struct val thy = cpure_thy end;
    1.31  
    1.32 -(* hide functors; saves space in PolyML *)
    1.33 -functor TypeFun() = struct end;
    1.34 -functor SignFun() = struct end;
    1.35 -functor SequenceFun() = struct end;
    1.36 -functor EnvirFun() = struct end;
    1.37 -functor PatternFun() = struct end;
    1.38 -functor UnifyFun() = struct end;
    1.39 -functor NetFun() = struct end;
    1.40 -functor LogicFun() = struct end;
    1.41 -functor ThmFun() = struct end;
    1.42 -functor DruleFun() = struct end;
    1.43 -functor TacticalFun() = struct end;
    1.44 -functor TacticFun() = struct end;
    1.45 -functor GoalsFun() = struct end;
    1.46 -functor AxClassFun() = struct end;
    1.47 -
    1.48  (*Theory parser and loader*)
    1.49  cd "Thy";
    1.50  use "ROOT.ML";
     2.1 --- a/src/Pure/axclass.ML	Thu Feb 15 10:51:22 1996 +0100
     2.2 +++ b/src/Pure/axclass.ML	Fri Feb 16 11:35:52 1996 +0100
     2.3 @@ -6,43 +6,30 @@
     2.4  *)
     2.5  
     2.6  signature AX_CLASS =
     2.7 -sig
     2.8 -  structure Tactical: TACTICAL
     2.9 -  local open Tactical Tactical.Thm in
    2.10 -    val add_thms_as_axms: (string * thm) list -> theory -> theory
    2.11 -    val add_classrel_thms: thm list -> theory -> theory
    2.12 -    val add_arity_thms: thm list -> theory -> theory
    2.13 -    val add_axclass: class * class list -> (string * string) list
    2.14 -      -> theory -> theory
    2.15 -    val add_axclass_i: class * class list -> (string * term) list
    2.16 -      -> theory -> theory
    2.17 -    val add_inst_subclass: class * class -> string list -> thm list
    2.18 -      -> tactic option -> theory -> theory
    2.19 -    val add_inst_arity: string * sort list * class list -> string list
    2.20 -      -> thm list -> tactic option -> theory -> theory
    2.21 -    val axclass_tac: theory -> thm list -> tactic
    2.22 -    val prove_subclass: theory -> class * class -> thm list
    2.23 -      -> tactic option -> thm
    2.24 -    val prove_arity: theory -> string * sort list * class -> thm list
    2.25 -      -> tactic option -> thm
    2.26 -    val goal_subclass: theory -> class * class -> thm list
    2.27 -    val goal_arity: theory -> string * sort list * class -> thm list
    2.28 -  end
    2.29 -end;
    2.30 +  sig
    2.31 +  val add_thms_as_axms: (string * thm) list -> theory -> theory
    2.32 +  val add_classrel_thms: thm list -> theory -> theory
    2.33 +  val add_arity_thms: thm list -> theory -> theory
    2.34 +  val add_axclass: class * class list -> (string * string) list
    2.35 +    -> theory -> theory
    2.36 +  val add_axclass_i: class * class list -> (string * term) list
    2.37 +    -> theory -> theory
    2.38 +  val add_inst_subclass: class * class -> string list -> thm list
    2.39 +    -> tactic option -> theory -> theory
    2.40 +  val add_inst_arity: string * sort list * class list -> string list
    2.41 +    -> thm list -> tactic option -> theory -> theory
    2.42 +  val axclass_tac: theory -> thm list -> tactic
    2.43 +  val prove_subclass: theory -> class * class -> thm list
    2.44 +    -> tactic option -> thm
    2.45 +  val prove_arity: theory -> string * sort list * class -> thm list
    2.46 +    -> tactic option -> thm
    2.47 +  val goal_subclass: theory -> class * class -> thm list
    2.48 +  val goal_arity: theory -> string * sort list * class -> thm list
    2.49 +  end;
    2.50  
    2.51 -functor AxClassFun(structure Logic: LOGIC and Goals: GOALS and Tactic: TACTIC
    2.52 -  sharing Goals.Tactical = Tactic.Tactical): AX_CLASS =
    2.53 +structure AxClass : AX_CLASS =
    2.54  struct
    2.55  
    2.56 -structure Tactical = Goals.Tactical;
    2.57 -structure Thm = Tactical.Thm;
    2.58 -structure Sign = Thm.Sign;
    2.59 -structure Type = Sign.Type;
    2.60 -structure Pretty = Sign.Syntax.Pretty;
    2.61 -
    2.62 -open Logic Thm Tactical Tactic Goals;
    2.63 -
    2.64 -
    2.65  (** utilities **)
    2.66  
    2.67  (* type vars *)
    2.68 @@ -63,7 +50,7 @@
    2.69  
    2.70  val get_axioms = mapfilter o get_ax;
    2.71  
    2.72 -val is_def = is_equals o #prop o rep_thm;
    2.73 +val is_def = Logic.is_equals o #prop o rep_thm;
    2.74  
    2.75  fun witnesses thy axms thms =
    2.76    map (get_axiom thy) axms @ thms @ filter is_def (map snd (axioms_of thy));
    2.77 @@ -74,13 +61,14 @@
    2.78  
    2.79  (* subclass relations as terms *)
    2.80  
    2.81 -fun mk_classrel (c1, c2) = mk_inclass (aT [c1], c2);
    2.82 +fun mk_classrel (c1, c2) = Logic.mk_inclass (aT [c1], c2);
    2.83  
    2.84  fun dest_classrel tm =
    2.85    let
    2.86      fun err () = raise_term "dest_classrel" [tm];
    2.87  
    2.88 -    val (ty, c2) = dest_inclass (freeze_vars tm) handle TERM _ => err ();
    2.89 +    val (ty, c2) = Logic.dest_inclass (Logic.freeze_vars tm)
    2.90 +	           handle TERM _ => err ();
    2.91      val c1 = (case ty of TFree (_, [c]) => c | _ => err ());
    2.92    in
    2.93      (c1, c2)
    2.94 @@ -94,14 +82,15 @@
    2.95      val names = tl (variantlist (replicate (length ss + 1) "'", []));
    2.96      val tfrees = map TFree (names ~~ ss);
    2.97    in
    2.98 -    mk_inclass (Type (t, tfrees), c)
    2.99 +    Logic.mk_inclass (Type (t, tfrees), c)
   2.100    end;
   2.101  
   2.102  fun dest_arity tm =
   2.103    let
   2.104      fun err () = raise_term "dest_arity" [tm];
   2.105  
   2.106 -    val (ty, c) = dest_inclass (freeze_vars tm) handle TERM _ => err ();
   2.107 +    val (ty, c) = Logic.dest_inclass (Logic.freeze_vars tm) 
   2.108 +	          handle TERM _ => err ();
   2.109      val (t, tfrees) =
   2.110        (case ty of
   2.111          Type (t, tys) => (t, map (fn TFree x => x | _ => err ()) tys)
   2.112 @@ -189,7 +178,7 @@
   2.113  
   2.114      fun abs_axm ax =
   2.115        if null (term_tfrees ax) then
   2.116 -        mk_implies (mk_inclass (aT logicS, class), ax)
   2.117 +        Logic.mk_implies (Logic.mk_inclass (aT logicS, class), ax)
   2.118        else
   2.119          map_term_tfrees (K (aT [class])) ax;
   2.120  
   2.121 @@ -212,10 +201,10 @@
   2.122  
   2.123      val axS = Sign.norm_sort sign (logicC :: flat (map axm_sort axioms));
   2.124  
   2.125 -    val int_axm = close_form o map_term_tfrees (K (aT axS));
   2.126 -    fun inclass c = mk_inclass (aT axS, c);
   2.127 +    val int_axm = Logic.close_form o map_term_tfrees (K (aT axS));
   2.128 +    fun inclass c = Logic.mk_inclass (aT axS, c);
   2.129  
   2.130 -    val intro_axm = list_implies
   2.131 +    val intro_axm = Logic.list_implies
   2.132        (map inclass super_classes @ map (int_axm o snd) axioms, inclass class);
   2.133    in
   2.134      add_axioms_i ((class ^ "I", intro_axm) :: abs_axioms) thy