Added miniscoping to the simplifier: quantifiers are now pushed in
authorpaulson
Thu Sep 05 10:23:55 1996 +0200 (1996-09-05)
changeset 194878e5bfcbc1e9
parent 1947 f19a801a2bca
child 1949 1badf0b08040
Added miniscoping to the simplifier: quantifiers are now pushed in
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Tue Sep 03 19:07:23 1996 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Thu Sep 05 10:23:55 1996 +0200
     1.3 @@ -71,6 +71,7 @@
     1.4       "(P & False) = False", "(False & P) = False", "(P & P) = P",
     1.5       "(P | True) = True", "(True | P) = True", 
     1.6       "(P | False) = P", "(False | P) = P", "(P | P) = P",
     1.7 +     "((~P) = (~Q)) = (P=Q)",
     1.8       "(!x.P) = P", "(? x.P) = P", "? x. x=t", 
     1.9       "(? x. x=t & P(x)) = P(t)", "(! x. x=t --> P(x)) = P(t)" ];
    1.10  
    1.11 @@ -87,6 +88,9 @@
    1.12  
    1.13  val imp_disj   = prover "(P|Q --> R) = ((P-->R)&(Q-->R))";
    1.14  
    1.15 +(*Avoids duplication of subgoals after expand_if, when the true and false 
    1.16 +  cases boil down to the same thing.*) 
    1.17 +val cases_simp = prover "((P --> Q) & (~P --> Q)) = Q";
    1.18  
    1.19  val if_True = prove_goalw HOL.thy [if_def] "(if True then x else y) = x"
    1.20   (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
    1.21 @@ -131,18 +135,37 @@
    1.22  val o_apply = prove_goalw HOL.thy [o_def] "(f o g)(x) = f(g(x))"
    1.23   (fn _ => [rtac refl 1]);
    1.24  
    1.25 +(*Miniscoping: pushing in existential quantifiers*)
    1.26 +val ex_simps = map prover 
    1.27 +		["(EX x. P x & Q)   = ((EX x.P x) & Q)",
    1.28 +		 "(EX x. P & Q x)   = (P & (EX x.Q x))",
    1.29 +		 "(EX x. P x | Q)   = ((EX x.P x) | Q)",
    1.30 +		 "(EX x. P | Q x)   = (P | (EX x.Q x))",
    1.31 +		 "(EX x. P x --> Q) = ((ALL x.P x) --> Q)",
    1.32 +		 "(EX x. P --> Q x) = (P --> (EX x.Q x))"];
    1.33 +
    1.34 +(*Miniscoping: pushing in universal quantifiers*)
    1.35 +val all_simps = map prover
    1.36 +		["(ALL x. P x & Q)   = ((ALL x.P x) & Q)",
    1.37 +		 "(ALL x. P & Q x)   = (P & (ALL x.Q x))",
    1.38 +		 "(ALL x. P x | Q)   = ((ALL x.P x) | Q)",
    1.39 +		 "(ALL x. P | Q x)   = (P | (ALL x.Q x))",
    1.40 +		 "(ALL x. P x --> Q) = ((EX x.P x) --> Q)",
    1.41 +		 "(ALL x. P --> Q x) = (P --> (ALL x.Q x))"];
    1.42 +
    1.43  val HOL_ss = empty_ss
    1.44        setmksimps (mksimps mksimps_pairs)
    1.45        setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
    1.46                               ORELSE' etac FalseE)
    1.47        setsubgoaler asm_simp_tac
    1.48 -      addsimps ([if_True, if_False, o_apply, imp_disj, conj_assoc, disj_assoc]
    1.49 -        @ simp_thms)
    1.50 +      addsimps ([if_True, if_False, o_apply, imp_disj, conj_assoc, disj_assoc,
    1.51 +		 cases_simp]
    1.52 +        @ ex_simps @ all_simps @ simp_thms)
    1.53        addcongs [imp_cong];
    1.54  
    1.55  
    1.56  (*In general it seems wrong to add distributive laws by default: they
    1.57 -  might cause exponential blow-up.  This one has been added for a while
    1.58 +  might cause exponential blow-up.  But imp_disj has been in for a while
    1.59    and cannot be removed without affecting existing proofs.  Moreover, 
    1.60    rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
    1.61    grounds that it allows simplification of R in the two cases.*)