src/Provers/quantifier1.ML
 changeset 42456 13b4b6ba3593 parent 42361 23f352990944 child 42457 de868abd131e
```     1.1 --- a/src/Provers/quantifier1.ML	Fri Apr 22 13:58:13 2011 +0200
1.2 +++ b/src/Provers/quantifier1.ML	Fri Apr 22 14:30:32 2011 +0200
1.3 @@ -66,11 +66,11 @@
1.4  sig
1.5    val prove_one_point_all_tac: tactic
1.6    val prove_one_point_ex_tac: tactic
1.7 -  val rearrange_all: theory -> simpset -> term -> thm option
1.8 -  val rearrange_ex:  theory -> simpset -> term -> thm option
1.9 -  val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option
1.10 -  val rearrange_bex:  (simpset -> tactic) -> theory -> simpset -> term -> thm option
1.11 -  val rearrange_Coll: tactic -> theory -> simpset -> term -> thm option
1.12 +  val rearrange_all: simpset -> term -> thm option
1.13 +  val rearrange_ex: simpset -> term -> thm option
1.14 +  val rearrange_ball: tactic -> simpset -> term -> thm option
1.15 +  val rearrange_bex: tactic -> simpset -> term -> thm option
1.16 +  val rearrange_Collect: tactic -> simpset -> term -> thm option
1.17  end;
1.18
1.19  functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
1.20 @@ -112,14 +112,14 @@
1.21          | exqu xs P = extract (null xs) xs P
1.22    in exqu [] end;
1.23
1.24 -fun prove_conv tac thy tu =
1.25 -  let val ctxt = Proof_Context.init_global thy;
1.26 -      val eq_tu = Logic.mk_equals tu;
1.27 -      val ([fixed_goal], ctxt') = Variable.import_terms true [eq_tu] ctxt;
1.28 -      val thm = Goal.prove ctxt' [] [] fixed_goal
1.29 -            (K (rtac iff_reflection 1 THEN tac));
1.30 -      val [gen_thm] = Variable.export ctxt' ctxt [thm];
1.31 -  in gen_thm end;
1.32 +fun prove_conv tac ss tu =
1.33 +  let
1.34 +    val ctxt = Simplifier.the_context ss;
1.35 +    val (goal, ctxt') =
1.36 +      yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt;
1.37 +    val thm =
1.38 +      Goal.prove ctxt' [] [] goal (K (rtac iff_reflection 1 THEN tac));
1.39 +  in singleton (Variable.export ctxt' ctxt) thm end;
1.40
1.41  fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i)
1.42
1.43 @@ -160,42 +160,42 @@
1.44        val Q = if n=0 then P else renumber 0 n P
1.45    in quant xs (qC \$ Abs(x,T,Q)) end;
1.46
1.47 -fun rearrange_all thy _ (F as (all as Const(q,_)) \$ Abs(x,T, P)) =
1.48 +fun rearrange_all ss (F as (all as Const(q,_)) \$ Abs(x,T, P)) =
1.49       (case extract_quant extract_imp q P of
1.50          NONE => NONE
1.51        | SOME(xs,eq,Q) =>
1.52            let val R = quantify all x T xs (imp \$ eq \$ Q)
1.53 -          in SOME(prove_conv prove_one_point_all_tac thy (F,R)) end)
1.54 -  | rearrange_all _ _ _ = NONE;
1.55 +          in SOME (prove_conv prove_one_point_all_tac ss (F,R)) end)
1.56 +  | rearrange_all _ _ = NONE;
1.57
1.58 -fun rearrange_ball tac thy ss (F as Ball \$ A \$ Abs(x,T,P)) =
1.59 +fun rearrange_ball tac ss (F as Ball \$ A \$ Abs(x,T,P)) =
1.60       (case extract_imp true [] P of
1.61          NONE => NONE
1.62        | SOME(xs,eq,Q) => if not(null xs) then NONE else
1.63            let val R = imp \$ eq \$ Q
1.64 -          in SOME(prove_conv (tac ss) thy (F,Ball \$ A \$ Abs(x,T,R))) end)
1.65 -  | rearrange_ball _ _ _ _ = NONE;
1.66 +          in SOME (prove_conv tac ss (F,Ball \$ A \$ Abs(x,T,R))) end)
1.67 +  | rearrange_ball _ _ _ = NONE;
1.68
1.69 -fun rearrange_ex thy _ (F as (ex as Const(q,_)) \$ Abs(x,T,P)) =
1.70 +fun rearrange_ex ss (F as (ex as Const(q,_)) \$ Abs(x,T,P)) =
1.71       (case extract_quant extract_conj q P of
1.72          NONE => NONE
1.73        | SOME(xs,eq,Q) =>
1.74            let val R = quantify ex x T xs (conj \$ eq \$ Q)
1.75 -          in SOME(prove_conv prove_one_point_ex_tac thy (F,R)) end)
1.76 -  | rearrange_ex _ _ _ = NONE;
1.77 +          in SOME(prove_conv prove_one_point_ex_tac ss (F,R)) end)
1.78 +  | rearrange_ex _ _ = NONE;
1.79
1.80 -fun rearrange_bex tac thy ss (F as Bex \$ A \$ Abs(x,T,P)) =
1.81 +fun rearrange_bex tac ss (F as Bex \$ A \$ Abs(x,T,P)) =
1.82       (case extract_conj true [] P of
1.83          NONE => NONE
1.84        | SOME(xs,eq,Q) => if not(null xs) then NONE else
1.85 -          SOME(prove_conv (tac ss) thy (F,Bex \$ A \$ Abs(x,T,conj\$eq\$Q))))
1.86 -  | rearrange_bex _ _ _ _ = NONE;
1.87 +          SOME(prove_conv tac ss (F,Bex \$ A \$ Abs(x,T,conj\$eq\$Q))))
1.88 +  | rearrange_bex _ _ _ = NONE;
1.89
1.90 -fun rearrange_Coll tac thy _ (F as Coll \$ Abs(x,T,P)) =
1.91 +fun rearrange_Collect tac ss (F as Coll \$ Abs(x,T,P)) =
1.92       (case extract_conj true [] P of
1.93          NONE => NONE
1.94        | SOME(_,eq,Q) =>
1.95            let val R = Coll \$ Abs(x,T, conj \$ eq \$ Q)
1.96 -          in SOME(prove_conv tac thy (F,R)) end);
1.97 +          in SOME(prove_conv tac ss (F,R)) end);
1.98
1.99  end;
```