src/HOL/Tools/rewrite_hol_proof.ML
changeset 13404 eeac2bbfe958
child 13602 4cecd1e0f4a9
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Sun Jul 21 15:43:14 2002 +0200
     1.3 @@ -0,0 +1,285 @@
     1.4 +(*  Title:      HOL/Tools/rewrite_hol_proof.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Stefan Berghofer, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +
     1.9 +Rewrite rules for HOL proofs
    1.10 +*)
    1.11 +
    1.12 +signature REWRITE_HOL_PROOF =
    1.13 +sig
    1.14 +  val rews: (Proofterm.proof * Proofterm.proof) list
    1.15 +  val elim_cong: typ list -> Proofterm.proof -> Proofterm.proof option
    1.16 +end;
    1.17 +
    1.18 +structure RewriteHOLProof : REWRITE_HOL_PROOF =
    1.19 +struct
    1.20 +
    1.21 +open Proofterm;
    1.22 +
    1.23 +val rews = map (pairself (ProofSyntax.proof_of_term (the_context ()) Symtab.empty true) o
    1.24 +    Logic.dest_equals o Logic.varify o ProofSyntax.read_term (the_context ()) propT)
    1.25 +
    1.26 +  (** eliminate meta-equality rules **)
    1.27 +
    1.28 +  ["(equal_elim % x1 % x2 %% \
    1.29 + \    (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %%  \
    1.30 + \      (axm.reflexive % TYPE('T3) % x4) %% prf1) %% prf2) ==  \
    1.31 + \  (iffD1 % A % B %%  \
    1.32 + \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1) %% prf2)",
    1.33 +
    1.34 +   "(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %%  \
    1.35 + \    (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %%  \
    1.36 + \      (axm.reflexive % TYPE('T4) % x6) %% prf1)) %% prf2) ==  \
    1.37 + \  (iffD2 % A % B %%  \
    1.38 + \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1) %% prf2)",
    1.39 +
    1.40 +   "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %%  \
    1.41 + \    (combination % TYPE('U) % TYPE('T) % f % g % x % y %% prf1 %% prf2)) ==  \
    1.42 + \  (cong % TYPE('U) % TYPE('T) % f % g % x % y %%  \
    1.43 + \    (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% prf1) %%  \
    1.44 + \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf2))",
    1.45 +
    1.46 +   "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %%  \
    1.47 + \    (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) ==  \
    1.48 + \  (trans % TYPE('T) % x % y % z %%  \
    1.49 + \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf1) %%  \
    1.50 + \    (meta_eq_to_obj_eq % TYPE('T) % y % z %% prf2))",
    1.51 +
    1.52 +   "(meta_eq_to_obj_eq % TYPE('T) % x % x %% (axm.reflexive % TYPE('T) % x)) ==  \
    1.53 + \  (refl % TYPE('T) % x)",
    1.54 +
    1.55 +   "(meta_eq_to_obj_eq % TYPE('T) % x % y %%  \
    1.56 + \    (axm.symmetric % TYPE('T) % x % y %% prf)) ==  \
    1.57 + \  (sym % TYPE('T) % x % y %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf))",
    1.58 +
    1.59 +   "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %%  \
    1.60 + \    (abstract_rule % TYPE('U) % TYPE('T) % f % g %% prf)) ==  \
    1.61 + \  (ext % TYPE('U) % TYPE('T) % f % g %%  \
    1.62 + \    (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% (prf % x)))",
    1.63 +
    1.64 +   "(meta_eq_to_obj_eq % TYPE('T) % x % y %%  \
    1.65 + \    (eq_reflection % TYPE('T) % x % y %% prf)) == prf",
    1.66 +
    1.67 +   "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %%  \
    1.68 + \    (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %%  \
    1.69 + \      (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %%  \
    1.70 + \        (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) ==  \
    1.71 + \  (iffD1 % A = C % B = D %%  \
    1.72 + \    (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %%  \
    1.73 + \      (cong % TYPE('T=>bool) % TYPE('T) %  \
    1.74 + \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
    1.75 + \        (refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
    1.76 + \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
    1.77 + \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %%  \
    1.78 + \    (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))",
    1.79 +
    1.80 +   "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %%  \
    1.81 + \    (axm.symmetric % TYPE('T2) % x5 % x6 %%  \
    1.82 + \      (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %%  \
    1.83 + \        (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %%  \
    1.84 + \          (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) ==  \
    1.85 + \  (iffD2 % A = C % B = D %%  \
    1.86 + \    (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %%  \
    1.87 + \      (cong % TYPE('T=>bool) % TYPE('T) %  \
    1.88 + \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
    1.89 + \        (refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
    1.90 + \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
    1.91 + \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %%  \
    1.92 + \    (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))",
    1.93 +
    1.94 +   (** rewriting on bool: insert proper congruence rules for logical connectives **)
    1.95 +
    1.96 +   (* All *)
    1.97 +
    1.98 +   "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %%  \
    1.99 + \    (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
   1.100 + \  (allI % TYPE('a) % Q %%  \
   1.101 + \    (Lam x.  \
   1.102 + \        iffD1 % P x % Q x %% (prf % x) %%  \
   1.103 + \         (spec % TYPE('a) % P % x %% prf')))",
   1.104 +
   1.105 +   "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %%  \
   1.106 + \    (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
   1.107 + \  (allI % TYPE('a) % P %%  \
   1.108 + \    (Lam x.  \
   1.109 + \        iffD2 % P x % Q x %% (prf % x) %%  \
   1.110 + \         (spec % TYPE('a) % ?Q % x %% prf')))",
   1.111 +
   1.112 +   (* Ex *)
   1.113 +
   1.114 +   "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %%  \
   1.115 + \    (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
   1.116 + \  (exE % TYPE('a) % P % EX x. Q x %% prf' %%  \
   1.117 + \    (Lam x H : P x.  \
   1.118 + \        exI % TYPE('a) % Q % x %%  \
   1.119 + \         (iffD1 % P x % Q x %% (prf % x) %% H)))",
   1.120 +
   1.121 +   "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %%  \
   1.122 + \    (refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') ==  \
   1.123 + \  (exE % TYPE('a) % Q % EX x. P x %% prf' %%  \
   1.124 + \    (Lam x H : Q x.  \
   1.125 + \        exI % TYPE('a) % P % x %%  \
   1.126 + \         (iffD2 % P x % Q x %% (prf % x) %% H)))",
   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 + \  (conjI % B % D %%  \
   1.134 + \    (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %%  \
   1.135 + \    (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))",
   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 + \  (conjI % A % C %%  \
   1.141 + \    (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %%  \
   1.142 + \    (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))",
   1.143 +
   1.144 +   (* | *)
   1.145 +
   1.146 +   "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   1.147 + \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %%  \
   1.148 + \      (refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) ==  \
   1.149 + \  (disjE % A % C % B | D %% prf3 %%  \
   1.150 + \    (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %%  \
   1.151 + \    (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))",
   1.152 +
   1.153 +   "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   1.154 + \    (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %%  \
   1.155 + \      (refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) ==  \
   1.156 + \  (disjE % B % D % A | C %% prf3 %%  \
   1.157 + \    (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %%  \
   1.158 + \    (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))",
   1.159 +
   1.160 +   (* --> *)
   1.161 +
   1.162 +   "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   1.163 + \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %%  \
   1.164 + \      (refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) ==  \
   1.165 + \  (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %%  \
   1.166 + \    (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))",
   1.167 +
   1.168 +   "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %%  \
   1.169 + \    (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %%  \
   1.170 + \      (refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) ==  \
   1.171 + \  (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %%  \
   1.172 + \    (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))",
   1.173 +
   1.174 +   (* ~ *)
   1.175 +
   1.176 +   "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %%  \
   1.177 + \    (refl % TYPE('T3) % Not) %% prf1) %% prf2) ==  \
   1.178 + \  (notI % Q %% (Lam H: Q.  \
   1.179 + \    notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))",
   1.180 +
   1.181 +   "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %%  \
   1.182 + \    (refl % TYPE('T3) % Not) %% prf1) %% prf2) ==  \
   1.183 + \  (notI % P %% (Lam H: P.  \
   1.184 + \    notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))",
   1.185 +
   1.186 +   (* = *)
   1.187 +
   1.188 +   "(iffD1 % B % D %%  \
   1.189 + \    (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
   1.190 + \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
   1.191 + \        (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   1.192 + \  (iffD1 % C % D %% prf2 %%  \
   1.193 + \    (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))",
   1.194 +
   1.195 +   "(iffD2 % B % D %%  \
   1.196 + \    (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
   1.197 + \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
   1.198 + \        (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   1.199 + \  (iffD1 % A % B %% prf1 %%  \
   1.200 + \    (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))",
   1.201 +
   1.202 +   "(iffD1 % A % C %%  \
   1.203 + \    (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
   1.204 + \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
   1.205 + \        (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)==  \
   1.206 + \  (iffD2 % C % D %% prf2 %%  \
   1.207 + \    (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))",
   1.208 +
   1.209 +   "(iffD2 % A % C %%  \
   1.210 + \    (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %%  \
   1.211 + \      (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %%  \
   1.212 + \        (refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   1.213 + \  (iffD2 % A % B %% prf1 %%  \
   1.214 + \    (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
   1.215 +
   1.216 +   "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
   1.217 + \    (refl % TYPE(bool) % op = A)) ==  \
   1.218 + \  (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %%  \
   1.219 + \    (cong % TYPE(bool=>bool) % TYPE(bool) %  \
   1.220 + \      (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %%  \
   1.221 + \        (refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %%  \
   1.222 + \        (refl % TYPE(bool) % A % A)))",
   1.223 +
   1.224 +   "(iffD1 % A % C %% (trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
   1.225 + \  (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))",
   1.226 +
   1.227 +   "(iffD2 % A % C %% (trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) ==  \
   1.228 + \  (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))",
   1.229 +
   1.230 +   "(iffD1 % A % A %% (refl % TYPE(bool) % A) %% prf) == prf",
   1.231 +
   1.232 +   "(iffD2 % A % A %% (refl % TYPE(bool) % A) %% prf) == prf",
   1.233 +
   1.234 +   (** normalization of HOL proofs **)
   1.235 +
   1.236 +   "(mp % A % B %% (impI % A % B %% prf)) == prf",
   1.237 +
   1.238 +   "(impI % A % B %% (mp % A % B %% prf)) == prf",
   1.239 +
   1.240 +   "(spec % TYPE('a) % P % x %% (allI % TYPE('a) % P %% prf)) == prf % x",
   1.241 +
   1.242 +   "(allI % TYPE('a) % P %% (Lam x::'a. spec % TYPE('a) % P % x %% prf)) == prf",
   1.243 +
   1.244 +   "(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)",
   1.245 +
   1.246 +   "(disjE % P % Q % R %% (disjI2 % Q % P %% prf1) %% prf2 %% prf3) == (prf3 %% prf1)",
   1.247 +
   1.248 +   "(conjunct1 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf1",
   1.249 +
   1.250 +   "(conjunct2 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf2",
   1.251 +
   1.252 +   "(iffD1 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf1",
   1.253 +
   1.254 +   "(iffD2 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf2"];
   1.255 +
   1.256 +
   1.257 +(** Replace congruence rules by substitution rules **)
   1.258 +
   1.259 +fun strip_cong ps (PThm (("HOL.cong", _), _, _, _) % _ % _ % Some x % Some y %%
   1.260 +      prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1
   1.261 +  | strip_cong ps (PThm (("HOL.refl", _), _, _, _) % Some f) = Some (f, ps)
   1.262 +  | strip_cong _ _ = None;
   1.263 +
   1.264 +val subst_prf = fst (strip_combt (#2 (#der (rep_thm subst))));
   1.265 +val sym_prf = fst (strip_combt (#2 (#der (rep_thm sym))));
   1.266 +
   1.267 +fun make_subst Ts prf xs (_, []) = prf
   1.268 +  | make_subst Ts prf xs (f, ((x, y), prf') :: ps) =
   1.269 +      let val T = fastype_of1 (Ts, x)
   1.270 +      in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
   1.271 +        else change_type (Some [T]) subst_prf %> x %> y %>
   1.272 +          Abs ("z", T, list_comb (incr_boundvars 1 f,
   1.273 +            map (incr_boundvars 1) xs @ Bound 0 ::
   1.274 +            map (incr_boundvars 1 o snd o fst) ps)) %% prf' %%
   1.275 +          make_subst Ts prf (xs @ [x]) (f, ps)
   1.276 +      end;
   1.277 +
   1.278 +fun make_sym Ts ((x, y), prf) =
   1.279 +  ((y, x), change_type (Some [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% prf);
   1.280 +
   1.281 +fun elim_cong Ts (PThm (("HOL.iffD1", _), _, _, _) % _ % _ %% prf1 %% prf2) =
   1.282 +      apsome (make_subst Ts prf2 []) (strip_cong [] prf1)
   1.283 +  | elim_cong Ts (PThm (("HOL.iffD2", _), _, _, _) % _ % _ %% prf1 %% prf2) =
   1.284 +      apsome (make_subst Ts prf2 [] o
   1.285 +        apsnd (map (make_sym Ts))) (strip_cong [] prf1)
   1.286 +  | elim_cong _ _ = None;
   1.287 +
   1.288 +end;