generalization of 1 point rules for ALL
authornipkow
Thu Mar 29 13:59:54 2001 +0200 (2001-03-29 ago)
changeset 11232558a4feebb04
parent 11231 30d96882f915
child 11233 34c81a796ee3
generalization of 1 point rules for ALL
src/FOL/simpdata.ML
src/HOL/Lex/AutoChopper.ML
src/HOL/Lex/RegExp2NAe.ML
src/HOL/MiniML/W.ML
src/HOL/Set.ML
src/HOL/W0/I.ML
src/HOL/W0/W.ML
src/HOL/simpdata.ML
src/Provers/quantifier1.ML
     1.1 --- a/src/FOL/simpdata.ML	Thu Mar 29 12:26:37 2001 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Thu Mar 29 13:59:54 2001 +0200
     1.3 @@ -218,6 +218,15 @@
     1.4      "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))";
     1.5  
     1.6  
     1.7 +local
     1.8 +val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R"
     1.9 +              (fn prems => [cut_facts_tac prems 1, Blast_tac 1]);
    1.10 +
    1.11 +val iff_allI = allI RS
    1.12 +    prove_goal (the_context()) "ALL x. P(x) <-> Q(x) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"
    1.13 +               (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
    1.14 +in
    1.15 +
    1.16  (** make simplification procedures for quantifier elimination **)
    1.17  structure Quantifier1 = Quantifier1Fun(
    1.18  struct
    1.19 @@ -226,30 +235,32 @@
    1.20      | dest_eq _ = None;
    1.21    fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
    1.22      | dest_conj _ = None;
    1.23 +  fun dest_imp((c as Const("op -->",_)) $ s $ t) = Some(c,s,t)
    1.24 +    | dest_imp _ = None;
    1.25    val conj = FOLogic.conj
    1.26    val imp  = FOLogic.imp
    1.27    (*rules*)
    1.28    val iff_reflection = iff_reflection
    1.29    val iffI = iffI
    1.30 -  val sym  = sym
    1.31    val conjI= conjI
    1.32    val conjE= conjE
    1.33    val impI = impI
    1.34 -  val impE = impE
    1.35    val mp   = mp
    1.36 +  val uncurry = uncurry
    1.37    val exI  = exI
    1.38    val exE  = exE
    1.39 -  val allI = allI
    1.40 -  val allE = allE
    1.41 +  val iff_allI = iff_allI
    1.42  end);
    1.43  
    1.44 +end;
    1.45 +
    1.46  local
    1.47  
    1.48  val ex_pattern =
    1.49    read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)", FOLogic.oT)
    1.50  
    1.51  val all_pattern =
    1.52 -  read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
    1.53 +  read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) --> Q(x)", FOLogic.oT)
    1.54  
    1.55  in
    1.56  val defEX_regroup =
     2.1 --- a/src/HOL/Lex/AutoChopper.ML	Thu Mar 29 12:26:37 2001 +0200
     2.2 +++ b/src/HOL/Lex/AutoChopper.ML	Thu Mar 29 13:59:54 2001 +0200
     2.3 @@ -93,7 +93,6 @@
     2.4  by (Simp_tac 1);
     2.5  by (induct_tac "xs" 1);
     2.6   by (simp_tac (simpset() addcongs [conj_cong]) 1);
     2.7 - by (Fast_tac 1);
     2.8  by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
     2.9  by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1);
    2.10  by (rename_tac "vss lrst" 1);  
    2.11 @@ -116,7 +115,6 @@
    2.12  by (Simp_tac 1);
    2.13  by (induct_tac "xs" 1);
    2.14   by (simp_tac (simpset() addcongs [conj_cong]) 1);
    2.15 - by (Fast_tac 1);
    2.16  by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
    2.17  by (strip_tac 1);
    2.18  by (rtac conjI 1);
    2.19 @@ -155,7 +153,6 @@
    2.20  by (Simp_tac 1);
    2.21  by (induct_tac "xs" 1);
    2.22   by (simp_tac (simpset() addcongs [conj_cong]) 1);
    2.23 - by (Fast_tac 1);
    2.24  by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
    2.25  by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1);
    2.26  by (rename_tac "vss lrst" 1);  
    2.27 @@ -193,7 +190,6 @@
    2.28  by (Simp_tac 1);
    2.29  by (induct_tac "xs" 1);
    2.30   by (simp_tac (simpset() addcongs [conj_cong]) 1);
    2.31 - by (Fast_tac 1);
    2.32  by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
    2.33  by (strip_tac 1);
    2.34  by (case_tac "acc_prefix A list (next A a st)" 1);
     3.1 --- a/src/HOL/Lex/RegExp2NAe.ML	Thu Mar 29 12:26:37 2001 +0200
     3.2 +++ b/src/HOL/Lex/RegExp2NAe.ML	Thu Mar 29 13:59:54 2001 +0200
     3.3 @@ -396,7 +396,7 @@
     3.4  \  (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & \
     3.5  \          (? s. (start R,s) : steps R v & q = False#s))))";
     3.6  by (blast_tac (claset() addDs [True_steps_concD]
     3.7 -     addIs [True_True_steps_concI,in_steps_epsclosure,r_into_rtrancl]) 1);
     3.8 +     addIs [True_True_steps_concI,in_steps_epsclosure]) 1);
     3.9  qed "True_steps_conc";
    3.10  
    3.11  (** starting from the start **)
    3.12 @@ -537,7 +537,7 @@
    3.13  by (induct_tac "us" 1);
    3.14   by (Simp_tac 1);
    3.15  by (Simp_tac 1);
    3.16 -by (blast_tac (claset() addIs [True_True_steps_starI,True_start_eps_starI,r_into_rtrancl,in_epsclosure_steps]) 1);
    3.17 +by (blast_tac (claset() addIs [True_True_steps_starI,True_start_eps_starI,in_epsclosure_steps]) 1);
    3.18  qed_spec_mp "steps_star_cycle";
    3.19  
    3.20  (* Better stated directly with start(star A)? Loop in star A back to start(star A)?*)
    3.21 @@ -578,7 +578,7 @@
    3.22   by (Blast_tac 1);
    3.23  by (etac disjE 1);
    3.24   by (Asm_simp_tac 1);
    3.25 -by (blast_tac (claset() addIs [in_steps_epsclosure,r_into_rtrancl]) 1);
    3.26 +by (blast_tac (claset() addIs [in_steps_epsclosure]) 1);
    3.27  qed "start_steps_star";
    3.28  
    3.29  Goalw [star_def] "!A. fin (star A) (True#p) = fin A p";
     4.1 --- a/src/HOL/MiniML/W.ML	Thu Mar 29 12:26:37 2001 +0200
     4.2 +++ b/src/HOL/MiniML/W.ML	Thu Mar 29 13:59:54 2001 +0200
     4.3 @@ -317,63 +317,61 @@
     4.4  (* case Let e1 e2 *)
     4.5  by (simp_tac (simpset() addsplits [split_option_bind]) 1);
     4.6  by (strip_tac 1);
     4.7 -by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); 
     4.8 +(*by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); *)
     4.9 +by (rename_tac "S1 t1 m1 S2" 1); 
    4.10  by (res_inst_tac [("t1.0","$ S2 t1")] has_type.LETI 1);
    4.11 -by (simp_tac (simpset() addsimps [o_def]) 1);
    4.12 -by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
    4.13 -by (rtac (has_type_cl_sub RS spec) 1);
    4.14 -by (dres_inst_tac [("x","A")] spec 1);
    4.15 -by (dres_inst_tac [("x","S1")] spec 1);
    4.16 -by (dres_inst_tac [("x","t1")] spec 1);
    4.17 -by (dres_inst_tac [("x","m2")] spec 1);
    4.18 -by (rotate_tac 4 1);
    4.19 -by (dres_inst_tac [("x","m1")] spec 1);
    4.20 -by (mp_tac 1);
    4.21 -by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
    4.22 + by (simp_tac (simpset() addsimps [o_def]) 1);
    4.23 + by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
    4.24 + by (rtac (has_type_cl_sub RS spec) 1);
    4.25 + by (dres_inst_tac [("x","A")] spec 1);
    4.26 + by (dres_inst_tac [("x","S1")] spec 1);
    4.27 + by (dres_inst_tac [("x","t1")] spec 1);
    4.28 + by (dres_inst_tac [("x","m1")] spec 1);
    4.29 + by (dres_inst_tac [("x","n")] spec 1);
    4.30 + by (mp_tac 1);
    4.31 + by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
    4.32  by (simp_tac (simpset() addsimps [o_def]) 1);
    4.33  by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
    4.34  by (rtac (gen_subst_commutes RS sym RS subst) 1);
    4.35 -by (rtac (app_subst_Cons RS subst) 2);
    4.36 -by (etac thin_rl 2);
    4.37 -by (dres_inst_tac [("x","gen ($S1 A) t1 # $ S1 A")] spec 2);
    4.38 -by (dres_inst_tac [("x","S2")] spec 2);
    4.39 -by (dres_inst_tac [("x","t")] spec 2);
    4.40 -by (dres_inst_tac [("x","n2")] spec 2);
    4.41 -by (dres_inst_tac [("x","m2")] spec 2);
    4.42 -by (ftac new_tv_W 2);
    4.43 -by (assume_tac 2);
    4.44 -by (dtac conjunct1 2);
    4.45 -by (dtac conjunct1 2);
    4.46 -by (ftac new_tv_subst_scheme_list 2);
    4.47 -by (rtac new_scheme_list_le 2);
    4.48 -by (rtac W_var_ge 2);
    4.49 -by (assume_tac 2);
    4.50 -by (assume_tac 2);
    4.51 -by (etac impE 2);
    4.52 -by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2);
    4.53 -by (Simp_tac 2);
    4.54 -by (Fast_tac 2);
    4.55 -by (assume_tac 2);
    4.56 -by (Asm_full_simp_tac 2);
    4.57 + by (rtac (app_subst_Cons RS subst) 2);
    4.58 + by (etac thin_rl 2);
    4.59 + by (dres_inst_tac [("x","gen ($S1 A) t1 # $ S1 A")] spec 2);
    4.60 + by (dres_inst_tac [("x","S2")] spec 2);
    4.61 + by (dres_inst_tac [("x","t")] spec 2);
    4.62 + by (dres_inst_tac [("x","m")] spec 2);
    4.63 + by (dres_inst_tac [("x","m1")] spec 2);
    4.64 + by (ftac new_tv_W 2);
    4.65 +  by (assume_tac 2);
    4.66 + by (dtac conjunct1 2);
    4.67 + by (ftac new_tv_subst_scheme_list 2);
    4.68 +  by (rtac new_scheme_list_le 2);
    4.69 +   by (rtac W_var_ge 2);
    4.70 +   by (assume_tac 2);
    4.71 +  by (assume_tac 2);
    4.72 + by (etac impE 2);
    4.73 +  by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2);
    4.74 +   by (Simp_tac 2);
    4.75 +   by (Fast_tac 2);
    4.76 +  by (assume_tac 2);
    4.77 + by (Asm_full_simp_tac 2);
    4.78  by (rtac weaken_A_Int_B_eq_empty 1);
    4.79  by (rtac allI 1);
    4.80  by (strip_tac 1);
    4.81  by (rtac weaken_not_elem_A_minus_B 1);
    4.82 -by (case_tac "x < m2" 1);
    4.83 -by (rtac disjI2 1);
    4.84 -by (rtac (free_tv_gen_cons RS subst) 1);
    4.85 -by (rtac free_tv_W 1);
    4.86 -by (assume_tac 1);
    4.87 -by (Asm_full_simp_tac 1);
    4.88 -by (assume_tac 1);
    4.89 +by (case_tac "x < m1" 1);
    4.90 + by (rtac disjI2 1);
    4.91 + by (rtac (free_tv_gen_cons RS subst) 1);
    4.92 + by (rtac free_tv_W 1);
    4.93 +   by (assume_tac 1);
    4.94 +  by (Asm_full_simp_tac 1);
    4.95 + by (assume_tac 1);
    4.96  by (rtac disjI1 1);
    4.97  by (dtac new_tv_W 1);
    4.98  by (assume_tac 1);
    4.99  by (dtac conjunct2 1);
   4.100 -by (dtac conjunct2 1);
   4.101  by (rtac new_tv_not_free_tv 1);
   4.102  by (rtac new_tv_le 1);
   4.103 -by (assume_tac 2);
   4.104 + by (assume_tac 2);
   4.105  by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le]) 1);
   4.106  qed_spec_mp "W_correct_lemma";
   4.107  
     5.1 --- a/src/HOL/Set.ML	Thu Mar 29 12:26:37 2001 +0200
     5.2 +++ b/src/HOL/Set.ML	Thu Mar 29 13:59:54 2001 +0200
     5.3 @@ -100,6 +100,17 @@
     5.4  
     5.5  Addsimps [ball_triv, bex_triv];
     5.6  
     5.7 +(* Blast cannot prove these (yet?).
     5.8 +   Move somewhere else?
     5.9 +Goal "(ALL x:A. x=a) = (A = {a})";
    5.10 +by(Blast_tac 1);
    5.11 +qed "ball_triv_one_point1";
    5.12 +
    5.13 +Goal "(ALL x:A. a=x) = (A = {a})";
    5.14 +by(Blast_tac 1);
    5.15 +qed "ball_triv_one_point2";
    5.16 +*)
    5.17 +
    5.18  Goal "(EX x:A. x=a) = (a:A)";
    5.19  by(Blast_tac 1);
    5.20  qed "bex_triv_one_point1";
    5.21 @@ -112,6 +123,10 @@
    5.22  by(Blast_tac 1);
    5.23  qed "bex_one_point1";
    5.24  
    5.25 +Goal "(EX x:A. a=x & P x) = (a:A & P a)";
    5.26 +by(Blast_tac 1);
    5.27 +qed "bex_one_point2";
    5.28 +
    5.29  Goal "(ALL x:A. x=a --> P x) = (a:A --> P a)";
    5.30  by(Blast_tac 1);
    5.31  qed "ball_one_point1";
    5.32 @@ -120,7 +135,8 @@
    5.33  by(Blast_tac 1);
    5.34  qed "ball_one_point2";
    5.35  
    5.36 -Addsimps [bex_triv_one_point1,bex_triv_one_point2,bex_one_point1,
    5.37 +Addsimps [bex_triv_one_point1,bex_triv_one_point2,
    5.38 +          bex_one_point1,bex_one_point2,
    5.39            ball_one_point1,ball_one_point2];
    5.40  
    5.41  let
    5.42 @@ -133,14 +149,9 @@
    5.43  val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
    5.44  
    5.45  val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
    5.46 -    ("ALL x:A. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
    5.47 +    ("ALL x:A. P(x) --> Q(x)",HOLogic.boolT)
    5.48  
    5.49 -val swap = prove_goal thy
    5.50 -  "((!x. A x & EP x --> Q x) = (!x. E x --> A x & P x --> Q x)) ==> \
    5.51 -\  ((!x. A x --> EP x --> Q x) = (!x. A x --> E x --> P x --> Q x))"
    5.52 -  (fn ths => [cut_facts_tac ths 1, Blast_tac 1]);
    5.53 -
    5.54 -val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN rtac swap 1 THEN
    5.55 +val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN
    5.56                       Quantifier1.prove_one_point_all_tac;
    5.57  
    5.58  val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
     6.1 --- a/src/HOL/W0/I.ML	Thu Mar 29 12:26:37 2001 +0200
     6.2 +++ b/src/HOL/W0/I.ML	Thu Mar 29 13:59:54 2001 +0200
     6.3 @@ -58,10 +58,12 @@
     6.4  (** LEVEL 34 **)
     6.5  by (rtac conjI 1);
     6.6   by (strip_tac 1);
     6.7 - by (mp_tac 1);
     6.8 + by (rtac notI 1);
     6.9 + by (Asm_full_simp_tac 1);
    6.10 +(* by (mp_tac 1);
    6.11   by (mp_tac 1);
    6.12   by (etac exE 1);
    6.13 - by (etac conjE 1);
    6.14 + by (etac conjE 1);*)
    6.15   by (etac impE 1);
    6.16    by ((ftac new_tv_subst_tel 1) THEN (atac 1)); 
    6.17    by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
    6.18 @@ -73,10 +75,13 @@
    6.19  by (rename_tac "s2 t2' n2'" 1);
    6.20  by (rtac conjI 1);
    6.21   by (strip_tac 1);
    6.22 + by (rtac notI 1);
    6.23 + by (Asm_full_simp_tac 1);
    6.24 +(*
    6.25   by (mp_tac 1);
    6.26   by (mp_tac 1);
    6.27   by (etac exE 1);
    6.28 - by (etac conjE 1);
    6.29 + by (etac conjE 1);*)
    6.30   by (etac impE 1);
    6.31    by ((ftac new_tv_subst_tel 1) THEN (atac 1)); 
    6.32    by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
     7.1 --- a/src/HOL/W0/W.ML	Thu Mar 29 12:26:37 2001 +0200
     7.2 +++ b/src/HOL/W0/W.ML	Thu Mar 29 13:59:54 2001 +0200
     7.3 @@ -50,7 +50,7 @@
     7.4  (* case App e1 e2 *)
     7.5  by (simp_tac (simpset() addsplits [split_bind]) 1);
     7.6  by (strip_tac 1);
     7.7 -by (rename_tac "s t na sa ta nb sb sc tb m" 1);
     7.8 +by (rename_tac "s t na sa ta nb sb" 1);
     7.9  by (eres_inst_tac [("x","a")] allE 1);
    7.10  by (eres_inst_tac [("x","n")] allE 1);
    7.11  by (eres_inst_tac [("x","$ s a")] allE 1);
    7.12 @@ -59,7 +59,6 @@
    7.13  by (eres_inst_tac [("x","na")] allE 1);
    7.14  by (eres_inst_tac [("x","na")] allE 1);
    7.15  by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
    7.16 -by (etac conjE 1);
    7.17  by (eres_inst_tac [("x","sa")] allE 1);
    7.18  by (eres_inst_tac [("x","ta")] allE 1);
    7.19  by (eres_inst_tac [("x","nb")] allE 1);
    7.20 @@ -99,7 +98,7 @@
    7.21  (* case App e1 e2 *)
    7.22  by (simp_tac (simpset() addsplits [split_bind]) 1);
    7.23  by (strip_tac 1);
    7.24 -by (rename_tac "s t na sa ta nb sb sc tb m" 1);
    7.25 +by (rename_tac "s t na sa ta nb sb" 1);
    7.26  by (eres_inst_tac [("x","n")] allE 1);
    7.27  by (eres_inst_tac [("x","a")] allE 1);
    7.28  by (eres_inst_tac [("x","s")] allE 1);
     8.1 --- a/src/HOL/simpdata.ML	Thu Mar 29 12:26:37 2001 +0200
     8.2 +++ b/src/HOL/simpdata.ML	Thu Mar 29 13:59:54 2001 +0200
     8.3 @@ -66,9 +66,12 @@
     8.4     "(P | ~P) = True",    "(~P | P) = True",
     8.5     "((~P) = (~Q)) = (P=Q)",
     8.6     "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x",
     8.7 -(*two needed for the one-point-rule quantifier simplification procs*)
     8.8 -   "(? x. x=t & P(x)) = P(t)",          (*essential for termination!!*)
     8.9 -   "(! x. t=x --> P(x)) = P(t)" ];      (*covers a stray case*)
    8.10 +(* needed for the one-point-rule quantifier simplification procs*)
    8.11 +(*essential for termination!!*)
    8.12 +   "(? x. x=t & P(x)) = P(t)",
    8.13 +   "(? x. t=x & P(x)) = P(t)",
    8.14 +   "(! x. x=t --> P(x)) = P(t)",
    8.15 +   "(! x. t=x --> P(x)) = P(t)" ];
    8.16  
    8.17  val imp_cong = standard(impI RSN
    8.18      (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
    8.19 @@ -256,6 +259,14 @@
    8.20  by (Blast_tac 1);
    8.21  qed "if_bool_eq_disj";
    8.22  
    8.23 +local
    8.24 +val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R"
    8.25 +              (fn prems => [cut_facts_tac prems 1, Blast_tac 1]);
    8.26 +
    8.27 +val iff_allI = allI RS
    8.28 +    prove_goal (the_context()) "!x. P x = Q x ==> (!x. P x) = (!x. Q x)"
    8.29 +               (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
    8.30 +in
    8.31  
    8.32  (*** make simplification procedures for quantifier elimination ***)
    8.33  
    8.34 @@ -266,28 +277,30 @@
    8.35      | dest_eq _ = None;
    8.36    fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
    8.37      | dest_conj _ = None;
    8.38 +  fun dest_imp((c as Const("op -->",_)) $ s $ t) = Some(c,s,t)
    8.39 +    | dest_imp _ = None;
    8.40    val conj = HOLogic.conj
    8.41    val imp  = HOLogic.imp
    8.42    (*rules*)
    8.43    val iff_reflection = eq_reflection
    8.44    val iffI = iffI
    8.45 -  val sym  = sym
    8.46    val conjI= conjI
    8.47    val conjE= conjE
    8.48    val impI = impI
    8.49 -  val impE = impE
    8.50    val mp   = mp
    8.51 +  val uncurry = uncurry
    8.52    val exI  = exI
    8.53    val exE  = exE
    8.54 -  val allI = allI
    8.55 -  val allE = allE
    8.56 +  val iff_allI = iff_allI
    8.57  end);
    8.58  
    8.59 +end;
    8.60 +
    8.61  local
    8.62  val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
    8.63      ("EX x. P(x) & Q(x)",HOLogic.boolT)
    8.64  val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
    8.65 -    ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
    8.66 +    ("ALL x. P(x) --> Q(x)",HOLogic.boolT)
    8.67  in
    8.68  val defEX_regroup = mk_simproc "defined EX" [ex_pattern]
    8.69        Quantifier1.rearrange_ex
     9.1 --- a/src/Provers/quantifier1.ML	Thu Mar 29 12:26:37 2001 +0200
     9.2 +++ b/src/Provers/quantifier1.ML	Thu Mar 29 13:59:54 2001 +0200
     9.3 @@ -7,7 +7,7 @@
     9.4  
     9.5              ? x. ... & x = t & ...
     9.6       into   ? x. x = t & ... & ...
     9.7 -     where the `? x. x = t &' in the latter formula is eliminated
     9.8 +     where the `? x. x = t &' in the latter formula must be eliminated
     9.9             by ordinary simplification. 
    9.10  
    9.11       and   ! x. (... & x = t & ...) --> P x
    9.12 @@ -15,10 +15,14 @@
    9.13       where the `!x. x=t -->' in the latter formula is eliminated
    9.14             by ordinary simplification.
    9.15  
    9.16 +     And analogously for t=x, but the eqn is not turned around!
    9.17 +
    9.18       NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
    9.19          "!x. x=t --> P(x)" is covered by the congreunce rule for -->;
    9.20          "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
    9.21 +        As must be "? x. t=x & P(x)".
    9.22  
    9.23 +        
    9.24       And similarly for the bounded quantifiers.
    9.25  
    9.26  Gries etc call this the "1 point rules"
    9.27 @@ -29,21 +33,20 @@
    9.28    (*abstract syntax*)
    9.29    val dest_eq: term -> (term*term*term)option
    9.30    val dest_conj: term -> (term*term*term)option
    9.31 +  val dest_imp:  term -> (term*term*term)option
    9.32    val conj: term
    9.33    val imp:  term
    9.34    (*rules*)
    9.35    val iff_reflection: thm (* P <-> Q ==> P == Q *)
    9.36    val iffI:  thm
    9.37 -  val sym:   thm
    9.38    val conjI: thm
    9.39    val conjE: thm
    9.40    val impI:  thm
    9.41 -  val impE:  thm
    9.42    val mp:    thm
    9.43    val exI:   thm
    9.44    val exE:   thm
    9.45 -  val allI:  thm
    9.46 -  val allE:  thm
    9.47 +  val uncurry: thm (* P --> Q --> R ==> P & Q --> R *)
    9.48 +  val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *)
    9.49  end;
    9.50  
    9.51  signature QUANTIFIER1 =
    9.52 @@ -61,28 +64,31 @@
    9.53  
    9.54  open Data;
    9.55  
    9.56 +(* FIXME: only test! *)
    9.57  fun def eq = case dest_eq eq of
    9.58        Some(c,s,t) =>
    9.59 -        if s = Bound 0 andalso not(loose_bvar1(t,0)) then Some eq else
    9.60 -        if t = Bound 0 andalso not(loose_bvar1(s,0)) then Some(c$t$s)
    9.61 -        else None
    9.62 -    | None => None;
    9.63 +        s = Bound 0 andalso not(loose_bvar1(t,0)) orelse
    9.64 +        t = Bound 0 andalso not(loose_bvar1(s,0))
    9.65 +    | None => false;
    9.66  
    9.67 -fun extract conj = case dest_conj conj of
    9.68 -      Some(conj,P,Q) =>
    9.69 -        (case def P of
    9.70 -           Some eq => Some(eq,Q)
    9.71 -         | None =>
    9.72 -             (case def Q of
    9.73 -                Some eq => Some(eq,P)
    9.74 -              | None =>
    9.75 -                 (case extract P of
    9.76 -                    Some(eq,P') => Some(eq, conj $ P' $ Q)
    9.77 -                  | None =>
    9.78 -                      (case extract Q of
    9.79 -                         Some(eq,Q') => Some(eq,conj $ P $ Q')
    9.80 -                       | None => None))))
    9.81 -    | None => None;
    9.82 +fun extract_conj t = case dest_conj t of None => None
    9.83 +    | Some(conj,P,Q) =>
    9.84 +        (if def P then Some(P,Q) else
    9.85 +         if def Q then Some(Q,P) else
    9.86 +         (case extract_conj P of
    9.87 +            Some(eq,P') => Some(eq, conj $ P' $ Q)
    9.88 +          | None => (case extract_conj Q of
    9.89 +                       Some(eq,Q') => Some(eq,conj $ P $ Q')
    9.90 +                     | None => None)));
    9.91 +
    9.92 +fun extract_imp t = case dest_imp t of None => None
    9.93 +    | Some(imp,P,Q) => if def P then Some(P,Q)
    9.94 +                       else (case extract_conj P of
    9.95 +                               Some(eq,P') => Some(eq, imp $ P' $ Q)
    9.96 +                             | None => (case extract_imp Q of
    9.97 +                                          None => None
    9.98 +                                        | Some(eq,Q') => Some(eq, imp$P$Q')));
    9.99 +    
   9.100  
   9.101  fun prove_conv tac sg tu =
   9.102    let val meta_eq = cterm_of sg (Logic.mk_equals tu)
   9.103 @@ -97,44 +103,44 @@
   9.104  *)
   9.105  val prove_one_point_ex_tac = rtac iffI 1 THEN
   9.106      ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
   9.107 -                    DEPTH_SOLVE_1 o (ares_tac [conjI] APPEND' etac sym)]);
   9.108 +                    DEPTH_SOLVE_1 o (ares_tac [conjI])]);
   9.109  
   9.110  (* Proves (! x. (... & x = t & ...) --> P x) =
   9.111            (! x. x = t --> (... & ...) --> P x)
   9.112  *)
   9.113 -val prove_one_point_all_tac = EVERY1[rtac iffI,
   9.114 -                       rtac allI, etac allE, rtac impI, rtac impI, etac mp,
   9.115 -                          REPEAT o (etac conjE),
   9.116 -                          REPEAT o (ares_tac [conjI] ORELSE' etac sym),
   9.117 -                       rtac allI, etac allE, rtac impI, REPEAT o (etac conjE),
   9.118 -                          etac impE, atac ORELSE' etac sym, etac mp,
   9.119 -                          REPEAT o (ares_tac [conjI])];
   9.120 +local
   9.121 +val tac = SELECT_GOAL
   9.122 +          (EVERY1[REPEAT o (dtac uncurry), REPEAT o (rtac impI), etac mp,
   9.123 +                  REPEAT o (etac conjE), REPEAT o (ares_tac [conjI])])
   9.124 +in
   9.125 +val prove_one_point_all_tac = EVERY1[rtac iff_allI, rtac iffI, tac, tac]
   9.126 +end
   9.127  
   9.128 -fun rearrange_all sg _ (F as all $ Abs(x,T,(* --> *)_ $ P $ Q)) =
   9.129 -     (case extract P of
   9.130 +fun rearrange_all sg _ (F as all $ Abs(x,T, P)) =
   9.131 +     (case extract_imp P of
   9.132          None => None
   9.133 -      | Some(eq,P') =>
   9.134 -          let val R = imp $ eq $ (imp $ P' $ Q)
   9.135 +      | Some(eq,Q) =>
   9.136 +          let val R = imp $ eq $ Q
   9.137            in Some(prove_conv prove_one_point_all_tac sg (F,all$Abs(x,T,R))) end)
   9.138    | rearrange_all _ _ _ = None;
   9.139  
   9.140 -fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,(* --> *)_ $ P $ Q)) =
   9.141 -     (case extract P of
   9.142 +fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,P)) =
   9.143 +     (case extract_imp P of
   9.144          None => None
   9.145 -      | Some(eq,P') =>
   9.146 -          let val R = imp $ eq $ (imp $ P' $ Q)
   9.147 +      | Some(eq,Q) =>
   9.148 +          let val R = imp $ eq $ Q
   9.149            in Some(prove_conv tac sg (F,Ball $ A $ Abs(x,T,R))) end)
   9.150    | rearrange_ball _ _ _ _ = None;
   9.151  
   9.152  fun rearrange_ex sg _ (F as ex $ Abs(x,T,P)) =
   9.153 -     (case extract P of
   9.154 +     (case extract_conj P of
   9.155          None => None
   9.156        | Some(eq,Q) =>
   9.157            Some(prove_conv prove_one_point_ex_tac sg (F,ex $ Abs(x,T,conj$eq$Q))))
   9.158    | rearrange_ex _ _ _ = None;
   9.159  
   9.160  fun rearrange_bex tac sg _ (F as Bex $ A $ Abs(x,T,P)) =
   9.161 -     (case extract P of
   9.162 +     (case extract_conj P of
   9.163          None => None
   9.164        | Some(eq,Q) =>
   9.165            Some(prove_conv tac sg (F,Bex $ A $ Abs(x,T,conj$eq$Q))))