Theory Propositional_Logic

(*<*)
theory Propositional_Logic
imports Abstract_Completeness
begin
(*>*)

section ‹Toy instantiation: Propositional Logic›

datatype fmla = Atom nat | Neg fmla | Conj fmla fmla

primrec max_depth where
  "max_depth (Atom _) = 0"
| "max_depth (Neg φ) = Suc (max_depth φ)"
| "max_depth (Conj φ ψ) = Suc (max (max_depth φ) (max_depth ψ))"

lemma max_depth_0: "max_depth φ = 0 = (∃n. φ = Atom n)"
  by (cases φ) auto

lemma max_depth_Suc: "max_depth φ = Suc n = ((∃ψ. φ = Neg ψ ∧ max_depth ψ = n) ∨
  (∃ψ1 ψ2. φ = Conj ψ1 ψ2 ∧ max (max_depth ψ1) (max_depth ψ2) = n))"
  by (cases φ) auto

abbreviation "atoms ≡ smap Atom nats"
abbreviation "depth1 ≡
  sinterleave (smap Neg atoms) (smap (case_prod Conj) (sproduct atoms atoms))"

abbreviation "sinterleaves ≡ fold sinterleave"

fun extendLevel where "extendLevel (belowN, N) =
  (let Next = sinterleaves
    (map (smap (case_prod Conj)) [sproduct belowN N, sproduct N belowN, sproduct N N])
    (smap Neg N)
  in (sinterleave belowN N, Next))"

lemma extendLevel_step:
  "⟦sset belowN = {φ. max_depth φ < n};
    sset N = {φ. max_depth φ = n}; st = (belowN, N)⟧ ⟹
  ∃belowNext Next. extendLevel st = (belowNext, Next) ∧
     sset belowNext = {φ. max_depth φ < Suc n} ∧ sset Next = {φ. max_depth φ = Suc n}"
  by (auto simp: sset_sinterleave sset_sproduct stream.set_map
    image_iff max_depth_Suc)

lemma sset_atoms: "sset atoms = {φ. max_depth φ < 1}"
  by (auto simp: stream.set_map max_depth_0)

lemma sset_depth1: "sset depth1 = {φ. max_depth φ = 1}"
  by (auto simp: sset_sinterleave sset_sproduct stream.set_map
    max_depth_Suc max_depth_0 max_def image_iff)

lemma extendLevel_Nsteps:
  "⟦sset belowN = {φ. max_depth φ < n}; sset N = {φ. max_depth φ = n}⟧ ⟹
  ∃belowNext Next. (extendLevel ^^ m) (belowN, N) = (belowNext, Next) ∧
     sset belowNext = {φ. max_depth φ < n + m} ∧ sset Next = {φ. max_depth φ = n + m}"
proof (induction m arbitrary: belowN N n)
  case (Suc m)
  then obtain belowNext Next where "(extendLevel ^^ m) (belowN, N) = (belowNext, Next)"
    "sset belowNext = {φ. max_depth φ < n + m}" "sset Next = {φ. max_depth φ = n + m}"
    by blast
  thus ?case unfolding funpow.simps o_apply add_Suc_right
    by (intro extendLevel_step[of belowNext _ Next])
qed simp

corollary extendLevel:
  "∃belowNext Next. (extendLevel ^^ m) (atoms, depth1) = (belowNext, Next) ∧
     sset belowNext = {φ. max_depth φ < 1 + m} ∧ sset Next = {φ. max_depth φ = 1 + m}"
  by (rule extendLevel_Nsteps) (auto simp: sset_atoms sset_depth1)


definition "fmlas = sinterleave atoms (smerge (smap snd (siterate extendLevel (atoms, depth1))))"

lemma fmlas_UNIV: "sset fmlas = (UNIV :: fmla set)"
proof (intro equalityI subsetI UNIV_I)
  fix φ
  show "φ ∈ sset fmlas"
  proof (cases "max_depth φ")
    case 0 thus ?thesis unfolding fmlas_def sset_sinterleave stream.set_map
      by (intro UnI1) (auto simp: max_depth_0)
  next
    case (Suc m) thus ?thesis using extendLevel[of m]
    unfolding fmlas_def sset_smerge sset_siterate sset_sinterleave stream.set_map
      by (intro UnI2) (auto, metis (mono_tags) mem_Collect_eq)
  qed
qed

datatype rule = Idle | Ax nat | NegL fmla | NegR fmla | ConjL fmla fmla | ConjR fmla fmla

abbreviation "mkRules f ≡ smap f fmlas"
abbreviation "mkRulePairs f ≡ smap (case_prod f) (sproduct fmlas fmlas)"

definition rules where
  "rules = Idle ## 
     sinterleaves [mkRules NegL, mkRules NegR, mkRulePairs ConjL, mkRulePairs ConjR]
     (smap Ax nats)"

lemma rules_UNIV: "sset rules = (UNIV :: rule set)"
  unfolding rules_def by (auto simp: sset_sinterleave sset_sproduct stream.set_map
    fmlas_UNIV image_iff) (metis rule.exhaust)

type_synonym state = "fmla fset * fmla fset"

fun eff' :: "rule ⇒ state ⇒ state fset option" where
  "eff' Idle (Γ, Δ) = Some {|(Γ, Δ)|}"
| "eff' (Ax n) (Γ, Δ) =
    (if Atom n |∈| Γ ∧ Atom n |∈| Δ then Some {||} else None)"
| "eff' (NegL φ) (Γ, Δ) =
    (if Neg φ |∈| Γ then Some {|(Γ |-| {| Neg φ |}, finsert φ Δ)|} else None)"
| "eff' (NegR φ) (Γ, Δ) =
    (if Neg φ |∈| Δ then Some {|(finsert φ Γ, Δ |-| {| Neg φ |})|} else None)"
| "eff' (ConjL φ ψ) (Γ, Δ) =
    (if Conj φ ψ |∈| Γ
    then Some {|(finsert φ (finsert ψ (Γ |-| {| Conj φ ψ |})), Δ)|}
    else None)"
| "eff' (ConjR φ ψ) (Γ, Δ) =
    (if Conj φ ψ |∈| Δ
    then Some {|(Γ, finsert φ (Δ |-| {| Conj φ ψ |})), (Γ, finsert ψ (Δ |-| {| Conj φ ψ |}))|}
    else None)"


abbreviation "Disj φ ψ ≡ Neg (Conj (Neg φ) (Neg ψ))"
abbreviation "Imp φ ψ ≡ Disj (Neg φ) ψ"
abbreviation "Iff φ ψ ≡ Conj (Imp φ ψ) (Imp ψ φ)"

definition "thm1 ≡ ({|Conj (Atom 0) (Neg (Atom 0))|}, {||})"

declare Stream.smember_code [code del]
lemma [code]: "Stream.smember x (y ## s) = (x = y ∨ Stream.smember x s)"
  unfolding Stream.smember_def by auto

interpretation RuleSystem "λr s ss. eff' r s = Some ss" rules UNIV
  by unfold_locales (auto simp: rules_UNIV intro: exI[of _ Idle])

interpretation PersistentRuleSystem "λr s ss. eff' r s = Some ss" rules UNIV
proof (unfold_locales, unfold enabled_def per_def rules_UNIV, clarsimp)
  fix r Γ Δ ss r' Γ' Δ' ss'
  assume "r' ≠ r" "eff' r (Γ, Δ) = Some ss" "eff' r' (Γ, Δ) = Some ss'" "(Γ', Δ') |∈| ss'"
  then show "∃sl. eff' r (Γ', Δ') = Some sl"
    by (cases r r' rule: rule.exhaust[case_product rule.exhaust]) (auto split: if_splits)
qed

definition "rho ≡ i.fenum rules"
definition "propTree ≡ i.mkTree eff' rho"

export_code propTree thm1 in Haskell module_name PropInstance (* file "." *)

(*<*)
end
(*>*)