author nipkow Wed, 23 Jul 1997 17:43:42 +0200 changeset 3568 36ff1ab12021 parent 3567 e2539e1980b4 child 3569 4467015d5080
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to automate reasoning about products. simpdata.ML: added simplification procedure for simplifying existential statements of the form ? x. ... & x = t & ...
 src/HOL/Prod.ML file | annotate | diff | comparison | revisions src/HOL/simpdata.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/Prod.ML	Wed Jul 23 16:03:19 1997 +0200
+++ b/src/HOL/Prod.ML	Wed Jul 23 17:43:42 1997 +0200
@@ -78,16 +78,62 @@

end;

+(* Could be nice, but breaks too many proofs:
+*)
+
+(*** lemmas for splitting paired `!!'
+Does not work with simplifier because it also affects premises in
+congrence rules, where is can lead to premises of the form
+!!a b. ... = ?P(a,b)
+which cannot be solved by reflexivity.
+
+val [prem] = goal Prod.thy "(!!x.PROP P x) ==> (!!a b. PROP P(a,b))";
+br prem 1;
+val lemma1 = result();
+
+local
+    val psig = sign_of Prod.thy;
+    val pT = Sign.read_typ (psig, K None) "?'a*?'b=>prop";
+    val PeqP = reflexive(read_cterm psig ("P", pT));
+    val psplit = zero_var_indexes(read_instantiate [("p","x")]
+                                  surjective_pairing RS eq_reflection)
+in
+val adhoc = combination PeqP psplit
+end;
+
+
+val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> PROP P x";
+br prem 1;
+val lemma = result();
+
+val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> (!!x. PROP P x)";
+br lemma 1;
+br prem 1;
+val lemma2 = result();
+
+bind_thm("split_paired_all", equal_intr lemma1 lemma2);
+***)
+
goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
by (fast_tac (!claset addbefore split_all_tac) 1);
qed "split_paired_All";
+(* AddIffs is not a good idea because it makes Blast_tac loop *)
+
+goal Prod.thy "(? x. P x) = (? a b. P(a,b))";
+by (fast_tac (!claset addbefore split_all_tac) 1);
+qed "split_paired_Ex";
+(* Addsimps [split_paired_Ex]; breaks a number of IOA proofs *)

goalw Prod.thy [split_def] "split c (a,b) = c a b";
by (EVERY1[stac fst_conv, stac snd_conv]);
by (rtac refl 1);
qed "split";

goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
by (res_inst_tac[("p","s")] PairE 1);
@@ -121,6 +167,12 @@
by (Blast_tac 1);
qed "expand_split";

+(* could be done after split_tac has been speeded up significantly:
+simpset := (!simpset setloop split_tac[expand_split]);
+   precompute the constants involved and don't do anything unless
+   the current goal contains one of those constants
+*)
+
(** split used as a logical connective or set former **)

(*These rules are for use with blast_tac.
@@ -252,7 +304,7 @@
goal Prod.thy "((a,b): Sigma A B) = (a:A & b:B(a))";
by (Blast_tac 1);
qed "mem_Sigma_iff";

(*Suggested by Pierre Chartier*)```
```--- a/src/HOL/simpdata.ML	Wed Jul 23 16:03:19 1997 +0200
+++ b/src/HOL/simpdata.ML	Wed Jul 23 17:43:42 1997 +0200
@@ -103,8 +103,8 @@
"(P | P) = P", "(P | (P | Q)) = (P | Q)",
"((~P) = (~Q)) = (P=Q)",
"(!x.P) = P", "(? x.P) = P", "? x. x=t", "? x. t=x",
-   "(? 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)" ];
+   "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)",
+   "(! x. t=x --> P(x)) = P(t)" ];

@@ -138,6 +138,52 @@
"(ALL x. P x --> Q) = ((EX x.P x) --> Q)",
"(ALL x. P --> Q x) = (P --> (ALL x.Q x))"];

+(*** Simplification procedure for turning  ? x. ... & x = t & ...
+     into                                  ? x. x = t & ... & ...
+     where the latter can be rewritten via (? x. x = t & P(x)) = P(t)
+ ***)
+
+local
+
+fun def(eq as (c as Const("op =",_)) \$ 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
+  | def _ = None;
+
+fun extract(Const("op &",_) \$ 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, HOLogic.conj \$ P' \$ Q)
+       | None => (case extract Q of
+                   Some(eq,Q') => Some(eq,HOLogic.conj \$ P \$ Q')
+                 | None => None))))
+  | extract _ = None;
+
+fun prove_eq(ceqt) =
+  let val tac = rtac eq_reflection 1 THEN rtac iffI 1 THEN
+                ALLGOALS(EVERY'[etac exE, REPEAT o (etac conjE),
+                 rtac exI, REPEAT o (ares_tac [conjI] ORELSE' etac sym)])
+  in rule_by_tactic tac (trivial ceqt) end;
+
+fun rearrange sg (F as ex \$ Abs(x,T,P)) =
+     (case extract P of
+        None => None
+      | Some(eq,Q) =>
+          let val ceqt = cterm_of sg
+                       (Logic.mk_equals(F,ex \$ Abs(x,T,HOLogic.conj\$eq\$Q)))
+          in Some(prove_eq ceqt) end)
+  | rearrange _ _ = None;
+
+val pattern = read_cterm (sign_of HOL.thy) ("? x.P(x) & Q(x)",HOLogic.boolT)
+
+in
+val defEX_regroup = mk_simproc "defined EX" [pattern] rearrange;
+end;

(* elimination of existential quantifiers in assumptions *)
@@ -314,6 +360,7 @@
de_Morgan_conj, de_Morgan_disj, not_imp,
not_all, not_ex, cases_simp]
@ ex_simps @ all_simps @ simp_thms)