Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
authornipkow
Wed Jul 23 17:43:42 1997 +0200 (1997-07-23)
changeset 356836ff1ab12021
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
src/HOL/simpdata.ML
     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.33 +bw adhoc;
    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.43 +Addsimps [split_paired_all];
    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.49 +Addsimps [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.63 +Addsimps [fst_conv, snd_conv, 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.84 -Addsimps [mem_Sigma_iff]; 
    1.85 +AddIffs [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.12  (*Add congruence rules for = (instead of ==) *)
    2.13  infix 4 addcongs delcongs;
    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)
    2.71 +     addsimprocs [defEX_regroup]
    2.72       addcongs [imp_cong];
    2.73  
    2.74  qed_goal "if_distrib" HOL.thy