src/Pure/Proof/proof_rewrite_rules.ML

Symbol.bump_string;

(*  Title:      Pure/Proof/proof_rewrite_rules.ML
    ID:         $Id$
    Author:     Stefan Berghofer, TU Muenchen
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

Simplification function for partial proof terms involving
meta level rules.
*)

signature PROOF_REWRITE_RULES =
sig
  val rew : bool -> typ list -> Proofterm.proof -> Proofterm.proof option
  val rprocs : bool -> (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list
  val setup : (theory -> theory) list
end;

structure ProofRewriteRules : PROOF_REWRITE_RULES =
struct

open Proofterm;

fun rew b =
  let
    fun ? x = if b then Some x else None;
    fun ax (prf as PAxm (s, prop, _)) Ts =
      if b then PAxm (s, prop, Some Ts) else prf;
    fun ty T = if b then
        let val Type (_, [Type (_, [U, _]), _]) = T
        in Some T end
      else None;
    val equal_intr_axm = ax equal_intr_axm [];
    val equal_elim_axm = ax equal_elim_axm [];
    val symmetric_axm = ax symmetric_axm [propT];

    fun rew' _ (PThm (("ProtoPure.rev_triv_goal", _), _, _, _) % _ %%
        (PThm (("ProtoPure.triv_goal", _), _, _, _) % _ %% prf)) = Some prf
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
        (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = Some prf
      | rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
        (PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
            Some (equal_intr_axm % B % A %% prf2 %% prf1)

      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
        (PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) %
          _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
        ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
        Some (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))

      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
          (PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) %
             _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
        ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
        Some (tg %> B %% (equal_elim_axm %> A %> B %%
          (symmetric_axm % ? B % ? A %% prf1) %% prf2))

      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
        (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
          (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %%
             (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) =
        let
          val _ $ A $ C = Envir.beta_norm X;
          val _ $ B $ D = Envir.beta_norm Y
        in Some (AbsP ("H1", ? X, AbsP ("H2", ? B,
          equal_elim_axm %> C %> D %% incr_pboundvars 2 0 prf2 %%
            (PBound 1 %% (equal_elim_axm %> B %> A %%
              (symmetric_axm % ? A % ? B %% incr_pboundvars 2 0 prf1) %% PBound 0)))))
        end

      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
            (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %%
               (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2))) =
        let
          val _ $ A $ C = Envir.beta_norm Y;
          val _ $ B $ D = Envir.beta_norm X
        in Some (AbsP ("H1", ? X, AbsP ("H2", ? A,
          equal_elim_axm %> D %> C %%
            (symmetric_axm % ? C % ? D %% incr_pboundvars 2 0 prf2)
              %% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0)))))
        end

      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
        (PAxm ("ProtoPure.combination", _, _) % Some (Const ("all", _)) % _ % _ % _ %%
          (PAxm ("ProtoPure.reflexive", _, _) % _) %%
            (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf))) =
        let
          val Const (_, T) $ P = Envir.beta_norm X;
          val _ $ Q = Envir.beta_norm Y;
        in Some (AbsP ("H", ? X, Abst ("x", ty T,
            equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
              (incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
        end

      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%        
          (PAxm ("ProtoPure.combination", _, _) % Some (Const ("all", _)) % _ % _ % _ %%
            (PAxm ("ProtoPure.reflexive", _, _) % _) %%
              (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf)))) =
        let
          val Const (_, T) $ P = Envir.beta_norm X;
          val _ $ Q = Envir.beta_norm Y;
          val t = incr_boundvars 1 P $ Bound 0;
          val u = incr_boundvars 1 Q $ Bound 0
        in Some (AbsP ("H", ? X, Abst ("x", ty T,
          equal_elim_axm %> t %> u %%
            (symmetric_axm % ? u % ? t %% (incr_pboundvars 1 1 prf %> Bound 0))
              %% (PBound 0 %> Bound 0))))
        end

      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some A % Some C %%
        (PAxm ("ProtoPure.transitive", _, _) % _ % Some B % _ %% prf1 %% prf2) %% prf3) =
           Some (equal_elim_axm %> B %> C %% prf2 %%
             (equal_elim_axm %> A %> B %% prf1 %% prf3))
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some A % Some C %%
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
          (PAxm ("ProtoPure.transitive", _, _) % _ % Some B % _ %% prf1 %% prf2)) %% prf3) =
           Some (equal_elim_axm %> B %> C %% (symmetric_axm % ? C % ? B %% prf1) %%
             (equal_elim_axm %> A %> B %% (symmetric_axm % ? B % ? A %% prf2) %% prf3))

      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
        (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf) = Some prf
      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
          (PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = Some prf

      | rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf)) = Some prf

      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
        (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A $ C) % Some (_ $ B $ D) %%
          (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
            (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
              (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
          Some (equal_elim_axm %> C %> D %% prf2 %%
            (equal_elim_axm %> A %> C %% prf3 %%
              (equal_elim_axm %> B %> A %% (symmetric_axm % ? A % ? B %% prf1) %% prf4)))

      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
          (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A $ C) % Some (_ $ B $ D) %%
            (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
              (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
          Some (equal_elim_axm %> A %> B %% prf1 %%
            (equal_elim_axm %> C %> A %% (symmetric_axm % ? A % ? C %% prf3) %%
              (equal_elim_axm %> D %> C %% (symmetric_axm % ? C % ? D %% prf2) %% prf4)))

      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
        (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ B $ D) % Some (_ $ A $ C) %%
          (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
            (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
              (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
          Some (equal_elim_axm %> D %> C %% (symmetric_axm % ? C % ? D %% prf2) %%
            (equal_elim_axm %> B %> D %% prf3 %%
              (equal_elim_axm %> A %> B %% prf1 %% prf4)))

      | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
        (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
          (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ B $ D) % Some (_ $ A $ C) %%
            (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
              (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
                (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %%
                  (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
          Some (equal_elim_axm %> B %> A %% (symmetric_axm % ? A % ? B %% prf1) %%
            (equal_elim_axm %> D %> B %% (symmetric_axm % ? B % ? D %% prf3) %%
              (equal_elim_axm %> C %> D %% prf2 %% prf4)))

      | rew' _ _ = None;
  in rew' end;

fun rprocs b = [("Pure/meta_equality", rew b)];
val setup = [Proofterm.add_prf_rprocs (rprocs false)];

end;