src/Pure/axclass.ML
changeset 15876 a67343c6ab2a
parent 15853 68b615bc110e
child 15973 5fd94d84470f
--- a/src/Pure/axclass.ML	Thu Apr 28 21:35:47 2005 +0200
+++ b/src/Pure/axclass.ML	Thu Apr 28 21:36:08 2005 +0200
@@ -9,27 +9,29 @@
 sig
   val quiet_mode: bool ref
   val print_axclasses: theory -> unit
-  val add_classrel_thms: thm list -> theory -> theory
-  val add_arity_thms: thm list -> theory -> theory
   val add_axclass: bclass * xclass list -> ((bstring * string) * Attrib.src list) list
     -> theory -> theory * {intro: thm, axioms: thm list}
   val add_axclass_i: bclass * class list -> ((bstring * term) * theory attribute list) list
     -> theory -> theory * {intro: thm, axioms: thm list}
-  val add_inst_subclass_x: xclass * xclass -> string list -> thm list
-    -> tactic option -> theory -> theory
+  val add_classrel_thms: thm list -> theory -> theory
+  val add_arity_thms: thm list -> theory -> theory
   val add_inst_subclass: xclass * xclass -> tactic -> theory -> theory
   val add_inst_subclass_i: class * class -> tactic -> theory -> theory
-  val add_inst_arity_x: xstring * string list * string -> string list
-    -> thm list -> tactic option -> theory -> theory
   val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory
   val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
-  val intro_classes_tac: thm list -> tactic
-  val default_intro_classes_tac: thm list -> tactic
-  val axclass_tac: thm list -> tactic
   val instance_subclass_proof: xclass * xclass -> bool -> theory -> ProofHistory.T
   val instance_subclass_proof_i: class * class -> bool -> theory -> ProofHistory.T
   val instance_arity_proof: xstring * string list * string -> bool -> theory -> ProofHistory.T
   val instance_arity_proof_i: string * sort list * sort -> bool -> theory -> ProofHistory.T
+  val intro_classes_tac: thm list -> tactic
+  val default_intro_classes_tac: thm list -> tactic
+
+  (*legacy interfaces*)
+  val axclass_tac: thm list -> tactic
+  val add_inst_subclass_x: xclass * xclass -> string list -> thm list
+    -> tactic option -> theory -> theory
+  val add_inst_arity_x: xstring * string list * string -> string list
+    -> thm list -> tactic option -> theory -> theory
 end;
 
 structure AxClass: AX_CLASS =
@@ -59,14 +61,6 @@
   | dest_varT T = raise TYPE ("dest_varT", [T], []);
 
 
-(* get axioms and theorems *)
-
-val is_def = Logic.is_equals o #prop o rep_thm;
-
-fun witnesses thy names thms =
-  PureThy.get_thmss thy (map (rpair NONE) names) @ thms @ List.filter is_def (map snd (axioms_of thy));
-
-
 
 (** abstract syntax operations **)
 
@@ -116,45 +110,6 @@
 
 
 
-(** add theorems as axioms **)
-
-fun prep_thm_axm thy thm =
-  let
-    fun err msg = raise THM ("prep_thm_axm: " ^ msg, 0, [thm]);
-
-    val {sign, hyps, prop, ...} = rep_thm thm;
-  in
-    if not (Sign.subsig (sign, Theory.sign_of thy)) then
-      err "theorem not of same theory"
-    else if not (null (extra_shyps thm)) orelse not (null hyps) then
-      err "theorem may not contain hypotheses"
-    else prop
-  end;
-
-(*theorems expressing class relations*)
-fun add_classrel_thms thms thy =
-  let
-    fun prep_thm thm =
-      let
-        val prop = prep_thm_axm thy thm;
-        val (c1, c2) = dest_classrel prop handle TERM _ =>
-          raise THM ("add_classrel_thms: theorem is not a class relation", 0, [thm]);
-      in (c1, c2) end;
-  in Theory.add_classrel_i (map prep_thm thms) thy end;
-
-(*theorems expressing arities*)
-fun add_arity_thms thms thy =
-  let
-    fun prep_thm thm =
-      let
-        val prop = prep_thm_axm thy thm;
-        val (t, ss, c) = dest_arity prop handle TERM _ =>
-          raise THM ("add_arity_thms: theorem is not an arity", 0, [thm]);
-      in (t, ss, [c]) end;
-  in Theory.add_arities_i (map prep_thm thms) thy end;
-
-
-
 (** axclass info **)
 
 (* data kind 'Pure/axclasses' *)
@@ -209,10 +164,19 @@
   thy |> AxclassesData.put (Symtab.update ((c, info), AxclassesData.get thy));
 
 
+(* class_axms *)
+
+fun class_axms sign =
+  let val classes = Sign.classes sign in
+    map (Thm.class_triv sign) classes @
+    List.mapPartial (Option.map #intro o lookup_axclass_info_sg sign) classes
+  end;
+
+
 
 (** add axiomatic type classes **)
 
-(* errors *)
+local
 
 fun err_bad_axsort ax c =
   error ("Sort constraint in axiom " ^ quote ax ^ " not supersort of " ^ quote c);
@@ -220,9 +184,6 @@
 fun err_bad_tfrees ax =
   error ("More than one type variable in axiom " ^ quote ax);
 
-
-(* ext_axclass *)
-
 fun ext_axclass prep_class prep_axm prep_att (bclass, raw_super_classes) raw_axioms_atts thy =
   let
     val sign = Theory.sign_of thy;
@@ -274,26 +235,116 @@
       |> put_axclass_info class info;
   in (final_thy, {intro = intro, axioms = axioms}) end;
 
-
-(* external interfaces *)
+in
 
 val add_axclass = ext_axclass Sign.intern_class Theory.read_axm Attrib.global_attribute;
 val add_axclass_i = ext_axclass (K I) Theory.cert_axm (K I);
 
+end;
+
+
+
+(** proven class instantiation **)
+
+(* add thms to type signature *)
+
+fun add_classrel_thms thms thy =
+  let
+    fun prep_thm thm =
+      let
+        val prop = Drule.plain_prop_of (Thm.transfer thy thm);
+        val (c1, c2) = dest_classrel prop handle TERM _ =>
+          raise THM ("add_classrel_thms: not a class relation", 0, [thm]);
+      in (c1, c2) end;
+  in Theory.add_classrel_i (map prep_thm thms) thy end;
+
+fun add_arity_thms thms thy =
+  let
+    fun prep_thm thm =
+      let
+        val prop = Drule.plain_prop_of (Thm.transfer thy thm);
+        val (t, ss, c) = dest_arity prop handle TERM _ =>
+          raise THM ("add_arity_thms: not an arity", 0, [thm]);
+      in (t, ss, [c]) end;
+  in Theory.add_arities_i (map prep_thm thms) thy end;
+
+
+(* prepare classes and arities *)
+
+fun read_class sg c = Sign.certify_class sg (Sign.intern_class sg c);
+
+fun test_classrel sg cc = (Type.add_classrel (Sign.pp sg) [cc] (Sign.tsig_of sg); cc);
+fun cert_classrel sg = test_classrel sg o Library.pairself (Sign.certify_class sg);
+fun read_classrel sg = test_classrel sg o Library.pairself (read_class sg);
+
+fun test_arity sg ar = (Type.add_arities (Sign.pp sg) [ar] (Sign.tsig_of sg); ar);
+
+fun prep_arity prep_tycon prep_sort prep sg (t, Ss, x) =
+  test_arity sg (prep_tycon sg t, map (prep_sort sg) Ss, prep sg x);
+
+val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort;
+val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
 
 
-(** prove class relations and type arities **)
+(* instance declarations -- tactical proof *)
+
+local
 
-(* class_axms *)
+fun ext_inst_subclass prep_classrel raw_cc tac thy =
+  let
+    val sign = Theory.sign_of thy;
+    val (c1, c2) = prep_classrel sign raw_cc;
+    val txt = quote (Sign.string_of_classrel sign [c1, c2]);
+    val _ = message ("Proving class inclusion " ^ txt ^ " ...");
+    val th = Tactic.prove sign [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR =>
+      error ("The error(s) above occurred while trying to prove " ^ txt);
+  in add_classrel_thms [th] thy end;
 
-fun class_axms sign =
-  let val classes = Sign.classes sign in
-    map (Thm.class_triv sign) classes @
-    List.mapPartial (Option.map #intro o lookup_axclass_info_sg sign) classes
-  end;
+fun ext_inst_arity prep_arity raw_arity tac thy =
+  let
+    val sign = Theory.sign_of thy;
+    val arity = prep_arity sign raw_arity;
+    val txt = quote (Sign.string_of_arity sign arity);
+    val _ = message ("Proving type arity " ^ txt ^ " ...");
+    val props = (mk_arities arity);
+    val ths = Tactic.prove_multi sign [] [] props
+        (fn _ => Tactic.smart_conjunction_tac (length props) THEN tac)
+      handle ERROR => error ("The error(s) above occurred while trying to prove " ^ txt);
+  in add_arity_thms ths thy end;
+
+in
+
+val add_inst_subclass = ext_inst_subclass read_classrel;
+val add_inst_subclass_i = ext_inst_subclass cert_classrel;
+val add_inst_arity = ext_inst_arity read_arity;
+val add_inst_arity_i = ext_inst_arity cert_arity;
+
+end;
 
 
-(* proof methods *)
+(* instance declarations -- Isar proof *)
+
+local
+
+fun inst_proof mk_prop add_thms inst int theory =
+  theory
+  |> IsarThy.multi_theorem_i Drule.internalK I ProofContext.export_standard
+    ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
+    (map (fn t => (("", []), [(t, ([], []))])) (mk_prop (Theory.sign_of theory) inst)) int;
+
+in
+
+val instance_subclass_proof =
+  inst_proof (single oo (mk_classrel oo read_classrel)) add_classrel_thms;
+val instance_subclass_proof_i =
+  inst_proof (single oo (mk_classrel oo cert_classrel)) add_classrel_thms;
+val instance_arity_proof = inst_proof (mk_arities oo read_arity) add_arity_thms;
+val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms;
+
+end;
+
+
+(* tactics and methods *)
 
 fun intro_classes_tac facts st =
   (ALLGOALS (Method.insert_tac facts THEN'
@@ -313,109 +364,8 @@
   ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]];
 
 
-(* old-style axclass_tac *)
 
-(*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)",
-      try class_trivs first, then "cI" axioms
-  (2) rewrite goals using user supplied definitions
-  (3) repeatedly resolve goals with user supplied non-definitions*)
-
-fun axclass_tac thms =
-  let
-    val defs = List.filter is_def thms;
-    val non_defs = filter_out is_def thms;
-  in
-    intro_classes_tac [] THEN
-    TRY (rewrite_goals_tac defs) THEN
-    TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i))
-  end;
-
-
-(* old-style provers *)
-
-fun prove mk_prop str_of sign prop thms usr_tac =
-  (Tactic.prove sign [] [] (mk_prop prop) (K (axclass_tac thms THEN (getOpt (usr_tac,all_tac))))
-    handle ERROR => error ("The error(s) above occurred while trying to prove " ^
-     quote (str_of sign prop))) |> Drule.standard;
-
-val prove_subclass = prove mk_classrel (fn sg => fn (c1, c2) =>
-  Pretty.string_of_classrel (Sign.pp sg) [c1, c2]);
-
-val prove_arity = prove mk_arity (fn sg => fn (t, Ss, c) =>
-  Pretty.string_of_arity (Sign.pp sg) (t, Ss, [c]));
-
-
-
-(** add proved subclass relations and arities **)
-
-(* prepare classes and arities *)
-
-fun read_class sg c = Sign.certify_class sg (Sign.intern_class sg c);
-
-fun test_classrel sg cc = (Type.add_classrel (Sign.pp sg) [cc] (Sign.tsig_of sg); cc);
-fun cert_classrel sg = test_classrel sg o Library.pairself (Sign.certify_class sg);
-fun read_classrel sg = test_classrel sg o Library.pairself (read_class sg);
-
-fun test_arity sg ar = (Type.add_arities (Sign.pp sg) [ar] (Sign.tsig_of sg); ar);
-
-fun prep_arity prep_tycon prep_sort prep_x sg (t, Ss, x) =
-  test_arity sg (prep_tycon sg t, map (prep_sort sg) Ss, prep_x sg x);
-
-val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort;
-val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
-
-
-(* old-style instance declarations *)
-
-fun ext_inst_subclass prep_classrel raw_c1_c2 names thms usr_tac thy =
-  let
-    val sign = Theory.sign_of thy;
-    val (c1, c2) = prep_classrel sign raw_c1_c2;
-  in
-    message ("Proving class inclusion " ^ quote (Sign.string_of_classrel sign [c1, c2]) ^ " ...");
-    thy |> add_classrel_thms [prove_subclass sign (c1, c2) (witnesses thy names thms) usr_tac]
-  end;
-
-fun ext_inst_arity prep_arity (raw_t, raw_Ss, raw_cs) names thms usr_tac thy =
-  let
-    val sign = Theory.sign_of thy;
-    val (t, Ss, cs) = prep_arity sign (raw_t, raw_Ss, raw_cs);
-    val wthms = witnesses thy names thms;
-    fun prove c =
-     (message ("Proving type arity " ^
-        quote (Sign.string_of_arity sign (t, Ss, [c])) ^ " ...");
-        prove_arity sign (t, Ss, c) wthms usr_tac);
-  in add_arity_thms (map prove cs) thy end;
-
-fun sane_inst_subclass prep sub tac = ext_inst_subclass prep sub [] [] (SOME tac);
-fun sane_inst_arity prep arity tac = ext_inst_arity prep arity [] [] (SOME tac);
-
-val add_inst_subclass_x = ext_inst_subclass read_classrel;
-val add_inst_subclass = sane_inst_subclass read_classrel;
-val add_inst_subclass_i = sane_inst_subclass cert_classrel;
-val add_inst_arity_x = ext_inst_arity read_arity;
-val add_inst_arity = sane_inst_arity read_arity;
-val add_inst_arity_i = sane_inst_arity cert_arity;
-
-
-
-(** instance proof interfaces **)
-
-fun inst_proof mk_prop add_thms inst int theory =
-  theory
-  |> IsarThy.multi_theorem_i Drule.internalK I ProofContext.export_standard
-    ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
-    (map (fn t => (("", []), [(t, ([], []))])) (mk_prop (Theory.sign_of theory) inst)) int;
-
-val instance_subclass_proof =
-  inst_proof (single oo (mk_classrel oo read_classrel)) add_classrel_thms;
-val instance_subclass_proof_i =
-  inst_proof (single oo (mk_classrel oo cert_classrel)) add_classrel_thms;
-val instance_arity_proof = inst_proof (mk_arities oo read_arity) add_arity_thms;
-val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms;
-
-
-(* outer syntax *)
+(** outer syntax **)
 
 local structure P = OuterParse and K = OuterSyntax.Keyword in
 
@@ -435,4 +385,71 @@
 
 end;
 
+
+
+(** old-style instantiation proofs **)
+
+(* axclass_tac *)
+
+(*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)",
+      try class_trivs first, then "cI" axioms
+  (2) rewrite goals using user supplied definitions
+  (3) repeatedly resolve goals with user supplied non-definitions*)
+
+val is_def = Logic.is_equals o #prop o rep_thm;
+
+fun axclass_tac thms =
+  let
+    val defs = List.filter is_def thms;
+    val non_defs = filter_out is_def thms;
+  in
+    intro_classes_tac [] THEN
+    TRY (rewrite_goals_tac defs) THEN
+    TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i))
+  end;
+
+
+(* instance declarations *)
+
+local
+
+fun prove mk_prop str_of sign prop thms usr_tac =
+  (Tactic.prove sign [] [] (mk_prop prop)
+      (K (axclass_tac thms THEN (getOpt (usr_tac, all_tac))))
+    handle ERROR => error ("The error(s) above occurred while trying to prove " ^
+     quote (str_of sign prop))) |> Drule.standard;
+
+val prove_subclass = prove mk_classrel (fn sg => fn (c1, c2) =>
+  Pretty.string_of_classrel (Sign.pp sg) [c1, c2]);
+
+val prove_arity = prove mk_arity (fn sg => fn (t, Ss, c) =>
+  Pretty.string_of_arity (Sign.pp sg) (t, Ss, [c]));
+
+fun witnesses thy names thms =
+  PureThy.get_thmss thy (map (rpair NONE) names) @ thms @ List.filter is_def (map snd (axioms_of thy));
+
+in
+
+fun add_inst_subclass_x raw_c1_c2 names thms usr_tac thy =
+  let
+    val sign = Theory.sign_of thy;
+    val (c1, c2) = read_classrel sign raw_c1_c2;
+  in
+    message ("Proving class inclusion " ^ quote (Sign.string_of_classrel sign [c1, c2]) ^ " ...");
+    thy |> add_classrel_thms [prove_subclass sign (c1, c2) (witnesses thy names thms) usr_tac]
+  end;
+
+fun add_inst_arity_x raw_arity names thms usr_tac thy =
+  let
+    val sign = Theory.sign_of thy;
+    val (t, Ss, cs) = read_arity sign raw_arity;
+    val wthms = witnesses thy names thms;
+    fun prove c =
+     (message ("Proving type arity " ^
+        quote (Sign.string_of_arity sign (t, Ss, [c])) ^ " ...");
+        prove_arity sign (t, Ss, c) wthms usr_tac);
+  in add_arity_thms (map prove cs) thy end;
+
 end;
+
+end;