src/Pure/Proof/proof_rewrite_rules.ML
changeset 12866 c00df7765656
parent 12237 39aeccee9e1c
child 12906 165f4e1937f4
     1.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Jan 30 14:05:29 2002 +0100
     1.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Sat Feb 02 13:26:51 2002 +0100
     1.3 @@ -9,7 +9,8 @@
     1.4  
     1.5  signature PROOF_REWRITE_RULES =
     1.6  sig
     1.7 -  val rprocs : (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list
     1.8 +  val rew : bool -> typ list -> Proofterm.proof -> Proofterm.proof option
     1.9 +  val rprocs : bool -> (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list
    1.10    val setup : (theory -> theory) list
    1.11  end;
    1.12  
    1.13 @@ -18,100 +19,159 @@
    1.14  
    1.15  open Proofterm;
    1.16  
    1.17 -fun rew _ (PThm (("ProtoPure.rev_triv_goal", _), _, _, _) % _ %%
    1.18 -      (PThm (("ProtoPure.triv_goal", _), _, _, _) % _ %% prf)) = Some prf
    1.19 -  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
    1.20 -      (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = Some prf
    1.21 -  | rew _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    1.22 -      (PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
    1.23 -          Some (equal_intr_axm % B % A %% prf2 %% prf1)
    1.24 +fun rew b =
    1.25 +  let
    1.26 +    fun ? x = if b then Some x else None;
    1.27 +    fun ax (prf as PAxm (s, prop, _)) Ts =
    1.28 +      if b then PAxm (s, prop, Some Ts) else prf;
    1.29 +    fun ty T = if b then
    1.30 +        let val Type (_, [Type (_, [U, _]), _]) = T
    1.31 +        in Some T end
    1.32 +      else None;
    1.33 +    val equal_intr_axm = ax equal_intr_axm [];
    1.34 +    val equal_elim_axm = ax equal_elim_axm [];
    1.35 +    val symmetric_axm = ax symmetric_axm [propT];
    1.36  
    1.37 -  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
    1.38 -      (PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) %
    1.39 -        _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
    1.40 -      ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
    1.41 -      Some (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
    1.42 +    fun rew' _ (PThm (("ProtoPure.rev_triv_goal", _), _, _, _) % _ %%
    1.43 +        (PThm (("ProtoPure.triv_goal", _), _, _, _) % _ %% prf)) = Some prf
    1.44 +      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
    1.45 +        (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = Some prf
    1.46 +      | rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    1.47 +        (PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
    1.48 +            Some (equal_intr_axm % B % A %% prf2 %% prf1)
    1.49  
    1.50 -  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
    1.51 -      (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    1.52 +      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
    1.53          (PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) %
    1.54 -           _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
    1.55 -      ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
    1.56 -      Some (tg %> B %% (equal_elim_axm %> A %> B %%
    1.57 -        (symmetric_axm % None % None %% prf1) %% prf2))
    1.58 +          _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
    1.59 +        ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
    1.60 +        Some (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
    1.61  
    1.62 -  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
    1.63 -      (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
    1.64 -        (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %%
    1.65 -           (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) =
    1.66 -      let
    1.67 -        val _ $ A $ C = Envir.beta_norm X;
    1.68 -        val _ $ B $ D = Envir.beta_norm Y
    1.69 -      in Some (AbsP ("H1", None, AbsP ("H2", None,
    1.70 -        equal_elim_axm %> C %> D %% incr_pboundvars 2 0 prf2 %%
    1.71 -          (PBound 1 %% (equal_elim_axm %> B %> A %%
    1.72 -            (symmetric_axm % None % None %% incr_pboundvars 2 0 prf1) %% PBound 0)))))
    1.73 -      end
    1.74 +      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
    1.75 +        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    1.76 +          (PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) %
    1.77 +             _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
    1.78 +        ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
    1.79 +        Some (tg %> B %% (equal_elim_axm %> A %> B %%
    1.80 +          (symmetric_axm % ? B % ? A %% prf1) %% prf2))
    1.81  
    1.82 -  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
    1.83 -      (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    1.84 +      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
    1.85          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
    1.86            (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %%
    1.87 -             (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2))) =
    1.88 -      let
    1.89 -        val _ $ A $ C = Envir.beta_norm Y;
    1.90 -        val _ $ B $ D = Envir.beta_norm X
    1.91 -      in Some (AbsP ("H1", None, AbsP ("H2", None,
    1.92 -        equal_elim_axm %> D %> C %%
    1.93 -          (symmetric_axm % None % None %% incr_pboundvars 2 0 prf2)
    1.94 -            %% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0)))))
    1.95 -      end
    1.96 +             (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) =
    1.97 +        let
    1.98 +          val _ $ A $ C = Envir.beta_norm X;
    1.99 +          val _ $ B $ D = Envir.beta_norm Y
   1.100 +        in Some (AbsP ("H1", ? X, AbsP ("H2", ? B,
   1.101 +          equal_elim_axm %> C %> D %% incr_pboundvars 2 0 prf2 %%
   1.102 +            (PBound 1 %% (equal_elim_axm %> B %> A %%
   1.103 +              (symmetric_axm % ? A % ? B %% incr_pboundvars 2 0 prf1) %% PBound 0)))))
   1.104 +        end
   1.105  
   1.106 -  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
   1.107 -      (PAxm ("ProtoPure.combination", _, _) % Some (Const ("all", _)) % _ % _ % _ %%
   1.108 -        (PAxm ("ProtoPure.reflexive", _, _) % _) %%
   1.109 -          (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf))) =
   1.110 -      let
   1.111 -        val _ $ P = Envir.beta_norm X;
   1.112 -        val _ $ Q = Envir.beta_norm Y;
   1.113 -      in Some (AbsP ("H", None, Abst ("x", None,
   1.114 -          equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
   1.115 -            (incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
   1.116 -      end
   1.117 +      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
   1.118 +        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   1.119 +          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
   1.120 +            (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %%
   1.121 +               (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2))) =
   1.122 +        let
   1.123 +          val _ $ A $ C = Envir.beta_norm Y;
   1.124 +          val _ $ B $ D = Envir.beta_norm X
   1.125 +        in Some (AbsP ("H1", ? X, AbsP ("H2", ? A,
   1.126 +          equal_elim_axm %> D %> C %%
   1.127 +            (symmetric_axm % ? C % ? D %% incr_pboundvars 2 0 prf2)
   1.128 +              %% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0)))))
   1.129 +        end
   1.130  
   1.131 -  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
   1.132 -      (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%        
   1.133 +      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
   1.134          (PAxm ("ProtoPure.combination", _, _) % Some (Const ("all", _)) % _ % _ % _ %%
   1.135            (PAxm ("ProtoPure.reflexive", _, _) % _) %%
   1.136 -            (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf)))) =
   1.137 -      let
   1.138 -        val _ $ P = Envir.beta_norm X;
   1.139 -        val _ $ Q = Envir.beta_norm Y;
   1.140 -      in Some (AbsP ("H", None, Abst ("x", None,
   1.141 -        equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
   1.142 -          (symmetric_axm % None % None %% (incr_pboundvars 1 1 prf %> Bound 0))
   1.143 -            %% (PBound 0 %> Bound 0))))
   1.144 -      end
   1.145 +            (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf))) =
   1.146 +        let
   1.147 +          val Const (_, T) $ P = Envir.beta_norm X;
   1.148 +          val _ $ Q = Envir.beta_norm Y;
   1.149 +        in Some (AbsP ("H", ? X, Abst ("x", ty T,
   1.150 +            equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
   1.151 +              (incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
   1.152 +        end
   1.153 +
   1.154 +      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
   1.155 +        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%        
   1.156 +          (PAxm ("ProtoPure.combination", _, _) % Some (Const ("all", _)) % _ % _ % _ %%
   1.157 +            (PAxm ("ProtoPure.reflexive", _, _) % _) %%
   1.158 +              (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf)))) =
   1.159 +        let
   1.160 +          val Const (_, T) $ P = Envir.beta_norm X;
   1.161 +          val _ $ Q = Envir.beta_norm Y;
   1.162 +          val t = incr_boundvars 1 P $ Bound 0;
   1.163 +          val u = incr_boundvars 1 Q $ Bound 0
   1.164 +        in Some (AbsP ("H", ? X, Abst ("x", ty T,
   1.165 +          equal_elim_axm %> t %> u %%
   1.166 +            (symmetric_axm % ? u % ? t %% (incr_pboundvars 1 1 prf %> Bound 0))
   1.167 +              %% (PBound 0 %> Bound 0))))
   1.168 +        end
   1.169 +
   1.170 +      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some A % Some C %%
   1.171 +        (PAxm ("ProtoPure.transitive", _, _) % _ % Some B % _ %% prf1 %% prf2) %% prf3) =
   1.172 +           Some (equal_elim_axm %> B %> C %% prf2 %%
   1.173 +             (equal_elim_axm %> A %> B %% prf1 %% prf3))
   1.174 +      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some A % Some C %%
   1.175 +        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   1.176 +          (PAxm ("ProtoPure.transitive", _, _) % _ % Some B % _ %% prf1 %% prf2)) %% prf3) =
   1.177 +           Some (equal_elim_axm %> B %> C %% (symmetric_axm % ? C % ? B %% prf1) %%
   1.178 +             (equal_elim_axm %> A %> B %% (symmetric_axm % ? B % ? A %% prf2) %% prf3))
   1.179 +
   1.180 +      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   1.181 +        (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf) = Some prf
   1.182 +      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   1.183 +        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   1.184 +          (PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = Some prf
   1.185 +
   1.186 +      | rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   1.187 +        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf)) = Some prf
   1.188  
   1.189 -  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some A % Some C %%
   1.190 -      (PAxm ("ProtoPure.transitive", _, _) % _ % Some B % _ %% prf1 %% prf2) %% prf3) =
   1.191 -         Some (equal_elim_axm %> B %> C %% prf2 %%
   1.192 -           (equal_elim_axm %> A %> B %% prf1 %% prf3))
   1.193 -  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some A % Some C %%
   1.194 -      (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   1.195 -        (PAxm ("ProtoPure.transitive", _, _) % _ % Some B % _ %% prf1 %% prf2)) %% prf3) =
   1.196 -         Some (equal_elim_axm %> B %> C %% (symmetric_axm % None % None %% prf1) %%
   1.197 -           (equal_elim_axm %> A %> B %% (symmetric_axm % None % None %% prf2) %% prf3))
   1.198 +      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   1.199 +        (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A $ C) % Some (_ $ B $ D) %%
   1.200 +          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
   1.201 +            (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
   1.202 +              (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
   1.203 +          Some (equal_elim_axm %> C %> D %% prf2 %%
   1.204 +            (equal_elim_axm %> A %> C %% prf3 %%
   1.205 +              (equal_elim_axm %> B %> A %% (symmetric_axm % ? A % ? B %% prf1) %% prf4)))
   1.206 +
   1.207 +      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   1.208 +        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   1.209 +          (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A $ C) % Some (_ $ B $ D) %%
   1.210 +            (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
   1.211 +              (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
   1.212 +                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
   1.213 +          Some (equal_elim_axm %> A %> B %% prf1 %%
   1.214 +            (equal_elim_axm %> C %> A %% (symmetric_axm % ? A % ? C %% prf3) %%
   1.215 +              (equal_elim_axm %> D %> C %% (symmetric_axm % ? C % ? D %% prf2) %% prf4)))
   1.216  
   1.217 -  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   1.218 -      (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf) = Some prf
   1.219 -  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   1.220 -      (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   1.221 -        (PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = Some prf
   1.222 +      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   1.223 +        (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ B $ D) % Some (_ $ A $ C) %%
   1.224 +          (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   1.225 +            (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
   1.226 +              (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
   1.227 +                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
   1.228 +          Some (equal_elim_axm %> D %> C %% (symmetric_axm % ? C % ? D %% prf2) %%
   1.229 +            (equal_elim_axm %> B %> D %% prf3 %%
   1.230 +              (equal_elim_axm %> A %> B %% prf1 %% prf4)))
   1.231  
   1.232 -  | rew _ _ = None;
   1.233 +      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   1.234 +        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   1.235 +          (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ B $ D) % Some (_ $ A $ C) %%
   1.236 +            (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   1.237 +              (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
   1.238 +                (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
   1.239 +                  (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
   1.240 +          Some (equal_elim_axm %> B %> A %% (symmetric_axm % ? A % ? B %% prf1) %%
   1.241 +            (equal_elim_axm %> D %> B %% (symmetric_axm % ? B % ? D %% prf3) %%
   1.242 +              (equal_elim_axm %> C %> D %% prf2 %% prf4)))
   1.243  
   1.244 -val rprocs = [("Pure/meta_equality", rew)];
   1.245 -val setup = [Proofterm.add_prf_rprocs rprocs];
   1.246 +      | rew' _ _ = None;
   1.247 +  in rew' end;
   1.248 +
   1.249 +fun rprocs b = [("Pure/meta_equality", rew b)];
   1.250 +val setup = [Proofterm.add_prf_rprocs (rprocs false)];
   1.251  
   1.252  end;