modernized Quantifier1 simproc setup;
authorwenzelm
Fri Apr 22 13:58:13 2011 +0200 (2011-04-22)
changeset 424556702c984bf5a
parent 42454 12a752aeee98
child 42456 13b4b6ba3593
modernized Quantifier1 simproc setup;
src/FOL/FOL.thy
src/FOL/simpdata.ML
src/HOL/HOL.thy
src/HOL/Set.thy
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/simpdata.ML
src/ZF/OrdQuant.thy
src/ZF/pair.thy
src/ZF/simpdata.ML
     1.1 --- a/src/FOL/FOL.thy	Fri Apr 22 13:07:47 2011 +0200
     1.2 +++ b/src/FOL/FOL.thy	Fri Apr 22 13:58:13 2011 +0200
     1.3 @@ -305,12 +305,21 @@
     1.4  
     1.5  
     1.6  use "simpdata.ML"
     1.7 +
     1.8 +simproc_setup defined_Ex ("EX x. P(x)") = {*
     1.9 +  fn _ => fn ss => fn ct => Quantifier1.rearrange_ex (theory_of_cterm ct) ss (term_of ct)
    1.10 +*}
    1.11 +
    1.12 +simproc_setup defined_All ("ALL x. P(x)") = {*
    1.13 +  fn _ => fn ss => fn ct => Quantifier1.rearrange_all (theory_of_cterm ct) ss (term_of ct)
    1.14 +*}
    1.15 +
    1.16  ML {*
    1.17  (*intuitionistic simprules only*)
    1.18  val IFOL_ss =
    1.19    FOL_basic_ss
    1.20    addsimps (@{thms meta_simps} @ @{thms IFOL_simps} @ @{thms int_ex_simps} @ @{thms int_all_simps})
    1.21 -  addsimprocs [defALL_regroup, defEX_regroup]
    1.22 +  addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}]
    1.23    addcongs [@{thm imp_cong}];
    1.24  
    1.25  (*classical simprules too*)
    1.26 @@ -318,6 +327,7 @@
    1.27  *}
    1.28  
    1.29  setup {* Simplifier.map_simpset (K FOL_ss) *}
    1.30 +
    1.31  setup "Simplifier.method_setup Splitter.split_modifiers"
    1.32  setup Splitter.setup
    1.33  setup clasimp_setup
     2.1 --- a/src/FOL/simpdata.ML	Fri Apr 22 13:07:47 2011 +0200
     2.2 +++ b/src/FOL/simpdata.ML	Fri Apr 22 13:58:13 2011 +0200
     2.3 @@ -80,14 +80,6 @@
     2.4    val ex_comm = @{thm ex_comm}
     2.5  end);
     2.6  
     2.7 -val defEX_regroup =
     2.8 -  Simplifier.simproc_global @{theory}
     2.9 -    "defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
    2.10 -
    2.11 -val defALL_regroup =
    2.12 -  Simplifier.simproc_global @{theory}
    2.13 -    "defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;
    2.14 -
    2.15  
    2.16  (*** Case splitting ***)
    2.17  
     3.1 --- a/src/HOL/HOL.thy	Fri Apr 22 13:07:47 2011 +0200
     3.2 +++ b/src/HOL/HOL.thy	Fri Apr 22 13:58:13 2011 +0200
     3.3 @@ -1209,8 +1209,15 @@
     3.4  
     3.5  use "Tools/simpdata.ML"
     3.6  ML {* open Simpdata *}
     3.7 -setup {*
     3.8 -  Simplifier.map_simpset (K (HOL_basic_ss addsimprocs [defALL_regroup, defEX_regroup]))
     3.9 +
    3.10 +setup {* Simplifier.map_simpset (K HOL_basic_ss) *}
    3.11 +
    3.12 +simproc_setup defined_Ex ("EX x. P x") = {*
    3.13 +  fn _ => fn ss => fn ct => Quantifier1.rearrange_ex (theory_of_cterm ct) ss (term_of ct)
    3.14 +*}
    3.15 +
    3.16 +simproc_setup defined_All ("ALL x. P x") = {*
    3.17 +  fn _ => fn ss => fn ct => Quantifier1.rearrange_all (theory_of_cterm ct) ss (term_of ct)
    3.18  *}
    3.19  
    3.20  setup {*
     4.1 --- a/src/HOL/Set.thy	Fri Apr 22 13:07:47 2011 +0200
     4.2 +++ b/src/HOL/Set.thy	Fri Apr 22 13:58:13 2011 +0200
     4.3 @@ -75,17 +75,16 @@
     4.4  to the front (and similarly for @{text "t=x"}):
     4.5  *}
     4.6  
     4.7 -setup {*
     4.8 -let
     4.9 -  val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
    4.10 -    ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
    4.11 -                    DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
    4.12 -  val defColl_regroup = Simplifier.simproc_global @{theory}
    4.13 -    "defined Collect" ["{x. P x & Q x}"]
    4.14 -    (Quantifier1.rearrange_Coll Coll_perm_tac)
    4.15 -in
    4.16 -  Simplifier.map_simpset (fn ss => ss addsimprocs [defColl_regroup])
    4.17 -end
    4.18 +simproc_setup defined_Collect ("{x. P x & Q x}") = {*
    4.19 +  let
    4.20 +    val Coll_perm_tac =
    4.21 +      rtac @{thm Collect_cong} 1 THEN
    4.22 +      rtac @{thm iffI} 1 THEN
    4.23 +      ALLGOALS (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]);
    4.24 +  in
    4.25 +    fn _ => fn ss => fn ct =>
    4.26 +      Quantifier1.rearrange_Coll Coll_perm_tac (theory_of_cterm ct) ss (term_of ct)
    4.27 +  end
    4.28  *}
    4.29  
    4.30  lemmas CollectE = CollectD [elim_format]
    4.31 @@ -329,21 +328,24 @@
    4.32    in [(@{const_syntax Collect}, setcompr_tr')] end;
    4.33  *}
    4.34  
    4.35 -setup {*
    4.36 -let
    4.37 -  val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
    4.38 -  fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    4.39 -  val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
    4.40 -  val unfold_ball_tac = unfold_tac @{thms "Ball_def"};
    4.41 -  fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    4.42 -  val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
    4.43 -  val defBEX_regroup = Simplifier.simproc_global @{theory}
    4.44 -    "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
    4.45 -  val defBALL_regroup = Simplifier.simproc_global @{theory}
    4.46 -    "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
    4.47 -in
    4.48 -  Simplifier.map_simpset (fn ss => ss addsimprocs [defBALL_regroup, defBEX_regroup])
    4.49 -end
    4.50 +simproc_setup defined_Bex ("EX x:A. P x & Q x") = {*
    4.51 +  let
    4.52 +    val unfold_bex_tac = unfold_tac @{thms Bex_def};
    4.53 +    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    4.54 +  in
    4.55 +    fn _ => fn ss => fn ct =>
    4.56 +      Quantifier1.rearrange_bex prove_bex_tac (theory_of_cterm ct) ss (term_of ct)
    4.57 +  end
    4.58 +*}
    4.59 +
    4.60 +simproc_setup defined_All ("ALL x:A. P x --> Q x") = {*
    4.61 +  let
    4.62 +    val unfold_ball_tac = unfold_tac @{thms Ball_def};
    4.63 +    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    4.64 +  in
    4.65 +    fn _ => fn ss => fn ct =>
    4.66 +      Quantifier1.rearrange_ball prove_ball_tac (theory_of_cterm ct) ss (term_of ct)
    4.67 +  end
    4.68  *}
    4.69  
    4.70  lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
     5.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri Apr 22 13:07:47 2011 +0200
     5.2 +++ b/src/HOL/Tools/Meson/meson.ML	Fri Apr 22 13:58:13 2011 +0200
     5.3 @@ -567,7 +567,7 @@
     5.4  
     5.5  val nnf_ss =
     5.6    HOL_basic_ss addsimps nnf_extra_simps
     5.7 -    addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
     5.8 +    addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq}, @{simproc let_simp}];
     5.9  
    5.10  val presimplify =
    5.11    rewrite_rule (map safe_mk_meta_eq nnf_simps) #> simplify nnf_ss
     6.1 --- a/src/HOL/Tools/simpdata.ML	Fri Apr 22 13:07:47 2011 +0200
     6.2 +++ b/src/HOL/Tools/simpdata.ML	Fri Apr 22 13:58:13 2011 +0200
     6.3 @@ -183,14 +183,6 @@
     6.4    let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths
     6.5    in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
     6.6  
     6.7 -val defALL_regroup =
     6.8 -  Simplifier.simproc_global @{theory}
     6.9 -    "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
    6.10 -
    6.11 -val defEX_regroup =
    6.12 -  Simplifier.simproc_global @{theory}
    6.13 -    "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
    6.14 -
    6.15  end;
    6.16  
    6.17  structure Splitter = Simpdata.Splitter;
     7.1 --- a/src/ZF/OrdQuant.thy	Fri Apr 22 13:07:47 2011 +0200
     7.2 +++ b/src/ZF/OrdQuant.thy	Fri Apr 22 13:58:13 2011 +0200
     7.3 @@ -368,27 +368,24 @@
     7.4  
     7.5  text {* Setting up the one-point-rule simproc *}
     7.6  
     7.7 -ML {*
     7.8 -local
     7.9 -
    7.10 -val unfold_rex_tac = unfold_tac [@{thm rex_def}];
    7.11 -fun prove_rex_tac ss = unfold_rex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    7.12 -val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac;
    7.13 -
    7.14 -val unfold_rall_tac = unfold_tac [@{thm rall_def}];
    7.15 -fun prove_rall_tac ss = unfold_rall_tac ss THEN Quantifier1.prove_one_point_all_tac;
    7.16 -val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac;
    7.17 +simproc_setup defined_rex ("EX x[M]. P(x) & Q(x)") = {*
    7.18 +  let
    7.19 +    val unfold_rex_tac = unfold_tac @{thms rex_def};
    7.20 +    fun prove_rex_tac ss = unfold_rex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    7.21 +  in
    7.22 +    fn _ => fn ss => fn ct =>
    7.23 +      Quantifier1.rearrange_bex prove_rex_tac (theory_of_cterm ct) ss (term_of ct)
    7.24 +  end
    7.25 +*}
    7.26  
    7.27 -in
    7.28 -
    7.29 -val defREX_regroup = Simplifier.simproc_global @{theory}
    7.30 -  "defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex;
    7.31 -val defRALL_regroup = Simplifier.simproc_global @{theory}
    7.32 -  "defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball;
    7.33 -
    7.34 -end;
    7.35 -
    7.36 -Addsimprocs [defRALL_regroup,defREX_regroup];
    7.37 +simproc_setup defined_rall ("ALL x[M]. P(x) --> Q(x)") = {*
    7.38 +  let
    7.39 +    val unfold_rall_tac = unfold_tac @{thms rall_def};
    7.40 +    fun prove_rall_tac ss = unfold_rall_tac ss THEN Quantifier1.prove_one_point_all_tac;
    7.41 +  in
    7.42 +    fn _ => fn ss => fn ct =>
    7.43 +      Quantifier1.rearrange_ball prove_rall_tac (theory_of_cterm ct) ss (term_of ct)
    7.44 +  end
    7.45  *}
    7.46  
    7.47  end
     8.1 --- a/src/ZF/pair.thy	Fri Apr 22 13:07:47 2011 +0200
     8.2 +++ b/src/ZF/pair.thy	Fri Apr 22 13:58:13 2011 +0200
     8.3 @@ -7,7 +7,29 @@
     8.4  header{*Ordered Pairs*}
     8.5  
     8.6  theory pair imports upair
     8.7 -uses "simpdata.ML" begin
     8.8 +uses "simpdata.ML"
     8.9 +begin
    8.10 +
    8.11 +simproc_setup defined_Bex ("EX x:A. P(x) & Q(x)") = {*
    8.12 +  let
    8.13 +    val unfold_bex_tac = unfold_tac @{thms Bex_def};
    8.14 +    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    8.15 +  in
    8.16 +    fn _ => fn ss => fn ct =>
    8.17 +      Quantifier1.rearrange_bex prove_bex_tac (theory_of_cterm ct) ss (term_of ct)
    8.18 +  end
    8.19 +*}
    8.20 +
    8.21 +simproc_setup defined_Ball ("ALL x:A. P(x) --> Q(x)") = {*
    8.22 +  let
    8.23 +    val unfold_ball_tac = unfold_tac @{thms Ball_def};
    8.24 +    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    8.25 +  in
    8.26 +    fn _ => fn ss => fn ct =>
    8.27 +      Quantifier1.rearrange_ball prove_ball_tac (theory_of_cterm ct) ss (term_of ct)
    8.28 +  end
    8.29 +*}
    8.30 +
    8.31  
    8.32  (** Lemmas for showing that <a,b> uniquely determines a and b **)
    8.33  
     9.1 --- a/src/ZF/simpdata.ML	Fri Apr 22 13:07:47 2011 +0200
     9.2 +++ b/src/ZF/simpdata.ML	Fri Apr 22 13:58:13 2011 +0200
     9.3 @@ -47,28 +47,5 @@
     9.4    ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
     9.5    addcongs [@{thm if_weak_cong}]);
     9.6  
     9.7 -local
     9.8 -
     9.9 -val unfold_bex_tac = unfold_tac [@{thm Bex_def}];
    9.10 -fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    9.11 -val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
    9.12 -
    9.13 -val unfold_ball_tac = unfold_tac [@{thm Ball_def}];
    9.14 -fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    9.15 -val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
    9.16 -
    9.17 -in
    9.18 -
    9.19 -val defBEX_regroup = Simplifier.simproc_global @{theory}
    9.20 -  "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
    9.21 -
    9.22 -val defBALL_regroup = Simplifier.simproc_global @{theory}
    9.23 -  "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
    9.24 -
    9.25 -end;
    9.26 -
    9.27 -Addsimprocs [defBALL_regroup, defBEX_regroup];
    9.28 -
    9.29 -
    9.30  val ZF_ss = @{simpset};
    9.31