Theory MLSSmf_Semantics

theory MLSSmf_Semantics imports
  MLSSmf_Defs HereditarilyFinite.Finitary
begin

fun It :: "('v ⇒ hf) ⇒ ('f ⇒ hf ⇒ hf) ⇒ ('v, 'f) MLSSmf_term ⇒ hf" where
  "It Mv Mf (∅m _) = 0" |
  "It Mv Mf (Varm x) = Mv x" |
  "It Mv Mf (t1 ⊔m t2) = It Mv Mf t1 ⊔ It Mv Mf t2" |
  "It Mv Mf (t1 ⊓m t2) = It Mv Mf t1 ⊓ It Mv Mf t2" |
  "It Mv Mf (t1 -m t2) = It Mv Mf t1 - It Mv Mf t2" |
  "It Mv Mf (Singlem t) = HF {It Mv Mf t}" |
  "It Mv Mf (App f t) = (Mf f) (It Mv Mf t)"

fun Ia :: "('v ⇒ hf) ⇒ ('f ⇒ hf ⇒ hf) ⇒ ('v, 'f) MLSSmf_atom ⇒ bool" where
  "Ia Mv Mf (t1 ∈m t2) ⟷ It Mv Mf t1 ∈ It Mv Mf t2" |
  "Ia Mv Mf (t1 =m t2) ⟷ It Mv Mf t1 = It Mv Mf t2" |
  "Ia Mv Mf (inc(f)) = (∀s t. s ≤ t ⟶ (Mf f) s ≤ (Mf f) t)" |
  "Ia Mv Mf (dec(f)) = (∀s t. s ≤ t ⟶ (Mf f) t ≤ (Mf f) s)" |
  "Ia Mv Mf (add(f)) = (∀s t. (Mf f) (s ⊔ t) = (Mf f) s ⊔ (Mf f) t)" |
  "Ia Mv Mf (mul(f)) = (∀s t. (Mf f) (s ⊓ t) = (Mf f) s ⊓ (Mf f) t)" |
  "Ia Mv Mf (f ≼m g) = (∀s. (Mf f) s ≤ (Mf g) s)"

fun Il :: "('v ⇒ hf) ⇒ ('f ⇒ hf ⇒ hf) ⇒ ('v, 'f) MLSSmf_literal ⇒ bool" where
  "Il Mv Mf (ATm a) = Ia Mv Mf a" |
  "Il Mv Mf (AFm a) = (¬ Ia Mv Mf a)"

fun Icl :: "('v ⇒ hf) ⇒ ('f ⇒ hf ⇒ hf) ⇒ ('v, 'f) MLSSmf_clause ⇒ bool" where
  "Icl Mv Mf [] = True" |
  "Icl Mv Mf (l # ls) = (Il Mv Mf l ∧ Icl Mv Mf ls)"

lemma cl_is_true_iff_all_literals_true[iff]:
  "Icl Mv Mf 𝒞 ⟷ (∀l ∈ set 𝒞. Il Mv Mf l)"
proof
  assume "Icl Mv Mf 𝒞"
  then show "∀l∈set 𝒞. Il Mv Mf l"
    by (induction 𝒞) auto
next
  assume "∀l∈set 𝒞. Il Mv Mf l"
  then show "Icl Mv Mf 𝒞"
    by (induction 𝒞) auto
qed

end