# Theory FOR_Certificate

theory FOR_Certificate
imports Rewriting
begin

section ‹Certificate syntax and type declarations›

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 *)

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$›
definition R2StepEq where                 ― ‹at most one step $\to^=$›
definition R2Steps where                  ― ‹at least one step $\to^+$›
definition R2StepsEq where                ― ‹many steps $\to^*$›
definition R2StepsNF where                ― ‹rewrite to normal form $\to^!$›
definition R2ParStep where                ― ‹parallel step›
definition R2RootStep where               ― ‹root step $\to_\epsilon$›
definition R2RootStepEq where             ― ‹at most one root step $\to_\epsilon^=$›
(* alternatively R2GTT_Rel (ARoot trss) PRoot SParallel *)
definition R2RootSteps where              ― ‹at least one root step $\to_\epsilon^+$›
definition R2RootStepsEq where            ― ‹many root steps $\to_\epsilon^*$›
definition R2NonRootStep where            ― ‹non-root step $\to_{>\epsilon}$›
definition R2NonRootStepEq where          ― ‹at most one non-root step $\to_{>\epsilon}^=$›
definition R2NonRootSteps where           ― ‹at least one non-root step $\to_{>\epsilon}^+$›
definition R2NonRootStepsEq where         ― ‹many non-root steps $\to_{>\epsilon}^*$›
definition R2Meet where                   ― ‹meet $\uparrow$›
definition R2Join where                   ― ‹join $\downarrow$›

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_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 $\land$ and $\lor$›
| 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›

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), [])
, (1, (IExists 0),
(FExists (FRR2 (R2Step [Fwd 0]) 1 0)), [])
, (2, (INot 1),
(FNot (FExists (FRR2 (R2Step [Fwd 0]) 1 0))), [])
, (3, (IExists 2),
(FExists (FNot (FExists (FRR2 (R2Step [Fwd 0]) 1 0)))), [])
, (4, (INot 3),
(FNot (FExists (FNot (FExists (FRR2 (R2Step [Fwd 0]) 1 0))))), [])
, (5, (INNFPlus 4),
(FForall (FExists (FRR2 (R2Step [Fwd 0]) 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'' [])}]
(FForall (FExists (FRR2 (R2Step [Fwd 0]) 1 0)))"

end