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;