src/HOL/Tools/rewrite_hol_proof.ML
changeset 13602 4cecd1e0f4a9
parent 13404 eeac2bbfe958
child 13916 f078a758e5d8
     1.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Mon Sep 30 16:14:02 2002 +0200
     1.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Mon Sep 30 16:27:38 2002 +0200
     1.3 @@ -138,6 +138,14 @@
     1.4   \    (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %%  \
     1.5   \    (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))",
     1.6  
     1.7 +   "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %%  \
     1.8 + \    (refl % TYPE(bool=>bool) % op & A)) ==  \
     1.9 + \  (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %%  \
    1.10 + \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
    1.11 + \      (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %%  \
    1.12 + \        (refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %%  \
    1.13 + \        (refl % TYPE(bool) % A)))",
    1.14 +
    1.15     (* | *)
    1.16  
    1.17     "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
    1.18 @@ -154,6 +162,14 @@
    1.19   \    (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %%  \
    1.20   \    (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))",
    1.21  
    1.22 +   "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %%  \
    1.23 + \    (refl % TYPE(bool=>bool) % op | A)) ==  \
    1.24 + \  (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %%  \
    1.25 + \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
    1.26 + \      (op | :: bool=>bool=>bool) % (op | :: bool=>bool=>bool) % A % A %%  \
    1.27 + \        (refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool)) %%  \
    1.28 + \        (refl % TYPE(bool) % A)))",
    1.29 +
    1.30     (* --> *)
    1.31  
    1.32     "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
    1.33 @@ -168,6 +184,14 @@
    1.34   \  (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %%  \
    1.35   \    (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))",
    1.36  
    1.37 +   "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %%  \
    1.38 + \    (refl % TYPE(bool=>bool) % op --> A)) ==  \
    1.39 + \  (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %%  \
    1.40 + \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
    1.41 + \      (op --> :: bool=>bool=>bool) % (op --> :: bool=>bool=>bool) % A % A %%  \
    1.42 + \        (refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool)) %%  \
    1.43 + \        (refl % TYPE(bool) % A)))",
    1.44 +
    1.45     (* ~ *)
    1.46  
    1.47     "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %%  \
    1.48 @@ -211,12 +235,12 @@
    1.49   \    (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
    1.50  
    1.51     "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
    1.52 - \    (refl % TYPE(bool) % op = A)) ==  \
    1.53 + \    (refl % TYPE(bool=>bool) % op = A)) ==  \
    1.54   \  (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
    1.55   \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
    1.56   \      (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %%  \
    1.57   \        (refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %%  \
    1.58 - \        (refl % TYPE(bool) % A % A)))",
    1.59 + \        (refl % TYPE(bool) % A)))",
    1.60  
    1.61     "(iffD1 % A % C %% (trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
    1.62   \  (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))",
    1.63 @@ -228,6 +252,10 @@
    1.64  
    1.65     "(iffD2 % A % A %% (refl % TYPE(bool) % A) %% prf) == prf",
    1.66  
    1.67 +   "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD2 % B % A %% prf)",
    1.68 +
    1.69 +   "(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD1 % B % A %% prf)",
    1.70 +
    1.71     (** normalization of HOL proofs **)
    1.72  
    1.73     "(mp % A % B %% (impI % A % B %% prf)) == prf",
    1.74 @@ -238,6 +266,10 @@
    1.75  
    1.76     "(allI % TYPE('a) % P %% (Lam x::'a. spec % TYPE('a) % P % x %% prf)) == prf",
    1.77  
    1.78 +   "(exE % TYPE('a) % P % Q %% (exI % TYPE('a) % P % x %% prf1) %% prf2) == (prf2 % x %% prf1)",
    1.79 +
    1.80 +   "(exE % TYPE('a) % P % Q %% prf %% (exI % TYPE('a) % P)) == prf",
    1.81 +
    1.82     "(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)",
    1.83  
    1.84     "(disjE % P % Q % R %% (disjI2 % Q % P %% prf1) %% prf2 %% prf3) == (prf3 %% prf1)",