author nipkow Wed Jul 23 17:43:42 1997 +0200 (1997-07-23) changeset 3568 36ff1ab12021 parent 3567 e2539e1980b4 child 3569 4467015d5080

simpdata.ML: added simplification procedure for simplifying existential
statements of the form ? x. ... & x = t & ...
 src/HOL/Prod.ML file | annotate | diff | revisions src/HOL/simpdata.ML file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Prod.ML	Wed Jul 23 16:03:19 1997 +0200
1.2 +++ b/src/HOL/Prod.ML	Wed Jul 23 17:43:42 1997 +0200
1.3 @@ -78,16 +78,62 @@
1.4
1.5  end;
1.6
1.7 +(* Could be nice, but breaks too many proofs:
1.8 +claset := !claset addbefore split_all_tac;
1.9 +*)
1.10 +
1.11 +(*** lemmas for splitting paired `!!'
1.12 +Does not work with simplifier because it also affects premises in
1.13 +congrence rules, where is can lead to premises of the form
1.14 +!!a b. ... = ?P(a,b)
1.15 +which cannot be solved by reflexivity.
1.16 +
1.17 +val [prem] = goal Prod.thy "(!!x.PROP P x) ==> (!!a b. PROP P(a,b))";
1.18 +br prem 1;
1.19 +val lemma1 = result();
1.20 +
1.21 +local
1.22 +    val psig = sign_of Prod.thy;
1.23 +    val pT = Sign.read_typ (psig, K None) "?'a*?'b=>prop";
1.24 +    val PeqP = reflexive(read_cterm psig ("P", pT));
1.25 +    val psplit = zero_var_indexes(read_instantiate [("p","x")]
1.26 +                                  surjective_pairing RS eq_reflection)
1.27 +in
1.28 +val adhoc = combination PeqP psplit
1.29 +end;
1.30 +
1.31 +
1.32 +val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> PROP P x";
1.34 +br prem 1;
1.35 +val lemma = result();
1.36 +
1.37 +val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> (!!x. PROP P x)";
1.38 +br lemma 1;
1.39 +br prem 1;
1.40 +val lemma2 = result();
1.41 +
1.42 +bind_thm("split_paired_all", equal_intr lemma1 lemma2);
1.44 +***)
1.45 +
1.46  goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
1.47  by (fast_tac (!claset addbefore split_all_tac) 1);
1.48  qed "split_paired_All";
1.50 +(* AddIffs is not a good idea because it makes Blast_tac loop *)
1.51 +
1.52 +goal Prod.thy "(? x. P x) = (? a b. P(a,b))";
1.53 +by (fast_tac (!claset addbefore split_all_tac) 1);
1.54 +qed "split_paired_Ex";
1.55 +(* Addsimps [split_paired_Ex]; breaks a number of IOA proofs *)
1.56
1.57  goalw Prod.thy [split_def] "split c (a,b) = c a b";
1.58  by (EVERY1[stac fst_conv, stac snd_conv]);
1.59  by (rtac refl 1);
1.60  qed "split";
1.61
1.62 -Addsimps [fst_conv, snd_conv, split_paired_All, split];
1.64
1.65  goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
1.66  by (res_inst_tac[("p","s")] PairE 1);
1.67 @@ -121,6 +167,12 @@
1.68  by (Blast_tac 1);
1.69  qed "expand_split";
1.70
1.71 +(* could be done after split_tac has been speeded up significantly:
1.72 +simpset := (!simpset setloop split_tac[expand_split]);
1.73 +   precompute the constants involved and don't do anything unless
1.74 +   the current goal contains one of those constants
1.75 +*)
1.76 +
1.77  (** split used as a logical connective or set former **)
1.78
1.79  (*These rules are for use with blast_tac.
1.80 @@ -252,7 +304,7 @@
1.81  goal Prod.thy "((a,b): Sigma A B) = (a:A & b:B(a))";
1.82  by (Blast_tac 1);
1.83  qed "mem_Sigma_iff";
1.86
1.87
1.88  (*Suggested by Pierre Chartier*)
```
```     2.1 --- a/src/HOL/simpdata.ML	Wed Jul 23 16:03:19 1997 +0200
2.2 +++ b/src/HOL/simpdata.ML	Wed Jul 23 17:43:42 1997 +0200
2.3 @@ -103,8 +103,8 @@
2.4     "(P | P) = P", "(P | (P | Q)) = (P | Q)",
2.5     "((~P) = (~Q)) = (P=Q)",
2.6     "(!x.P) = P", "(? x.P) = P", "? x. x=t", "? x. t=x",
2.7 -   "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)",
2.8 -   "(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ];
2.9 +   "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)",
2.10 +   "(! x. t=x --> P(x)) = P(t)" ];
2.11
2.14 @@ -138,6 +138,52 @@
2.15                   "(ALL x. P x --> Q) = ((EX x.P x) --> Q)",
2.16                   "(ALL x. P --> Q x) = (P --> (ALL x.Q x))"];
2.17
2.18 +(*** Simplification procedure for turning  ? x. ... & x = t & ...
2.19 +     into                                  ? x. x = t & ... & ...
2.20 +     where the latter can be rewritten via (? x. x = t & P(x)) = P(t)
2.21 + ***)
2.22 +
2.23 +local
2.24 +
2.25 +fun def(eq as (c as Const("op =",_)) \$ s \$ t) =
2.26 +      if s = Bound 0 andalso not(loose_bvar1(t,0)) then Some eq else
2.27 +      if t = Bound 0 andalso not(loose_bvar1(s,0)) then Some(c\$t\$s)
2.28 +      else None
2.29 +  | def _ = None;
2.30 +
2.31 +fun extract(Const("op &",_) \$ P \$ Q) =
2.32 +      (case def P of
2.33 +         Some eq => Some(eq,Q)
2.34 +       | None => (case def Q of
2.35 +                   Some eq => Some(eq,P)
2.36 +                 | None =>
2.37 +       (case extract P of
2.38 +         Some(eq,P') => Some(eq, HOLogic.conj \$ P' \$ Q)
2.39 +       | None => (case extract Q of
2.40 +                   Some(eq,Q') => Some(eq,HOLogic.conj \$ P \$ Q')
2.41 +                 | None => None))))
2.42 +  | extract _ = None;
2.43 +
2.44 +fun prove_eq(ceqt) =
2.45 +  let val tac = rtac eq_reflection 1 THEN rtac iffI 1 THEN
2.46 +                ALLGOALS(EVERY'[etac exE, REPEAT o (etac conjE),
2.47 +                 rtac exI, REPEAT o (ares_tac [conjI] ORELSE' etac sym)])
2.48 +  in rule_by_tactic tac (trivial ceqt) end;
2.49 +
2.50 +fun rearrange sg (F as ex \$ Abs(x,T,P)) =
2.51 +     (case extract P of
2.52 +        None => None
2.53 +      | Some(eq,Q) =>
2.54 +          let val ceqt = cterm_of sg
2.55 +                       (Logic.mk_equals(F,ex \$ Abs(x,T,HOLogic.conj\$eq\$Q)))
2.56 +          in Some(prove_eq ceqt) end)
2.57 +  | rearrange _ _ = None;
2.58 +
2.59 +val pattern = read_cterm (sign_of HOL.thy) ("? x.P(x) & Q(x)",HOLogic.boolT)
2.60 +
2.61 +in
2.62 +val defEX_regroup = mk_simproc "defined EX" [pattern] rearrange;
2.63 +end;
2.64
2.65
2.66  (* elimination of existential quantifiers in assumptions *)
2.67 @@ -314,6 +360,7 @@
2.68         de_Morgan_conj, de_Morgan_disj, not_imp,
2.69         not_all, not_ex, cases_simp]
2.70       @ ex_simps @ all_simps @ simp_thms)