better closeup and more consistent terminology
authorhaftmann
Sun May 24 19:57:13 2020 +0000 (6 weeks ago)
changeset 718864f4695757980
parent 71885 45f85e283ce0
child 71887 f7d15620dd8e
better closeup and more consistent terminology
src/FOL/FOL.thy
src/HOL/HOL.thy
src/HOL/Library/Quantified_Premise_Simproc.thy
src/HOL/Set.thy
src/Provers/quantifier1.ML
src/ZF/OrdQuant.thy
src/ZF/pair.thy
     1.1 --- a/src/FOL/FOL.thy	Sun May 24 21:11:23 2020 +0200
     1.2 +++ b/src/FOL/FOL.thy	Sun May 24 19:57:13 2020 +0000
     1.3 @@ -337,8 +337,8 @@
     1.4  
     1.5  ML_file \<open>simpdata.ML\<close>
     1.6  
     1.7 -simproc_setup defined_Ex (\<open>\<exists>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_ex\<close>
     1.8 -simproc_setup defined_All (\<open>\<forall>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_all\<close>
     1.9 +simproc_setup defined_Ex (\<open>\<exists>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_Ex\<close>
    1.10 +simproc_setup defined_All (\<open>\<forall>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_All\<close>
    1.11  
    1.12  ML \<open>
    1.13  (*intuitionistic simprules only*)
     2.1 --- a/src/HOL/HOL.thy	Sun May 24 21:11:23 2020 +0200
     2.2 +++ b/src/HOL/HOL.thy	Sun May 24 19:57:13 2020 +0000
     2.3 @@ -1198,8 +1198,8 @@
     2.4    Simplifier.method_setup Splitter.split_modifiers
     2.5  \<close>
     2.6  
     2.7 -simproc_setup defined_Ex ("\<exists>x. P x") = \<open>K Quantifier1.rearrange_ex\<close>
     2.8 -simproc_setup defined_All ("\<forall>x. P x") = \<open>K Quantifier1.rearrange_all\<close>
     2.9 +simproc_setup defined_Ex ("\<exists>x. P x") = \<open>K Quantifier1.rearrange_Ex\<close>
    2.10 +simproc_setup defined_All ("\<forall>x. P x") = \<open>K Quantifier1.rearrange_All\<close>
    2.11  
    2.12  text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>
    2.13  
     3.1 --- a/src/HOL/Library/Quantified_Premise_Simproc.thy	Sun May 24 21:11:23 2020 +0200
     3.2 +++ b/src/HOL/Library/Quantified_Premise_Simproc.thy	Sun May 24 19:57:13 2020 +0000
     3.3 @@ -4,6 +4,6 @@
     3.4    imports Main
     3.5  begin
     3.6  
     3.7 -simproc_setup defined_forall ("\<And>x. PROP P x") = \<open>K Quantifier1.rearrange_All\<close>
     3.8 +simproc_setup defined_all ("\<And>x. PROP P x") = \<open>K Quantifier1.rearrange_all\<close>
     3.9  
    3.10  end
     4.1 --- a/src/HOL/Set.thy	Sun May 24 21:11:23 2020 +0200
     4.2 +++ b/src/HOL/Set.thy	Sun May 24 19:57:13 2020 +0000
     4.3 @@ -330,17 +330,13 @@
     4.4  \<close>
     4.5  
     4.6  simproc_setup defined_Bex ("\<exists>x\<in>A. P x \<and> Q x") = \<open>
     4.7 -  fn _ => Quantifier1.rearrange_bex
     4.8 -    (fn ctxt =>
     4.9 -      unfold_tac ctxt @{thms Bex_def} THEN
    4.10 -      Quantifier1.prove_one_point_ex_tac ctxt)
    4.11 +  fn _ => Quantifier1.rearrange_Bex
    4.12 +    (fn ctxt => unfold_tac ctxt @{thms Bex_def})
    4.13  \<close>
    4.14  
    4.15  simproc_setup defined_All ("\<forall>x\<in>A. P x \<longrightarrow> Q x") = \<open>
    4.16 -  fn _ => Quantifier1.rearrange_ball
    4.17 -    (fn ctxt =>
    4.18 -      unfold_tac ctxt @{thms Ball_def} THEN
    4.19 -      Quantifier1.prove_one_point_all_tac ctxt)
    4.20 +  fn _ => Quantifier1.rearrange_Ball
    4.21 +    (fn ctxt => unfold_tac ctxt @{thms Ball_def})
    4.22  \<close>
    4.23  
    4.24  lemma ballI [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> P x) \<Longrightarrow> \<forall>x\<in>A. P x"
     5.1 --- a/src/Provers/quantifier1.ML	Sun May 24 21:11:23 2020 +0200
     5.2 +++ b/src/Provers/quantifier1.ML	Sun May 24 19:57:13 2020 +0000
     5.3 @@ -64,13 +64,11 @@
     5.4  
     5.5  signature QUANTIFIER1 =
     5.6  sig
     5.7 -  val prove_one_point_all_tac: Proof.context -> tactic
     5.8 -  val prove_one_point_ex_tac: Proof.context -> tactic
     5.9    val rearrange_all: Proof.context -> cterm -> thm option
    5.10    val rearrange_All: Proof.context -> cterm -> thm option
    5.11 -  val rearrange_ex: Proof.context -> cterm -> thm option
    5.12 -  val rearrange_ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
    5.13 -  val rearrange_bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
    5.14 +  val rearrange_Ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
    5.15 +  val rearrange_Ex: Proof.context -> cterm -> thm option
    5.16 +  val rearrange_Bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
    5.17    val rearrange_Collect: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
    5.18  end;
    5.19  
    5.20 @@ -158,7 +156,7 @@
    5.21  local
    5.22    val excomm = Data.ex_comm RS Data.iff_trans;
    5.23  in
    5.24 -  fun prove_one_point_ex_tac ctxt =
    5.25 +  fun prove_one_point_Ex_tac ctxt =
    5.26      qcomm_tac ctxt excomm Data.iff_exI 1 THEN resolve_tac ctxt [Data.iffI] 1 THEN
    5.27      ALLGOALS
    5.28        (EVERY' [eresolve_tac ctxt [Data.exE], REPEAT_DETERM o eresolve_tac ctxt [Data.conjE],
    5.29 @@ -180,13 +178,13 @@
    5.30    val all_comm = Data.all_comm RS Data.iff_trans;
    5.31    val All_comm = @{thm swap_params [THEN transitive]};
    5.32  in
    5.33 -  fun prove_one_point_all_tac ctxt =
    5.34 +  fun prove_one_point_All_tac ctxt =
    5.35      EVERY1 [qcomm_tac ctxt all_comm Data.iff_allI,
    5.36        resolve_tac ctxt [Data.iff_allI],
    5.37        resolve_tac ctxt [Data.iffI],
    5.38        tac ctxt,
    5.39        tac ctxt];
    5.40 -  fun prove_one_point_All_tac ctxt =
    5.41 +  fun prove_one_point_all_tac ctxt =
    5.42      EVERY1 [qcomm_tac ctxt All_comm @{thm equal_allI},
    5.43        resolve_tac ctxt [@{thm equal_allI}],
    5.44        resolve_tac ctxt [@{thm equal_intr_rule}],
    5.45 @@ -222,24 +220,24 @@
    5.46  fun rearrange_all ctxt ct =
    5.47    (case Thm.term_of ct of
    5.48      F as (all as Const (q, _)) $ Abs (x, T, P) =>
    5.49 -      (case extract_quant ctxt (K extract_imp) q P of
    5.50 +      (case extract_quant ctxt extract_implies q P of
    5.51          NONE => NONE
    5.52        | SOME (xs, eq, Q) =>
    5.53 -          let val R = quantify all x T xs (Data.imp $ eq $ Q)
    5.54 -          in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_all_tac)) end)
    5.55 +          let val R = quantify all x T xs (Logic.implies $ eq $ Q)
    5.56 +            in SOME (prove_conv ctxt (F, R) prove_one_point_all_tac) end)
    5.57    | _ => NONE);
    5.58  
    5.59  fun rearrange_All ctxt ct =
    5.60    (case Thm.term_of ct of
    5.61      F as (all as Const (q, _)) $ Abs (x, T, P) =>
    5.62 -      (case extract_quant ctxt extract_implies q P of
    5.63 +      (case extract_quant ctxt (K extract_imp) q P of
    5.64          NONE => NONE
    5.65        | SOME (xs, eq, Q) =>
    5.66 -          let val R = quantify all x T xs (Logic.implies $ eq $ Q)
    5.67 -            in SOME (prove_conv ctxt (F, R) prove_one_point_All_tac) end)
    5.68 +          let val R = quantify all x T xs (Data.imp $ eq $ Q)
    5.69 +          in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_All_tac)) end)
    5.70    | _ => NONE);
    5.71  
    5.72 -fun rearrange_ball tac ctxt ct =
    5.73 +fun rearrange_Ball tac ctxt ct =
    5.74    (case Thm.term_of ct of
    5.75      F as Ball $ A $ Abs (x, T, P) =>
    5.76        (case extract_imp true [] P of
    5.77 @@ -248,27 +246,29 @@
    5.78            if not (null xs) then NONE
    5.79            else
    5.80              let val R = Data.imp $ eq $ Q
    5.81 -            in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R)) (iff_reflection_tac THEN' tac)) end)
    5.82 +            in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R))
    5.83 +              (iff_reflection_tac THEN' tac THEN' prove_one_point_All_tac)) end)
    5.84    | _ => NONE);
    5.85  
    5.86 -fun rearrange_ex ctxt ct =
    5.87 +fun rearrange_Ex ctxt ct =
    5.88    (case Thm.term_of ct of
    5.89      F as (ex as Const (q, _)) $ Abs (x, T, P) =>
    5.90        (case extract_quant ctxt (K extract_conj) q P of
    5.91          NONE => NONE
    5.92        | SOME (xs, eq, Q) =>
    5.93            let val R = quantify ex x T xs (Data.conj $ eq $ Q)
    5.94 -          in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_ex_tac)) end)
    5.95 +          in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_Ex_tac)) end)
    5.96    | _ => NONE);
    5.97  
    5.98 -fun rearrange_bex tac ctxt ct =
    5.99 +fun rearrange_Bex tac ctxt ct =
   5.100    (case Thm.term_of ct of
   5.101      F as Bex $ A $ Abs (x, T, P) =>
   5.102        (case extract_conj true [] P of
   5.103          NONE => NONE
   5.104        | SOME (xs, eq, Q) =>
   5.105            if not (null xs) then NONE
   5.106 -          else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) (iff_reflection_tac THEN' tac)))
   5.107 +          else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q))
   5.108 +            (iff_reflection_tac THEN' tac THEN' prove_one_point_Ex_tac)))
   5.109    | _ => NONE);
   5.110  
   5.111  fun rearrange_Collect tac ctxt ct =
     6.1 --- a/src/ZF/OrdQuant.thy	Sun May 24 21:11:23 2020 +0200
     6.2 +++ b/src/ZF/OrdQuant.thy	Sun May 24 19:57:13 2020 +0000
     6.3 @@ -350,17 +350,13 @@
     6.4  text \<open>Setting up the one-point-rule simproc\<close>
     6.5  
     6.6  simproc_setup defined_rex ("\<exists>x[M]. P(x) & Q(x)") = \<open>
     6.7 -  fn _ => Quantifier1.rearrange_bex
     6.8 -    (fn ctxt =>
     6.9 -      unfold_tac ctxt @{thms rex_def} THEN
    6.10 -      Quantifier1.prove_one_point_ex_tac ctxt)
    6.11 +  fn _ => Quantifier1.rearrange_Bex
    6.12 +    (fn ctxt => unfold_tac ctxt @{thms rex_def})
    6.13  \<close>
    6.14  
    6.15  simproc_setup defined_rall ("\<forall>x[M]. P(x) \<longrightarrow> Q(x)") = \<open>
    6.16 -  fn _ => Quantifier1.rearrange_ball
    6.17 -    (fn ctxt =>
    6.18 -      unfold_tac ctxt @{thms rall_def} THEN
    6.19 -      Quantifier1.prove_one_point_all_tac ctxt)
    6.20 +  fn _ => Quantifier1.rearrange_Ball
    6.21 +    (fn ctxt => unfold_tac ctxt @{thms rall_def})
    6.22  \<close>
    6.23  
    6.24  end
     7.1 --- a/src/ZF/pair.thy	Sun May 24 21:11:23 2020 +0200
     7.2 +++ b/src/ZF/pair.thy	Sun May 24 19:57:13 2020 +0000
     7.3 @@ -19,17 +19,13 @@
     7.4  ML \<open>val ZF_ss = simpset_of \<^context>\<close>
     7.5  
     7.6  simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = \<open>
     7.7 -  fn _ => Quantifier1.rearrange_bex
     7.8 -    (fn ctxt =>
     7.9 -      unfold_tac ctxt @{thms Bex_def} THEN
    7.10 -      Quantifier1.prove_one_point_ex_tac ctxt)
    7.11 +  fn _ => Quantifier1.rearrange_Bex
    7.12 +    (fn ctxt => unfold_tac ctxt @{thms Bex_def})
    7.13  \<close>
    7.14  
    7.15  simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = \<open>
    7.16 -  fn _ => Quantifier1.rearrange_ball
    7.17 -    (fn ctxt =>
    7.18 -      unfold_tac ctxt @{thms Ball_def} THEN
    7.19 -      Quantifier1.prove_one_point_all_tac ctxt)
    7.20 +  fn _ => Quantifier1.rearrange_Ball
    7.21 +    (fn ctxt => unfold_tac ctxt @{thms Ball_def})
    7.22  \<close>
    7.23  
    7.24