src/Pure/axclass.ML
changeset 15876 a67343c6ab2a
parent 15853 68b615bc110e
child 15973 5fd94d84470f
     1.1 --- a/src/Pure/axclass.ML	Thu Apr 28 21:35:47 2005 +0200
     1.2 +++ b/src/Pure/axclass.ML	Thu Apr 28 21:36:08 2005 +0200
     1.3 @@ -9,27 +9,29 @@
     1.4  sig
     1.5    val quiet_mode: bool ref
     1.6    val print_axclasses: theory -> unit
     1.7 -  val add_classrel_thms: thm list -> theory -> theory
     1.8 -  val add_arity_thms: thm list -> theory -> theory
     1.9    val add_axclass: bclass * xclass list -> ((bstring * string) * Attrib.src list) list
    1.10      -> theory -> theory * {intro: thm, axioms: thm list}
    1.11    val add_axclass_i: bclass * class list -> ((bstring * term) * theory attribute list) list
    1.12      -> theory -> theory * {intro: thm, axioms: thm list}
    1.13 -  val add_inst_subclass_x: xclass * xclass -> string list -> thm list
    1.14 -    -> tactic option -> theory -> theory
    1.15 +  val add_classrel_thms: thm list -> theory -> theory
    1.16 +  val add_arity_thms: thm list -> theory -> theory
    1.17    val add_inst_subclass: xclass * xclass -> tactic -> theory -> theory
    1.18    val add_inst_subclass_i: class * class -> tactic -> theory -> theory
    1.19 -  val add_inst_arity_x: xstring * string list * string -> string list
    1.20 -    -> thm list -> tactic option -> theory -> theory
    1.21    val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory
    1.22    val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
    1.23 -  val intro_classes_tac: thm list -> tactic
    1.24 -  val default_intro_classes_tac: thm list -> tactic
    1.25 -  val axclass_tac: thm list -> tactic
    1.26    val instance_subclass_proof: xclass * xclass -> bool -> theory -> ProofHistory.T
    1.27    val instance_subclass_proof_i: class * class -> bool -> theory -> ProofHistory.T
    1.28    val instance_arity_proof: xstring * string list * string -> bool -> theory -> ProofHistory.T
    1.29    val instance_arity_proof_i: string * sort list * sort -> bool -> theory -> ProofHistory.T
    1.30 +  val intro_classes_tac: thm list -> tactic
    1.31 +  val default_intro_classes_tac: thm list -> tactic
    1.32 +
    1.33 +  (*legacy interfaces*)
    1.34 +  val axclass_tac: thm list -> tactic
    1.35 +  val add_inst_subclass_x: xclass * xclass -> string list -> thm list
    1.36 +    -> tactic option -> theory -> theory
    1.37 +  val add_inst_arity_x: xstring * string list * string -> string list
    1.38 +    -> thm list -> tactic option -> theory -> theory
    1.39  end;
    1.40  
    1.41  structure AxClass: AX_CLASS =
    1.42 @@ -59,14 +61,6 @@
    1.43    | dest_varT T = raise TYPE ("dest_varT", [T], []);
    1.44  
    1.45  
    1.46 -(* get axioms and theorems *)
    1.47 -
    1.48 -val is_def = Logic.is_equals o #prop o rep_thm;
    1.49 -
    1.50 -fun witnesses thy names thms =
    1.51 -  PureThy.get_thmss thy (map (rpair NONE) names) @ thms @ List.filter is_def (map snd (axioms_of thy));
    1.52 -
    1.53 -
    1.54  
    1.55  (** abstract syntax operations **)
    1.56  
    1.57 @@ -116,45 +110,6 @@
    1.58  
    1.59  
    1.60  
    1.61 -(** add theorems as axioms **)
    1.62 -
    1.63 -fun prep_thm_axm thy thm =
    1.64 -  let
    1.65 -    fun err msg = raise THM ("prep_thm_axm: " ^ msg, 0, [thm]);
    1.66 -
    1.67 -    val {sign, hyps, prop, ...} = rep_thm thm;
    1.68 -  in
    1.69 -    if not (Sign.subsig (sign, Theory.sign_of thy)) then
    1.70 -      err "theorem not of same theory"
    1.71 -    else if not (null (extra_shyps thm)) orelse not (null hyps) then
    1.72 -      err "theorem may not contain hypotheses"
    1.73 -    else prop
    1.74 -  end;
    1.75 -
    1.76 -(*theorems expressing class relations*)
    1.77 -fun add_classrel_thms thms thy =
    1.78 -  let
    1.79 -    fun prep_thm thm =
    1.80 -      let
    1.81 -        val prop = prep_thm_axm thy thm;
    1.82 -        val (c1, c2) = dest_classrel prop handle TERM _ =>
    1.83 -          raise THM ("add_classrel_thms: theorem is not a class relation", 0, [thm]);
    1.84 -      in (c1, c2) end;
    1.85 -  in Theory.add_classrel_i (map prep_thm thms) thy end;
    1.86 -
    1.87 -(*theorems expressing arities*)
    1.88 -fun add_arity_thms thms thy =
    1.89 -  let
    1.90 -    fun prep_thm thm =
    1.91 -      let
    1.92 -        val prop = prep_thm_axm thy thm;
    1.93 -        val (t, ss, c) = dest_arity prop handle TERM _ =>
    1.94 -          raise THM ("add_arity_thms: theorem is not an arity", 0, [thm]);
    1.95 -      in (t, ss, [c]) end;
    1.96 -  in Theory.add_arities_i (map prep_thm thms) thy end;
    1.97 -
    1.98 -
    1.99 -
   1.100  (** axclass info **)
   1.101  
   1.102  (* data kind 'Pure/axclasses' *)
   1.103 @@ -209,10 +164,19 @@
   1.104    thy |> AxclassesData.put (Symtab.update ((c, info), AxclassesData.get thy));
   1.105  
   1.106  
   1.107 +(* class_axms *)
   1.108 +
   1.109 +fun class_axms sign =
   1.110 +  let val classes = Sign.classes sign in
   1.111 +    map (Thm.class_triv sign) classes @
   1.112 +    List.mapPartial (Option.map #intro o lookup_axclass_info_sg sign) classes
   1.113 +  end;
   1.114 +
   1.115 +
   1.116  
   1.117  (** add axiomatic type classes **)
   1.118  
   1.119 -(* errors *)
   1.120 +local
   1.121  
   1.122  fun err_bad_axsort ax c =
   1.123    error ("Sort constraint in axiom " ^ quote ax ^ " not supersort of " ^ quote c);
   1.124 @@ -220,9 +184,6 @@
   1.125  fun err_bad_tfrees ax =
   1.126    error ("More than one type variable in axiom " ^ quote ax);
   1.127  
   1.128 -
   1.129 -(* ext_axclass *)
   1.130 -
   1.131  fun ext_axclass prep_class prep_axm prep_att (bclass, raw_super_classes) raw_axioms_atts thy =
   1.132    let
   1.133      val sign = Theory.sign_of thy;
   1.134 @@ -274,26 +235,116 @@
   1.135        |> put_axclass_info class info;
   1.136    in (final_thy, {intro = intro, axioms = axioms}) end;
   1.137  
   1.138 -
   1.139 -(* external interfaces *)
   1.140 +in
   1.141  
   1.142  val add_axclass = ext_axclass Sign.intern_class Theory.read_axm Attrib.global_attribute;
   1.143  val add_axclass_i = ext_axclass (K I) Theory.cert_axm (K I);
   1.144  
   1.145 +end;
   1.146 +
   1.147 +
   1.148 +
   1.149 +(** proven class instantiation **)
   1.150 +
   1.151 +(* add thms to type signature *)
   1.152 +
   1.153 +fun add_classrel_thms thms thy =
   1.154 +  let
   1.155 +    fun prep_thm thm =
   1.156 +      let
   1.157 +        val prop = Drule.plain_prop_of (Thm.transfer thy thm);
   1.158 +        val (c1, c2) = dest_classrel prop handle TERM _ =>
   1.159 +          raise THM ("add_classrel_thms: not a class relation", 0, [thm]);
   1.160 +      in (c1, c2) end;
   1.161 +  in Theory.add_classrel_i (map prep_thm thms) thy end;
   1.162 +
   1.163 +fun add_arity_thms thms thy =
   1.164 +  let
   1.165 +    fun prep_thm thm =
   1.166 +      let
   1.167 +        val prop = Drule.plain_prop_of (Thm.transfer thy thm);
   1.168 +        val (t, ss, c) = dest_arity prop handle TERM _ =>
   1.169 +          raise THM ("add_arity_thms: not an arity", 0, [thm]);
   1.170 +      in (t, ss, [c]) end;
   1.171 +  in Theory.add_arities_i (map prep_thm thms) thy end;
   1.172 +
   1.173 +
   1.174 +(* prepare classes and arities *)
   1.175 +
   1.176 +fun read_class sg c = Sign.certify_class sg (Sign.intern_class sg c);
   1.177 +
   1.178 +fun test_classrel sg cc = (Type.add_classrel (Sign.pp sg) [cc] (Sign.tsig_of sg); cc);
   1.179 +fun cert_classrel sg = test_classrel sg o Library.pairself (Sign.certify_class sg);
   1.180 +fun read_classrel sg = test_classrel sg o Library.pairself (read_class sg);
   1.181 +
   1.182 +fun test_arity sg ar = (Type.add_arities (Sign.pp sg) [ar] (Sign.tsig_of sg); ar);
   1.183 +
   1.184 +fun prep_arity prep_tycon prep_sort prep sg (t, Ss, x) =
   1.185 +  test_arity sg (prep_tycon sg t, map (prep_sort sg) Ss, prep sg x);
   1.186 +
   1.187 +val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort;
   1.188 +val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
   1.189  
   1.190  
   1.191 -(** prove class relations and type arities **)
   1.192 +(* instance declarations -- tactical proof *)
   1.193 +
   1.194 +local
   1.195  
   1.196 -(* class_axms *)
   1.197 +fun ext_inst_subclass prep_classrel raw_cc tac thy =
   1.198 +  let
   1.199 +    val sign = Theory.sign_of thy;
   1.200 +    val (c1, c2) = prep_classrel sign raw_cc;
   1.201 +    val txt = quote (Sign.string_of_classrel sign [c1, c2]);
   1.202 +    val _ = message ("Proving class inclusion " ^ txt ^ " ...");
   1.203 +    val th = Tactic.prove sign [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR =>
   1.204 +      error ("The error(s) above occurred while trying to prove " ^ txt);
   1.205 +  in add_classrel_thms [th] thy end;
   1.206  
   1.207 -fun class_axms sign =
   1.208 -  let val classes = Sign.classes sign in
   1.209 -    map (Thm.class_triv sign) classes @
   1.210 -    List.mapPartial (Option.map #intro o lookup_axclass_info_sg sign) classes
   1.211 -  end;
   1.212 +fun ext_inst_arity prep_arity raw_arity tac thy =
   1.213 +  let
   1.214 +    val sign = Theory.sign_of thy;
   1.215 +    val arity = prep_arity sign raw_arity;
   1.216 +    val txt = quote (Sign.string_of_arity sign arity);
   1.217 +    val _ = message ("Proving type arity " ^ txt ^ " ...");
   1.218 +    val props = (mk_arities arity);
   1.219 +    val ths = Tactic.prove_multi sign [] [] props
   1.220 +        (fn _ => Tactic.smart_conjunction_tac (length props) THEN tac)
   1.221 +      handle ERROR => error ("The error(s) above occurred while trying to prove " ^ txt);
   1.222 +  in add_arity_thms ths thy end;
   1.223 +
   1.224 +in
   1.225 +
   1.226 +val add_inst_subclass = ext_inst_subclass read_classrel;
   1.227 +val add_inst_subclass_i = ext_inst_subclass cert_classrel;
   1.228 +val add_inst_arity = ext_inst_arity read_arity;
   1.229 +val add_inst_arity_i = ext_inst_arity cert_arity;
   1.230 +
   1.231 +end;
   1.232  
   1.233  
   1.234 -(* proof methods *)
   1.235 +(* instance declarations -- Isar proof *)
   1.236 +
   1.237 +local
   1.238 +
   1.239 +fun inst_proof mk_prop add_thms inst int theory =
   1.240 +  theory
   1.241 +  |> IsarThy.multi_theorem_i Drule.internalK I ProofContext.export_standard
   1.242 +    ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
   1.243 +    (map (fn t => (("", []), [(t, ([], []))])) (mk_prop (Theory.sign_of theory) inst)) int;
   1.244 +
   1.245 +in
   1.246 +
   1.247 +val instance_subclass_proof =
   1.248 +  inst_proof (single oo (mk_classrel oo read_classrel)) add_classrel_thms;
   1.249 +val instance_subclass_proof_i =
   1.250 +  inst_proof (single oo (mk_classrel oo cert_classrel)) add_classrel_thms;
   1.251 +val instance_arity_proof = inst_proof (mk_arities oo read_arity) add_arity_thms;
   1.252 +val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms;
   1.253 +
   1.254 +end;
   1.255 +
   1.256 +
   1.257 +(* tactics and methods *)
   1.258  
   1.259  fun intro_classes_tac facts st =
   1.260    (ALLGOALS (Method.insert_tac facts THEN'
   1.261 @@ -313,109 +364,8 @@
   1.262    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]];
   1.263  
   1.264  
   1.265 -(* old-style axclass_tac *)
   1.266  
   1.267 -(*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)",
   1.268 -      try class_trivs first, then "cI" axioms
   1.269 -  (2) rewrite goals using user supplied definitions
   1.270 -  (3) repeatedly resolve goals with user supplied non-definitions*)
   1.271 -
   1.272 -fun axclass_tac thms =
   1.273 -  let
   1.274 -    val defs = List.filter is_def thms;
   1.275 -    val non_defs = filter_out is_def thms;
   1.276 -  in
   1.277 -    intro_classes_tac [] THEN
   1.278 -    TRY (rewrite_goals_tac defs) THEN
   1.279 -    TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i))
   1.280 -  end;
   1.281 -
   1.282 -
   1.283 -(* old-style provers *)
   1.284 -
   1.285 -fun prove mk_prop str_of sign prop thms usr_tac =
   1.286 -  (Tactic.prove sign [] [] (mk_prop prop) (K (axclass_tac thms THEN (getOpt (usr_tac,all_tac))))
   1.287 -    handle ERROR => error ("The error(s) above occurred while trying to prove " ^
   1.288 -     quote (str_of sign prop))) |> Drule.standard;
   1.289 -
   1.290 -val prove_subclass = prove mk_classrel (fn sg => fn (c1, c2) =>
   1.291 -  Pretty.string_of_classrel (Sign.pp sg) [c1, c2]);
   1.292 -
   1.293 -val prove_arity = prove mk_arity (fn sg => fn (t, Ss, c) =>
   1.294 -  Pretty.string_of_arity (Sign.pp sg) (t, Ss, [c]));
   1.295 -
   1.296 -
   1.297 -
   1.298 -(** add proved subclass relations and arities **)
   1.299 -
   1.300 -(* prepare classes and arities *)
   1.301 -
   1.302 -fun read_class sg c = Sign.certify_class sg (Sign.intern_class sg c);
   1.303 -
   1.304 -fun test_classrel sg cc = (Type.add_classrel (Sign.pp sg) [cc] (Sign.tsig_of sg); cc);
   1.305 -fun cert_classrel sg = test_classrel sg o Library.pairself (Sign.certify_class sg);
   1.306 -fun read_classrel sg = test_classrel sg o Library.pairself (read_class sg);
   1.307 -
   1.308 -fun test_arity sg ar = (Type.add_arities (Sign.pp sg) [ar] (Sign.tsig_of sg); ar);
   1.309 -
   1.310 -fun prep_arity prep_tycon prep_sort prep_x sg (t, Ss, x) =
   1.311 -  test_arity sg (prep_tycon sg t, map (prep_sort sg) Ss, prep_x sg x);
   1.312 -
   1.313 -val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort;
   1.314 -val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
   1.315 -
   1.316 -
   1.317 -(* old-style instance declarations *)
   1.318 -
   1.319 -fun ext_inst_subclass prep_classrel raw_c1_c2 names thms usr_tac thy =
   1.320 -  let
   1.321 -    val sign = Theory.sign_of thy;
   1.322 -    val (c1, c2) = prep_classrel sign raw_c1_c2;
   1.323 -  in
   1.324 -    message ("Proving class inclusion " ^ quote (Sign.string_of_classrel sign [c1, c2]) ^ " ...");
   1.325 -    thy |> add_classrel_thms [prove_subclass sign (c1, c2) (witnesses thy names thms) usr_tac]
   1.326 -  end;
   1.327 -
   1.328 -fun ext_inst_arity prep_arity (raw_t, raw_Ss, raw_cs) names thms usr_tac thy =
   1.329 -  let
   1.330 -    val sign = Theory.sign_of thy;
   1.331 -    val (t, Ss, cs) = prep_arity sign (raw_t, raw_Ss, raw_cs);
   1.332 -    val wthms = witnesses thy names thms;
   1.333 -    fun prove c =
   1.334 -     (message ("Proving type arity " ^
   1.335 -        quote (Sign.string_of_arity sign (t, Ss, [c])) ^ " ...");
   1.336 -        prove_arity sign (t, Ss, c) wthms usr_tac);
   1.337 -  in add_arity_thms (map prove cs) thy end;
   1.338 -
   1.339 -fun sane_inst_subclass prep sub tac = ext_inst_subclass prep sub [] [] (SOME tac);
   1.340 -fun sane_inst_arity prep arity tac = ext_inst_arity prep arity [] [] (SOME tac);
   1.341 -
   1.342 -val add_inst_subclass_x = ext_inst_subclass read_classrel;
   1.343 -val add_inst_subclass = sane_inst_subclass read_classrel;
   1.344 -val add_inst_subclass_i = sane_inst_subclass cert_classrel;
   1.345 -val add_inst_arity_x = ext_inst_arity read_arity;
   1.346 -val add_inst_arity = sane_inst_arity read_arity;
   1.347 -val add_inst_arity_i = sane_inst_arity cert_arity;
   1.348 -
   1.349 -
   1.350 -
   1.351 -(** instance proof interfaces **)
   1.352 -
   1.353 -fun inst_proof mk_prop add_thms inst int theory =
   1.354 -  theory
   1.355 -  |> IsarThy.multi_theorem_i Drule.internalK I ProofContext.export_standard
   1.356 -    ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
   1.357 -    (map (fn t => (("", []), [(t, ([], []))])) (mk_prop (Theory.sign_of theory) inst)) int;
   1.358 -
   1.359 -val instance_subclass_proof =
   1.360 -  inst_proof (single oo (mk_classrel oo read_classrel)) add_classrel_thms;
   1.361 -val instance_subclass_proof_i =
   1.362 -  inst_proof (single oo (mk_classrel oo cert_classrel)) add_classrel_thms;
   1.363 -val instance_arity_proof = inst_proof (mk_arities oo read_arity) add_arity_thms;
   1.364 -val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms;
   1.365 -
   1.366 -
   1.367 -(* outer syntax *)
   1.368 +(** outer syntax **)
   1.369  
   1.370  local structure P = OuterParse and K = OuterSyntax.Keyword in
   1.371  
   1.372 @@ -435,4 +385,71 @@
   1.373  
   1.374  end;
   1.375  
   1.376 +
   1.377 +
   1.378 +(** old-style instantiation proofs **)
   1.379 +
   1.380 +(* axclass_tac *)
   1.381 +
   1.382 +(*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)",
   1.383 +      try class_trivs first, then "cI" axioms
   1.384 +  (2) rewrite goals using user supplied definitions
   1.385 +  (3) repeatedly resolve goals with user supplied non-definitions*)
   1.386 +
   1.387 +val is_def = Logic.is_equals o #prop o rep_thm;
   1.388 +
   1.389 +fun axclass_tac thms =
   1.390 +  let
   1.391 +    val defs = List.filter is_def thms;
   1.392 +    val non_defs = filter_out is_def thms;
   1.393 +  in
   1.394 +    intro_classes_tac [] THEN
   1.395 +    TRY (rewrite_goals_tac defs) THEN
   1.396 +    TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i))
   1.397 +  end;
   1.398 +
   1.399 +
   1.400 +(* instance declarations *)
   1.401 +
   1.402 +local
   1.403 +
   1.404 +fun prove mk_prop str_of sign prop thms usr_tac =
   1.405 +  (Tactic.prove sign [] [] (mk_prop prop)
   1.406 +      (K (axclass_tac thms THEN (getOpt (usr_tac, all_tac))))
   1.407 +    handle ERROR => error ("The error(s) above occurred while trying to prove " ^
   1.408 +     quote (str_of sign prop))) |> Drule.standard;
   1.409 +
   1.410 +val prove_subclass = prove mk_classrel (fn sg => fn (c1, c2) =>
   1.411 +  Pretty.string_of_classrel (Sign.pp sg) [c1, c2]);
   1.412 +
   1.413 +val prove_arity = prove mk_arity (fn sg => fn (t, Ss, c) =>
   1.414 +  Pretty.string_of_arity (Sign.pp sg) (t, Ss, [c]));
   1.415 +
   1.416 +fun witnesses thy names thms =
   1.417 +  PureThy.get_thmss thy (map (rpair NONE) names) @ thms @ List.filter is_def (map snd (axioms_of thy));
   1.418 +
   1.419 +in
   1.420 +
   1.421 +fun add_inst_subclass_x raw_c1_c2 names thms usr_tac thy =
   1.422 +  let
   1.423 +    val sign = Theory.sign_of thy;
   1.424 +    val (c1, c2) = read_classrel sign raw_c1_c2;
   1.425 +  in
   1.426 +    message ("Proving class inclusion " ^ quote (Sign.string_of_classrel sign [c1, c2]) ^ " ...");
   1.427 +    thy |> add_classrel_thms [prove_subclass sign (c1, c2) (witnesses thy names thms) usr_tac]
   1.428 +  end;
   1.429 +
   1.430 +fun add_inst_arity_x raw_arity names thms usr_tac thy =
   1.431 +  let
   1.432 +    val sign = Theory.sign_of thy;
   1.433 +    val (t, Ss, cs) = read_arity sign raw_arity;
   1.434 +    val wthms = witnesses thy names thms;
   1.435 +    fun prove c =
   1.436 +     (message ("Proving type arity " ^
   1.437 +        quote (Sign.string_of_arity sign (t, Ss, [c])) ^ " ...");
   1.438 +        prove_arity sign (t, Ss, c) wthms usr_tac);
   1.439 +  in add_arity_thms (map prove cs) thy end;
   1.440 +
   1.441  end;
   1.442 +
   1.443 +end;