src/Provers/classical.ML
changeset 51703 f2e92fc0c8aa
parent 51688 27ecd33d3366
child 51717 9e7d1c139569
     1.1 --- a/src/Provers/classical.ML	Fri Apr 12 17:02:55 2013 +0200
     1.2 +++ b/src/Provers/classical.ML	Fri Apr 12 17:21:51 2013 +0200
     1.3 @@ -41,18 +41,18 @@
     1.4    val addSEs: Proof.context * thm list -> Proof.context
     1.5    val addSIs: Proof.context * thm list -> Proof.context
     1.6    val delrules: Proof.context * thm list -> Proof.context
     1.7 -  val addSWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
     1.8 -  val delSWrapper: claset *  string -> claset
     1.9 -  val addWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
    1.10 -  val delWrapper: claset *  string -> claset
    1.11 -  val addSbefore: claset * (string * (int -> tactic)) -> claset
    1.12 -  val addSafter: claset * (string * (int -> tactic)) -> claset
    1.13 -  val addbefore: claset * (string * (int -> tactic)) -> claset
    1.14 -  val addafter: claset * (string * (int -> tactic)) -> claset
    1.15 -  val addD2: claset * (string * thm) -> claset
    1.16 -  val addE2: claset * (string * thm) -> claset
    1.17 -  val addSD2: claset * (string * thm) -> claset
    1.18 -  val addSE2: claset * (string * thm) -> claset
    1.19 +  val addSWrapper: Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context
    1.20 +  val delSWrapper: Proof.context * string -> Proof.context
    1.21 +  val addWrapper: Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context
    1.22 +  val delWrapper: Proof.context * string -> Proof.context
    1.23 +  val addSbefore: Proof.context * (string * (int -> tactic)) -> Proof.context
    1.24 +  val addSafter: Proof.context * (string * (int -> tactic)) -> Proof.context
    1.25 +  val addbefore: Proof.context * (string * (int -> tactic)) -> Proof.context
    1.26 +  val addafter: Proof.context * (string * (int -> tactic)) -> Proof.context
    1.27 +  val addD2: Proof.context * (string * thm) -> Proof.context
    1.28 +  val addE2: Proof.context * (string * thm) -> Proof.context
    1.29 +  val addSD2: Proof.context * (string * thm) -> Proof.context
    1.30 +  val addSE2: Proof.context * (string * thm) -> Proof.context
    1.31    val appSWrappers: Proof.context -> wrapper
    1.32    val appWrappers: Proof.context -> wrapper
    1.33  
    1.34 @@ -60,6 +60,8 @@
    1.35    val map_claset: (claset -> claset) -> Proof.context -> Proof.context
    1.36    val put_claset: claset -> Proof.context -> Proof.context
    1.37  
    1.38 +  val map_theory_claset: (Proof.context -> Proof.context) -> theory -> theory
    1.39 +
    1.40    val fast_tac: Proof.context -> int -> tactic
    1.41    val slow_tac: Proof.context -> int -> tactic
    1.42    val astar_tac: Proof.context -> int -> tactic
    1.43 @@ -601,6 +603,12 @@
    1.44  val get_cs = Claset.get;
    1.45  val map_cs = Claset.map;
    1.46  
    1.47 +fun map_theory_claset f thy =
    1.48 +  let
    1.49 +    val ctxt' = f (Proof_Context.init_global thy);
    1.50 +    val thy' = Proof_Context.theory_of ctxt';
    1.51 +  in Context.theory_map (Claset.map (K (claset_of ctxt'))) thy' end;
    1.52 +
    1.53  fun map_claset f = Context.proof_map (map_cs f);
    1.54  fun put_claset cs = map_claset (K cs);
    1.55  
    1.56 @@ -646,33 +654,33 @@
    1.57    else (warning msg; xs);
    1.58  
    1.59  (*Add/replace a safe wrapper*)
    1.60 -fun cs addSWrapper new_swrapper =
    1.61 -  map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs;
    1.62 +fun ctxt addSWrapper new_swrapper = ctxt |> map_claset
    1.63 +  (map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper));
    1.64  
    1.65  (*Add/replace an unsafe wrapper*)
    1.66 -fun cs addWrapper new_uwrapper =
    1.67 -  map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs;
    1.68 +fun ctxt addWrapper new_uwrapper = ctxt |> map_claset
    1.69 +  (map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper));
    1.70  
    1.71  (*Remove a safe wrapper*)
    1.72 -fun cs delSWrapper name =
    1.73 -  map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
    1.74 +fun ctxt delSWrapper name = ctxt |> map_claset
    1.75 +  (map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name));
    1.76  
    1.77  (*Remove an unsafe wrapper*)
    1.78 -fun cs delWrapper name =
    1.79 -  map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
    1.80 +fun ctxt delWrapper name = ctxt |> map_claset
    1.81 +  (map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name));
    1.82  
    1.83  (* compose a safe tactic alternatively before/after safe_step_tac *)
    1.84 -fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2);
    1.85 -fun cs addSafter (name, tac2) = cs addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2);
    1.86 +fun ctxt addSbefore (name, tac1) = ctxt addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2);
    1.87 +fun ctxt addSafter (name, tac2) = ctxt addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2);
    1.88  
    1.89  (*compose a tactic alternatively before/after the step tactic *)
    1.90 -fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
    1.91 -fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
    1.92 +fun ctxt addbefore (name, tac1) = ctxt addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
    1.93 +fun ctxt addafter (name, tac2) = ctxt addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
    1.94  
    1.95 -fun cs addD2 (name, thm) = cs addafter (name, dtac thm THEN' assume_tac);
    1.96 -fun cs addE2 (name, thm) = cs addafter (name, etac thm THEN' assume_tac);
    1.97 -fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
    1.98 -fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
    1.99 +fun ctxt addD2 (name, thm) = ctxt addafter (name, dtac thm THEN' assume_tac);
   1.100 +fun ctxt addE2 (name, thm) = ctxt addafter (name, etac thm THEN' assume_tac);
   1.101 +fun ctxt addSD2 (name, thm) = ctxt addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
   1.102 +fun ctxt addSE2 (name, thm) = ctxt addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
   1.103  
   1.104  
   1.105