src/Pure/axclass.ML
changeset 17928 c567e5f885bf
parent 17855 64c832a03a15
child 17956 369e2af8ee45
     1.1 --- a/src/Pure/axclass.ML	Wed Oct 19 21:52:40 2005 +0200
     1.2 +++ b/src/Pure/axclass.ML	Wed Oct 19 21:52:41 2005 +0200
     1.3 @@ -26,12 +26,6 @@
     1.4    val instance_arity_i: string * sort list * sort -> theory -> Proof.state
     1.5    val intro_classes_tac: thm list -> tactic
     1.6    val default_intro_classes_tac: thm list -> tactic
     1.7 -  (*legacy interfaces*)
     1.8 -  val axclass_tac: thm list -> tactic
     1.9 -  val add_inst_subclass_x: xstring * xstring -> string list -> thm list
    1.10 -    -> tactic option -> theory -> theory
    1.11 -  val add_inst_arity_x: xstring * string list * string -> string list
    1.12 -    -> thm list -> tactic option -> theory -> theory
    1.13  end;
    1.14  
    1.15  structure AxClass: AX_CLASS =
    1.16 @@ -111,8 +105,6 @@
    1.17  
    1.18  (** axclass info **)
    1.19  
    1.20 -(* data kind 'Pure/axclasses' *)
    1.21 -
    1.22  type axclass_info =
    1.23    {super_classes: class list,
    1.24      intro: thm,
    1.25 @@ -146,8 +138,6 @@
    1.26  val print_axclasses = AxclassesData.print;
    1.27  
    1.28  
    1.29 -(* get and put data *)
    1.30 -
    1.31  val lookup_info = Symtab.lookup o AxclassesData.get;
    1.32  
    1.33  fun get_info thy c =
    1.34 @@ -156,8 +146,6 @@
    1.35    | SOME info => info);
    1.36  
    1.37  
    1.38 -(* class_axms *)
    1.39 -
    1.40  fun class_axms thy =
    1.41    let val classes = Sign.classes thy in
    1.42      map (Thm.class_triv thy) classes @
    1.43 @@ -371,69 +359,4 @@
    1.44  
    1.45  end;
    1.46  
    1.47 -
    1.48 -
    1.49 -(** old-style instantiation proofs **)
    1.50 -
    1.51 -(* axclass_tac *)
    1.52 -
    1.53 -(*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)",
    1.54 -      try class_trivs first, then "cI" axioms
    1.55 -  (2) rewrite goals using user supplied definitions
    1.56 -  (3) repeatedly resolve goals with user supplied non-definitions*)
    1.57 -
    1.58 -val is_def = Logic.is_equals o #prop o rep_thm;
    1.59 -
    1.60 -fun axclass_tac thms =
    1.61 -  let
    1.62 -    val defs = List.filter is_def thms;
    1.63 -    val non_defs = filter_out is_def thms;
    1.64 -  in
    1.65 -    intro_classes_tac [] THEN
    1.66 -    TRY (rewrite_goals_tac defs) THEN
    1.67 -    TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i))
    1.68 -  end;
    1.69 -
    1.70 -
    1.71 -(* instance declarations *)
    1.72 -
    1.73 -local
    1.74 -
    1.75 -fun prove mk_prop str_of thy prop thms usr_tac =
    1.76 -  (Tactic.prove thy [] [] (mk_prop prop)
    1.77 -      (K (axclass_tac thms THEN (if_none usr_tac all_tac)))
    1.78 -    handle ERROR => error ("The error(s) above occurred while trying to prove " ^
    1.79 -     quote (str_of thy prop))) |> Drule.standard;
    1.80 -
    1.81 -val prove_subclass = prove mk_classrel (fn thy => fn (c1, c2) =>
    1.82 -  Pretty.string_of_classrel (Sign.pp thy) [c1, c2]);
    1.83 -
    1.84 -val prove_arity = prove mk_arity (fn thy => fn (t, Ss, c) =>
    1.85 -  Pretty.string_of_arity (Sign.pp thy) (t, Ss, [c]));
    1.86 -
    1.87 -fun witnesses thy names thms =
    1.88 -  PureThy.get_thmss thy (map Name names) @
    1.89 -  thms @
    1.90 -  List.filter is_def (map snd (axioms_of thy));
    1.91 -
    1.92 -in
    1.93 -
    1.94 -fun add_inst_subclass_x raw_c1_c2 names thms usr_tac thy =
    1.95 -  let val (c1, c2) = read_classrel thy raw_c1_c2 in
    1.96 -    message ("Proving class inclusion " ^ quote (Sign.string_of_classrel thy [c1, c2]) ^ " ...");
    1.97 -    thy |> add_classrel_thms [prove_subclass thy (c1, c2) (witnesses thy names thms) usr_tac]
    1.98 -  end;
    1.99 -
   1.100 -fun add_inst_arity_x raw_arity names thms usr_tac thy =
   1.101 -  let
   1.102 -    val (t, Ss, cs) = read_arity thy raw_arity;
   1.103 -    val wthms = witnesses thy names thms;
   1.104 -    fun prove c =
   1.105 -     (message ("Proving type arity " ^
   1.106 -        quote (Sign.string_of_arity thy (t, Ss, [c])) ^ " ...");
   1.107 -        prove_arity thy (t, Ss, c) wthms usr_tac);
   1.108 -  in add_arity_thms (map prove cs) thy end;
   1.109 -
   1.110  end;
   1.111 -
   1.112 -end;