Theory FOR_Certificate

theory FOR_Certificate
  imports TRS.Term_Rewriting
begin

section ‹Syntax›

type_alias fvar = nat              ― ‹variable id›
datatype ftrs = Fwd nat | Bwd nat  ― ‹TRS id and direction›

definition map_ftrs where
  "map_ftrs f = case_ftrs (Fwd ∘ f) (Bwd ∘ f)"

subsection ‹GTT relations›

(* note: the 'trs will always be trs, but this way we get map functions for free *)

datatype 'trs gtt_rel                    ― ‹GTT relations›
  = ARoot "'trs list"                    ― ‹root steps›
  | GInv "'trs gtt_rel"                  ― ‹inverse of anchored or ordinary GTT relation›
  | AUnion "'trs gtt_rel" "'trs gtt_rel" ― ‹union of anchored GTT relation›
  | ATrancl "'trs gtt_rel"               ― ‹transitive closure of anchored GTT relation›
  | GTrancl "'trs gtt_rel"               ― ‹transitive closure of ordinary GTT relation›
  | AComp "'trs gtt_rel" "'trs gtt_rel"  ― ‹composition of anchored GTT relations›
  | GComp "'trs gtt_rel" "'trs gtt_rel"  ― ‹composition of ordinary GTT relations›

(* derived constructs *)
definition GSteps where "GSteps trss = GTrancl (ARoot trss)"


subsection ‹RR1 and RR2 relations›

datatype pos_step ― ‹position specification for lifting anchored GTT relation›
  = PRoot         ― ‹allow only root steps›
  | PNonRoot      ― ‹allow only non-root steps›
  | PAny          ― ‹allow any position›

datatype ext_step   ― ‹kind of rewrite steps for lifting anchored GTT relation›
  = ESingle         ― ‹single steps›
  | EParallel       ― ‹parallel steps, allowing the empty step›
  | EStrictParallel ― ‹parallel steps, no allowing the empty step›

datatype 'trs rr1_rel                     ― ‹RR1 relations, aka regular tree languages›
  = R1Terms                               ― ‹all terms as RR1 relation (regular tree languages)›
  | R1NF "'trs list"                      ― ‹direct normal form construction wrt. single steps›
  | R1Inf "'trs rr2_rel"                  ― ‹infiniteness predicate›
  | R1Proj nat "'trs rr2_rel"             ― ‹projection of RR2 relation›
  | R1Union "'trs rr1_rel" "'trs rr1_rel" ― ‹union of RR1 relations›
  | R1Inter "'trs rr1_rel" "'trs rr1_rel" ― ‹intersection of RR1 relations›
  | R1Diff "'trs rr1_rel" "'trs rr1_rel"  ― ‹difference of RR1 relations›
and 'trs rr2_rel                          ― ‹RR2 relations›
  = R2GTT_Rel "'trs gtt_rel" pos_step ext_step ― ‹lifted GTT relations›
  | R2Diag "'trs rr1_rel"                 ― ‹diagonal relation›
  | R2Prod "'trs rr1_rel" "'trs rr1_rel"  ― ‹Cartesian product›
  | R2Inv "'trs rr2_rel"                  ― ‹inverse of RR2 relation›
  | R2Union "'trs rr2_rel" "'trs rr2_rel" ― ‹union of RR2 relations›
  | R2Inter "'trs rr2_rel" "'trs rr2_rel" ― ‹intersection of RR2 relations›
  | R2Diff "'trs rr2_rel" "'trs rr2_rel"  ― ‹difference of RR2 relations›
  | R2Comp "'trs rr2_rel" "'trs rr2_rel"  ― ‹composition of RR2 relations›

(* derived constructs *)
definition R1Fin where                    ― ‹finiteness predicate›
  "R1Fin r = R1Diff R1Terms (R1Inf r)"
definition R2Eq where                     ― ‹equality›
  "R2Eq = R2Diag R1Terms"
definition R2Reflc where                  ― ‹reflexive closure›
  "R2Reflc r = R2Union r R2Eq"
definition R2Step where                   ― ‹single step $\to$›
  "R2Step trss = R2GTT_Rel (ARoot trss) PAny ESingle"
definition R2StepEq where                 ― ‹at most one step $\to^=$›
  "R2StepEq trss = R2Reflc (R2Step trss)"
definition R2Steps where                  ― ‹at least one step $\to^+$›
  "R2Steps trss = R2GTT_Rel (GSteps trss) PAny EStrictParallel"
definition R2StepsEq where                ― ‹many steps $\to^*$›
  "R2StepsEq trss = R2GTT_Rel (GSteps trss) PAny EParallel"
definition R2StepsNF where                ― ‹rewrite to normal form $\to^!$›
  "R2StepsNF trss = R2Inter (R2StepsEq trss) (R2Prod R1Terms (R1NF trss))"
definition R2ParStep where                ― ‹parallel step›
  "R2ParStep trss = R2GTT_Rel (ARoot trss) PAny EParallel"
definition R2RootStep where               ― ‹root step $\to_\epsilon$›
  "R2RootStep trss = R2GTT_Rel (ARoot trss) PRoot ESingle"
definition R2RootStepEq where             ― ‹at most one root step $\to_\epsilon^=$›
  "R2RootStepEq trss = R2Reflc (R2RootStep trss)"
  (* alternatively R2GTT_Rel (ARoot trss) PRoot SParallel *)
definition R2RootSteps where              ― ‹at least one root step $\to_\epsilon^+$›
  "R2RootSteps trss = R2GTT_Rel (ATrancl (ARoot trss)) PRoot ESingle"
definition R2RootStepsEq where            ― ‹many root steps $\to_\epsilon^*$›
  "R2RootStepsEq trss = R2Reflc (R2RootSteps trss)"
definition R2NonRootStep where            ― ‹non-root step $\to_{>\epsilon}$›
  "R2NonRootStep trss = R2GTT_Rel (ARoot trss) PNonRoot ESingle"
definition R2NonRootStepEq where          ― ‹at most one non-root step $\to_{>\epsilon}^=$›
  "R2NonRootStepEq trss = R2Reflc (R2NonRootStep trss)"
definition R2NonRootSteps where           ― ‹at least one non-root step $\to_{>\epsilon}^+$›
  "R2NonRootSteps trss = R2GTT_Rel (GSteps trss) PNonRoot EStrictParallel"
definition R2NonRootStepsEq where         ― ‹many non-root steps $\to_{>\epsilon}^*$›
  "R2NonRootStepsEq trss = R2GTT_Rel (GSteps trss) PNonRoot EParallel"
definition R2Meet where                   ― ‹meet $\uparrow$›
  "R2Meet trss = R2GTT_Rel (GComp (GInv (GSteps trss)) (GSteps trss)) PAny EParallel"
definition R2Join where                   ― ‹join $\downarrow$›
  "R2Join trss = R2GTT_Rel (GComp (GSteps trss) (GInv (GSteps trss))) PAny EParallel"


subsection ‹Formulas›

datatype 'trs formula             ― ‹formulas›
  = FRR1 "'trs rr1_rel" fvar      ― ‹application of RR1 relation›
  | FRR2 "'trs rr2_rel" fvar fvar ― ‹application of RR2 relation›
  | FAnd "('trs formula) list"    ― ‹conjunction›
  | FOr "('trs formula) list"     ― ‹disjunction›
  | FNot "'trs formula"           ― ‹negation›
  | FExists "'trs formula"        ― ‹existential quantification›
  | FForall "'trs formula"        ― ‹universal quantification›

(* derived constructs *)
definition FTrue where            ― ‹true›
  "FTrue ≡ FAnd []"
definition FFalse where           ― ‹false›
  "FFalse ≡ FOr []"
(* FRestrict can be defined, but we may want to do out of bounds checking later *)
definition FRestrict where      ― ‹reorder/rename/restrict TRSs for subformula›
  "FRestrict f trss ≡ map_formula (map_ftrs (λn. if n ≥ length trss then 0 else trss ! n)) f"


subsection ‹Signatures and Problems›

datatype ('f, 'v, 't) many_sorted_sig
  = Many_Sorted_Sig (ms_functions: "('f × 't list × 't) list") (ms_variables: "('v × 't) list")

datatype ('f, 'v, 't) problem
  = Problem (p_signature: "('f, 'v, 't) many_sorted_sig")
            (p_trss: "('f, 'v) trs list")
            (p_formula: "ftrs formula")


subsection ‹Proofs›

datatype equivalence ― ‹formula equivalences›
  = EDistribAndOr    ― ‹distributivity: conjunction over disjunction›
  | EDistribOrAnd    ― ‹distributivity: disjunction over conjunction›

datatype 'trs inference           ― ‹inference rules for formula creation›
  = IRR1 "'trs rr1_rel" fvar      ― ‹formula from RR1 relation›
  | IRR2 "'trs rr2_rel" fvar fvar ― ‹formula from RR2 relation›
  | IAnd "nat list"               ― ‹conjunction›
  | IOr "nat list"                ― ‹disjunction›
  | INot nat                      ― ‹negation›
  | IExists nat                   ― ‹existential quantification›
  | IRename nat "fvar list"       ― ‹permute variables›
  | INNFPlus nat                  ― ‹equivalence modulo negation normal form plus ACIU0 for ∧ and ∨›
  | IRepl equivalence "nat list" nat ― ‹replacement according to given equivalence›

datatype claim = Empty | Nonempty

datatype info = Size nat nat nat

datatype 'trs certificate
  = Certificate "(nat × 'trs inference × 'trs formula × info list) list" claim nat


subsection ‹Example›

text ‹Certify truth of $\forall t.\: \exists u.\: t \to u$.›

definition no_normal_forms_cert :: "ftrs certificate" where
  "no_normal_forms_cert = Certificate
  [ (0, (IRR2 (R2Step [Fwd 0]) 1 0),
        (FRR2 (R2Step [Fwd 0]) 1 0), [])                                   ― ‹0: ... ↝ 1→0›
  , (1, (IExists 0),
        (FExists (FRR2 (R2Step [Fwd 0]) 1 0)), [])                         ― ‹1: ... ↝ ∃1→0›
  , (2, (INot 1),
        (FNot (FExists (FRR2 (R2Step [Fwd 0]) 1 0))), [])                  ― ‹2: ... ↝ ¬∃1→0›
  , (3, (IExists 2),
        (FExists (FNot (FExists (FRR2 (R2Step [Fwd 0]) 1 0)))), [])        ― ‹3: ... ↝ ∃¬∃1→0›
  , (4, (INot 3),
        (FNot (FExists (FNot (FExists (FRR2 (R2Step [Fwd 0]) 1 0))))), []) ― ‹4: ... ↝ ¬∃¬∃1→0›
  , (5, (INNFPlus 4),
        (FForall (FExists (FRR2 (R2Step [Fwd 0]) 1 0))), [])               ― ‹5: ... ↝ ∀∃1→0›
  ] Nonempty 5"

definition no_normal_forms_problem :: "(string, string, unit) problem" where
  "no_normal_forms_problem = Problem
    (Many_Sorted_Sig [(''f'',[()],()), (''a'',[],())] [(''x'',())])
    [{(Fun ''f'' [Var ''x''],Fun ''a'' [])}]                               ― ‹f(x) -> a›
    (FForall (FExists (FRR2 (R2Step [Fwd 0]) 1 0)))                        ― ‹∀∃1→0›"

end