src/Pure/Isar/isar_thy.ML
changeset 6371 8469852acbc0
parent 6354 a4c75cbd2fbf
child 6404 2daaf2943c79
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Wed Mar 17 13:34:49 1999 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed Mar 17 13:36:23 1999 +0100
     1.3 @@ -2,10 +2,9 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Derived theory operations.
     1.8 +Pure/Isar derived theory operations.
     1.9  
    1.10  TODO:
    1.11 -  - pure_thy.ML: add_constdefs (atomic!);
    1.12    - 'methods' section (proof macros, ML method defs) (!?);
    1.13    - next_block: ProofHistory open / close (!?);
    1.14  *)
    1.15 @@ -19,33 +18,61 @@
    1.16    val add_subsection: string -> theory -> theory
    1.17    val add_subsubsection: string -> theory -> theory
    1.18    val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory
    1.19 +  val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
    1.20    val add_defs: ((bstring * string) * Args.src list) list -> theory -> theory
    1.21 +  val add_defs_i: ((bstring * term) * theory attribute list) list -> theory -> theory
    1.22 +  val add_constdefs: ((bstring * string * mixfix) * string) list -> theory -> theory
    1.23 +  val add_constdefs_i: ((bstring * typ * mixfix) * term) list -> theory -> theory
    1.24 +  val apply_theorems: (xstring * Args.src list) list -> theory -> theory * thm list
    1.25 +  val apply_theorems_i: (thm * theory attribute list) list -> theory -> theory * thm list
    1.26    val have_theorems: (bstring * Args.src list) * (xstring * Args.src list) list
    1.27      -> theory -> theory
    1.28 +  val have_theorems_i: (bstring * theory attribute list) * (thm * theory attribute list) list
    1.29 +    -> theory -> theory
    1.30    val have_lemmas: (bstring * Args.src list) * (xstring * Args.src list) list
    1.31      -> theory -> theory
    1.32 +  val have_lemmas_i: (bstring * theory attribute list) * (thm * theory attribute list) list
    1.33 +    -> theory -> theory
    1.34    val have_facts: (string * Args.src list) * (string * Args.src list) list
    1.35      -> ProofHistory.T -> ProofHistory.T
    1.36 +  val have_facts_i: (string * Proof.context attribute list) *
    1.37 +    (thm * Proof.context attribute list) list -> ProofHistory.T -> ProofHistory.T
    1.38 +  val from_facts: (string * Args.src list) list -> ProofHistory.T -> ProofHistory.T
    1.39 +  val from_facts_i: (thm * Proof.context attribute list) list -> ProofHistory.T -> ProofHistory.T
    1.40 +  val chain: ProofHistory.T -> ProofHistory.T
    1.41    val fix: (string * string option) list -> ProofHistory.T -> ProofHistory.T
    1.42 +  val fix_i: (string * typ) list -> ProofHistory.T -> ProofHistory.T
    1.43    val match_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T
    1.44 +  val match_bind_i: (term list * term) list -> ProofHistory.T -> ProofHistory.T
    1.45    val theorem: string -> Args.src list -> string * string list -> theory -> ProofHistory.T
    1.46 +  val theorem_i: bstring -> theory attribute list -> term * term list -> theory -> ProofHistory.T
    1.47    val lemma: string -> Args.src list -> string * string list -> theory -> ProofHistory.T
    1.48 +  val lemma_i: bstring -> theory attribute list -> term * term list -> theory -> ProofHistory.T
    1.49    val assume: string -> Args.src list -> (string * string list) list
    1.50      -> ProofHistory.T -> ProofHistory.T
    1.51 +  val assume_i: string -> Proof.context attribute list -> (term * term list) list
    1.52 +    -> ProofHistory.T -> ProofHistory.T
    1.53    val show: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
    1.54 +  val show_i: string -> Proof.context attribute list -> term * term list
    1.55 +    -> ProofHistory.T -> ProofHistory.T
    1.56    val have: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
    1.57 -  val chain: ProofHistory.T -> ProofHistory.T
    1.58 -  val from_facts: (string * Args.src list) list -> ProofHistory.T -> ProofHistory.T
    1.59 +  val have_i: string -> Proof.context attribute list -> term * term list
    1.60 +    -> ProofHistory.T -> ProofHistory.T
    1.61    val begin_block: ProofHistory.T -> ProofHistory.T
    1.62    val next_block: ProofHistory.T -> ProofHistory.T
    1.63    val end_block: ProofHistory.T -> ProofHistory.T
    1.64    val qed_with: bstring option * Args.src list option -> ProofHistory.T -> theory
    1.65 +  val qed_with_i: bstring option * theory attribute list option -> ProofHistory.T -> theory
    1.66    val qed: ProofHistory.T -> theory
    1.67    val kill_proof: ProofHistory.T -> theory
    1.68    val tac: Method.text -> ProofHistory.T -> ProofHistory.T
    1.69 +  val tac_i: (Proof.context -> Proof.method) -> ProofHistory.T -> ProofHistory.T
    1.70    val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
    1.71 +  val then_tac_i: (Proof.context -> Proof.method) -> ProofHistory.T -> ProofHistory.T
    1.72    val proof: Method.text option -> ProofHistory.T -> ProofHistory.T
    1.73 +  val proof_i: (Proof.context -> Proof.method) option -> ProofHistory.T -> ProofHistory.T
    1.74    val terminal_proof: Method.text -> ProofHistory.T -> ProofHistory.T
    1.75 +  val terminal_proof_i: (Proof.context -> Proof.method) -> ProofHistory.T -> ProofHistory.T
    1.76    val immediate_proof: ProofHistory.T -> ProofHistory.T
    1.77    val default_proof: ProofHistory.T -> ProofHistory.T
    1.78    val use_mltext: string -> theory option -> theory option
    1.79 @@ -72,7 +99,7 @@
    1.80  
    1.81  (** derived theory and proof operations **)
    1.82  
    1.83 -(* formal comments *)	(* FIXME dummy *)
    1.84 +(* formal comments *)   (* FIXME dummy *)
    1.85  
    1.86  fun add_text (txt:string) (thy:theory) = thy;
    1.87  fun add_title title author date thy = thy;
    1.88 @@ -88,7 +115,20 @@
    1.89    f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;
    1.90  
    1.91  val add_axioms = add_axms PureThy.add_axioms;
    1.92 +val add_axioms_i = PureThy.add_axioms_i;
    1.93  val add_defs = add_axms PureThy.add_defs;
    1.94 +val add_defs_i = PureThy.add_defs_i;
    1.95 +
    1.96 +
    1.97 +(* constdefs *)
    1.98 +
    1.99 +fun gen_add_constdefs consts defs args thy =
   1.100 +  thy
   1.101 +  |> consts (map fst args)
   1.102 +  |> defs (map (fn ((c, _, mx), s) => ((Thm.def_name (Syntax.const_name c mx), s), [])) args);
   1.103 +
   1.104 +val add_constdefs = gen_add_constdefs Theory.add_consts add_defs;
   1.105 +val add_constdefs_i = gen_add_constdefs Theory.add_consts_i add_defs_i;
   1.106  
   1.107  
   1.108  (* theorems *)
   1.109 @@ -97,63 +137,86 @@
   1.110    f name (map (attrib x) more_srcs)
   1.111      (map (fn (s, srcs) => (get x s, map (attrib x) srcs)) th_srcs) x;
   1.112  
   1.113 -
   1.114 -val have_theorems =
   1.115 -  #1 oo gen_have_thmss PureThy.get_thms Attrib.global_attribute PureThy.have_thmss;
   1.116 +fun global_have_thmss x = gen_have_thmss PureThy.get_thms Attrib.global_attribute x;
   1.117  
   1.118 -val have_lemmas =
   1.119 -  #1 oo gen_have_thmss PureThy.get_thms Attrib.global_attribute
   1.120 -    (fn name => fn more_atts => PureThy.have_thmss name (more_atts @ [Drule.tag_lemma]));
   1.121 +fun local_have_thmss x =
   1.122 +  gen_have_thmss (ProofContext.get_thms o Proof.context_of)
   1.123 +    (Attrib.local_attribute o Proof.theory_of) x;
   1.124 +
   1.125 +fun have_thmss_i f ((name, more_atts), th_atts) =
   1.126 +  f name more_atts (map (apfst single) th_atts);
   1.127 +
   1.128 +fun have_lemss name atts = PureThy.have_thmss name (atts @ [Drule.tag_lemma]);
   1.129  
   1.130  
   1.131 -val have_thmss =
   1.132 -  gen_have_thmss (ProofContext.get_thms o Proof.context_of)
   1.133 -    (Attrib.local_attribute o Proof.theory_of) Proof.have_thmss;
   1.134 +fun apply_theorems th_srcs = global_have_thmss PureThy.have_thmss ((None, []), th_srcs);
   1.135 +fun apply_theorems_i th_srcs = have_thmss_i PureThy.have_thmss ((None, []), th_srcs);
   1.136 +val have_theorems = #1 oo global_have_thmss (PureThy.have_thmss o Some);
   1.137 +val have_theorems_i = #1 oo have_thmss_i (PureThy.have_thmss o Some);
   1.138 +val have_lemmas = #1 oo global_have_thmss (have_lemss o Some);
   1.139 +val have_lemmas_i = #1 oo have_thmss_i (have_lemss o Some);
   1.140 +val have_facts = ProofHistory.apply o local_have_thmss Proof.have_thmss;
   1.141 +val have_facts_i = ProofHistory.apply o have_thmss_i Proof.have_thmss;
   1.142 +
   1.143  
   1.144 -val have_facts = ProofHistory.apply o have_thmss;
   1.145 -val from_facts = ProofHistory.apply o (Proof.chain oo curry have_thmss ("", []));
   1.146 +(* forward chaining *)
   1.147 +
   1.148 +val from_facts =
   1.149 +  ProofHistory.apply o (Proof.chain oo curry (local_have_thmss Proof.have_thmss) ("", []));
   1.150 +
   1.151 +val from_facts_i =
   1.152 +  ProofHistory.apply o (Proof.chain oo curry (have_thmss_i Proof.have_thmss) ("", []));
   1.153 +
   1.154 +val chain = ProofHistory.apply Proof.chain;
   1.155  
   1.156  
   1.157  (* context *)
   1.158  
   1.159  val fix = ProofHistory.apply o Proof.fix;
   1.160 -
   1.161 +val fix_i = ProofHistory.apply o Proof.fix_i;
   1.162  val match_bind = ProofHistory.apply o Proof.match_bind;
   1.163 +val match_bind_i = ProofHistory.apply o Proof.match_bind_i;
   1.164  
   1.165  
   1.166  (* statements *)
   1.167  
   1.168 -fun global_statement f name tags s thy =
   1.169 -  ProofHistory.init (f name (map (Attrib.global_attribute thy) tags) s thy);
   1.170 +fun global_statement f name src s thy =
   1.171 +  ProofHistory.init (f name (map (Attrib.global_attribute thy) src) s thy);
   1.172  
   1.173 -fun local_statement f name tags s = ProofHistory.apply_open (fn state =>
   1.174 -  f name (map (Attrib.local_attribute (Proof.theory_of state)) tags) s state);
   1.175 +fun local_statement do_open f name src s = ProofHistory.apply_cond_open do_open (fn state =>
   1.176 +  f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s state);
   1.177 +
   1.178 +fun global_statement_i f name atts t thy = ProofHistory.init (f name atts t thy);
   1.179 +fun local_statement_i do_open f name atts t = ProofHistory.apply_cond_open do_open (f name atts t);
   1.180  
   1.181  val theorem = global_statement Proof.theorem;
   1.182 +val theorem_i = global_statement_i Proof.theorem_i;
   1.183  val lemma = global_statement Proof.lemma;
   1.184 -val assume = local_statement Proof.assume;
   1.185 -val show = local_statement Proof.show;
   1.186 -val have = local_statement Proof.have;
   1.187 -
   1.188 -
   1.189 -(* forward chaining *)
   1.190 -
   1.191 -val chain = ProofHistory.apply Proof.chain;
   1.192 +val lemma_i = global_statement_i Proof.lemma_i;
   1.193 +val assume = local_statement false Proof.assume;
   1.194 +val assume_i = local_statement_i false Proof.assume_i;
   1.195 +val show = local_statement true Proof.show;
   1.196 +val show_i = local_statement_i true Proof.show_i;
   1.197 +val have = local_statement true Proof.have;
   1.198 +val have_i = local_statement_i true Proof.have_i;
   1.199  
   1.200  
   1.201  (* end proof *)
   1.202  
   1.203 -fun qed_with (alt_name, alt_tags) prf =
   1.204 +fun gen_qed_with prep_att (alt_name, raw_atts) prf =
   1.205    let
   1.206      val state = ProofHistory.current prf;
   1.207      val thy = Proof.theory_of state;
   1.208 -    val alt_atts = apsome (map (Attrib.global_attribute thy)) alt_tags;
   1.209 +    val alt_atts = apsome (map (prep_att thy)) raw_atts;
   1.210      val (thy', (kind, name, thm)) = Method.qed alt_name alt_atts state;
   1.211  
   1.212      val prt_result = Pretty.block
   1.213        [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm thm];
   1.214    in Pretty.writeln prt_result; thy end;
   1.215  
   1.216 +val qed_with = gen_qed_with Attrib.global_attribute;
   1.217 +val qed_with_i = gen_qed_with (K I);
   1.218 +
   1.219  val qed = qed_with (None, None);
   1.220  
   1.221  val kill_proof = Proof.theory_of o ProofHistory.current;
   1.222 @@ -168,10 +231,14 @@
   1.223  (* backward steps *)
   1.224  
   1.225  val tac = ProofHistory.applys o Method.tac;
   1.226 +val tac_i = tac o Method.Basic;
   1.227  val then_tac = ProofHistory.applys o Method.then_tac;
   1.228 +val then_tac_i = then_tac o Method.Basic;
   1.229  val proof = ProofHistory.applys o Method.proof;
   1.230 +val proof_i = proof o apsome Method.Basic;
   1.231  val end_block = ProofHistory.applys_close Method.end_block;
   1.232  val terminal_proof = ProofHistory.applys_close o Method.terminal_proof;
   1.233 +val terminal_proof_i = terminal_proof o Method.Basic;
   1.234  val immediate_proof = ProofHistory.applys_close Method.immediate_proof;
   1.235  val default_proof = ProofHistory.applys_close Method.default_proof;
   1.236  
   1.237 @@ -226,7 +293,7 @@
   1.238      ("(" ^ quote name ^ ", " ^ txt ^ ")");
   1.239  
   1.240  
   1.241 -(* theory init and exit *)	(* FIXME move? rearrange? *)
   1.242 +(* theory init and exit *)      (* FIXME move? rearrange? *)
   1.243  
   1.244  fun begin_theory name parents files =
   1.245    let