proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
authorwenzelm
Fri Apr 22 14:30:32 2011 +0200 (2011-04-22)
changeset 4245613b4b6ba3593
parent 42455 6702c984bf5a
child 42457 de868abd131e
proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
tuned signature;
src/FOL/FOL.thy
src/HOL/HOL.thy
src/HOL/Set.thy
src/Provers/quantifier1.ML
src/ZF/OrdQuant.thy
src/ZF/pair.thy
     1.1 --- a/src/FOL/FOL.thy	Fri Apr 22 13:58:13 2011 +0200
     1.2 +++ b/src/FOL/FOL.thy	Fri Apr 22 14:30:32 2011 +0200
     1.3 @@ -307,11 +307,11 @@
     1.4  use "simpdata.ML"
     1.5  
     1.6  simproc_setup defined_Ex ("EX x. P(x)") = {*
     1.7 -  fn _ => fn ss => fn ct => Quantifier1.rearrange_ex (theory_of_cterm ct) ss (term_of ct)
     1.8 +  fn _ => fn ss => Quantifier1.rearrange_ex ss o term_of
     1.9  *}
    1.10  
    1.11  simproc_setup defined_All ("ALL x. P(x)") = {*
    1.12 -  fn _ => fn ss => fn ct => Quantifier1.rearrange_all (theory_of_cterm ct) ss (term_of ct)
    1.13 +  fn _ => fn ss => Quantifier1.rearrange_all ss o term_of
    1.14  *}
    1.15  
    1.16  ML {*
     2.1 --- a/src/HOL/HOL.thy	Fri Apr 22 13:58:13 2011 +0200
     2.2 +++ b/src/HOL/HOL.thy	Fri Apr 22 14:30:32 2011 +0200
     2.3 @@ -1213,11 +1213,11 @@
     2.4  setup {* Simplifier.map_simpset (K HOL_basic_ss) *}
     2.5  
     2.6  simproc_setup defined_Ex ("EX x. P x") = {*
     2.7 -  fn _ => fn ss => fn ct => Quantifier1.rearrange_ex (theory_of_cterm ct) ss (term_of ct)
     2.8 +  fn _ => fn ss => Quantifier1.rearrange_ex ss o term_of
     2.9  *}
    2.10  
    2.11  simproc_setup defined_All ("ALL x. P x") = {*
    2.12 -  fn _ => fn ss => fn ct => Quantifier1.rearrange_all (theory_of_cterm ct) ss (term_of ct)
    2.13 +  fn _ => fn ss => Quantifier1.rearrange_all ss o term_of
    2.14  *}
    2.15  
    2.16  setup {*
     3.1 --- a/src/HOL/Set.thy	Fri Apr 22 13:58:13 2011 +0200
     3.2 +++ b/src/HOL/Set.thy	Fri Apr 22 14:30:32 2011 +0200
     3.3 @@ -77,13 +77,12 @@
     3.4  
     3.5  simproc_setup defined_Collect ("{x. P x & Q x}") = {*
     3.6    let
     3.7 -    val Coll_perm_tac =
     3.8 +    val Collect_perm_tac =
     3.9        rtac @{thm Collect_cong} 1 THEN
    3.10        rtac @{thm iffI} 1 THEN
    3.11        ALLGOALS (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]);
    3.12    in
    3.13 -    fn _ => fn ss => fn ct =>
    3.14 -      Quantifier1.rearrange_Coll Coll_perm_tac (theory_of_cterm ct) ss (term_of ct)
    3.15 +    fn _ => fn ss => Quantifier1.rearrange_Collect Collect_perm_tac ss o term_of
    3.16    end
    3.17  *}
    3.18  
    3.19 @@ -333,8 +332,7 @@
    3.20      val unfold_bex_tac = unfold_tac @{thms Bex_def};
    3.21      fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    3.22    in
    3.23 -    fn _ => fn ss => fn ct =>
    3.24 -      Quantifier1.rearrange_bex prove_bex_tac (theory_of_cterm ct) ss (term_of ct)
    3.25 +    fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss o term_of
    3.26    end
    3.27  *}
    3.28  
    3.29 @@ -343,8 +341,7 @@
    3.30      val unfold_ball_tac = unfold_tac @{thms Ball_def};
    3.31      fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    3.32    in
    3.33 -    fn _ => fn ss => fn ct =>
    3.34 -      Quantifier1.rearrange_ball prove_ball_tac (theory_of_cterm ct) ss (term_of ct)
    3.35 +    fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss o term_of
    3.36    end
    3.37  *}
    3.38  
     4.1 --- a/src/Provers/quantifier1.ML	Fri Apr 22 13:58:13 2011 +0200
     4.2 +++ b/src/Provers/quantifier1.ML	Fri Apr 22 14:30:32 2011 +0200
     4.3 @@ -66,11 +66,11 @@
     4.4  sig
     4.5    val prove_one_point_all_tac: tactic
     4.6    val prove_one_point_ex_tac: tactic
     4.7 -  val rearrange_all: theory -> simpset -> term -> thm option
     4.8 -  val rearrange_ex:  theory -> simpset -> term -> thm option
     4.9 -  val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option
    4.10 -  val rearrange_bex:  (simpset -> tactic) -> theory -> simpset -> term -> thm option
    4.11 -  val rearrange_Coll: tactic -> theory -> simpset -> term -> thm option
    4.12 +  val rearrange_all: simpset -> term -> thm option
    4.13 +  val rearrange_ex: simpset -> term -> thm option
    4.14 +  val rearrange_ball: tactic -> simpset -> term -> thm option
    4.15 +  val rearrange_bex: tactic -> simpset -> term -> thm option
    4.16 +  val rearrange_Collect: tactic -> simpset -> term -> thm option
    4.17  end;
    4.18  
    4.19  functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
    4.20 @@ -112,14 +112,14 @@
    4.21          | exqu xs P = extract (null xs) xs P
    4.22    in exqu [] end;
    4.23  
    4.24 -fun prove_conv tac thy tu =
    4.25 -  let val ctxt = Proof_Context.init_global thy;
    4.26 -      val eq_tu = Logic.mk_equals tu;
    4.27 -      val ([fixed_goal], ctxt') = Variable.import_terms true [eq_tu] ctxt;
    4.28 -      val thm = Goal.prove ctxt' [] [] fixed_goal
    4.29 -            (K (rtac iff_reflection 1 THEN tac));
    4.30 -      val [gen_thm] = Variable.export ctxt' ctxt [thm];
    4.31 -  in gen_thm end;
    4.32 +fun prove_conv tac ss tu =
    4.33 +  let
    4.34 +    val ctxt = Simplifier.the_context ss;
    4.35 +    val (goal, ctxt') =
    4.36 +      yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt;
    4.37 +    val thm =
    4.38 +      Goal.prove ctxt' [] [] goal (K (rtac iff_reflection 1 THEN tac));
    4.39 +  in singleton (Variable.export ctxt' ctxt) thm end;
    4.40  
    4.41  fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) 
    4.42  
    4.43 @@ -160,42 +160,42 @@
    4.44        val Q = if n=0 then P else renumber 0 n P
    4.45    in quant xs (qC $ Abs(x,T,Q)) end;
    4.46  
    4.47 -fun rearrange_all thy _ (F as (all as Const(q,_)) $ Abs(x,T, P)) =
    4.48 +fun rearrange_all ss (F as (all as Const(q,_)) $ Abs(x,T, P)) =
    4.49       (case extract_quant extract_imp q P of
    4.50          NONE => NONE
    4.51        | SOME(xs,eq,Q) =>
    4.52            let val R = quantify all x T xs (imp $ eq $ Q)
    4.53 -          in SOME(prove_conv prove_one_point_all_tac thy (F,R)) end)
    4.54 -  | rearrange_all _ _ _ = NONE;
    4.55 +          in SOME (prove_conv prove_one_point_all_tac ss (F,R)) end)
    4.56 +  | rearrange_all _ _ = NONE;
    4.57  
    4.58 -fun rearrange_ball tac thy ss (F as Ball $ A $ Abs(x,T,P)) =
    4.59 +fun rearrange_ball tac ss (F as Ball $ A $ Abs(x,T,P)) =
    4.60       (case extract_imp true [] P of
    4.61          NONE => NONE
    4.62        | SOME(xs,eq,Q) => if not(null xs) then NONE else
    4.63            let val R = imp $ eq $ Q
    4.64 -          in SOME(prove_conv (tac ss) thy (F,Ball $ A $ Abs(x,T,R))) end)
    4.65 -  | rearrange_ball _ _ _ _ = NONE;
    4.66 +          in SOME (prove_conv tac ss (F,Ball $ A $ Abs(x,T,R))) end)
    4.67 +  | rearrange_ball _ _ _ = NONE;
    4.68  
    4.69 -fun rearrange_ex thy _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
    4.70 +fun rearrange_ex ss (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
    4.71       (case extract_quant extract_conj q P of
    4.72          NONE => NONE
    4.73        | SOME(xs,eq,Q) =>
    4.74            let val R = quantify ex x T xs (conj $ eq $ Q)
    4.75 -          in SOME(prove_conv prove_one_point_ex_tac thy (F,R)) end)
    4.76 -  | rearrange_ex _ _ _ = NONE;
    4.77 +          in SOME(prove_conv prove_one_point_ex_tac ss (F,R)) end)
    4.78 +  | rearrange_ex _ _ = NONE;
    4.79  
    4.80 -fun rearrange_bex tac thy ss (F as Bex $ A $ Abs(x,T,P)) =
    4.81 +fun rearrange_bex tac ss (F as Bex $ A $ Abs(x,T,P)) =
    4.82       (case extract_conj true [] P of
    4.83          NONE => NONE
    4.84        | SOME(xs,eq,Q) => if not(null xs) then NONE else
    4.85 -          SOME(prove_conv (tac ss) thy (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
    4.86 -  | rearrange_bex _ _ _ _ = NONE;
    4.87 +          SOME(prove_conv tac ss (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
    4.88 +  | rearrange_bex _ _ _ = NONE;
    4.89  
    4.90 -fun rearrange_Coll tac thy _ (F as Coll $ Abs(x,T,P)) =
    4.91 +fun rearrange_Collect tac ss (F as Coll $ Abs(x,T,P)) =
    4.92       (case extract_conj true [] P of
    4.93          NONE => NONE
    4.94        | SOME(_,eq,Q) =>
    4.95            let val R = Coll $ Abs(x,T, conj $ eq $ Q)
    4.96 -          in SOME(prove_conv tac thy (F,R)) end);
    4.97 +          in SOME(prove_conv tac ss (F,R)) end);
    4.98  
    4.99  end;
     5.1 --- a/src/ZF/OrdQuant.thy	Fri Apr 22 13:58:13 2011 +0200
     5.2 +++ b/src/ZF/OrdQuant.thy	Fri Apr 22 14:30:32 2011 +0200
     5.3 @@ -373,8 +373,7 @@
     5.4      val unfold_rex_tac = unfold_tac @{thms rex_def};
     5.5      fun prove_rex_tac ss = unfold_rex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
     5.6    in
     5.7 -    fn _ => fn ss => fn ct =>
     5.8 -      Quantifier1.rearrange_bex prove_rex_tac (theory_of_cterm ct) ss (term_of ct)
     5.9 +    fn _ => fn ss => Quantifier1.rearrange_bex (prove_rex_tac ss) ss o term_of
    5.10    end
    5.11  *}
    5.12  
    5.13 @@ -383,8 +382,7 @@
    5.14      val unfold_rall_tac = unfold_tac @{thms rall_def};
    5.15      fun prove_rall_tac ss = unfold_rall_tac ss THEN Quantifier1.prove_one_point_all_tac;
    5.16    in
    5.17 -    fn _ => fn ss => fn ct =>
    5.18 -      Quantifier1.rearrange_ball prove_rall_tac (theory_of_cterm ct) ss (term_of ct)
    5.19 +    fn _ => fn ss => Quantifier1.rearrange_ball (prove_rall_tac ss) ss o term_of
    5.20    end
    5.21  *}
    5.22  
     6.1 --- a/src/ZF/pair.thy	Fri Apr 22 13:58:13 2011 +0200
     6.2 +++ b/src/ZF/pair.thy	Fri Apr 22 14:30:32 2011 +0200
     6.3 @@ -15,8 +15,7 @@
     6.4      val unfold_bex_tac = unfold_tac @{thms Bex_def};
     6.5      fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
     6.6    in
     6.7 -    fn _ => fn ss => fn ct =>
     6.8 -      Quantifier1.rearrange_bex prove_bex_tac (theory_of_cterm ct) ss (term_of ct)
     6.9 +    fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss o term_of
    6.10    end
    6.11  *}
    6.12  
    6.13 @@ -25,8 +24,7 @@
    6.14      val unfold_ball_tac = unfold_tac @{thms Ball_def};
    6.15      fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    6.16    in
    6.17 -    fn _ => fn ss => fn ct =>
    6.18 -      Quantifier1.rearrange_ball prove_ball_tac (theory_of_cterm ct) ss (term_of ct)
    6.19 +    fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss o term_of
    6.20    end
    6.21  *}
    6.22