'instance' and intro_classes now handle general sorts;
authorwenzelm
Fri Apr 16 20:59:09 2004 +0200 (2004-04-16)
changeset 146059de4d64eee3b
parent 14604 1946097f7068
child 14606 0be6c11e7128
'instance' and intro_classes now handle general sorts;
doc-src/IsarRef/generic.tex
doc-src/IsarRef/syntax.tex
src/Provers/classical.ML
src/Pure/Isar/outer_parse.ML
src/Pure/axclass.ML
     1.1 --- a/doc-src/IsarRef/generic.tex	Fri Apr 16 20:34:41 2004 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Fri Apr 16 20:59:09 2004 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4  \begin{rail}
     1.5    'axclass' classdecl (axmdecl prop +)
     1.6    ;
     1.7 -  'instance' (nameref ('<' | subseteq) nameref | nameref '::' simplearity)
     1.8 +  'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
     1.9    ;
    1.10  \end{rail}
    1.11  
    1.12 @@ -39,8 +39,8 @@
    1.13    The ``axioms'' are stored as theorems according to the given name
    1.14    specifications, adding the class name $c$ as name space prefix; the same
    1.15    facts are also stored collectively as $c{\dtt}axioms$.
    1.16 -
    1.17 -\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)c$] setup a
    1.18 +  
    1.19 +\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)s$] setup a
    1.20    goal stating a class relation or type arity.  The proof would usually
    1.21    proceed by $intro_classes$, and then establish the characteristic theorems
    1.22    of the type classes involved.  After finishing the proof, the theory will be
     2.1 --- a/doc-src/IsarRef/syntax.tex	Fri Apr 16 20:34:41 2004 +0200
     2.2 +++ b/doc-src/IsarRef/syntax.tex	Fri Apr 16 20:59:09 2004 +0200
     2.3 @@ -204,7 +204,7 @@
     2.4  \railalias{subseteq}{\isasymsubseteq}
     2.5  \railterm{subseteq}
     2.6  
     2.7 -\indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
     2.8 +\indexouternonterm{sort}\indexouternonterm{arity}
     2.9  \indexouternonterm{classdecl}
    2.10  \begin{rail}
    2.11    classdecl: name (('<' | subseteq) (nameref + ','))?
    2.12 @@ -213,8 +213,6 @@
    2.13    ;
    2.14    arity: ('(' (sort + ',') ')')? sort
    2.15    ;
    2.16 -  simplearity: ('(' (sort + ',') ')')? nameref
    2.17 -  ;
    2.18  \end{rail}
    2.19  
    2.20  
     3.1 --- a/src/Provers/classical.ML	Fri Apr 16 20:34:41 2004 +0200
     3.2 +++ b/src/Provers/classical.ML	Fri Apr 16 20:59:09 2004 +0200
     3.3 @@ -924,7 +924,8 @@
     3.4  
     3.5  (** proof methods **)
     3.6  
     3.7 -(* METHOD_CLASET' *)
     3.8 +fun METHOD_CLASET tac ctxt =
     3.9 +  Method.METHOD (tac ctxt (get_local_claset ctxt));
    3.10  
    3.11  fun METHOD_CLASET' tac ctxt =
    3.12    Method.METHOD (HEADGOAL o tac ctxt (get_local_claset ctxt));
    3.13 @@ -947,12 +948,12 @@
    3.14    | rule_tac rules _ _ facts = Method.rule_tac rules facts;
    3.15  
    3.16  fun default_tac rules ctxt cs facts =
    3.17 -  rule_tac rules ctxt cs facts ORELSE'
    3.18 +  HEADGOAL (rule_tac rules ctxt cs facts) ORELSE
    3.19    AxClass.default_intro_classes_tac facts;
    3.20  
    3.21  in
    3.22    val rule = METHOD_CLASET' o rule_tac;
    3.23 -  val default = METHOD_CLASET' o default_tac;
    3.24 +  val default = METHOD_CLASET o default_tac;
    3.25  end;
    3.26  
    3.27  
     4.1 --- a/src/Pure/Isar/outer_parse.ML	Fri Apr 16 20:34:41 2004 +0200
     4.2 +++ b/src/Pure/Isar/outer_parse.ML	Fri Apr 16 20:59:09 2004 +0200
     4.3 @@ -47,7 +47,6 @@
     4.4    val uname: token list -> string option * token list
     4.5    val sort: token list -> string * token list
     4.6    val arity: token list -> (string list * string) * token list
     4.7 -  val simple_arity: token list -> (string list * xclass) * token list
     4.8    val type_args: token list -> string list * token list
     4.9    val typ: token list -> string * token list
    4.10    val opt_infix: token list -> Syntax.mixfix * token list
    4.11 @@ -185,7 +184,6 @@
    4.12    Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- cod;
    4.13  
    4.14  val arity = gen_arity sort;
    4.15 -val simple_arity = gen_arity xname;
    4.16  
    4.17  
    4.18  (* types *)
     5.1 --- a/src/Pure/axclass.ML	Fri Apr 16 20:34:41 2004 +0200
     5.2 +++ b/src/Pure/axclass.ML	Fri Apr 16 20:59:09 2004 +0200
     5.3 @@ -24,12 +24,12 @@
     5.4      -> thm list -> tactic option -> theory -> theory
     5.5    val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory
     5.6    val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
     5.7 -  val default_intro_classes_tac: thm list -> int -> tactic
     5.8 +  val default_intro_classes_tac: thm list -> tactic
     5.9    val axclass_tac: thm list -> tactic
    5.10    val instance_subclass_proof: xclass * xclass -> bool -> theory -> ProofHistory.T
    5.11    val instance_subclass_proof_i: class * class -> bool -> theory -> ProofHistory.T
    5.12 -  val instance_arity_proof: xstring * string list * xclass -> bool -> theory -> ProofHistory.T
    5.13 -  val instance_arity_proof_i: string * sort list * class -> bool -> theory -> ProofHistory.T
    5.14 +  val instance_arity_proof: xstring * string list * string -> bool -> theory -> ProofHistory.T
    5.15 +  val instance_arity_proof_i: string * sort list * sort -> bool -> theory -> ProofHistory.T
    5.16    val setup: (theory -> theory) list
    5.17  end;
    5.18  
    5.19 @@ -94,11 +94,13 @@
    5.20  
    5.21  (* arities as terms *)
    5.22  
    5.23 -fun mk_arity (t, ss, c) =
    5.24 +fun mk_arity (t, Ss, c) =
    5.25    let
    5.26 -    val tfrees = ListPair.map TFree (Term.invent_type_names [] (length ss), ss);
    5.27 +    val tfrees = ListPair.map TFree (Term.invent_type_names [] (length Ss), Ss);
    5.28    in Logic.mk_inclass (Type (t, tfrees), c) end;
    5.29  
    5.30 +fun mk_arities (t, Ss, S) = map (fn c => mk_arity (t, Ss, c)) S;
    5.31 +
    5.32  fun dest_arity tm =
    5.33    let
    5.34      fun err () = raise TERM ("dest_arity", [tm]);
    5.35 @@ -299,29 +301,30 @@
    5.36  
    5.37  (* intro_classes *)
    5.38  
    5.39 -fun intro_classes_tac facts i st =
    5.40 -  ((Method.insert_tac facts THEN'
    5.41 -    REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st)))) i
    5.42 -    THEN Tactic.distinct_subgoals_tac) st;    (*affects all subgoals!?*)
    5.43 +fun intro_classes_tac facts st =
    5.44 +  (ALLGOALS (Method.insert_tac facts THEN'
    5.45 +      REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st))))
    5.46 +    THEN Tactic.distinct_subgoals_tac) st;
    5.47  
    5.48  val intro_classes_method =
    5.49 -  ("intro_classes", Method.no_args (Method.METHOD (HEADGOAL o intro_classes_tac)),
    5.50 +  ("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
    5.51      "back-chain introduction rules of axiomatic type classes");
    5.52  
    5.53  
    5.54  (* default method *)
    5.55  
    5.56 -fun default_intro_classes_tac [] i = intro_classes_tac [] i
    5.57 -  | default_intro_classes_tac _ _ = Tactical.no_tac;    (*no error message!*)
    5.58 +fun default_intro_classes_tac [] = intro_classes_tac []
    5.59 +  | default_intro_classes_tac _ = Tactical.no_tac;    (*no error message!*)
    5.60  
    5.61  fun default_tac rules ctxt facts =
    5.62 -  HEADGOAL (Method.some_rule_tac rules ctxt facts ORELSE' default_intro_classes_tac facts);
    5.63 +  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
    5.64 +    default_intro_classes_tac facts;
    5.65  
    5.66  val default_method =
    5.67    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule");
    5.68  
    5.69  
    5.70 -(* axclass_tac *)
    5.71 +(* old-style axclass_tac *)
    5.72  
    5.73  (*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)",
    5.74        try class_trivs first, then "cI" axioms
    5.75 @@ -333,13 +336,13 @@
    5.76      val defs = filter is_def thms;
    5.77      val non_defs = filter_out is_def thms;
    5.78    in
    5.79 -    HEADGOAL (intro_classes_tac []) THEN
    5.80 +    intro_classes_tac [] THEN
    5.81      TRY (rewrite_goals_tac defs) THEN
    5.82      TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i))
    5.83    end;
    5.84  
    5.85  
    5.86 -(* provers *)
    5.87 +(* old-style provers *)
    5.88  
    5.89  fun prove mk_prop str_of sign prop thms usr_tac =
    5.90    (Tactic.prove sign [] [] (mk_prop prop) (K (axclass_tac thms THEN (if_none usr_tac all_tac)))
    5.91 @@ -377,8 +380,6 @@
    5.92  
    5.93  val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort;
    5.94  val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
    5.95 -val read_simple_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.intern_class;
    5.96 -fun cert_simple_arity arg = prep_arity (K I) Sign.certify_sort (K I) arg;
    5.97  
    5.98  
    5.99  (* old-style instance declarations *)
   5.100 @@ -417,17 +418,18 @@
   5.101  
   5.102  (** instance proof interfaces **)
   5.103  
   5.104 -fun inst_attribute add_thms (thy, thm) = (add_thms [thm] thy, thm);
   5.105 +fun inst_proof mk_prop add_thms inst int theory =
   5.106 +  theory
   5.107 +  |> IsarThy.multi_theorem_i Drule.internalK
   5.108 +    ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
   5.109 +    (map (fn t => (("", []), [(t, ([], []))])) (mk_prop (Theory.sign_of theory) inst)) int;
   5.110  
   5.111 -fun inst_proof mk_prop add_thms sig_prop int thy =
   5.112 -  thy
   5.113 -  |> IsarThy.theorem_i Drule.internalK (("", [inst_attribute add_thms]),
   5.114 -    (mk_prop (Theory.sign_of thy) sig_prop, ([], []))) int;
   5.115 -
   5.116 -val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms;
   5.117 -val instance_subclass_proof_i = inst_proof (mk_classrel oo cert_classrel) add_classrel_thms;
   5.118 -val instance_arity_proof = inst_proof (mk_arity oo read_simple_arity) add_arity_thms;
   5.119 -val instance_arity_proof_i = inst_proof (mk_arity oo cert_simple_arity) add_arity_thms;
   5.120 +val instance_subclass_proof =
   5.121 +  inst_proof (single oo (mk_classrel oo read_classrel)) add_classrel_thms;
   5.122 +val instance_subclass_proof_i =
   5.123 +  inst_proof (single oo (mk_classrel oo cert_classrel)) add_classrel_thms;
   5.124 +val instance_arity_proof = inst_proof (mk_arities oo read_arity) add_arity_thms;
   5.125 +val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms;
   5.126  
   5.127  
   5.128  
   5.129 @@ -453,7 +455,7 @@
   5.130  val instanceP =
   5.131    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
   5.132      ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.xname) >> instance_subclass_proof ||
   5.133 -      (P.xname -- (P.$$$ "::" |-- P.simple_arity) >> P.triple2) >> instance_arity_proof)
   5.134 +      (P.xname -- (P.$$$ "::" |-- P.arity) >> P.triple2) >> instance_arity_proof)
   5.135        >> (Toplevel.print oo Toplevel.theory_to_proof));
   5.136  
   5.137  val _ = OuterSyntax.add_parsers [axclassP, instanceP];