added with_facts(_i);
authorwenzelm
Thu Jul 01 21:27:46 1999 +0200 (1999-07-01 ago)
changeset 687970f8c0c34b8d
parent 6878 1e97e7fbcca5
child 6880 ce2b19e4402d
added with_facts(_i);
also, finally: opt_rules;
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Jul 01 21:27:04 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Jul 01 21:27:46 1999 +0200
     1.3 @@ -62,6 +62,9 @@
     1.4    val from_facts: (string * Args.src list) list * Comment.text -> ProofHistory.T -> ProofHistory.T
     1.5    val from_facts_i: (thm * Proof.context attribute list) list * Comment.text
     1.6      -> ProofHistory.T -> ProofHistory.T
     1.7 +  val with_facts: (string * Args.src list) list * Comment.text -> ProofHistory.T -> ProofHistory.T
     1.8 +  val with_facts_i: (thm * Proof.context attribute list) list * Comment.text
     1.9 +    -> ProofHistory.T -> ProofHistory.T
    1.10    val chain: Comment.text -> ProofHistory.T -> ProofHistory.T
    1.11    val fix: (string * string option) list * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.12    val fix_i: (string * typ) list * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.13 @@ -117,8 +120,14 @@
    1.14    val terminal_proof: Method.text * Comment.interest -> Toplevel.transition -> Toplevel.transition
    1.15    val immediate_proof: Toplevel.transition -> Toplevel.transition
    1.16    val default_proof: Toplevel.transition -> Toplevel.transition
    1.17 -  val also: Comment.text -> Toplevel.transition -> Toplevel.transition
    1.18 -  val finally: Comment.text -> Toplevel.transition -> Toplevel.transition
    1.19 +  val also: ((string * Args.src list) list * Comment.interest) option * Comment.text
    1.20 +    -> Toplevel.transition -> Toplevel.transition
    1.21 +  val also_i: (thm list * Comment.interest) option * Comment.text
    1.22 +    -> Toplevel.transition -> Toplevel.transition
    1.23 +  val finally: ((string * Args.src list) list * Comment.interest) option * Comment.text
    1.24 +    -> Toplevel.transition -> Toplevel.transition
    1.25 +  val finally_i: (thm list * Comment.interest) option * Comment.text
    1.26 +    -> Toplevel.transition -> Toplevel.transition
    1.27    val use_mltext: string -> theory option -> theory option
    1.28    val use_mltext_theory: string -> theory -> theory
    1.29    val use_setup: string -> theory -> theory
    1.30 @@ -223,16 +232,22 @@
    1.31  val have_theorems_i = #1 oo (have_thmss_i (PureThy.have_thmss o Some) o Comment.ignore);
    1.32  val have_lemmas = #1 oo (global_have_thmss (have_lemss o Some) o Comment.ignore);
    1.33  val have_lemmas_i = #1 oo (have_thmss_i (have_lemss o Some) o Comment.ignore);
    1.34 -val have_facts = ProofHistory.apply o local_have_thmss Proof.have_thmss o Comment.ignore;
    1.35 -val have_facts_i = ProofHistory.apply o have_thmss_i Proof.have_thmss o Comment.ignore;
    1.36 +val have_facts = ProofHistory.apply o local_have_thmss (Proof.have_thmss []) o Comment.ignore;
    1.37 +val have_facts_i = ProofHistory.apply o have_thmss_i (Proof.have_thmss []) o Comment.ignore;
    1.38  
    1.39  
    1.40  (* forward chaining *)
    1.41  
    1.42 -fun gen_from_facts f = ProofHistory.apply o (Proof.chain oo curry (f Proof.have_thmss) ("", []));
    1.43 +fun gen_from_facts f = ProofHistory.apply o (Proof.chain oo curry f ("", []));
    1.44 +
    1.45 +fun add_thmss name atts ths_atts state =
    1.46 +  Proof.have_thmss (Proof.the_facts state) name atts ths_atts state;
    1.47  
    1.48 -val from_facts = gen_from_facts local_have_thmss o Comment.ignore;
    1.49 -val from_facts_i = gen_from_facts have_thmss_i o Comment.ignore;
    1.50 +val from_facts = gen_from_facts (local_have_thmss (Proof.have_thmss [])) o Comment.ignore;
    1.51 +val from_facts_i = gen_from_facts (have_thmss_i (Proof.have_thmss [])) o Comment.ignore;
    1.52 +val with_facts = gen_from_facts (local_have_thmss add_thmss) o Comment.ignore;
    1.53 +val with_facts_i = gen_from_facts (have_thmss_i add_thmss) o Comment.ignore;
    1.54 +
    1.55  fun chain comment_ignore = ProofHistory.apply Proof.chain;
    1.56  
    1.57  
    1.58 @@ -352,14 +367,28 @@
    1.59  
    1.60  (* calculational proof commands *)
    1.61  
    1.62 +local
    1.63 +
    1.64  fun cond_print_calc int thm =
    1.65    if int then Pretty.writeln (Pretty.big_list "calculation:" [Display.pretty_thm thm])
    1.66    else ();
    1.67  
    1.68  fun proof''' f = Toplevel.proof' (f o cond_print_calc);
    1.69  
    1.70 -fun also _ = proof''' (ProofHistory.applys o Calculation.also);
    1.71 -fun finally _ = proof''' (ProofHistory.applys o Calculation.finally);
    1.72 +fun get_thmss srcs = Proof.the_facts o local_have_thmss (Proof.have_thmss []) (("", []), srcs); 
    1.73 +fun get_thmss_i thms _ = thms;
    1.74 +
    1.75 +fun gen_calc get f (args, _) prt state =
    1.76 +  f (apsome (fn (srcs, _) => get srcs state) args) prt state;
    1.77 +
    1.78 +in
    1.79 +
    1.80 +fun also x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.also x);
    1.81 +fun also_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.also x);
    1.82 +fun finally x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.finally x);
    1.83 +fun finally_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.finally x);
    1.84 +
    1.85 +end;
    1.86  
    1.87  
    1.88  (* use ML text *)