src/Pure/Isar/isar_thy.ML
author wenzelm
Sat Jan 21 23:02:14 2006 +0100 (2006-01-21)
changeset 18728 6790126ab5f6
parent 18678 dd0c569fa43d
child 18804 d42708f5c186
permissions -rw-r--r--
simplified type attribute;
     1 (*  Title:      Pure/Isar/isar_thy.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Derived theory and proof operations.
     6 *)
     7 
     8 signature ISAR_THY =
     9 sig
    10   val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
    11   val add_axioms_i: ((bstring * term) * attribute list) list -> theory -> theory
    12   val add_defs: bool * ((bstring * string) * Attrib.src list) list -> theory -> theory
    13   val add_defs_i: bool * ((bstring * term) * attribute list) list -> theory -> theory
    14   val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory
    15   val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory
    16   val theorems: string ->
    17     ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
    18     -> theory -> (string * thm list) list * theory 
    19   val theorems_i: string ->
    20     ((bstring * attribute list) * (thm list * attribute list) list) list
    21     -> theory -> (string * thm list) list * theory
    22   val smart_theorems: string -> xstring option ->
    23     ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
    24     theory -> theory * Proof.context
    25   val declare_theorems: xstring option ->
    26     (thmref * Attrib.src list) list -> theory -> theory * Proof.context
    27   val have: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    28     bool -> Proof.state -> Proof.state
    29   val hence: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    30     bool -> Proof.state -> Proof.state
    31   val show: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    32     bool -> Proof.state -> Proof.state
    33   val thus: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    34     bool -> Proof.state -> Proof.state
    35   val theorem: string -> string * Attrib.src list -> string * (string list * string list) ->
    36     theory -> Proof.state
    37   val theorem_i: string -> string * attribute list -> term * (term list * term list) ->
    38     theory -> Proof.state
    39   val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
    40   val terminal_proof: Method.text * Method.text option ->
    41     Toplevel.transition -> Toplevel.transition
    42   val default_proof: Toplevel.transition -> Toplevel.transition
    43   val immediate_proof: Toplevel.transition -> Toplevel.transition
    44   val done_proof: Toplevel.transition -> Toplevel.transition
    45   val skip_proof: Toplevel.transition -> Toplevel.transition
    46   val begin_theory: string -> string list -> (string * bool) list -> bool -> theory
    47   val end_theory: theory -> theory
    48   val kill_theory: string -> unit
    49   val theory: string * string list * (string * bool) list
    50     -> Toplevel.transition -> Toplevel.transition
    51   val init_context: ('a -> unit) -> 'a -> Toplevel.transition -> Toplevel.transition
    52   val context: string -> Toplevel.transition -> Toplevel.transition
    53 end;
    54 
    55 structure IsarThy: ISAR_THY =
    56 struct
    57 
    58 (* axioms and defs *)
    59 
    60 fun add_axms f args thy =
    61   f (map (fn (x, srcs) => (x, map (Attrib.attribute thy) srcs)) args) thy;
    62 
    63 val add_axioms = add_axms (snd oo PureThy.add_axioms);
    64 val add_axioms_i = snd oo PureThy.add_axioms_i;
    65 fun add_defs (x, args) = add_axms (snd oo PureThy.add_defs x) args;
    66 fun add_defs_i (x, args) = (snd oo PureThy.add_defs_i x) args;
    67 
    68 
    69 (* theorems *)
    70 
    71 fun present_theorems kind (named_thmss, thy) =
    72   conditional (kind <> "" andalso kind <> Drule.internalK) (fn () =>
    73     Context.setmp (SOME thy) (Present.results (kind ^ "s")) named_thmss);
    74 
    75 fun theorems kind args thy = thy
    76   |> PureThy.note_thmss (Drule.kind kind) (Attrib.map_facts (Attrib.attribute thy) args)
    77   |> tap (present_theorems kind);
    78 
    79 fun theorems_i kind args =
    80   PureThy.note_thmss_i (Drule.kind kind) args
    81   #> tap (present_theorems kind);
    82 
    83 fun apply_theorems args = apfst (List.concat o map snd) o theorems "" [(("", []), args)];
    84 fun apply_theorems_i args = apfst (List.concat o map snd) o theorems_i "" [(("", []), args)];
    85 
    86 fun smart_theorems kind NONE args thy = thy
    87       |> theorems kind args
    88       |> tap (present_theorems kind)
    89       |> (fn (_, thy) => (thy, ProofContext.init thy))
    90   | smart_theorems kind (SOME loc) args thy = thy
    91       |> Locale.note_thmss kind loc args
    92       |> tap (present_theorems kind o apsnd fst)
    93       |> #2;
    94 
    95 fun declare_theorems opt_loc args =
    96   smart_theorems "" opt_loc [(("", []), args)];
    97 
    98 
    99 (* goals *)
   100 
   101 local
   102 
   103 fun local_goal opt_chain goal stmt int =
   104   opt_chain #> goal NONE (K Seq.single) stmt int;
   105 
   106 fun global_goal goal kind a propp thy =
   107   goal kind NONE (K I) (SOME "") a [(("", []), [propp])] (ProofContext.init thy);
   108 
   109 in
   110 
   111 val have = local_goal I Proof.have;
   112 val hence = local_goal Proof.chain Proof.have;
   113 val show = local_goal I Proof.show;
   114 val thus = local_goal Proof.chain Proof.show;
   115 val theorem = global_goal Proof.theorem;
   116 val theorem_i = global_goal Proof.theorem_i;
   117 
   118 end;
   119 
   120 
   121 (* local endings *)
   122 
   123 fun local_qed m = Toplevel.proofs (Proof.local_qed (m, true));
   124 val local_terminal_proof = Toplevel.proofs o Proof.local_terminal_proof;
   125 val local_default_proof = Toplevel.proofs Proof.local_default_proof;
   126 val local_immediate_proof = Toplevel.proofs Proof.local_immediate_proof;
   127 val local_done_proof = Toplevel.proofs Proof.local_done_proof;
   128 val local_skip_proof = Toplevel.proofs' Proof.local_skip_proof;
   129 
   130 val skip_local_qed =
   131   Toplevel.skip_proof (History.apply (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF));
   132 
   133 
   134 (* global endings *)
   135 
   136 fun global_ending ending = Toplevel.proof_to_theory_context (fn int => fn state =>
   137   if can (Proof.assert_bottom true) state then ending int state
   138   else raise Toplevel.UNDEF);
   139 
   140 fun global_qed m = global_ending (K (Proof.global_qed (m, true)));
   141 val global_terminal_proof = global_ending o K o Proof.global_terminal_proof;
   142 val global_default_proof = global_ending (K Proof.global_default_proof);
   143 val global_immediate_proof = global_ending (K Proof.global_immediate_proof);
   144 val global_skip_proof = global_ending Proof.global_skip_proof;
   145 val global_done_proof = global_ending (K Proof.global_done_proof);
   146 
   147 val skip_global_qed = Toplevel.skip_proof_to_theory (equal 1);
   148 
   149 
   150 (* common endings *)
   151 
   152 fun qed m = local_qed m o global_qed m o skip_local_qed o skip_global_qed;
   153 fun terminal_proof m = local_terminal_proof m o global_terminal_proof m;
   154 val default_proof = local_default_proof o global_default_proof;
   155 val immediate_proof = local_immediate_proof o global_immediate_proof;
   156 val done_proof = local_done_proof o global_done_proof;
   157 val skip_proof = local_skip_proof o global_skip_proof;
   158 
   159 
   160 (* theory init and exit *)
   161 
   162 fun begin_theory name imports uses =
   163   ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.unpack) uses);
   164 
   165 val end_theory = (ThyInfo.check_known_thy o Context.theory_name) ? ThyInfo.end_theory;
   166 
   167 val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy;
   168 
   169 fun theory (name, imports, uses) =
   170   Toplevel.init_theory (begin_theory name imports uses)
   171     (fn thy => (end_theory thy; ()))
   172     (kill_theory o Context.theory_name);
   173 
   174 
   175 (* context switch *)
   176 
   177 fun fetch_context f x =
   178   (case Context.pass NONE f x of
   179     ((), NONE) => raise Toplevel.UNDEF
   180   | ((), SOME thy) => thy);
   181 
   182 fun init_context f x = Toplevel.init_theory (fn _ => fetch_context f x) (K ()) (K ());
   183 
   184 val context = init_context (ThyInfo.quiet_update_thy true);
   185 
   186 end;