# 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
(*>*)
```