misc tuning and simplification;
authorwenzelm
Fri Apr 22 15:05:04 2011 +0200 (2011-04-22)
changeset 4245938b9f023cc34
parent 42458 5dfae6d348fd
child 42460 1805c67dc7aa
misc tuning and simplification;
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 14:53:11 2011 +0200
     1.2 +++ b/src/FOL/FOL.thy	Fri Apr 22 15:05:04 2011 +0200
     1.3 @@ -306,13 +306,8 @@
     1.4  
     1.5  use "simpdata.ML"
     1.6  
     1.7 -simproc_setup defined_Ex ("EX x. P(x)") = {*
     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 => Quantifier1.rearrange_all ss o term_of
    1.13 -*}
    1.14 +simproc_setup defined_Ex ("EX x. P(x)") = {* fn _ => Quantifier1.rearrange_ex *}
    1.15 +simproc_setup defined_All ("ALL x. P(x)") = {* fn _ => Quantifier1.rearrange_all *}
    1.16  
    1.17  ML {*
    1.18  (*intuitionistic simprules only*)
     2.1 --- a/src/HOL/HOL.thy	Fri Apr 22 14:53:11 2011 +0200
     2.2 +++ b/src/HOL/HOL.thy	Fri Apr 22 15:05:04 2011 +0200
     2.3 @@ -1212,13 +1212,8 @@
     2.4  
     2.5  setup {* Simplifier.map_simpset (K HOL_basic_ss) *}
     2.6  
     2.7 -simproc_setup defined_Ex ("EX x. P x") = {*
     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 => Quantifier1.rearrange_all ss o term_of
    2.13 -*}
    2.14 +simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *}
    2.15 +simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *}
    2.16  
    2.17  setup {*
    2.18    Simplifier.method_setup Splitter.split_modifiers
     3.1 --- a/src/HOL/Set.thy	Fri Apr 22 14:53:11 2011 +0200
     3.2 +++ b/src/HOL/Set.thy	Fri Apr 22 15:05:04 2011 +0200
     3.3 @@ -76,14 +76,12 @@
     3.4  *}
     3.5  
     3.6  simproc_setup defined_Collect ("{x. P x & Q x}") = {*
     3.7 -  let
     3.8 -    val Collect_perm_tac =
     3.9 -      rtac @{thm Collect_cong} 1 THEN
    3.10 +  fn _ =>
    3.11 +    Quantifier1.rearrange_Collect
    3.12 +     (rtac @{thm Collect_cong} 1 THEN
    3.13        rtac @{thm iffI} 1 THEN
    3.14 -      ALLGOALS (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]);
    3.15 -  in
    3.16 -    fn _ => fn ss => Quantifier1.rearrange_Collect Collect_perm_tac ss o term_of
    3.17 -  end
    3.18 +      ALLGOALS
    3.19 +        (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
    3.20  *}
    3.21  
    3.22  lemmas CollectE = CollectD [elim_format]
    3.23 @@ -331,18 +329,14 @@
    3.24    let
    3.25      val unfold_bex_tac = unfold_tac @{thms Bex_def};
    3.26      fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    3.27 -  in
    3.28 -    fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss o term_of
    3.29 -  end
    3.30 +  in fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss end
    3.31  *}
    3.32  
    3.33  simproc_setup defined_All ("ALL x:A. P x --> Q x") = {*
    3.34    let
    3.35      val unfold_ball_tac = unfold_tac @{thms Ball_def};
    3.36      fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    3.37 -  in
    3.38 -    fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss o term_of
    3.39 -  end
    3.40 +  in fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss end
    3.41  *}
    3.42  
    3.43  lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
     4.1 --- a/src/Provers/quantifier1.ML	Fri Apr 22 14:53:11 2011 +0200
     4.2 +++ b/src/Provers/quantifier1.ML	Fri Apr 22 15:05:04 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: simpset -> term -> thm option
     4.8 -  val rearrange_ex: simpset -> term -> thm option
     4.9 -  val rearrange_ball: tactic -> simpset -> term -> thm option
    4.10 -  val rearrange_bex: tactic -> simpset -> term -> thm option
    4.11 -  val rearrange_Collect: tactic -> simpset -> term -> thm option
    4.12 +  val rearrange_all: simpset -> cterm -> thm option
    4.13 +  val rearrange_ex: simpset -> cterm -> thm option
    4.14 +  val rearrange_ball: tactic -> simpset -> cterm -> thm option
    4.15 +  val rearrange_bex: tactic -> simpset -> cterm -> thm option
    4.16 +  val rearrange_Collect: tactic -> simpset -> cterm -> thm option
    4.17  end;
    4.18  
    4.19  functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
    4.20 @@ -172,15 +172,19 @@
    4.21      val Q = if n = 0 then P else renumber 0 n P;
    4.22    in quant xs (qC $ Abs (x, T, Q)) end;
    4.23  
    4.24 -fun rearrange_all ss (F as (all as Const (q, _)) $ Abs (x, T, P)) =
    4.25 +fun rearrange_all ss ct =
    4.26 +  (case term_of ct of
    4.27 +    F as (all as Const (q, _)) $ Abs (x, T, P) =>
    4.28        (case extract_quant extract_imp q P of
    4.29          NONE => NONE
    4.30        | SOME (xs, eq, Q) =>
    4.31            let val R = quantify all x T xs (Data.imp $ eq $ Q)
    4.32            in SOME (prove_conv prove_one_point_all_tac ss (F, R)) end)
    4.33 -  | rearrange_all _ _ = NONE;
    4.34 +  | _ => NONE);
    4.35  
    4.36 -fun rearrange_ball tac ss (F as Ball $ A $ Abs (x, T, P)) =
    4.37 +fun rearrange_ball tac ss ct =
    4.38 +  (case term_of ct of
    4.39 +    F as Ball $ A $ Abs (x, T, P) =>
    4.40        (case extract_imp true [] P of
    4.41          NONE => NONE
    4.42        | SOME (xs, eq, Q) =>
    4.43 @@ -188,30 +192,36 @@
    4.44            else
    4.45              let val R = Data.imp $ eq $ Q
    4.46              in SOME (prove_conv tac ss (F, Ball $ A $ Abs (x, T, R))) end)
    4.47 -  | rearrange_ball _ _ _ = NONE;
    4.48 +  | _ => NONE);
    4.49  
    4.50 -fun rearrange_ex ss (F as (ex as Const (q, _)) $ Abs (x, T, P)) =
    4.51 +fun rearrange_ex ss ct =
    4.52 +  (case term_of ct of
    4.53 +    F as (ex as Const (q, _)) $ Abs (x, T, P) =>
    4.54        (case extract_quant extract_conj q P of
    4.55          NONE => NONE
    4.56        | SOME (xs, eq, Q) =>
    4.57            let val R = quantify ex x T xs (Data.conj $ eq $ Q)
    4.58            in SOME (prove_conv prove_one_point_ex_tac ss (F, R)) end)
    4.59 -  | rearrange_ex _ _ = NONE;
    4.60 +  | _ => NONE);
    4.61  
    4.62 -fun rearrange_bex tac ss (F as Bex $ A $ Abs (x, T, P)) =
    4.63 +fun rearrange_bex tac ss ct =
    4.64 +  (case term_of ct of
    4.65 +    F as Bex $ A $ Abs (x, T, P) =>
    4.66        (case extract_conj true [] P of
    4.67          NONE => NONE
    4.68        | SOME (xs, eq, Q) =>
    4.69            if not (null xs) then NONE
    4.70            else SOME (prove_conv tac ss (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q))))
    4.71 -  | rearrange_bex _ _ _ = NONE;
    4.72 +  | _ => NONE);
    4.73  
    4.74 -fun rearrange_Collect tac ss (F as Collect $ Abs (x, T, P)) =
    4.75 +fun rearrange_Collect tac ss ct =
    4.76 +  (case term_of ct of
    4.77 +    F as Collect $ Abs (x, T, P) =>
    4.78        (case extract_conj true [] P of
    4.79          NONE => NONE
    4.80        | SOME (_, eq, Q) =>
    4.81            let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q)
    4.82            in SOME (prove_conv tac ss (F, R)) end)
    4.83 -  | rearrange_Collect _ _ _ = NONE;
    4.84 +  | _ => NONE);
    4.85  
    4.86  end;
     5.1 --- a/src/ZF/OrdQuant.thy	Fri Apr 22 14:53:11 2011 +0200
     5.2 +++ b/src/ZF/OrdQuant.thy	Fri Apr 22 15:05:04 2011 +0200
     5.3 @@ -372,18 +372,14 @@
     5.4    let
     5.5      val unfold_rex_tac = unfold_tac @{thms rex_def};
     5.6      fun prove_rex_tac ss = unfold_rex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
     5.7 -  in
     5.8 -    fn _ => fn ss => Quantifier1.rearrange_bex (prove_rex_tac ss) ss o term_of
     5.9 -  end
    5.10 +  in fn _ => fn ss => Quantifier1.rearrange_bex (prove_rex_tac ss) ss end
    5.11  *}
    5.12  
    5.13  simproc_setup defined_rall ("ALL x[M]. P(x) --> Q(x)") = {*
    5.14    let
    5.15      val unfold_rall_tac = unfold_tac @{thms rall_def};
    5.16      fun prove_rall_tac ss = unfold_rall_tac ss THEN Quantifier1.prove_one_point_all_tac;
    5.17 -  in
    5.18 -    fn _ => fn ss => Quantifier1.rearrange_ball (prove_rall_tac ss) ss o term_of
    5.19 -  end
    5.20 +  in fn _ => fn ss => Quantifier1.rearrange_ball (prove_rall_tac ss) ss end
    5.21  *}
    5.22  
    5.23  end
     6.1 --- a/src/ZF/pair.thy	Fri Apr 22 14:53:11 2011 +0200
     6.2 +++ b/src/ZF/pair.thy	Fri Apr 22 15:05:04 2011 +0200
     6.3 @@ -14,18 +14,14 @@
     6.4    let
     6.5      val unfold_bex_tac = unfold_tac @{thms Bex_def};
     6.6      fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
     6.7 -  in
     6.8 -    fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss o term_of
     6.9 -  end
    6.10 +  in fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss end
    6.11  *}
    6.12  
    6.13  simproc_setup defined_Ball ("ALL x:A. P(x) --> Q(x)") = {*
    6.14    let
    6.15      val unfold_ball_tac = unfold_tac @{thms Ball_def};
    6.16      fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    6.17 -  in
    6.18 -    fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss o term_of
    6.19 -  end
    6.20 +  in fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss end
    6.21  *}
    6.22  
    6.23