src/Pure/axclass.ML
changeset 14605 9de4d64eee3b
parent 12876 a70df1e5bf10
child 14695 9c78044b99c3
     1.1 --- a/src/Pure/axclass.ML	Fri Apr 16 20:34:41 2004 +0200
     1.2 +++ b/src/Pure/axclass.ML	Fri Apr 16 20:59:09 2004 +0200
     1.3 @@ -24,12 +24,12 @@
     1.4      -> thm list -> tactic option -> theory -> theory
     1.5    val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory
     1.6    val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
     1.7 -  val default_intro_classes_tac: thm list -> int -> tactic
     1.8 +  val default_intro_classes_tac: thm list -> tactic
     1.9    val axclass_tac: thm list -> tactic
    1.10    val instance_subclass_proof: xclass * xclass -> bool -> theory -> ProofHistory.T
    1.11    val instance_subclass_proof_i: class * class -> bool -> theory -> ProofHistory.T
    1.12 -  val instance_arity_proof: xstring * string list * xclass -> bool -> theory -> ProofHistory.T
    1.13 -  val instance_arity_proof_i: string * sort list * class -> bool -> theory -> ProofHistory.T
    1.14 +  val instance_arity_proof: xstring * string list * string -> bool -> theory -> ProofHistory.T
    1.15 +  val instance_arity_proof_i: string * sort list * sort -> bool -> theory -> ProofHistory.T
    1.16    val setup: (theory -> theory) list
    1.17  end;
    1.18  
    1.19 @@ -94,11 +94,13 @@
    1.20  
    1.21  (* arities as terms *)
    1.22  
    1.23 -fun mk_arity (t, ss, c) =
    1.24 +fun mk_arity (t, Ss, c) =
    1.25    let
    1.26 -    val tfrees = ListPair.map TFree (Term.invent_type_names [] (length ss), ss);
    1.27 +    val tfrees = ListPair.map TFree (Term.invent_type_names [] (length Ss), Ss);
    1.28    in Logic.mk_inclass (Type (t, tfrees), c) end;
    1.29  
    1.30 +fun mk_arities (t, Ss, S) = map (fn c => mk_arity (t, Ss, c)) S;
    1.31 +
    1.32  fun dest_arity tm =
    1.33    let
    1.34      fun err () = raise TERM ("dest_arity", [tm]);
    1.35 @@ -299,29 +301,30 @@
    1.36  
    1.37  (* intro_classes *)
    1.38  
    1.39 -fun intro_classes_tac facts i st =
    1.40 -  ((Method.insert_tac facts THEN'
    1.41 -    REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st)))) i
    1.42 -    THEN Tactic.distinct_subgoals_tac) st;    (*affects all subgoals!?*)
    1.43 +fun intro_classes_tac facts st =
    1.44 +  (ALLGOALS (Method.insert_tac facts THEN'
    1.45 +      REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st))))
    1.46 +    THEN Tactic.distinct_subgoals_tac) st;
    1.47  
    1.48  val intro_classes_method =
    1.49 -  ("intro_classes", Method.no_args (Method.METHOD (HEADGOAL o intro_classes_tac)),
    1.50 +  ("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
    1.51      "back-chain introduction rules of axiomatic type classes");
    1.52  
    1.53  
    1.54  (* default method *)
    1.55  
    1.56 -fun default_intro_classes_tac [] i = intro_classes_tac [] i
    1.57 -  | default_intro_classes_tac _ _ = Tactical.no_tac;    (*no error message!*)
    1.58 +fun default_intro_classes_tac [] = intro_classes_tac []
    1.59 +  | default_intro_classes_tac _ = Tactical.no_tac;    (*no error message!*)
    1.60  
    1.61  fun default_tac rules ctxt facts =
    1.62 -  HEADGOAL (Method.some_rule_tac rules ctxt facts ORELSE' default_intro_classes_tac facts);
    1.63 +  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
    1.64 +    default_intro_classes_tac facts;
    1.65  
    1.66  val default_method =
    1.67    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule");
    1.68  
    1.69  
    1.70 -(* axclass_tac *)
    1.71 +(* old-style axclass_tac *)
    1.72  
    1.73  (*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)",
    1.74        try class_trivs first, then "cI" axioms
    1.75 @@ -333,13 +336,13 @@
    1.76      val defs = filter is_def thms;
    1.77      val non_defs = filter_out is_def thms;
    1.78    in
    1.79 -    HEADGOAL (intro_classes_tac []) THEN
    1.80 +    intro_classes_tac [] THEN
    1.81      TRY (rewrite_goals_tac defs) THEN
    1.82      TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i))
    1.83    end;
    1.84  
    1.85  
    1.86 -(* provers *)
    1.87 +(* old-style provers *)
    1.88  
    1.89  fun prove mk_prop str_of sign prop thms usr_tac =
    1.90    (Tactic.prove sign [] [] (mk_prop prop) (K (axclass_tac thms THEN (if_none usr_tac all_tac)))
    1.91 @@ -377,8 +380,6 @@
    1.92  
    1.93  val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort;
    1.94  val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
    1.95 -val read_simple_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.intern_class;
    1.96 -fun cert_simple_arity arg = prep_arity (K I) Sign.certify_sort (K I) arg;
    1.97  
    1.98  
    1.99  (* old-style instance declarations *)
   1.100 @@ -417,17 +418,18 @@
   1.101  
   1.102  (** instance proof interfaces **)
   1.103  
   1.104 -fun inst_attribute add_thms (thy, thm) = (add_thms [thm] thy, thm);
   1.105 +fun inst_proof mk_prop add_thms inst int theory =
   1.106 +  theory
   1.107 +  |> IsarThy.multi_theorem_i Drule.internalK
   1.108 +    ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
   1.109 +    (map (fn t => (("", []), [(t, ([], []))])) (mk_prop (Theory.sign_of theory) inst)) int;
   1.110  
   1.111 -fun inst_proof mk_prop add_thms sig_prop int thy =
   1.112 -  thy
   1.113 -  |> IsarThy.theorem_i Drule.internalK (("", [inst_attribute add_thms]),
   1.114 -    (mk_prop (Theory.sign_of thy) sig_prop, ([], []))) int;
   1.115 -
   1.116 -val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms;
   1.117 -val instance_subclass_proof_i = inst_proof (mk_classrel oo cert_classrel) add_classrel_thms;
   1.118 -val instance_arity_proof = inst_proof (mk_arity oo read_simple_arity) add_arity_thms;
   1.119 -val instance_arity_proof_i = inst_proof (mk_arity oo cert_simple_arity) add_arity_thms;
   1.120 +val instance_subclass_proof =
   1.121 +  inst_proof (single oo (mk_classrel oo read_classrel)) add_classrel_thms;
   1.122 +val instance_subclass_proof_i =
   1.123 +  inst_proof (single oo (mk_classrel oo cert_classrel)) add_classrel_thms;
   1.124 +val instance_arity_proof = inst_proof (mk_arities oo read_arity) add_arity_thms;
   1.125 +val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms;
   1.126  
   1.127  
   1.128  
   1.129 @@ -453,7 +455,7 @@
   1.130  val instanceP =
   1.131    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
   1.132      ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.xname) >> instance_subclass_proof ||
   1.133 -      (P.xname -- (P.$$$ "::" |-- P.simple_arity) >> P.triple2) >> instance_arity_proof)
   1.134 +      (P.xname -- (P.$$$ "::" |-- P.arity) >> P.triple2) >> instance_arity_proof)
   1.135        >> (Toplevel.print oo Toplevel.theory_to_proof));
   1.136  
   1.137  val _ = OuterSyntax.add_parsers [axclassP, instanceP];