--- a/src/FOL/simpdata.ML Thu Mar 29 12:26:37 2001 +0200
+++ b/src/FOL/simpdata.ML Thu Mar 29 13:59:54 2001 +0200
@@ -218,6 +218,15 @@
"(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))";
+local
+val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R"
+ (fn prems => [cut_facts_tac prems 1, Blast_tac 1]);
+
+val iff_allI = allI RS
+ prove_goal (the_context()) "ALL x. P(x) <-> Q(x) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"
+ (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
+in
+
(** make simplification procedures for quantifier elimination **)
structure Quantifier1 = Quantifier1Fun(
struct
@@ -226,30 +235,32 @@
| dest_eq _ = None;
fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
| dest_conj _ = None;
+ fun dest_imp((c as Const("op -->",_)) $ s $ t) = Some(c,s,t)
+ | dest_imp _ = None;
val conj = FOLogic.conj
val imp = FOLogic.imp
(*rules*)
val iff_reflection = iff_reflection
val iffI = iffI
- val sym = sym
val conjI= conjI
val conjE= conjE
val impI = impI
- val impE = impE
val mp = mp
+ val uncurry = uncurry
val exI = exI
val exE = exE
- val allI = allI
- val allE = allE
+ val iff_allI = iff_allI
end);
+end;
+
local
val ex_pattern =
read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)", FOLogic.oT)
val all_pattern =
- read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
+ read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) --> Q(x)", FOLogic.oT)
in
val defEX_regroup =
--- a/src/HOL/Lex/AutoChopper.ML Thu Mar 29 12:26:37 2001 +0200
+++ b/src/HOL/Lex/AutoChopper.ML Thu Mar 29 13:59:54 2001 +0200
@@ -93,7 +93,6 @@
by (Simp_tac 1);
by (induct_tac "xs" 1);
by (simp_tac (simpset() addcongs [conj_cong]) 1);
- by (Fast_tac 1);
by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1);
by (rename_tac "vss lrst" 1);
@@ -116,7 +115,6 @@
by (Simp_tac 1);
by (induct_tac "xs" 1);
by (simp_tac (simpset() addcongs [conj_cong]) 1);
- by (Fast_tac 1);
by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
by (strip_tac 1);
by (rtac conjI 1);
@@ -155,7 +153,6 @@
by (Simp_tac 1);
by (induct_tac "xs" 1);
by (simp_tac (simpset() addcongs [conj_cong]) 1);
- by (Fast_tac 1);
by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
by (res_inst_tac [("p","acc A (start A) ([],list) [] list []")] PairE 1);
by (rename_tac "vss lrst" 1);
@@ -193,7 +190,6 @@
by (Simp_tac 1);
by (induct_tac "xs" 1);
by (simp_tac (simpset() addcongs [conj_cong]) 1);
- by (Fast_tac 1);
by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
by (strip_tac 1);
by (case_tac "acc_prefix A list (next A a st)" 1);
--- a/src/HOL/Lex/RegExp2NAe.ML Thu Mar 29 12:26:37 2001 +0200
+++ b/src/HOL/Lex/RegExp2NAe.ML Thu Mar 29 13:59:54 2001 +0200
@@ -396,7 +396,7 @@
\ (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & \
\ (? s. (start R,s) : steps R v & q = False#s))))";
by (blast_tac (claset() addDs [True_steps_concD]
- addIs [True_True_steps_concI,in_steps_epsclosure,r_into_rtrancl]) 1);
+ addIs [True_True_steps_concI,in_steps_epsclosure]) 1);
qed "True_steps_conc";
(** starting from the start **)
@@ -537,7 +537,7 @@
by (induct_tac "us" 1);
by (Simp_tac 1);
by (Simp_tac 1);
-by (blast_tac (claset() addIs [True_True_steps_starI,True_start_eps_starI,r_into_rtrancl,in_epsclosure_steps]) 1);
+by (blast_tac (claset() addIs [True_True_steps_starI,True_start_eps_starI,in_epsclosure_steps]) 1);
qed_spec_mp "steps_star_cycle";
(* Better stated directly with start(star A)? Loop in star A back to start(star A)?*)
@@ -578,7 +578,7 @@
by (Blast_tac 1);
by (etac disjE 1);
by (Asm_simp_tac 1);
-by (blast_tac (claset() addIs [in_steps_epsclosure,r_into_rtrancl]) 1);
+by (blast_tac (claset() addIs [in_steps_epsclosure]) 1);
qed "start_steps_star";
Goalw [star_def] "!A. fin (star A) (True#p) = fin A p";
--- a/src/HOL/MiniML/W.ML Thu Mar 29 12:26:37 2001 +0200
+++ b/src/HOL/MiniML/W.ML Thu Mar 29 13:59:54 2001 +0200
@@ -317,63 +317,61 @@
(* case Let e1 e2 *)
by (simp_tac (simpset() addsplits [split_option_bind]) 1);
by (strip_tac 1);
-by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1);
+(*by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); *)
+by (rename_tac "S1 t1 m1 S2" 1);
by (res_inst_tac [("t1.0","$ S2 t1")] has_type.LETI 1);
-by (simp_tac (simpset() addsimps [o_def]) 1);
-by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
-by (rtac (has_type_cl_sub RS spec) 1);
-by (dres_inst_tac [("x","A")] spec 1);
-by (dres_inst_tac [("x","S1")] spec 1);
-by (dres_inst_tac [("x","t1")] spec 1);
-by (dres_inst_tac [("x","m2")] spec 1);
-by (rotate_tac 4 1);
-by (dres_inst_tac [("x","m1")] spec 1);
-by (mp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
+ by (simp_tac (simpset() addsimps [o_def]) 1);
+ by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
+ by (rtac (has_type_cl_sub RS spec) 1);
+ by (dres_inst_tac [("x","A")] spec 1);
+ by (dres_inst_tac [("x","S1")] spec 1);
+ by (dres_inst_tac [("x","t1")] spec 1);
+ by (dres_inst_tac [("x","m1")] spec 1);
+ by (dres_inst_tac [("x","n")] spec 1);
+ by (mp_tac 1);
+ by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
by (simp_tac (simpset() addsimps [o_def]) 1);
by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
by (rtac (gen_subst_commutes RS sym RS subst) 1);
-by (rtac (app_subst_Cons RS subst) 2);
-by (etac thin_rl 2);
-by (dres_inst_tac [("x","gen ($S1 A) t1 # $ S1 A")] spec 2);
-by (dres_inst_tac [("x","S2")] spec 2);
-by (dres_inst_tac [("x","t")] spec 2);
-by (dres_inst_tac [("x","n2")] spec 2);
-by (dres_inst_tac [("x","m2")] spec 2);
-by (ftac new_tv_W 2);
-by (assume_tac 2);
-by (dtac conjunct1 2);
-by (dtac conjunct1 2);
-by (ftac new_tv_subst_scheme_list 2);
-by (rtac new_scheme_list_le 2);
-by (rtac W_var_ge 2);
-by (assume_tac 2);
-by (assume_tac 2);
-by (etac impE 2);
-by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2);
-by (Simp_tac 2);
-by (Fast_tac 2);
-by (assume_tac 2);
-by (Asm_full_simp_tac 2);
+ by (rtac (app_subst_Cons RS subst) 2);
+ by (etac thin_rl 2);
+ by (dres_inst_tac [("x","gen ($S1 A) t1 # $ S1 A")] spec 2);
+ by (dres_inst_tac [("x","S2")] spec 2);
+ by (dres_inst_tac [("x","t")] spec 2);
+ by (dres_inst_tac [("x","m")] spec 2);
+ by (dres_inst_tac [("x","m1")] spec 2);
+ by (ftac new_tv_W 2);
+ by (assume_tac 2);
+ by (dtac conjunct1 2);
+ by (ftac new_tv_subst_scheme_list 2);
+ by (rtac new_scheme_list_le 2);
+ by (rtac W_var_ge 2);
+ by (assume_tac 2);
+ by (assume_tac 2);
+ by (etac impE 2);
+ by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2);
+ by (Simp_tac 2);
+ by (Fast_tac 2);
+ by (assume_tac 2);
+ by (Asm_full_simp_tac 2);
by (rtac weaken_A_Int_B_eq_empty 1);
by (rtac allI 1);
by (strip_tac 1);
by (rtac weaken_not_elem_A_minus_B 1);
-by (case_tac "x < m2" 1);
-by (rtac disjI2 1);
-by (rtac (free_tv_gen_cons RS subst) 1);
-by (rtac free_tv_W 1);
-by (assume_tac 1);
-by (Asm_full_simp_tac 1);
-by (assume_tac 1);
+by (case_tac "x < m1" 1);
+ by (rtac disjI2 1);
+ by (rtac (free_tv_gen_cons RS subst) 1);
+ by (rtac free_tv_W 1);
+ by (assume_tac 1);
+ by (Asm_full_simp_tac 1);
+ by (assume_tac 1);
by (rtac disjI1 1);
by (dtac new_tv_W 1);
by (assume_tac 1);
by (dtac conjunct2 1);
-by (dtac conjunct2 1);
by (rtac new_tv_not_free_tv 1);
by (rtac new_tv_le 1);
-by (assume_tac 2);
+ by (assume_tac 2);
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le]) 1);
qed_spec_mp "W_correct_lemma";
--- a/src/HOL/Set.ML Thu Mar 29 12:26:37 2001 +0200
+++ b/src/HOL/Set.ML Thu Mar 29 13:59:54 2001 +0200
@@ -100,6 +100,17 @@
Addsimps [ball_triv, bex_triv];
+(* Blast cannot prove these (yet?).
+ Move somewhere else?
+Goal "(ALL x:A. x=a) = (A = {a})";
+by(Blast_tac 1);
+qed "ball_triv_one_point1";
+
+Goal "(ALL x:A. a=x) = (A = {a})";
+by(Blast_tac 1);
+qed "ball_triv_one_point2";
+*)
+
Goal "(EX x:A. x=a) = (a:A)";
by(Blast_tac 1);
qed "bex_triv_one_point1";
@@ -112,6 +123,10 @@
by(Blast_tac 1);
qed "bex_one_point1";
+Goal "(EX x:A. a=x & P x) = (a:A & P a)";
+by(Blast_tac 1);
+qed "bex_one_point2";
+
Goal "(ALL x:A. x=a --> P x) = (a:A --> P a)";
by(Blast_tac 1);
qed "ball_one_point1";
@@ -120,7 +135,8 @@
by(Blast_tac 1);
qed "ball_one_point2";
-Addsimps [bex_triv_one_point1,bex_triv_one_point2,bex_one_point1,
+Addsimps [bex_triv_one_point1,bex_triv_one_point2,
+ bex_one_point1,bex_one_point2,
ball_one_point1,ball_one_point2];
let
@@ -133,14 +149,9 @@
val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
- ("ALL x:A. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
+ ("ALL x:A. P(x) --> Q(x)",HOLogic.boolT)
-val swap = prove_goal thy
- "((!x. A x & EP x --> Q x) = (!x. E x --> A x & P x --> Q x)) ==> \
-\ ((!x. A x --> EP x --> Q x) = (!x. A x --> E x --> P x --> Q x))"
- (fn ths => [cut_facts_tac ths 1, Blast_tac 1]);
-
-val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN rtac swap 1 THEN
+val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN
Quantifier1.prove_one_point_all_tac;
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
--- a/src/HOL/W0/I.ML Thu Mar 29 12:26:37 2001 +0200
+++ b/src/HOL/W0/I.ML Thu Mar 29 13:59:54 2001 +0200
@@ -58,10 +58,12 @@
(** LEVEL 34 **)
by (rtac conjI 1);
by (strip_tac 1);
- by (mp_tac 1);
+ by (rtac notI 1);
+ by (Asm_full_simp_tac 1);
+(* by (mp_tac 1);
by (mp_tac 1);
by (etac exE 1);
- by (etac conjE 1);
+ by (etac conjE 1);*)
by (etac impE 1);
by ((ftac new_tv_subst_tel 1) THEN (atac 1));
by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
@@ -73,10 +75,13 @@
by (rename_tac "s2 t2' n2'" 1);
by (rtac conjI 1);
by (strip_tac 1);
+ by (rtac notI 1);
+ by (Asm_full_simp_tac 1);
+(*
by (mp_tac 1);
by (mp_tac 1);
by (etac exE 1);
- by (etac conjE 1);
+ by (etac conjE 1);*)
by (etac impE 1);
by ((ftac new_tv_subst_tel 1) THEN (atac 1));
by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
--- a/src/HOL/W0/W.ML Thu Mar 29 12:26:37 2001 +0200
+++ b/src/HOL/W0/W.ML Thu Mar 29 13:59:54 2001 +0200
@@ -50,7 +50,7 @@
(* case App e1 e2 *)
by (simp_tac (simpset() addsplits [split_bind]) 1);
by (strip_tac 1);
-by (rename_tac "s t na sa ta nb sb sc tb m" 1);
+by (rename_tac "s t na sa ta nb sb" 1);
by (eres_inst_tac [("x","a")] allE 1);
by (eres_inst_tac [("x","n")] allE 1);
by (eres_inst_tac [("x","$ s a")] allE 1);
@@ -59,7 +59,6 @@
by (eres_inst_tac [("x","na")] allE 1);
by (eres_inst_tac [("x","na")] allE 1);
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
-by (etac conjE 1);
by (eres_inst_tac [("x","sa")] allE 1);
by (eres_inst_tac [("x","ta")] allE 1);
by (eres_inst_tac [("x","nb")] allE 1);
@@ -99,7 +98,7 @@
(* case App e1 e2 *)
by (simp_tac (simpset() addsplits [split_bind]) 1);
by (strip_tac 1);
-by (rename_tac "s t na sa ta nb sb sc tb m" 1);
+by (rename_tac "s t na sa ta nb sb" 1);
by (eres_inst_tac [("x","n")] allE 1);
by (eres_inst_tac [("x","a")] allE 1);
by (eres_inst_tac [("x","s")] allE 1);
--- a/src/HOL/simpdata.ML Thu Mar 29 12:26:37 2001 +0200
+++ b/src/HOL/simpdata.ML Thu Mar 29 13:59:54 2001 +0200
@@ -66,9 +66,12 @@
"(P | ~P) = True", "(~P | P) = True",
"((~P) = (~Q)) = (P=Q)",
"(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x",
-(*two needed for the one-point-rule quantifier simplification procs*)
- "(? x. x=t & P(x)) = P(t)", (*essential for termination!!*)
- "(! x. t=x --> P(x)) = P(t)" ]; (*covers a stray case*)
+(* needed for the one-point-rule quantifier simplification procs*)
+(*essential for termination!!*)
+ "(? x. x=t & P(x)) = P(t)",
+ "(? x. t=x & P(x)) = P(t)",
+ "(! x. x=t --> P(x)) = P(t)",
+ "(! x. t=x --> P(x)) = P(t)" ];
val imp_cong = standard(impI RSN
(2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
@@ -256,6 +259,14 @@
by (Blast_tac 1);
qed "if_bool_eq_disj";
+local
+val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R"
+ (fn prems => [cut_facts_tac prems 1, Blast_tac 1]);
+
+val iff_allI = allI RS
+ prove_goal (the_context()) "!x. P x = Q x ==> (!x. P x) = (!x. Q x)"
+ (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
+in
(*** make simplification procedures for quantifier elimination ***)
@@ -266,28 +277,30 @@
| dest_eq _ = None;
fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
| dest_conj _ = None;
+ fun dest_imp((c as Const("op -->",_)) $ s $ t) = Some(c,s,t)
+ | dest_imp _ = None;
val conj = HOLogic.conj
val imp = HOLogic.imp
(*rules*)
val iff_reflection = eq_reflection
val iffI = iffI
- val sym = sym
val conjI= conjI
val conjE= conjE
val impI = impI
- val impE = impE
val mp = mp
+ val uncurry = uncurry
val exI = exI
val exE = exE
- val allI = allI
- val allE = allE
+ val iff_allI = iff_allI
end);
+end;
+
local
val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
("EX x. P(x) & Q(x)",HOLogic.boolT)
val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
- ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
+ ("ALL x. P(x) --> Q(x)",HOLogic.boolT)
in
val defEX_regroup = mk_simproc "defined EX" [ex_pattern]
Quantifier1.rearrange_ex
--- a/src/Provers/quantifier1.ML Thu Mar 29 12:26:37 2001 +0200
+++ b/src/Provers/quantifier1.ML Thu Mar 29 13:59:54 2001 +0200
@@ -7,7 +7,7 @@
? x. ... & x = t & ...
into ? x. x = t & ... & ...
- where the `? x. x = t &' in the latter formula is eliminated
+ where the `? x. x = t &' in the latter formula must be eliminated
by ordinary simplification.
and ! x. (... & x = t & ...) --> P x
@@ -15,10 +15,14 @@
where the `!x. x=t -->' in the latter formula is eliminated
by ordinary simplification.
+ And analogously for t=x, but the eqn is not turned around!
+
NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
"!x. x=t --> P(x)" is covered by the congreunce rule for -->;
"!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
+ As must be "? x. t=x & P(x)".
+
And similarly for the bounded quantifiers.
Gries etc call this the "1 point rules"
@@ -29,21 +33,20 @@
(*abstract syntax*)
val dest_eq: term -> (term*term*term)option
val dest_conj: term -> (term*term*term)option
+ val dest_imp: term -> (term*term*term)option
val conj: term
val imp: term
(*rules*)
val iff_reflection: thm (* P <-> Q ==> P == Q *)
val iffI: thm
- val sym: thm
val conjI: thm
val conjE: thm
val impI: thm
- val impE: thm
val mp: thm
val exI: thm
val exE: thm
- val allI: thm
- val allE: thm
+ val uncurry: thm (* P --> Q --> R ==> P & Q --> R *)
+ val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *)
end;
signature QUANTIFIER1 =
@@ -61,28 +64,31 @@
open Data;
+(* FIXME: only test! *)
fun def eq = case dest_eq eq of
Some(c,s,t) =>
- if s = Bound 0 andalso not(loose_bvar1(t,0)) then Some eq else
- if t = Bound 0 andalso not(loose_bvar1(s,0)) then Some(c$t$s)
- else None
- | None => None;
+ s = Bound 0 andalso not(loose_bvar1(t,0)) orelse
+ t = Bound 0 andalso not(loose_bvar1(s,0))
+ | None => false;
-fun extract conj = case dest_conj conj of
- Some(conj,P,Q) =>
- (case def P of
- Some eq => Some(eq,Q)
- | None =>
- (case def Q of
- Some eq => Some(eq,P)
- | None =>
- (case extract P of
- Some(eq,P') => Some(eq, conj $ P' $ Q)
- | None =>
- (case extract Q of
- Some(eq,Q') => Some(eq,conj $ P $ Q')
- | None => None))))
- | None => None;
+fun extract_conj t = case dest_conj t of None => None
+ | Some(conj,P,Q) =>
+ (if def P then Some(P,Q) else
+ if def Q then Some(Q,P) else
+ (case extract_conj P of
+ Some(eq,P') => Some(eq, conj $ P' $ Q)
+ | None => (case extract_conj Q of
+ Some(eq,Q') => Some(eq,conj $ P $ Q')
+ | None => None)));
+
+fun extract_imp t = case dest_imp t of None => None
+ | Some(imp,P,Q) => if def P then Some(P,Q)
+ else (case extract_conj P of
+ Some(eq,P') => Some(eq, imp $ P' $ Q)
+ | None => (case extract_imp Q of
+ None => None
+ | Some(eq,Q') => Some(eq, imp$P$Q')));
+
fun prove_conv tac sg tu =
let val meta_eq = cterm_of sg (Logic.mk_equals tu)
@@ -97,44 +103,44 @@
*)
val prove_one_point_ex_tac = rtac iffI 1 THEN
ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
- DEPTH_SOLVE_1 o (ares_tac [conjI] APPEND' etac sym)]);
+ DEPTH_SOLVE_1 o (ares_tac [conjI])]);
(* Proves (! x. (... & x = t & ...) --> P x) =
(! x. x = t --> (... & ...) --> P x)
*)
-val prove_one_point_all_tac = EVERY1[rtac iffI,
- rtac allI, etac allE, rtac impI, rtac impI, etac mp,
- REPEAT o (etac conjE),
- REPEAT o (ares_tac [conjI] ORELSE' etac sym),
- rtac allI, etac allE, rtac impI, REPEAT o (etac conjE),
- etac impE, atac ORELSE' etac sym, etac mp,
- REPEAT o (ares_tac [conjI])];
+local
+val tac = SELECT_GOAL
+ (EVERY1[REPEAT o (dtac uncurry), REPEAT o (rtac impI), etac mp,
+ REPEAT o (etac conjE), REPEAT o (ares_tac [conjI])])
+in
+val prove_one_point_all_tac = EVERY1[rtac iff_allI, rtac iffI, tac, tac]
+end
-fun rearrange_all sg _ (F as all $ Abs(x,T,(* --> *)_ $ P $ Q)) =
- (case extract P of
+fun rearrange_all sg _ (F as all $ Abs(x,T, P)) =
+ (case extract_imp P of
None => None
- | Some(eq,P') =>
- let val R = imp $ eq $ (imp $ P' $ Q)
+ | Some(eq,Q) =>
+ let val R = imp $ eq $ Q
in Some(prove_conv prove_one_point_all_tac sg (F,all$Abs(x,T,R))) end)
| rearrange_all _ _ _ = None;
-fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,(* --> *)_ $ P $ Q)) =
- (case extract P of
+fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,P)) =
+ (case extract_imp P of
None => None
- | Some(eq,P') =>
- let val R = imp $ eq $ (imp $ P' $ Q)
+ | Some(eq,Q) =>
+ let val R = imp $ eq $ Q
in Some(prove_conv tac sg (F,Ball $ A $ Abs(x,T,R))) end)
| rearrange_ball _ _ _ _ = None;
fun rearrange_ex sg _ (F as ex $ Abs(x,T,P)) =
- (case extract P of
+ (case extract_conj P of
None => None
| Some(eq,Q) =>
Some(prove_conv prove_one_point_ex_tac sg (F,ex $ Abs(x,T,conj$eq$Q))))
| rearrange_ex _ _ _ = None;
fun rearrange_bex tac sg _ (F as Bex $ A $ Abs(x,T,P)) =
- (case extract P of
+ (case extract_conj P of
None => None
| Some(eq,Q) =>
Some(prove_conv tac sg (F,Bex $ A $ Abs(x,T,conj$eq$Q))))