theory Non_Inf_Order_Impl
imports
Non_Inf_Order
Show.Show
"Certification_Monads.Check_Monad"
begin
datatype ('f,'v) c_constraint =
Conditional_C bool "('f, 'v) rule" "('f, 'v) rule" |
Unconditional_C bool "('f, 'v) rule"
fun cc_satisfied :: "'f sig ⇒ ('f, 'v) trs ⇒ ('f, 'v) trs ⇒ ('f, 'v) c_constraint ⇒ bool" where
"cc_satisfied F S NS (Unconditional_C stri (s, t)) =
(∀ σ. ⋃(funas_term ` range σ) ⊆ F ⟶ (s ⋅ σ, t ⋅ σ) ∈ (if stri then S else NS))"
| "cc_satisfied F S NS (Conditional_C stri (u, v) (s, t)) =
(∀ σ. ⋃(funas_term ` range σ) ⊆ F ⟶ (u ⋅ σ, v ⋅ σ) ∈ (if stri then S else NS) ⟶ (s ⋅ σ, t ⋅ σ) ∈ (if stri then S else NS))"
record ('f, 'v) non_inf_order =
valid :: "shows check"
ns :: "('f, 'v) rule ⇒ shows check"
cc :: "('f, 'v) c_constraint ⇒ shows check"
af :: "'f dep"
desc :: "shows"
hide_const (open) valid ns af desc cc
locale generic_non_inf_order_impl =
fixes generate_non_inf_order :: "'a ⇒ ('f × nat) list ⇒ ('f :: show,'v :: show)non_inf_order"
assumes generate_non_inf_order: "isOK(non_inf_order.valid (generate_non_inf_order rp F))
⟹ isOK (check_allm (non_inf_order.ns (generate_non_inf_order rp F)) ns_list)
⟹ isOK (check_allm (non_inf_order.cc (generate_non_inf_order rp F)) cc)
⟹ ∃ S NS.
non_inf_order_trs S NS (set F) (non_inf_order.af (generate_non_inf_order rp F)) ∧
set ns_list ⊆ NS ∧
Ball (set cc) (cc_satisfied (set F) S NS)"
end