# HG changeset patch
# User berghofe
# Date 1033396058 -7200
# Node ID 4cecd1e0f4a98801e6b28e299eb0a6283b05d392
# Parent  fd3e3d6b37b28ba6b98738e58d903b09556426b5
- additional congruence rules for boolean operators
- additional rewrite rules for exI / exE

diff -r fd3e3d6b37b2 -r 4cecd1e0f4a9 src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Mon Sep 30 16:14:02 2002 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Mon Sep 30 16:27:38 2002 +0200
@@ -138,6 +138,14 @@
  \    (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %%  \
  \    (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))",
 
+   "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %%  \
+ \    (refl % TYPE(bool=>bool) % op & A)) ==  \
+ \  (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %%  \
+ \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
+ \      (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %%  \
+ \        (refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %%  \
+ \        (refl % TYPE(bool) % A)))",
+
    (* | *)
 
    "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
@@ -154,6 +162,14 @@
  \    (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %%  \
  \    (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))",
 
+   "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %%  \
+ \    (refl % TYPE(bool=>bool) % op | A)) ==  \
+ \  (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %%  \
+ \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
+ \      (op | :: bool=>bool=>bool) % (op | :: bool=>bool=>bool) % A % A %%  \
+ \        (refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool)) %%  \
+ \        (refl % TYPE(bool) % A)))",
+
    (* --> *)
 
    "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
@@ -168,6 +184,14 @@
  \  (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %%  \
  \    (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))",
 
+   "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %%  \
+ \    (refl % TYPE(bool=>bool) % op --> A)) ==  \
+ \  (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %%  \
+ \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
+ \      (op --> :: bool=>bool=>bool) % (op --> :: bool=>bool=>bool) % A % A %%  \
+ \        (refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool)) %%  \
+ \        (refl % TYPE(bool) % A)))",
+
    (* ~ *)
 
    "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %%  \
@@ -211,12 +235,12 @@
  \    (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
 
    "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
- \    (refl % TYPE(bool) % op = A)) ==  \
+ \    (refl % TYPE(bool=>bool) % op = A)) ==  \
  \  (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
  \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
  \      (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %%  \
  \        (refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %%  \
- \        (refl % TYPE(bool) % A % A)))",
+ \        (refl % TYPE(bool) % A)))",
 
    "(iffD1 % A % C %% (trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
  \  (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))",
@@ -228,6 +252,10 @@
 
    "(iffD2 % A % A %% (refl % TYPE(bool) % A) %% prf) == prf",
 
+   "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD2 % B % A %% prf)",
+
+   "(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD1 % B % A %% prf)",
+
    (** normalization of HOL proofs **)
 
    "(mp % A % B %% (impI % A % B %% prf)) == prf",
@@ -238,6 +266,10 @@
 
    "(allI % TYPE('a) % P %% (Lam x::'a. spec % TYPE('a) % P % x %% prf)) == prf",
 
+   "(exE % TYPE('a) % P % Q %% (exI % TYPE('a) % P % x %% prf1) %% prf2) == (prf2 % x %% prf1)",
+
+   "(exE % TYPE('a) % P % Q %% prf %% (exI % TYPE('a) % P)) == prf",
+
    "(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)",
 
    "(disjE % P % Q % R %% (disjI2 % Q % P %% prf1) %% prf2 %% prf3) == (prf3 %% prf1)",