theory Check_Common
imports
Processors.Processors
"Check-NT.Nontermination_Processors"
begin
instantiation list :: (type) default
begin
definition "default_list ≡ []"
instance ..
end
instantiation lab :: (default, type) default
begin
definition "default_lab = UnLab default_class.default"
instance ..
end
type_synonym ('f, 'l, 'v) ruleLL = "(('f, 'l) lab, 'v) rule"
type_synonym ('f, 'l, 'v) trsLL = "(('f, 'l) lab, 'v) rules"
type_synonym ('f, 'l, 'v) termsLL = "(('f, 'l) lab, 'v) term list"
type_synonym ('f, 'l, 'v) rseqL = "((('f, 'l) lab, 'v) rule × (('f, 'l) lab, 'v) rseq) list"
type_synonym ('f, 'l, 'v) dppLL =
"bool × bool × ('f, 'l, 'v) trsLL × ('f, 'l, 'v) trsLL ×
('f, 'l, 'v) termsLL ×
('f, 'l, 'v) trsLL × ('f, 'l, 'v) trsLL"
type_synonym ('f, 'l, 'v) qreltrsLL =
"bool × ('f, 'l, 'v) termsLL × ('f, 'l, 'v) trsLL × ('f, 'l, 'v) trsLL"
type_synonym ('f, 'l, 'v) qtrsLL =
"bool × ('f, 'l, 'v) termsLL × ('f, 'l, 'v) trsLL"
type_synonym ('f, 'l, 'v) fptrsLL =
"(('f, 'l)lab, 'v) forb_pattern list × ('f, 'l, 'v) trsLL"
type_synonym ('f, 'l, 'v) prob = "('f, 'l, 'v) qreltrsLL + ('f, 'l, 'v) dppLL"
type_synonym ('f, 'l, 'v) complexityLL =
"('f, 'l, 'v) termsLL ×
('f, 'l, 'v) trsLL ×
('f, 'l, 'v) trsLL ×
(('f,'l)lab,'v) complexity_measure ×
complexity_class"
fun mk_dpp_set where
"mk_dpp_set (nfs, m, p, pw, q, r, rw) = (nfs, m, set p, set pw, set q, set r, set rw)"
fun mk_dpp_nt_set where
"mk_dpp_nt_set (nfs, m, p, pw, q, r, rw) = (nfs, set p ∪ set pw, set q, set r ∪ set rw)"
fun mk_tp_set where
"mk_tp_set (nfs, q, r, rw) = (nfs, set q, set r, set rw)"
fun mk_tp_nt_set where
"mk_tp_nt_set (nfs, q, r) = (nfs, set q, set r, {})"
fun mk_fptp_set where
"mk_fptp_set (fp, r) = (set fp, set r)"
type_synonym unknown_info = string
datatype (dead 'f, dead 'l, dead 'v)problem =
SN_TRS "('f,'l,'v)qreltrsLL"
| SN_FP_TRS "('f,'l,'v)fptrsLL"
| Finite_DPP "('f,'l,'v) dppLL"
| Unknown_Problem unknown_info
| Not_SN_TRS "('f,'l,'v)qtrsLL"
| Not_RelSN_TRS "('f,'l,'v)qreltrsLL"
| Infinite_DPP "('f,'l,'v) dppLL"
| Not_SN_FP_TRS "('f,'l,'v)fptrsLL"
| Complexity_Problem "('f,'l,'v)complexityLL"
consts unknown_satisfied :: "unknown_info ⇒ bool"
definition "SN_fpstep fptrs ≡ case fptrs of (p,r) ⇒ SN (fpstep p r)"
fun satisfied :: "('f,'l,'v)problem ⇒ bool" where
"satisfied (SN_TRS t) = SN_qrel (mk_tp_set t)"
| "satisfied (SN_FP_TRS t) = SN_fpstep (mk_fptp_set t)"
| "satisfied (Finite_DPP d) = finite_dpp (mk_dpp_set d)"
| "satisfied (Unknown_Problem s) = unknown_satisfied s"
| "satisfied (Not_SN_TRS (nfs,q,r)) = (¬ SN (qrstep nfs (set q) (set r)))"
| "satisfied (Not_RelSN_TRS (nfs,q,r,rw)) = (¬ SN_qrel (nfs, set q, set r, set rw))"
| "satisfied (Infinite_DPP d) = infinite_dpp (mk_dpp_nt_set d)"
| "satisfied (Not_SN_FP_TRS t) = (¬ SN_fpstep (mk_fptp_set t))"
| "satisfied (Complexity_Problem (q,s,w,cm,cc)) = deriv_bound_measure_class (rel_qrstep (False, set q, set s, set w)) cm cc"
datatype (dead 'f, dead 'l, dead 'v)assm =
SN_assm "('f,'l,'v)problem list" "('f,'l,'v)qreltrsLL"
| SN_FP_assm "('f,'l,'v)problem list" "('f,'l,'v)fptrsLL"
| Finite_assm "('f,'l,'v)problem list" "('f,'l,'v)dppLL"
| Unknown_assm "('f,'l,'v)problem list" unknown_info
| Not_SN_assm "('f,'l,'v)problem list" "('f,'l,'v)qtrsLL"
| Not_RelSN_assm "('f,'l,'v)problem list" "('f,'l,'v)qreltrsLL"
| Not_SN_FP_assm "('f,'l,'v)problem list" "('f,'l,'v)fptrsLL"
| Infinite_assm "('f,'l,'v)problem list" "('f,'l,'v)dppLL"
| Complexity_assm "('f,'l,'v)problem list" "('f,'l,'v)complexityLL"
primrec holds :: "('f, 'l, 'v) assm ⇒ bool" where
"holds (SN_assm as p) = ((∀ a ∈ set as. satisfied a) ⟶ satisfied (SN_TRS p))"
| "holds (SN_FP_assm as p) = ((∀ a ∈ set as. satisfied a) ⟶ satisfied (SN_FP_TRS p))"
| "holds (Finite_assm as p) = ((∀ a ∈ set as. satisfied a) ⟶ satisfied (Finite_DPP p))"
| "holds (Unknown_assm as s) = ((∀ a ∈ set as. satisfied a) ⟶ unknown_satisfied s)"
| "holds (Not_SN_assm as p) = ((∀ a ∈ set as. satisfied a) ⟶ satisfied (Not_SN_TRS p))"
| "holds (Not_RelSN_assm as p) = ((∀ a ∈ set as. satisfied a) ⟶ satisfied (Not_RelSN_TRS p))"
| "holds (Infinite_assm as p) = ((∀ a ∈ set as. satisfied a) ⟶ satisfied (Infinite_DPP p))"
| "holds (Not_SN_FP_assm as p) = ((∀ a ∈ set as. satisfied a) ⟶ satisfied (Not_SN_FP_TRS p))"
| "holds (Complexity_assm as p) = ((∀ a ∈ set as. satisfied a) ⟶ satisfied (Complexity_Problem p))"
datatype (dead 'f,dead 'l,dead 'v,'a,'b,'c,'d,'e)generic_assm_proof =
SN_assm_proof "('f,'l,'v)qreltrsLL" 'a
| Finite_assm_proof "('f,'l,'v)dppLL" 'b
| SN_FP_assm_proof "('f,'l,'v)fptrsLL" 'c
| Not_SN_assm_proof "('f,'l,'v)qtrsLL" 'a
| Infinite_assm_proof "('f,'l,'v)dppLL" 'b
| Not_RelSN_assm_proof "('f,'l,'v)qreltrsLL" 'c
| Not_SN_FP_assm_proof "('f,'l,'v)fptrsLL" 'd
| Complexity_assm_proof "('f,'l,'v)complexityLL" 'a
| Unknown_assm_proof unknown_info 'e
primrec assm_proof_to_problem :: "('f,'l,'v,'a,'b,'c,'d,'e) generic_assm_proof ⇒ ('f,'l,'v) problem" where
"assm_proof_to_problem (SN_assm_proof t prf) = SN_TRS t"
| "assm_proof_to_problem (SN_FP_assm_proof t prf) = SN_FP_TRS t"
| "assm_proof_to_problem (Finite_assm_proof d prf) = Finite_DPP d"
| "assm_proof_to_problem (Unknown_assm_proof p prf) = Unknown_Problem p"
| "assm_proof_to_problem (Not_SN_assm_proof t prf) = Not_SN_TRS t"
| "assm_proof_to_problem (Not_RelSN_assm_proof t prf) = Not_RelSN_TRS t"
| "assm_proof_to_problem (Infinite_assm_proof d prf) = Infinite_DPP d"
| "assm_proof_to_problem (Not_SN_FP_assm_proof t prf) = Not_SN_FP_TRS t"
| "assm_proof_to_problem (Complexity_assm_proof t prf) = Complexity_Problem t"
type_synonym dummy_prf = unit
type_synonym ('f,'l,'v,'a,'b,'c,'d)assm_proof = "('f,'l,'v,'a,'b,'c,dummy_prf,'d)generic_assm_proof"
type_synonym ('f,'l,'v,'a)cpx_assm_proof = "('f,'l,'v,'a,dummy_prf,dummy_prf,dummy_prf,dummy_prf)generic_assm_proof"
definition missing :: "string ⇒ shows ⇒ shows"
where
"missing s x = shows ''the '' ∘ shows s ∘ shows '' '' ∘ x ∘ shows '' is missing''"
definition toomuch :: "string ⇒ shows ⇒ shows"
where
"toomuch s x = shows ''superfluous '' ∘ shows s ∘ shows '' '' ∘ x ∘ x"
datatype ('f, 'v) equation_literal =
Equation "('f, 'v) term × ('f, 'v) term" |
Inequality "('f, 'v) term × ('f, 'v) term"
end