unfold_tac: static evaluation of simpset;
authorwenzelm
Thu Dec 01 22:03:01 2005 +0100 (2005-12-01)
changeset 18324d1c4b1112e33
parent 18323 4365c8d84f69
child 18325 2d504ea54e5b
unfold_tac: static evaluation of simpset;
src/FOL/simpdata.ML
src/HOL/simpdata.ML
src/ZF/OrdQuant.thy
src/ZF/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Thu Dec 01 18:45:24 2005 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Thu Dec 01 22:03:01 2005 +0100
     1.3 @@ -338,9 +338,9 @@
     1.4    setmksimps (mksimps mksimps_pairs)
     1.5    setmkcong mk_meta_cong;
     1.6  
     1.7 -fun unfold_tac ss ths =
     1.8 -  ALLGOALS (full_simp_tac
     1.9 -    (Simplifier.inherit_context ss (Simplifier.clear_ss FOL_basic_ss) addsimps ths));
    1.10 +fun unfold_tac ths =
    1.11 +  let val ss0 = Simplifier.clear_ss FOL_basic_ss addsimps ths
    1.12 +  in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
    1.13  
    1.14  
    1.15  (*intuitionistic simprules only*)
     2.1 --- a/src/HOL/simpdata.ML	Thu Dec 01 18:45:24 2005 +0100
     2.2 +++ b/src/HOL/simpdata.ML	Thu Dec 01 22:03:01 2005 +0100
     2.3 @@ -350,9 +350,9 @@
     2.4      setmkeqTrue mk_eq_True
     2.5      setmkcong mk_meta_cong;
     2.6  
     2.7 -fun unfold_tac ss ths =
     2.8 -  ALLGOALS (full_simp_tac
     2.9 -    (Simplifier.inherit_context ss (Simplifier.clear_ss HOL_basic_ss) addsimps ths));
    2.10 +fun unfold_tac ths =
    2.11 +  let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths
    2.12 +  in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
    2.13  
    2.14  (*In general it seems wrong to add distributive laws by default: they
    2.15    might cause exponential blow-up.  But imp_disjL has been in for a while
     3.1 --- a/src/ZF/OrdQuant.thy	Thu Dec 01 18:45:24 2005 +0100
     3.2 +++ b/src/ZF/OrdQuant.thy	Thu Dec 01 22:03:01 2005 +0100
     3.3 @@ -400,10 +400,12 @@
     3.4  ML_setup {*
     3.5  local
     3.6  
     3.7 -fun prove_rex_tac ss = unfold_tac ss [rex_def] THEN Quantifier1.prove_one_point_ex_tac;
     3.8 +val unfold_rex_tac = unfold_tac [rex_def];
     3.9 +fun prove_rex_tac ss = unfold_rex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    3.10  val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac;
    3.11  
    3.12 -fun prove_rall_tac ss = unfold_tac ss [rall_def] THEN Quantifier1.prove_one_point_all_tac;
    3.13 +val unfold_rall_tac = unfold_tac [rall_def];
    3.14 +fun prove_rall_tac ss = unfold_rall_tac ss THEN Quantifier1.prove_one_point_all_tac;
    3.15  val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac;
    3.16  
    3.17  in
     4.1 --- a/src/ZF/simpdata.ML	Thu Dec 01 18:45:24 2005 +0100
     4.2 +++ b/src/ZF/simpdata.ML	Thu Dec 01 22:03:01 2005 +0100
     4.3 @@ -55,10 +55,12 @@
     4.4  
     4.5  local
     4.6  
     4.7 -fun prove_bex_tac ss = unfold_tac ss [Bex_def] THEN Quantifier1.prove_one_point_ex_tac;
     4.8 +val unfold_bex_tac = unfold_tac [Bex_def];
     4.9 +fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    4.10  val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
    4.11  
    4.12 -fun prove_ball_tac ss = unfold_tac ss [Ball_def] THEN Quantifier1.prove_one_point_all_tac;
    4.13 +val unfold_ball_tac = unfold_tac [Ball_def];
    4.14 +fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    4.15  val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
    4.16  
    4.17  in