theory Semantic_Labeling_Carrier
imports
Show.Show
QTRS.Lexicographic_Extension
Semantic_Labeling_Impl
"Check-NT.Labelings_Impl"
begin
subsection ‹carrier {0..n}›
datatype arithFun =
Arg nat
| Const nat
| Sum "arithFun list"
| Max "arithFun list"
| Min "arithFun list"
| Prod "arithFun list"
| IfEqual arithFun arithFun arithFun arithFun
text ‹An alternative induction scheme for arithFuns.›
lemma
fixes P :: "arithFun ⇒ bool"
assumes "⋀n. P(Arg n)" and "⋀n. P(Const n)"
and "⋀fs. (⋀f. f ∈ set fs ⟹ P f) ⟹ P(Sum fs)"
and "⋀fs. (⋀f. f ∈ set fs ⟹ P f) ⟹ P(Max fs)"
and "⋀fs. (⋀f. f ∈ set fs ⟹ P f) ⟹ P(Min fs)"
and "⋀fs. (⋀f. f ∈ set fs ⟹ P f) ⟹ P(Prod fs)"
and "⋀ f1 f2 ft fe. P f1 ⟹ P f2 ⟹ P ft ⟹ P fe ⟹ P(IfEqual f1 f2 ft fe)"
shows arithFun_induct[case_names Arg Const Sum Max Min Prod IfEqual,induct type: arithFun]: "P f"
by (rule arithFun.induct, insert assms, auto)
instantiation arithFun :: "show"
begin
fun shows_arithFun :: "arithFun ⇒ shows"
where
"shows_arithFun (Arg i) = shows ''x_'' ∘ shows (Suc i)" |
"shows_arithFun (Const n) = shows n" |
"shows_arithFun (Sum fs) = shows_list_gen shows_arithFun [] [] '' + '' [] fs" |
"shows_arithFun (Prod fs) = shows_list_gen shows_arithFun [] [] '' * '' [] fs" |
"shows_arithFun (Min fs) = shows_list_gen shows_arithFun [] ''min('' '','' '')'' fs" |
"shows_arithFun (Max fs) = shows_list_gen shows_arithFun [] ''max('' '','' '')'' fs" |
"shows_arithFun (IfEqual f1 f2 ft fe) =
shows ''if '' ∘ shows_arithFun f1 ∘ shows '' = '' ∘ shows_arithFun f2 ∘
shows '' then '' ∘ shows_arithFun ft ∘
shows '' else '' ∘ shows_arithFun fe ∘ shows '' fi''"
definition "shows_prec (p::nat) (f :: arithFun) = shows_arithFun f"
lemma shows_prec_arithFun_append [show_law_simps]:
"shows_prec p (f :: arithFun) (r @ s) = shows_prec p f r @ s"
by (induct f arbitrary: r s) (simp_all add: shows_prec_arithFun_def show_law_simps)
definition "shows_list (fs :: arithFun list) = showsp_list shows_prec 0 fs"
instance by standard (simp_all add: shows_list_arithFun_def show_law_simps)
end
fun take_default where
"take_default def [] _ = def"
| "take_default _ (x # xs) 0 = x"
| "take_default def (_ # xs) (Suc i) = take_default def xs i"
fun eval_arithFun_unbound :: "nat ⇒ nat list ⇒ arithFun ⇒ nat" and
eval_arithFun :: "nat ⇒ nat list ⇒ arithFun ⇒ nat"
where
"eval_arithFun_unbound c nats (Arg i) = take_default 0 nats i"
| "eval_arithFun_unbound c nats (Const n) = n"
| "eval_arithFun_unbound c nats (Sum []) = 0"
| "eval_arithFun_unbound c nats (Sum (f # fs)) = (eval_arithFun c nats f + eval_arithFun c nats (Sum fs))"
| "eval_arithFun_unbound c nats (Prod []) = 1"
| "eval_arithFun_unbound c nats (Prod (f # fs)) = (eval_arithFun c nats f * eval_arithFun c nats (Prod fs))"
| "eval_arithFun_unbound c nats (Max [f]) = eval_arithFun c nats f"
| "eval_arithFun_unbound c nats (Max (f # fs)) = (max (eval_arithFun c nats f) (eval_arithFun c nats (Max fs)))"
| "eval_arithFun_unbound c nats (Min [f]) = eval_arithFun c nats f"
| "eval_arithFun_unbound c nats (Min (f # fs)) = (min (eval_arithFun c nats f) (eval_arithFun c nats (Min fs)))"
| "eval_arithFun_unbound c nats (IfEqual f1 f2 ft fe) = (if (eval_arithFun c nats f1 = eval_arithFun c nats f2)
then eval_arithFun c nats ft else eval_arithFun c nats fe)"
| "eval_arithFun c nats f = (eval_arithFun_unbound c nats f) mod c"
declare eval_arithFun_unbound.simps[simp del]
datatype ('f) sl_inter = SL_Inter nat "(('f × nat) × arithFun) list"
instantiation sl_inter :: ("show") "show"
begin
fun shows_sl_inter :: "('a :: show) sl_inter ⇒ shows"
where
"shows_sl_inter(SL_Inter n fnas) =
shows ''carrier {0,...,'' ∘ shows n ∘ shows ''}'' ∘ shows_nl ∘
foldr (λ((f, n), a).
shows ''['' ∘ shows f ∘ shows ''/'' ∘ shows n ∘ shows ''] = '' ∘ shows a ∘ shows_nl) fnas"
definition "shows_prec (p::nat) sli = shows_sl_inter sli"
definition "shows_list (ss :: 'a sl_inter list) ≡ showsp_list shows_prec 0 ss"
lemma shows_prec_sl_inter_append [show_law_simps]:
"shows_prec p (sli :: 'a sl_inter) (r @ s) = shows_prec p sli r @ s"
proof (cases sli)
fix n :: nat and fnas
assume *: "sli = SL_Inter n fnas"
let ?elt = "λ((f :: 'a, n :: nat), a :: arithFun).
shows ''['' ∘ shows f ∘ shows ''/'' ∘ shows n ∘ shows ''] = '' ∘ shows a ∘ shows_nl"
have "⋀r s. ∀x ∈ set fnas. ?elt x (r @ s) = ?elt x r @ s" by (auto simp add: show_law_simps)
then show ?thesis by (simp add: * shows_prec_sl_inter_def show_law_simps)
qed
instance by standard (simp_all add: show_law_simps shows_list_sl_inter_def)
end
primrec get_largest_element where "get_largest_element (SL_Inter n _) = n"
primrec sl_inter_to_inter :: "'f sl_inter ⇒ ('f, nat) inter" where
"sl_inter_to_inter (SL_Inter c ls) fl cs =
(case map_of ls (fl, length cs) of
None ⇒ 0
| Some f ⇒ eval_arithFun (Suc c) cs f)"
lemma wf_sl_inter:
"wf_inter (sl_inter_to_inter sli) {x | x. x < Suc (get_largest_element sli)}"
proof (cases sli)
case (SL_Inter c ls)
thus ?thesis unfolding wf_inter_def
proof (intro allI, intro impI)
fix f cs
show "sl_inter_to_inter sli f cs ∈ {x | x. x < Suc (get_largest_element sli)}" using SL_Inter
by (cases "map_of ls (f, length cs)", auto)
qed
qed
lemma sl_helper: "set [0..<Suc n] = {x | x. x < Suc n}" by auto
text ‹lets consider different finite carriers / variants›
type_synonym label_type = "nat list"
subsection ‹arithmetic modulo, for models›
definition
sli_to_slm :: "('f, label_type) lab sl_inter ⇒ (('f, label_type) lab, nat, label_type + ('f, label_type) lab list, 'v) slm_ops"
where
"sli_to_slm sli ≡
let c = get_largest_element sli in ⦇
slm_L = λ _. Inl,
slm_I = sl_inter_to_inter sli,
slm_C = [0..< Suc c],
slm_c = c,
slm_L'' = λ _. Inl
⦈"
interpretation sl_fin_model: sl_finite_model_impl label label_decomp "λ _ _. return (sli_to_slm sli)"
proof (unfold_locales, rule label_decomp_label)
fix F G ops
assume "Inr (sli_to_slm sli) = Inr ops"
hence ops: "ops = sli_to_slm sli" by simp
show "slm_c ops ∈ set (slm_C ops) ∧ wf_inter (slm_I ops) (set (slm_C ops))"
unfolding ops sli_to_slm_def Let_def slm_ops.simps sl_helper
using wf_sl_inter by auto
qed
subsection ‹root-labeling›
definition rl_slm :: "(('f,'l)lab × nat) option ⇒ (('f,'l)lab × nat) list ⇒ (('f,'l)lab × nat) list ⇒ shows + (('f,'l)lab,('f,'l)lab,'l + ('f,'l)lab list,'v)slm_ops"
where "rl_slm delt_opt pre_fs G ≡ do {
let fs = (if delt_opt = None then pre_fs else filter (λ f. f ≠ the delt_opt) pre_fs);
check (fs ≠ [])
(''root-labeling requires at least one function symbol in the signature'' +#+ shows_nl);
let f = fst (hd fs);
return ⦇
slm_L = (λ _. Inr),
slm_I = (λ g cs. if (g,length cs) ∈ set fs then g else f),
slm_C = map fst fs,
slm_c = f,
slm_L'' = (if delt_opt = None then (λ _. Inr) else (λ _ gs. Inr (replicate (length gs) (fst (the (delt_opt))))))
⦈
}
"
interpretation rl_fin_model: sl_finite_model_impl label label_decomp "rl_slm delt_opt"
proof(unfold_locales, rule label_decomp_label)
fix F H ops
assume F: "rl_slm delt_opt F H = Inr ops"
obtain G where G: "G = (if delt_opt = None then F else filter (λ f. f ≠ the delt_opt) F)" by auto
note F = F[unfolded rl_slm_def Let_def G[symmetric]]
from F obtain f fs where f: "G = f # fs"
by (cases G, auto simp: check_def)
from F[unfolded f] have c: "slm_c ops = fst f" and I: "slm_I ops = (λ g cs. if (g,length cs) ∈ set (f # fs) then g else fst f)" and C: "slm_C ops = fst f # map fst fs"
unfolding list.sel
by (auto simp: check_def)
show "slm_c ops ∈ set (slm_C ops) ∧ wf_inter (slm_I ops) (set (slm_C ops))"
unfolding c C I wf_inter_def by force
qed
subsection ‹arithmetic modulo, for quasi-models›
fun enum_vectors_nat :: "'c list ⇒ nat ⇒ 'c list list"
where "enum_vectors_nat C 0 = [[]]"
| "enum_vectors_nat C (Suc n) = (let rec = enum_vectors_nat C n in concat (map (λ vec. map (λ c. c # vec) C) rec))"
lemma enum_vectors_nat[simp]:
shows "set (enum_vectors_nat C n) = { xs. set xs ⊆ set C ∧ length xs = n}"
proof (induct n)
case 0
show ?case by auto
next
case (Suc n)
have "set (enum_vectors_nat C (Suc n)) =
(⋃a∈{xs. set xs ⊆ set C ∧ length xs = n}. (λc. c # a) ` set C)"
unfolding enum_vectors_nat.simps Let_def
by (simp add: Suc)
also have "… = {xs. set xs ⊆ set C ∧ length xs = Suc n}" (is "?l = ?r")
proof (intro set_eqI iffI)
fix xs
assume "xs ∈ ?l"
thus "xs ∈ ?r" by auto
next
fix xs
assume "xs ∈ ?r"
thus "xs ∈ ?l" by (cases xs, auto)
qed
finally show ?case .
qed
declare enum_vectors_nat.simps[simp del]
definition qmodel_LS_gen: "qmodel_LS_gen sig LS = (λ f n. if (f,n) ∈ set sig then map Inl (enum_vectors_nat LS n) else [Inl []])"
definition qmodel_LS :: "('f × nat) list ⇒ 'l list ⇒ ('f,'l list + 'b)labels"
where [code del]: "qmodel_LS sig LS ≡ λ f n x. x ∈ (if (f,n) ∈ set sig then {Inl xs | xs. set xs ⊆ set LS ∧ length xs = n} else {Inl []})"
lemma qmodel_LS_gen': "⋀ f n. set (qmodel_LS_gen sig LS f n) = Collect (qmodel_LS sig LS f n)"
unfolding qmodel_LS_gen qmodel_LS_def set_map enum_vectors_nat image_Collect by auto
lemma [code]: "qmodel_LS sig LS = (λ f n x. x ∈ set (qmodel_LS_gen sig LS f n))"
unfolding qmodel_LS_gen' by simp
definition qmodel_L :: "(('f,'l)lab × nat) list ⇒ (('f,'l)lab,'c,'c list + 'a)label"
where "qmodel_L sig ≡ λ f cs. if (f,length cs) ∈ set sig then Inl cs else Inl []"
definition qmodel_cge where "qmodel_cge ≡ greater_eq :: nat ⇒ nat ⇒ bool"
definition qmodel_lge where "qmodel_lge f n ≡ λ l r. case (l,r) of
(Inl cs1, Inl cs2) ⇒ snd (pointwise_ext (λ x y :: nat. (y < x, y ≤ x)) cs1 cs2)
| _ ⇒ False"
definition qmodel_check_interpretation :: "arithFun ⇒ nat ⇒ nat ⇒ shows check"
where "qmodel_check_interpretation f n c ≡
let C = [0 ..< Suc c];
css = enum_vectors_nat C n
in check_allm
(λ cs. check_allm
(λ i. check_allm
(λ l. check (eval_arithFun (Suc c) cs f ≤ eval_arithFun (Suc c) (cs [i := l]) f) (shows ''not monotone in '' +@+ shows (Suc i) +@+ shows ''. argument''))
[cs ! i ..< Suc c])
[0 ..< n])
css
"
fun qmodel_check_valid :: "('f :: show)sl_inter ⇒ shows check"
where "qmodel_check_valid (SL_Inter c ls) = check_allm (λ ((f,n),g). qmodel_check_interpretation g n c <+?
(λ e. shows ''problem in weak-monotonicity of interpretation of '' +@+ shows f +@+ shows_nl +@+ e )) ls"
lemma qmodel_check_valid: assumes valid: "isOK(qmodel_check_valid sli)"
shows "cge_wm (sl_inter_to_inter sli) {x | x. x < Suc (get_largest_element sli)} qmodel_cge"
proof (cases sli)
case (SL_Inter n fas)
thus ?thesis
proof (simp, unfold cge_wm qmodel_cge_def, intro allI impI, clarify)
fix f bef c d aft
assume mem: "set ([c,d] @ bef @ aft) ⊆ {u. u < Suc n}" and dc: "d ≤ c"
let ?n = "Suc (length bef + length aft)"
let ?i = "length bef"
show "sl_inter_to_inter (SL_Inter n fas) f (bef @ d # aft) ≤ sl_inter_to_inter (SL_Inter n fas) f (bef @ c # aft)"
proof (cases "map_of fas (f, ?n)")
case None
thus ?thesis by simp
next
case (Some g)
let ?cs = "bef @ d # aft"
let ?ccs = "bef @ c # aft"
have elem: "((f, ?n), g) ∈ set fas" by (rule map_of_SomeD[OF Some])
from elem valid[unfolded SL_Inter]
have ok: "isOK(qmodel_check_interpretation g ?n n)" by auto
from mem have mem: "bef @ d # aft ∈ set (enum_vectors_nat [0 ..< Suc n] ?n)" and c: "c < Suc n" by auto
have i: "?i ∈ set [0 ..< ?n]" by auto
from dc c have c: "c ∈ set [?cs ! ?i ..< Suc n]" by auto
from ok[unfolded qmodel_check_interpretation_def Let_def,
unfolded isOK_update_error isOK_forallM,
THEN bspec[OF _ mem], THEN bspec[OF _ i], THEN bspec[OF _ c]]
have "eval_arithFun (Suc n) ?cs g ≤ eval_arithFun (Suc n) ?ccs g" by auto
thus ?thesis by (simp add: Some)
qed
qed
qed
lemma qmodel_lge_wm: "lge_wm I (qmodel_L sig) C qmodel_cge qmodel_lge"
unfolding lge_wm qmodel_cge_def qmodel_lge_def qmodel_L_def pointwise_ext_iff
proof (simp, intro allI impI, clarify)
fix f bef and c d :: nat and aft i
assume dc: "d ≤ c"
show "(bef @ d # aft) ! i ≤ (bef @ c # aft) ! i"
proof (cases "i = length bef")
case True thus ?thesis by (simp add: dc)
next
case False note oFalse = this
thus ?thesis
proof (cases "i < length bef")
case True
thus ?thesis by (simp add: nth_append)
next
case False
with oFalse have "i - length bef > 0" by auto
then obtain j where "i - length bef = Suc j"
by (cases "i - length bef") auto
thus ?thesis by (simp add: nth_append)
qed
qed
qed
definition
check_decr_present_aux_1 :: "('f, 'v × nat)rules ⇒ 'v ⇒ 'f ⇒ 'f ⇒ nat ⇒ ('f,'v × nat) rule check"
where
"check_decr_present_aux_1 R v f1 f2 n ≡
let
vs = map (λ n. Var (v,n)) [0 ..< n];
rule = (Fun f1 vs, Fun f2 vs)
in check (List.find (instance_rule rule) R ≠ None) rule"
lemma check_decr_present_aux_1:
fixes R :: "('f,'v × nat)rules"
assumes check: "isOK(check_decr_present_aux_1 R v f1 f2 n)"
shows "{(Fun f1 ts,Fun f2 ts) | ts. length ts = n} ⊆ subst.closure (set R)"
proof -
{
fix ts :: "('f,'v × nat) term list"
assume len: "length ts = n"
let ?n = "[0 ..< n]"
let ?vs = "map (λ n. Var (v,n)) ?n"
let ?rule = "(Fun f1 ?vs, Fun f2 ?vs)"
have "List.find (instance_rule ?rule) R ≠ None" (is "?f ≠ None")
using check[unfolded check_decr_present_aux_1_def Let_def] by auto
then obtain rule where "?f = Some rule" by (cases ?f, auto)
from this[unfolded find_Some_iff] have rule: "rule ∈ set R"
and inst: "instance_rule ?rule rule" by auto
from inst[unfolded instance_rule_def] obtain σ where
id: "?rule = (fst rule ⋅ σ, snd rule ⋅ σ)" by auto
obtain δ :: "('f, 'v × nat) subst" where delta: "δ = (λ(_,i). ts ! i)" by auto
obtain γ where gamma: "γ = σ ∘⇩s δ" by auto
have ts_delta: "map (λ t. t ⋅ δ) ?vs = ts" unfolding delta
by (rule nth_equalityI, auto simp add: len)
hence "(Fun f1 ts, Fun f2 ts) = (Fun f1 ?vs ⋅ δ, Fun f2 ?vs ⋅ δ)" by auto
with id have id: "(Fun f1 ts, Fun f2 ts) = (fst rule ⋅ γ, snd rule ⋅ γ)"
by (auto simp: gamma)
have "(Fun f1 ts, Fun f2 ts) ∈ subst.closure (set R)"
unfolding id by (auto simp: rule)
}
thus ?thesis by auto
qed
definition
check_decr_present_aux_2 ::
"('f, 'v) rules ⇒ 'v ⇒ ('f × 'f × nat) list ⇒ ('f, 'v × nat) rule check"
where
"check_decr_present_aux_2 R v req = (
let
(add_nats :: ('f, 'v) term ⇒ ('f,'v × nat) term) = map_vars_term (λ v. (v, 0));
R' = map (λ(l, r). (add_nats l, add_nats r)) R
in check_allm (λ(f1 :: 'f, f2, n). check_decr_present_aux_1 R' v f1 f2 n) req)"
lemma check_decr_present_aux_2:
fixes R :: "('f,'v)rules"
assumes check: "isOK(check_decr_present_aux_2 R v req)"
shows "{(Fun f1 ts, Fun f2 ts) | f1 f2 n ts. (f1,f2,n) ∈ set req ∧ length ts = n} ⊆ subst.closure (set R)"
proof -
{
fix f1 f2 :: 'f and n :: nat and ts :: "('f,'v)term list"
let ?add_nats = "map_vars_term (λ v. (v, 0)) :: ('f,'v)term ⇒ ('f,'v × nat)term"
let ?rem_nats = "map_vars_term (λ (v,n). v) :: ('f,'v × nat)term ⇒ ('f,'v)term"
let ?R = "map (λ (l,r). (?add_nats l, ?add_nats r)) R"
let ?ts = "map ?add_nats ts"
assume "(f1,f2,n) ∈ set req" and len: "length ts = n"
from this check[unfolded check_decr_present_aux_2_def Let_def]
have "isOK(check_decr_present_aux_1 ?R v f1 f2 n)" by auto
from check_decr_present_aux_1[OF this] len
have "(Fun f1 ?ts, Fun f2 ?ts) ∈ subst.closure (set ?R)" by auto
hence "(?rem_nats (Fun f1 ?ts), ?rem_nats (Fun f2 ?ts)) ∈ (λ (l,r). (?rem_nats l, ?rem_nats r)) ` subst.closure (set ?R)" (is "_ ∈ ?RR") by force
hence mem: "(Fun f1 ts, Fun f2 ts) ∈ ?RR"
unfolding term.map(2) [of "λx. x", symmetric] map_vars_term_compose
by (simp add: o_def map_vars_term_id [simplified id_def])
then obtain l r where mem: "(l,r) ∈ subst.closure (set ?R)"
and "Fun f1 ts = ?rem_nats l" and "Fun f2 ts = ?rem_nats r" by force
then obtain l r σ where mem: "(l,r) ∈ set R"
and l: "Fun f1 ts = ?rem_nats (?add_nats l ⋅ σ)" and r: "Fun f2 ts = ?rem_nats (?add_nats r ⋅ σ)" by (force elim: subst.closure.cases)
obtain δ where delta: "δ = (λv. ?rem_nats (Var (v,0) ⋅ σ))" by auto
{
fix t
have "?rem_nats (?add_nats t ⋅ σ) = t ⋅ δ"
proof (induct t)
case (Var x)
show ?case unfolding delta by (auto)
next
case (Fun f ts)
thus ?case by auto
qed
}
with l r have "Fun f1 ts = l ⋅ δ" and "Fun f2 ts = r ⋅ δ" by auto
with mem have "(Fun f1 ts, Fun f2 ts) ∈ subst.closure (set R)"
by (auto) (metis subst.closureI2)
}
thus ?thesis by auto
qed
definition check_decr_present :: "('f × nat)list ⇒ ('f ⇒ nat list ⇒ 'f) ⇒ 'v ⇒ nat ⇒ ('f,'v)rules ⇒ ('f,'v × nat) rule check"
where "check_decr_present sig l v c R ≡
let C = [0 ..< Suc c];
ls = λ (f,n). concat (map (λ cs.
concat (map (λ i. let ci = cs ! i in if ci < c then [(l f (cs[ i:= Suc ci]),l f cs,n)] else []) [0 ..< n])
) (enum_vectors_nat C n))
in check_decr_present_aux_2 R v (concat (map ls sig))"
lemma check_decr_present_1:
assumes check: "isOK(check_decr_present sig l v c R)"
and f: "(f,n) ∈ set sig"
and i: "i < n"
and d: "d < c"
and cs: "set cs ⊆ {0 ..< Suc c}"
and ts: "length ts = n"
and lcs: "length cs = n"
shows "(Fun (l f (cs[i := Suc d])) ts, Fun (l f (cs[i := d])) ts) ∈ subst.closure (set R)"
proof -
let ?C = "[0 ..< Suc c]"
let ?ls = "λ (f,n). concat (map (λ cs.
concat (map (λ i. let ci = cs ! i in if ci < c then [(l f (cs[ i:= Suc ci]),l f cs,n)] else []) [0 ..< n])
) (enum_vectors_nat ?C n))"
let ?ll = "l f (cs[i := Suc d])"
let ?lr = "l f (cs[i := d])"
let ?req = "set (concat (map ?ls sig))"
have "set (cs[i := d]) ⊆ {0 ..< Suc c}" using cs
proof (induct cs arbitrary: i)
case (Cons e cs)
from d have "d < Suc c" by simp
with Cons show ?case by (cases i, auto)
qed simp
moreover have "∃a∈{0..<n}.
(?ll, ?lr, n) ∈ set (let ci = cs[i := d] ! a
in if ci < c
then [(l f (cs[i := d, a := Suc ci]), l f (cs[i := d]), n)]
else [])"
by (rule bexI[of _ i], auto simp: Let_def i lcs d)
moreover have "length (cs[i := d]) = n" using lcs by simp
ultimately have "(?ll,?lr,n) ∈ ?req"
by (simp del: upt_Suc, intro bexI[OF _ f], simp del: upt_Suc, intro exI[of _ "cs[i := d]"], auto)
thus ?thesis using check_decr_present_aux_2[OF check[unfolded check_decr_present_def Let_def]] ts
unfolding Let_def by blast
qed
lemma check_decr_present_2:
assumes check: "isOK(check_decr_present sig Lab v c R)"
and f: "(f,n) ∈ set sig"
and i: "i < n"
and d: "d < e"
and e: "e ≤ c"
and cs: "set cs ⊆ {0 ..< Suc c}"
and ts: "length ts = n"
and lcs: "length cs = n"
shows "(Fun (Lab f (cs[i := e])) ts, Fun (Lab f (cs[i := d])) ts) ∈ (subst.closure (set R) ∩ (decr_of_ord (lge_to_lgr_rel qmodel_lge (qmodel_LS sig [0..<Suc c])) label (qmodel_LS sig [0..<Suc c])))^+" (is "_ ∈ (_ ∩ ?Ord)^+")
proof -
from d obtain diff where "e - d = Suc diff" by (cases "e - d", auto)
with d e have e: "e = Suc (d + diff)" and diff: "Suc (d + diff) ≤ c" by auto
have ord: "⋀ d e :: nat. ⟦d ≤ c; d > e⟧ ⟹ (Fun (Lab f (cs[i := d])) ts, Fun (Lab f (cs[i := e])) ts) ∈ ?Ord"
proof -
fix d e :: nat
assume ed: "e < d" and dc: "d ≤ c"
hence ec: "e < Suc c" and dc: "d < Suc c" by auto
have csd: "set (cs[i := d]) ⊆ {0 ..< Suc c}"
by (rule set_update_subsetI[OF cs], simp add: dc)
have cse: "set (cs[i := e]) ⊆ {0 ..< Suc c}"
by (rule set_update_subsetI[OF cs], simp add: ec)
have csde: "cs[i := d] ≠ cs[i := e]" (is "?d ≠ ?e")
proof
assume "?d = ?e"
hence "?d ! i = ?e ! i" by simp
thus False using i[unfolded lcs[symmetric]] ed by auto
qed
show "(Fun (Lab f (cs[i := d])) ts, Fun (Lab f (cs[i := e])) ts) ∈ ?Ord"
unfolding decr_of_ord_def lge_to_lgr_rel_def lge_to_lgr_def Let_def qmodel_lge_def qmodel_LS_def
proof (intro CollectI, rule exI[of _ f], rule exI[of _ "Inl (cs[i := d])"], rule exI[of _ "Inl (cs[i := e])"], rule exI[of _ ts],
simp add: f ts lcs pointwise_ext_iff csd cse csde del: upt_Suc)
show "∀ j < n. ?e ! j ≤ ?d ! j"
proof (intro allI impI)
fix j
assume "j < n"
with ed show "?e ! j ≤ ?d ! j"
unfolding lcs[symmetric] by (cases "j = i", auto)
qed
qed
qed
from diff have "(Fun (Lab f (cs[i := Suc (d + diff)])) ts, Fun (Lab f (cs[i := d])) ts) ∈ (subst.closure (set R) ∩ ?Ord)^+"
proof (induct diff)
case 0
hence dc1: "d < c" and dc2: "Suc d ≤ c" by auto
from check_decr_present_1[OF check f i dc1 cs ts lcs]
have one: "(Fun (Lab f (cs[i := Suc d])) ts, Fun (Lab f (cs[i := d])) ts) ∈ subst.closure (set R)" (is "?pair ∈ ?subst_closure") .
have "?pair ∈ ?Ord" by (rule ord[OF dc2], simp)
with one show ?case by force
next
case (Suc diff)
hence rec: "(Fun (Lab f (cs[i := Suc (d + diff)])) ts, Fun (Lab f (cs[i := d])) ts) ∈ (subst.closure (set R) ∩ ?Ord)^+" (is "(?m,?r) ∈ _") by auto
from Suc(2) have dc1: "Suc (d + diff) < c" and dc2: "Suc (Suc (d + diff)) ≤ c" by auto
from check_decr_present_1[OF check f i dc1 cs ts lcs]
have cs: "(Fun (Lab f (cs[i := Suc (Suc (d + diff))])) ts, ?m) ∈ subst.closure (set R)" (is "(?l,_) ∈ ?subst_closure") .
obtain rel where rel: "?subst_closure ∩ ?Ord = rel" by auto
have "(?l,?m) ∈ ?Ord" by (rule ord[OF dc2], simp)
with cs have "(?l,?m) ∈ ?subst_closure ∩ ?Ord" by auto
with rec show ?case unfolding rel by auto
qed
with e show ?thesis by simp
qed
lemma check_decr_present: assumes check: "isOK(check_decr_present sig Lab v c R)"
and f: "(f,n) ∈ set sig"
and cs: "set cs ⊆ {0 ..< Suc c}"
and ds: "set ds ⊆ {0 ..< Suc c}"
and ts: "length ts = n"
and lcs: "length cs = n"
and gt: "fst (pointwise_ext (λ x y :: nat. (y < x, y ≤ x)) cs ds)"
shows "(Fun (Lab f cs) ts, Fun (Lab f ds) ts) ∈ (subst.closure (set R) ∩ (decr_of_ord (lge_to_lgr_rel qmodel_lge (qmodel_LS sig [0..<Suc c])) label (qmodel_LS sig [0..<Suc c])))^+" (is "_ ∈ (_ ∩ ?Ord)^+")
proof -
note check = check_decr_present_2[OF check f _ _ _ _ ts]
let ?subst_closure = "subst.closure (set R)"
let ?R = "?subst_closure ∩ ?Ord"
let ?C = "{0 ..< Suc c}"
from gt[unfolded pointwise_ext_iff] lcs obtain i where
lds: "length ds = n" and ids: "i < length ds" and ics: "i < length cs" and gt: "ds ! i < cs ! i"
and ge: "⋀ i. i < length ds ⟹ ds ! i ≤ cs ! i" and i: "i < n" by auto
let ?csds = "λ i. take i ds @ drop i cs"
let ?l = "Fun (Lab f cs) ts"
let ?r = "λ j. Fun (Lab f (?csds j)) ts"
from lcs lds have lcsds: "⋀ j. length (?csds j) = n" by auto
{
fix j
assume "j ≤ length ds"
hence "(?l, ?r j) ∈ ?R^* ∧ set (?csds j) ⊆ ?C ∧ (j > i ⟶ (?l, ?r j) ∈ ?R^+)"
proof (induct j)
case 0
show ?case by (simp add: cs)
next
case (Suc j)
with lds
have ind1: "(?l, ?r j) ∈ ?R^*" and ind2: "set (?csds j) ⊆ ?C" and ind3: "j > i ⟶ (?l, ?r j) ∈ ?R^+" and j: "j < n" by auto
from j lcs have idd: "(?csds j)[ j := ds ! j] = ?csds (Suc j)" unfolding lds[symmetric] by (rule take_drop_update_first)
from j lcs have idc: "(?csds j)[ j := cs ! j] = ?csds j" unfolding lds[symmetric] by (rule take_drop_update_second)
from j cs lcs have csj: "cs ! j ≤ c" unfolding set_conv_nth by auto
{
assume "cs ! j > ds ! j"
from check[OF j this csj ind2 lcsds]
have "(Fun (Lab f ((?csds j)[ j := cs ! j])) ts, Fun (Lab f ((?csds j)[ j := ds ! j])) ts) ∈ ?R^+" .
hence "(?r j, ?r (Suc j)) ∈ ?R^+" by (simp only: idd idc)
} note strict = this
{
assume "¬ (cs ! j > ds ! j)"
with j ge lds have "cs ! j = ds ! j" by force
hence "(?csds j)[j := ds ! j] = (?csds j)[j := cs ! j]" by simp
hence "?csds (Suc j) = ?csds j" unfolding idd idc .
hence "(?r j, ?r (Suc j)) ∈ ?R^*" by simp
} note non_strict = this
from strict non_strict have non_strict: "(?r j, ?r (Suc j)) ∈ ?R^*" by (cases "cs ! j > ds ! j", auto)
with ind1 have "(?l, ?r (Suc j)) ∈ ?R^*" by auto
moreover have "set (?csds (Suc j)) ⊆ ?C"
proof
fix x
assume "x ∈ set (?csds (Suc j))"
hence "x ∈ set (take (Suc j) ds) ∨ x ∈ set (drop (Suc j) cs)" by auto
thus "x ∈ ?C"
proof
assume "x ∈ set (drop (Suc j) cs)"
with set_drop_subset[of "Suc j" cs] cs
show "x ∈ ?C" by auto
next
assume "x ∈ set (take (Suc j) ds)"
with set_take_subset[of "Suc j" ds] ds
show "x ∈ ?C" by auto
qed
qed
moreover have "Suc j > i ⟶ (?l, ?r (Suc j)) ∈ ?R^+"
proof
assume sj: "Suc j > i"
show "(?l, ?r (Suc j)) ∈ ?R^+"
proof (cases "i = j")
case False
with sj have "j > i" by auto
with ind3 non_strict show ?thesis by auto
next
case True
from strict[OF gt[unfolded True]] ind1 show ?thesis by auto
qed
qed
ultimately show ?case by blast
qed
}
from this[of "length ds"] ids have "(?l, ?r (length ds)) ∈ ?R^+" by simp
with lcs lds show ?thesis by auto
qed
definition "qmodel_check_decr sig v c ≡ λ lR. check_decr_present sig Lab v c lR
<+? (λ r. let display = map_vars_term (λ (_,n). (shows ''x'' +@+ shows n) []) in
shows ''decreasing rule '' +@+ shows_rule (display (fst r), display (snd r)) +@+ shows '' missing'')"
lemma qmodel_check_decr:
assumes ok: "isOK(qmodel_check_decr sig v n lR)"
shows "decr_of_ord (lge_to_lgr_rel qmodel_lge (qmodel_LS sig [0 ..< Suc n])) label (qmodel_LS sig [0 ..< Suc n])
⊆ (subst.closure (set lR) ∩ decr_of_ord (lge_to_lgr_rel qmodel_lge (qmodel_LS sig [0 ..< Suc n])) label (qmodel_LS sig [0 ..< Suc n]))^+" (is "?Decr ⊆ _")
proof -
let ?g = "λ x y :: nat. (y < x, y ≤ x)"
let ?C = "{0 ..< Suc n}"
have C: "?C = insert n {0 ..< n}" by auto
let ?labs = "λ f ts. if (f, length ts) ∈ set sig then {Inl xs |xs. set xs ⊆ set [0..<Suc n] ∧ length xs = length ts} else {Inl []}"
{
fix l r :: "(('a,nat list)lab,'b)term"
assume mem: "(l,r) ∈ ?Decr"
then obtain f ts lab1 lab2 where l: "l = Fun (label f (length ts) lab1) ts" and r: "r = Fun (label f (length ts) lab2) ts"
and neq: "lab1 ≠ lab2" and lab1: "lab1 ∈ ?labs f ts" and lab2: "lab2 ∈ ?labs f ts" and ll: "(lab1,lab2) ∈ {(l,l') | l l'. case (l, l') of
(Inl cs1, Inl cs2) ⇒
snd (pointwise_ext ?g cs1 cs2)
| (Inl cs1, Inr ba) ⇒ False | (Inr bb, b) ⇒ False}" (is "_ ∈ ?ll")
unfolding qmodel_LS_def lge_to_lgr_rel_def lge_to_lgr_def qmodel_lge_def decr_of_ord_def Let_def by auto
note mem = mem[unfolded l r]
let ?labs = "?labs f ts"
from lab1 obtain cs1 where cs1: "lab1 = Inl cs1" by (cases lab1, simp, cases "(f,length ts) ∈ set sig", auto)
from lab2 obtain cs2 where cs2: "lab2 = Inl cs2" by (cases lab2, simp, cases "(f,length ts) ∈ set sig", auto)
have sig: "(f,length ts) ∈ set sig"
proof (rule ccontr)
assume "¬ ?thesis"
with lab1 lab2 neq show False unfolding cs1 cs2 by auto
qed
note mem = mem[unfolded cs1 cs2]
from ll neq
have snd: "snd (pointwise_ext ?g cs1 cs2)" and neq: "cs1 ≠ cs2" unfolding cs1 cs2 by auto
let ?pair = "(Fun (Lab f cs1) ts, Fun (Lab f cs2) ts)"
from pointwise_ext_snd_neq_imp_fst[OF _ snd neq]
have fst: "fst (pointwise_ext ?g cs1 cs2)" by auto
from lab1[unfolded cs1] have cs1C: "set cs1 ⊆ ?C" and lcs1: "length cs1 = length ts" by (auto simp: sig)
from lab2[unfolded cs2] have cs2C: "set cs2 ⊆ ?C" and lcs2: "length cs2 = length ts" by (auto simp: sig)
from ok[unfolded qmodel_check_decr_def]
have "isOK(check_decr_present sig Lab v n lR)" by simp
from check_decr_present[OF this sig cs1C cs2C refl lcs1 fst]
have "(l,r) ∈ (subst.closure (set lR) ∩ ?Decr)^+" unfolding l r cs1 cs2 by simp
}
thus ?thesis ..
qed
lemma qmodel_wf_label: "wf_label (qmodel_L F) (qmodel_LS F [0..<Suc (get_largest_element sli)])
{x |x. x < Suc (get_largest_element sli)}"
unfolding qmodel_L_def qmodel_LS_def sl_helper wf_label_def by auto
lemma qmodel_SN: "SN (lge_to_lgr_rel qmodel_lge U f n)" (is "SN ?r")
proof
fix S
assume "∀ i. (S i, S (Suc i)) ∈ ?r"
hence steps: "⋀ i. (S i, S (Suc i)) ∈ ?r" ..
{
fix i
from steps[of i] obtain xs where Si: "S i = Inl xs"
unfolding lge_to_lgr_rel_def qmodel_lge_def lge_to_lgr_def Let_def
by (cases "S i", auto)
hence "∃ xs. S i = Inl xs" ..
}
hence "∀ i. ∃ xs. S i = Inl xs" ..
from choice[OF this] obtain z where "⋀ i. S i = Inl (z i)" by auto
with steps have steps: "⋀ i. (Inl (z i), Inl (z (Suc i))) ∈ ?r" by auto
let ?g = "λ x y :: nat. (y < x, y ≤ x)"
{
fix i
from steps[of i]
have "snd (pointwise_ext ?g (z i) (z (Suc i)))" and "z i ≠ z (Suc i)"
unfolding lge_to_lgr_rel_def qmodel_lge_def lge_to_lgr_def Let_def
by auto
from pointwise_ext_snd_neq_imp_fst[OF _ this]
have "fst (pointwise_ext ?g (z i) (z (Suc i)))" by auto
} note steps = this
have "SN {(ys, xs). fst (pointwise_ext ?g ys xs)}"
by (rule pointwise_ext_SN_2[of ?g], auto simp: SN_iff_wf converse_def wf_less)
with steps show False by auto
qed
definition pointwise_lgen :: "label_type ⇒ label_type list"
where "pointwise_lgen ns ≡ concat_lists (map (λ n. [0 ..< Suc n]) ns)"
lemma pointwise_lgen: "set (pointwise_lgen ns) = {ms. snd (pointwise_ext (λ n m. (n > m, n ≥ m)) ns ms)}"
unfolding pointwise_lgen_def set_concat_lists pointwise_ext_iff by auto
definition qmodel_lgen :: "label_type + 'a ⇒ (label_type + 'a) list"
where "qmodel_lgen l ≡ case l of Inl ns ⇒ map Inl (pointwise_lgen ns) | _ ⇒ []"
lemma qmodel_lgen: "set (qmodel_lgen l) = {l'. qmodel_lge f n l l'}"
proof (cases l)
case (Inr x)
thus ?thesis unfolding qmodel_lge_def qmodel_lgen_def by auto
next
case (Inl x)
have "set (qmodel_lgen l) = Inl ` {ms. snd (pointwise_ext (λn m. (m < n, m ≤ n)) x ms)}"
unfolding qmodel_lgen_def Inl set_map pointwise_lgen sum.simps ..
also have "... = {l'. case l' of Inl cs2 ⇒ snd (pointwise_ext (λx y. (y < x, y ≤ x)) x cs2)
| Inr ba ⇒ False}" (is "?l = ?r")
proof -
{
fix x
assume "x ∈ ?l" hence "x ∈ ?r" by auto
}
moreover
{
fix x
assume r: "x ∈ ?r"
then obtain l' where x: "x = Inl l'" by (cases x, auto)
from r have "x ∈ ?l" unfolding x by auto
}
ultimately show ?thesis by blast
qed
finally
show ?thesis unfolding Inl qmodel_lge_def sum.simps split
by blast
qed
definition
qmodel_LS' :: "(('f, label_type) lab, label_type + ('f, label_type) lab list) labels"
where
"qmodel_LS' ≡ λ _ _ x. case x of Inl _ ⇒ True | Inr _ ⇒ False"
definition qsli_to_sl_unsafe :: "'v ⇒ (('f :: show,label_type)lab × nat)list ⇒ (('f,label_type)lab × nat)list ⇒ ('f,label_type)lab sl_inter ⇒ (('f,label_type)lab,nat,label_type + ('f,label_type)lab list,'v)sl_ops"
where "qsli_to_sl_unsafe v F G sli ≡
let c = get_largest_element sli;
C = [0..< Suc c] in
⦇
sl_L = qmodel_L F,
sl_LS = qmodel_LS F C,
sl_I = sl_inter_to_inter sli,
sl_C = C,
sl_c = c,
sl_check_decr = qmodel_check_decr F v c,
sl_L'' = qmodel_L G,
sl_LS'' = qmodel_LS',
sl_lgen = qmodel_lgen,
sl_LS_gen = qmodel_LS_gen F C
⦈"
definition qsli_to_sl :: "'v ⇒ (('f :: show,label_type)lab × nat)list ⇒ (('f,label_type)lab × nat)list ⇒ ('f,label_type)lab sl_inter ⇒ shows + (('f,label_type)lab,nat,label_type + ('f,label_type)lab list,'v)sl_ops"
where "qsli_to_sl v F G sli ≡ do {
qmodel_check_valid sli;
return (qsli_to_sl_unsafe v F G sli)
}"
interpretation arith_finite_qmodel: sl_finite_impl label label_decomp qmodel_cge qmodel_lge "λ F G. qsli_to_sl v F G sli"
unfolding sl_finite_impl_def
proof (intro allI impI conjI)
fix F G ops f n and l l' :: "nat list + ('a,nat list)lab list"
assume ok: "qsli_to_sl v F G sli = Inr ops" and lge: "qmodel_lge f n l l'"
hence ops: "ops = qsli_to_sl_unsafe v F G sli"
by (cases "qmodel_check_valid sli", auto simp: qsli_to_sl_def)
show "l' ∈ set (sl_lgen ops l)"
using lge
unfolding ops qsli_to_sl_unsafe_def Let_def sl_ops.simps
unfolding qmodel_lgen[of l, of f n] by auto
next
fix F G ops D
assume ok: "isOK (sl_check_decr ops D)" and "qsli_to_sl v F G sli = Inr ops"
hence ops: "ops = qsli_to_sl_unsafe v F G sli"
by (cases "qmodel_check_valid sli", auto simp: qsli_to_sl_def)
show " decr_of_ord (lge_to_lgr_rel qmodel_lge (sl_LS ops)) label (sl_LS ops)
⊆ (subst.closure (set D) ∩
decr_of_ord (lge_to_lgr_rel qmodel_lge (sl_LS ops)) label
(sl_LS ops))⇧+"
unfolding ops qsli_to_sl_unsafe_def Let_def sl_ops.simps
by (rule qmodel_check_decr, insert ok, auto simp: ops qsli_to_sl_unsafe_def Let_def)
next
fix F G ops
assume ok: "qsli_to_sl v F G sli = Inr ops"
hence ops: "ops = qsli_to_sl_unsafe v F G sli ∧ isOK(qmodel_check_valid sli)"
by (cases "qmodel_check_valid sli", auto simp: qsli_to_sl_def)
note ok = ops[THEN conjunct2]
note ops = ops[THEN conjunct1]
show "sl_interpr_root_same (set (sl_C ops)) (sl_c ops) (sl_I ops) qmodel_cge
qmodel_lge (sl_L ops) label label_decomp (sl_LS ops) (sl_L'' ops) (sl_LS'' ops)"
unfolding ops qsli_to_sl_unsafe_def Let_def sl_ops.simps sl_helper
proof(unfold_locales, simp, rule wf_sl_inter, rule qmodel_wf_label, rule qmodel_check_valid[OF ok],
rule qmodel_lge_wm, rule qmodel_SN, rule label_decomp_label)
fix f n x y z
assume one: "qmodel_lge f n x y" and two: "qmodel_lge f n y z"
from one obtain xx where x: "x = Inl xx" by (unfold qmodel_lge_def, cases x,simp, cases y, auto)
from one obtain yy where y: "y = Inl yy" by (unfold qmodel_lge_def, cases x,simp, cases y, auto)
from two obtain zz where z: "z = Inl zz" by (unfold qmodel_lge_def, cases y,simp, cases z, auto)
from one two
show "qmodel_lge f n x z"
unfolding qmodel_lge_def x y z
using pointwise_snd_trans[of _ xx yy zz] by force
next
show "wf_label (qmodel_L G) qmodel_LS' { x | x. x < Suc (get_largest_element sli)}"
unfolding wf_label_def qmodel_L_def qmodel_LS'_def by auto
next
fix f n x
assume "qmodel_LS' f n x"
thus "qmodel_lge f n x x" unfolding qmodel_lge_def qmodel_LS'_def
by (cases x, auto intro: pointwise_ext_refl)
next
show "lge_wm (sl_inter_to_inter sli) (qmodel_L G)
{x | x. x < Suc (get_largest_element sli)} qmodel_cge qmodel_lge"
by (rule qmodel_lge_wm)
qed (insert qmodel_SN, auto)
qed
interpretation arith_finite_LS_qmodel: sl_finite_LS_impl label label_decomp qmodel_cge qmodel_lge "λ F G. qsli_to_sl v F G sli"
proof(unfold_locales)
fix F G ops f n
assume "qsli_to_sl v F G sli = Inr ops"
hence ops: "ops = qsli_to_sl_unsafe v F G sli"
by (cases "qmodel_check_valid sli", auto simp: qsli_to_sl_def)
thus "set (sl_LS_gen ops f n) = Collect (sl_LS ops f n)" unfolding ops
by (simp add: qsli_to_sl_unsafe_def Let_def qmodel_LS_gen')
qed
datatype ('f,'v)sl_variant = Rootlab "('f × nat) option" | Finitelab "'f sl_inter" | QuasiFinitelab "'f sl_inter" 'v
fun semlab_fin_tt :: "('tp,('f :: show,label_type)lab,'v :: show)tp_ops ⇒ (('f,label_type)lab,'v)sl_variant ⇒ (('f,label_type)lab,'v) term list ⇒ (('f,label_type)lab,'v)rules ⇒ 'tp proc"
where "semlab_fin_tt J (Rootlab _) =
sem_lab_fin_tt (model_splitter label_decomp) label label_decomp model_cge J (slm_gen_to_sl_gen (rl_slm None))"
| "semlab_fin_tt J (Finitelab sli) =
sem_lab_fin_tt (model_splitter label_decomp) label label_decomp model_cge J (slm_gen_to_sl_gen (λ_ _. return (sli_to_slm sli)))"
| "semlab_fin_tt J (QuasiFinitelab sli v) =
sem_lab_fin_tt (quasi_splitter label_decomp) label label_decomp qmodel_cge J (λ F G . qsli_to_sl v F G sli)"
lemma semlab_fin_tt: assumes I: "tp_spec I"
shows "tp_spec.sound_tt_impl I (semlab_fin_tt I sli lQ lAll)"
proof -
interpret tp_spec I by fact
show ?thesis
using sl_fin_model.sem_lab_fin_tt[OF I]
rl_fin_model.sem_lab_fin_tt[OF I]
arith_finite_qmodel.sem_lab_fin_tt[OF I]
unfolding sound_tt_impl_def
by (cases sli, auto)
qed
fun semlab_fin_proc :: "('dp,('f :: show,label_type)lab,'v :: show)dpp_ops ⇒ (('f,label_type)lab,'v) sl_variant ⇒
(('f,label_type)lab,'v)rules ⇒
(('f,label_type)lab,'v)term list ⇒
(('f,label_type)lab,'v)rules ⇒ 'dp proc"
where "semlab_fin_proc J (Rootlab None) =
sem_lab_fin_proc label label_decomp J (slm_gen_to_sl_gen (rl_slm None))"
| "semlab_fin_proc J (Rootlab (Some d)) =
sem_lab_fin_root_proc label label_decomp J (slm_gen_to_sl_gen (rl_slm (Some d)))"
| "semlab_fin_proc J (Finitelab sli) =
sem_lab_fin_proc label label_decomp J (slm_gen_to_sl_gen (λ_ _. return (sli_to_slm sli)))"
| "semlab_fin_proc J (QuasiFinitelab sli v) =
sem_lab_fin_quasi_root_proc label label_decomp qmodel_cge qmodel_lge J (λ F G. qsli_to_sl v F G sli)"
lemma semlab_fin_proc: assumes I: "dpp_spec I"
shows "dpp_spec.sound_proc_impl I (semlab_fin_proc I sli lPAll lQ lRAll)"
proof -
interpret dpp_spec I by fact
show ?thesis
proof (cases sli)
case (Rootlab d_opt)
show ?thesis
proof (cases d_opt)
case None
show ?thesis unfolding Rootlab None semlab_fin_proc.simps
proof (rule rl_fin_model.sem_lab_fin_model_proc[OF I])
fix F G ops f
assume "rl_slm None F G = Inr ops"
thus "inj (slm_L ops f)" unfolding inj_on_def rl_slm_def Let_def
by (cases F, auto simp: check_def)
qed
next
case (Some d)
show ?thesis unfolding Rootlab Some semlab_fin_proc.simps
proof (rule rl_fin_model.sem_lab_fin_model_root_proc[OF I])
fix F G ops f
assume "rl_slm (Some d) F G = Inr ops"
thus "inj (slm_L ops f)" unfolding inj_on_def rl_slm_def Let_def
by (cases "[f ← F. f ≠ d]", auto simp: check_def)
qed
qed
next
case (Finitelab sl)
show ?thesis
unfolding Finitelab semlab_fin_proc.simps
proof (rule sl_fin_model.sem_lab_fin_model_proc[OF I])
fix F G ops f
assume "Inr (sli_to_slm sl) = Inr ops"
thus "inj (slm_L ops f)" unfolding inj_on_def sli_to_slm_def Let_def
by auto
qed
next
case (QuasiFinitelab sli v)
show ?thesis
unfolding QuasiFinitelab semlab_fin_proc.simps
by (rule arith_finite_LS_qmodel.sem_lab_fin_quasi_root_proc[OF I])
qed
qed
end