Additional rules for simplifying inside "Goal"
authorberghofe
Wed Oct 31 20:00:35 2001 +0100 (2001-10-31 ago)
changeset 12002bc9b5bad0e7b
parent 12001 81be0a855397
child 12003 c09427e5f554
Additional rules for simplifying inside "Goal"
src/Pure/Proof/proof_rewrite_rules.ML
     1.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Oct 31 19:59:21 2001 +0100
     1.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Wed Oct 31 20:00:35 2001 +0100
     1.3 @@ -25,6 +25,20 @@
     1.4        (PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
     1.5            Some (equal_intr_axm % B % A %% prf2 %% prf1)
     1.6  
     1.7 +  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
     1.8 +      (PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) %
     1.9 +        _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
    1.10 +      ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
    1.11 +      Some (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
    1.12 +
    1.13 +  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
    1.14 +      (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    1.15 +        (PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) %
    1.16 +           _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
    1.17 +      ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
    1.18 +      Some (tg %> B %% (equal_elim_axm %> A %> B %%
    1.19 +        (symmetric_axm % None % None %% prf1) %% prf2))
    1.20 +
    1.21    | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
    1.22        (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
    1.23          (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %%