src/Pure/Isar/isar_thy.ML
changeset 5830 95b619c7289b
child 5882 c8096461f5c8
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Mon Nov 09 15:34:23 1998 +0100
     1.3 @@ -0,0 +1,218 @@
     1.4 +(*  Title:      Pure/Isar/isar_thy.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Derived theory operations.
     1.9 +
    1.10 +TODO:
    1.11 +  - add_defs: handle empty name (pure_thy.ML (!?));
    1.12 +  - add_constdefs (atomic!);
    1.13 +  - have_theorems, have_lemmas;
    1.14 +  - load theory;
    1.15 +  - 'methods' section (proof macros, ML method defs) (!?);
    1.16 +  - now_block: ProofHistory open / close (!?);
    1.17 +  - from_facts: attribs, args (!?) (beware of termination!!);
    1.18 +*)
    1.19 +
    1.20 +signature ISAR_THY =
    1.21 +sig
    1.22 +  val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory
    1.23 +  val add_defs: ((bstring * string) * Args.src list) list -> theory -> theory
    1.24 +  val fix: (string * string option) list -> ProofHistory.T -> ProofHistory.T
    1.25 +  val match_bind: (string * string) list -> ProofHistory.T -> ProofHistory.T
    1.26 +  val theorem: string -> Args.src list -> string -> theory -> ProofHistory.T
    1.27 +  val lemma: string -> Args.src list -> string -> theory -> ProofHistory.T
    1.28 +  val assume: string -> Args.src list -> string list -> ProofHistory.T -> ProofHistory.T
    1.29 +  val show: string -> Args.src list -> string -> ProofHistory.T -> ProofHistory.T
    1.30 +  val have: string -> Args.src list -> string -> ProofHistory.T -> ProofHistory.T
    1.31 +  val chain: ProofHistory.T -> ProofHistory.T
    1.32 +  val from_facts: string list -> ProofHistory.T -> ProofHistory.T
    1.33 +  val begin_block: ProofHistory.T -> ProofHistory.T
    1.34 +  val next_block: ProofHistory.T -> ProofHistory.T
    1.35 +  val end_block: ProofHistory.T -> ProofHistory.T
    1.36 +  val qed_with: bstring option * Args.src list option -> ProofHistory.T -> theory
    1.37 +  val qed: ProofHistory.T -> theory
    1.38 +  val kill_proof: ProofHistory.T -> theory
    1.39 +  val tac: Method.text -> ProofHistory.T -> ProofHistory.T
    1.40 +  val etac: Method.text -> ProofHistory.T -> ProofHistory.T
    1.41 +  val proof: Method.text option -> ProofHistory.T -> ProofHistory.T
    1.42 +  val terminal_proof: Method.text -> ProofHistory.T -> ProofHistory.T
    1.43 +  val trivial_proof: ProofHistory.T -> ProofHistory.T
    1.44 +  val default_proof: ProofHistory.T -> ProofHistory.T
    1.45 +  val use_mltext: string -> theory option -> theory option
    1.46 +  val use_mltext_theory: string -> theory -> theory
    1.47 +  val use_setup: string -> theory -> theory
    1.48 +  val parse_ast_translation: string -> theory -> theory
    1.49 +  val parse_translation: string -> theory -> theory
    1.50 +  val print_translation: string -> theory -> theory
    1.51 +  val typed_print_translation: string -> theory -> theory
    1.52 +  val print_ast_translation: string -> theory -> theory
    1.53 +  val token_translation: string -> theory -> theory
    1.54 +  val add_oracle: bstring * string -> theory -> theory
    1.55 +  val the_theory: string -> unit -> theory
    1.56 +  val begin_theory: string * string list -> unit -> theory
    1.57 +  val end_theory: theory -> unit
    1.58 +end;
    1.59 +
    1.60 +structure IsarThy: ISAR_THY =
    1.61 +struct
    1.62 +
    1.63 +
    1.64 +(** derived theory and proof operations **)
    1.65 +
    1.66 +(* axioms and defs *)
    1.67 +
    1.68 +fun attributize thy (x, srcs) = (x, map (Attrib.global_attribute thy) srcs);
    1.69 +
    1.70 +fun add_axioms axms thy = PureThy.add_axioms (map (attributize thy) axms) thy;
    1.71 +fun add_defs defs thy = PureThy.add_defs (map (attributize thy) defs) thy;
    1.72 +
    1.73 +
    1.74 +(* context *)
    1.75 +
    1.76 +val fix = ProofHistory.apply o Proof.fix;
    1.77 +
    1.78 +val match_bind = ProofHistory.apply o Proof.match_bind;
    1.79 +
    1.80 +
    1.81 +(* statements *)
    1.82 +
    1.83 +fun global_statement f name tags s thy =
    1.84 +  ProofHistory.init (f name (map (Attrib.global_attribute thy) tags) s thy);
    1.85 +
    1.86 +fun local_statement f name tags s = ProofHistory.apply_open (fn state =>
    1.87 +  f name (map (Attrib.local_attribute (Proof.theory_of state)) tags) s state);
    1.88 +
    1.89 +val theorem = global_statement Proof.theorem;
    1.90 +val lemma = global_statement Proof.lemma;
    1.91 +val assume = local_statement Proof.assume;
    1.92 +val show = local_statement Proof.show;
    1.93 +val have = local_statement Proof.have;
    1.94 +
    1.95 +
    1.96 +(* forward chaining *)
    1.97 +
    1.98 +val chain = ProofHistory.apply Proof.chain;
    1.99 +
   1.100 +fun from_facts names = ProofHistory.apply (fn state =>
   1.101 +  state
   1.102 +  |> Proof.from_facts (ProofContext.get_tthmss (Proof.context_of state) names));
   1.103 +
   1.104 +
   1.105 +(* end proof *)
   1.106 +
   1.107 +fun qed_with (alt_name, alt_tags) prf =
   1.108 +  let
   1.109 +    val state = ProofHistory.current prf;
   1.110 +    val thy = Proof.theory_of state;
   1.111 +    val alt_atts = apsome (map (Attrib.global_attribute thy)) alt_tags;
   1.112 +    val (thy', (kind, name, tthm)) = Method.qed alt_name alt_atts state;
   1.113 +
   1.114 +    val prt_result = Pretty.block
   1.115 +      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Attribute.pretty_tthm tthm];
   1.116 +  in Pretty.writeln prt_result; thy end;
   1.117 +
   1.118 +val qed = qed_with (None, None);
   1.119 +
   1.120 +val kill_proof = Proof.theory_of o ProofHistory.current;
   1.121 +
   1.122 +
   1.123 +(* blocks *)
   1.124 +
   1.125 +val begin_block = ProofHistory.apply_open Proof.begin_block;
   1.126 +val next_block = ProofHistory.apply Proof.next_block;
   1.127 +
   1.128 +
   1.129 +(* backward steps *)
   1.130 +
   1.131 +val tac = ProofHistory.applys o Method.tac;
   1.132 +val etac = ProofHistory.applys o Method.etac;
   1.133 +val proof = ProofHistory.applys o Method.proof;
   1.134 +val end_block = ProofHistory.applys_close Method.end_block;
   1.135 +val terminal_proof = ProofHistory.applys_close o Method.terminal_proof;
   1.136 +val trivial_proof = ProofHistory.applys_close Method.trivial_proof;
   1.137 +val default_proof = ProofHistory.applys_close Method.default_proof;
   1.138 +
   1.139 +
   1.140 +(* use ML text *)
   1.141 +
   1.142 +fun use_mltext txt opt_thy =
   1.143 +  let
   1.144 +    val save_context = Context.get_context ();
   1.145 +    val _ = Context.set_context opt_thy;
   1.146 +    val opt_exn = (transform_error (use_text false) txt; None) handle exn => Some exn;
   1.147 +    val opt_thy' = Context.get_context ();
   1.148 +  in
   1.149 +    Context.set_context save_context;
   1.150 +    (case opt_exn of
   1.151 +      None => opt_thy'
   1.152 +    | Some exn => raise exn)
   1.153 +  end;
   1.154 +
   1.155 +fun use_mltext_theory txt thy =
   1.156 +  (case use_mltext txt (Some thy) of
   1.157 +    Some thy' => thy'
   1.158 +  | None => error "Missing result ML theory context");
   1.159 +
   1.160 +
   1.161 +fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");");
   1.162 +
   1.163 +fun use_let name body txt =
   1.164 +  use_context ("let val " ^ name ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
   1.165 +
   1.166 +val use_setup =
   1.167 +  use_let "setup: (theory -> theory) list" "Theory.apply setup";
   1.168 +
   1.169 +
   1.170 +(* translation functions *)
   1.171 +
   1.172 +val parse_ast_translation =
   1.173 +  use_let "parse_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
   1.174 +    "Theory.add_trfuns (parse_ast_translation, [], [], [])";
   1.175 +
   1.176 +val parse_translation =
   1.177 +  use_let "parse_translation: (string * (term list -> term)) list"
   1.178 +    "Theory.add_trfuns ([], parse_translation, [], [])";
   1.179 +
   1.180 +val print_translation =
   1.181 +  use_let "print_translation: (string * (term list -> term)) list"
   1.182 +    "Theory.add_trfuns ([], [], print_translation, [])";
   1.183 +
   1.184 +val print_ast_translation =
   1.185 +  use_let "print_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
   1.186 +    "Theory.add_trfuns ([], [], [], print_ast_translation)";
   1.187 +
   1.188 +val typed_print_translation =
   1.189 +  use_let "typed_print_translation: (string * (bool -> typ -> term list -> term)) list"
   1.190 +    "Theory.add_trfunsT typed_print_translation";
   1.191 +
   1.192 +val token_translation =
   1.193 +  use_let "token_translation: (string * string * (string -> string * int)) list"
   1.194 +    "Theory.add_tokentrfuns token_translation";
   1.195 +
   1.196 +
   1.197 +(* add_oracle *)
   1.198 +
   1.199 +fun add_oracle (name, txt) =
   1.200 +  use_let
   1.201 +    "oracle: bstring * (Sign.sg * Object.T -> term)"
   1.202 +    "Theory.add_oracle oracle"
   1.203 +    ("(" ^ quote name ^ ", " ^ txt ^ ")");
   1.204 +
   1.205 +
   1.206 +(* theory init and exit *)
   1.207 +
   1.208 +fun the_theory name () = ThyInfo.theory name;
   1.209 +
   1.210 +fun begin_theory (name, names) () =
   1.211 +  PureThy.begin_theory name (map ThyInfo.theory names);
   1.212 +
   1.213 +
   1.214 +fun end_theory thy =
   1.215 +  let val thy' = PureThy.end_theory thy in
   1.216 +    transform_error ThyInfo.store_theory thy'
   1.217 +      handle exn => raise PureThy.ROLLBACK (thy', Some exn)     (* FIXME !!?? *)
   1.218 +  end;
   1.219 +
   1.220 +
   1.221 +end;