src/HOL/Tools/rewrite_hol_proof.ML
changeset 15530 6f43714517ee
parent 14981 e73f8140af78
child 15531 08c8dad8e399
     1.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Fri Feb 11 17:11:24 2005 +0100
     1.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Fri Feb 11 18:51:00 2005 +0100
     1.3 @@ -41,12 +41,12 @@
     1.4  
     1.5     "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %%  \
     1.6   \    (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) ==  \
     1.7 - \  (trans % TYPE('T) % x % y % z %%  \
     1.8 + \  (HOL.trans % TYPE('T) % x % y % z %%  \
     1.9   \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf1) %%  \
    1.10   \    (meta_eq_to_obj_eq % TYPE('T) % y % z %% prf2))",
    1.11  
    1.12     "(meta_eq_to_obj_eq % TYPE('T) % x % x %% (axm.reflexive % TYPE('T) % x)) ==  \
    1.13 - \  (refl % TYPE('T) % x)",
    1.14 + \  (HOL.refl % TYPE('T) % x)",
    1.15  
    1.16     "(meta_eq_to_obj_eq % TYPE('T) % x % y %%  \
    1.17   \    (axm.symmetric % TYPE('T) % x % y %% prf)) ==  \
    1.18 @@ -68,7 +68,7 @@
    1.19   \    (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %%  \
    1.20   \      (cong % TYPE('T=>bool) % TYPE('T) %  \
    1.21   \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
    1.22 - \        (refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
    1.23 + \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
    1.24   \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
    1.25   \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %%  \
    1.26   \    (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))",
    1.27 @@ -82,7 +82,7 @@
    1.28   \    (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %%  \
    1.29   \      (cong % TYPE('T=>bool) % TYPE('T) %  \
    1.30   \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
    1.31 - \        (refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
    1.32 + \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
    1.33   \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
    1.34   \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %%  \
    1.35   \    (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))",
    1.36 @@ -92,14 +92,14 @@
    1.37     (* All *)
    1.38  
    1.39     "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %%  \
    1.40 - \    (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
    1.41 + \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
    1.42   \  (allI % TYPE('a) % Q %%  \
    1.43   \    (Lam x.  \
    1.44   \        iffD1 % P x % Q x %% (prf % x) %%  \
    1.45   \         (spec % TYPE('a) % P % x %% prf')))",
    1.46  
    1.47     "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %%  \
    1.48 - \    (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
    1.49 + \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
    1.50   \  (allI % TYPE('a) % P %%  \
    1.51   \    (Lam x.  \
    1.52   \        iffD2 % P x % Q x %% (prf % x) %%  \
    1.53 @@ -108,14 +108,14 @@
    1.54     (* Ex *)
    1.55  
    1.56     "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %%  \
    1.57 - \    (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
    1.58 + \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
    1.59   \  (exE % TYPE('a) % P % EX x. Q x %% prf' %%  \
    1.60   \    (Lam x H : P x.  \
    1.61   \        exI % TYPE('a) % Q % x %%  \
    1.62   \         (iffD1 % P x % Q x %% (prf % x) %% H)))",
    1.63  
    1.64     "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %%  \
    1.65 - \    (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
    1.66 + \    (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
    1.67   \  (exE % TYPE('a) % Q % EX x. P x %% prf' %%  \
    1.68   \    (Lam x H : Q x.  \
    1.69   \        exI % TYPE('a) % P % x %%  \
    1.70 @@ -125,81 +125,81 @@
    1.71  
    1.72     "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
    1.73   \    (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %%  \
    1.74 - \      (refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) ==  \
    1.75 + \      (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) ==  \
    1.76   \  (conjI % B % D %%  \
    1.77   \    (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %%  \
    1.78   \    (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))",
    1.79  
    1.80     "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
    1.81   \    (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %%  \
    1.82 - \      (refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) ==  \
    1.83 + \      (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) ==  \
    1.84   \  (conjI % A % C %%  \
    1.85   \    (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %%  \
    1.86   \    (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))",
    1.87  
    1.88     "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %%  \
    1.89 - \    (refl % TYPE(bool=>bool) % op & A)) ==  \
    1.90 + \    (HOL.refl % TYPE(bool=>bool) % op & A)) ==  \
    1.91   \  (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %%  \
    1.92   \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
    1.93   \      (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %%  \
    1.94 - \        (refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %%  \
    1.95 - \        (refl % TYPE(bool) % A)))",
    1.96 + \        (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %%  \
    1.97 + \        (HOL.refl % TYPE(bool) % A)))",
    1.98  
    1.99     (* | *)
   1.100  
   1.101     "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   1.102   \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %%  \
   1.103 - \      (refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) ==  \
   1.104 + \      (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) ==  \
   1.105   \  (disjE % A % C % B | D %% prf3 %%  \
   1.106   \    (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %%  \
   1.107   \    (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))",
   1.108  
   1.109     "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   1.110   \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %%  \
   1.111 - \      (refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) ==  \
   1.112 + \      (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) ==  \
   1.113   \  (disjE % B % D % A | C %% prf3 %%  \
   1.114   \    (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %%  \
   1.115   \    (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))",
   1.116  
   1.117     "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %%  \
   1.118 - \    (refl % TYPE(bool=>bool) % op | A)) ==  \
   1.119 + \    (HOL.refl % TYPE(bool=>bool) % op | A)) ==  \
   1.120   \  (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %%  \
   1.121   \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
   1.122   \      (op | :: bool=>bool=>bool) % (op | :: bool=>bool=>bool) % A % A %%  \
   1.123 - \        (refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool)) %%  \
   1.124 - \        (refl % TYPE(bool) % A)))",
   1.125 + \        (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool)) %%  \
   1.126 + \        (HOL.refl % TYPE(bool) % A)))",
   1.127  
   1.128     (* --> *)
   1.129  
   1.130     "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   1.131   \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %%  \
   1.132 - \      (refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) ==  \
   1.133 + \      (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) ==  \
   1.134   \  (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %%  \
   1.135   \    (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))",
   1.136  
   1.137     "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   1.138   \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %%  \
   1.139 - \      (refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) ==  \
   1.140 + \      (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) ==  \
   1.141   \  (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %%  \
   1.142   \    (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))",
   1.143  
   1.144     "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %%  \
   1.145 - \    (refl % TYPE(bool=>bool) % op --> A)) ==  \
   1.146 + \    (HOL.refl % TYPE(bool=>bool) % op --> A)) ==  \
   1.147   \  (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %%  \
   1.148   \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
   1.149   \      (op --> :: bool=>bool=>bool) % (op --> :: bool=>bool=>bool) % A % A %%  \
   1.150 - \        (refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool)) %%  \
   1.151 - \        (refl % TYPE(bool) % A)))",
   1.152 + \        (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool)) %%  \
   1.153 + \        (HOL.refl % TYPE(bool) % A)))",
   1.154  
   1.155     (* ~ *)
   1.156  
   1.157     "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %%  \
   1.158 - \    (refl % TYPE('T3) % Not) %% prf1) %% prf2) ==  \
   1.159 + \    (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) ==  \
   1.160   \  (notI % Q %% (Lam H: Q.  \
   1.161   \    notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))",
   1.162  
   1.163     "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %%  \
   1.164 - \    (refl % TYPE('T3) % Not) %% prf1) %% prf2) ==  \
   1.165 + \    (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) ==  \
   1.166   \  (notI % P %% (Lam H: P.  \
   1.167   \    notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))",
   1.168  
   1.169 @@ -208,50 +208,50 @@
   1.170     "(iffD1 % B % D %%  \
   1.171   \    (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
   1.172   \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
   1.173 - \        (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   1.174 + \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   1.175   \  (iffD1 % C % D %% prf2 %%  \
   1.176   \    (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))",
   1.177  
   1.178     "(iffD2 % B % D %%  \
   1.179   \    (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
   1.180   \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
   1.181 - \        (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   1.182 + \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   1.183   \  (iffD1 % A % B %% prf1 %%  \
   1.184   \    (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))",
   1.185  
   1.186     "(iffD1 % A % C %%  \
   1.187   \    (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
   1.188   \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
   1.189 - \        (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)==  \
   1.190 + \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)==  \
   1.191   \  (iffD2 % C % D %% prf2 %%  \
   1.192   \    (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))",
   1.193  
   1.194     "(iffD2 % A % C %%  \
   1.195   \    (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
   1.196   \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
   1.197 - \        (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   1.198 + \        (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   1.199   \  (iffD2 % A % B %% prf1 %%  \
   1.200   \    (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
   1.201  
   1.202     "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
   1.203 - \    (refl % TYPE(bool=>bool) % op = A)) ==  \
   1.204 + \    (HOL.refl % TYPE(bool=>bool) % op = A)) ==  \
   1.205   \  (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
   1.206   \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
   1.207   \      (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %%  \
   1.208 - \        (refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %%  \
   1.209 - \        (refl % TYPE(bool) % A)))",
   1.210 + \        (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %%  \
   1.211 + \        (HOL.refl % TYPE(bool) % A)))",
   1.212  
   1.213     (** transitivity, reflexivity, and symmetry **)
   1.214  
   1.215 -   "(iffD1 % A % C %% (trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
   1.216 +   "(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
   1.217   \  (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))",
   1.218  
   1.219 -   "(iffD2 % A % C %% (trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
   1.220 +   "(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
   1.221   \  (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))",
   1.222  
   1.223 -   "(iffD1 % A % A %% (refl % TYPE(bool) % A) %% prf) == prf",
   1.224 +   "(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf",
   1.225  
   1.226 -   "(iffD2 % A % A %% (refl % TYPE(bool) % A) %% prf) == prf",
   1.227 +   "(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf",
   1.228  
   1.229     "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD2 % B % A %% prf)",
   1.230