Theory AnswerIndexedFamilies

theory AnswerIndexedFamilies
imports Main
begin

chapter ‹Answer-Indexed Families›

typedecl 'a state
consts L :: ‹'a state => 'a set›
datatype answer = T | F
type_synonym 'a AiF = ‹answer ⇒ 'a set›

fun and_AiF :: ‹'a AiF ⇒ 'a AiF ⇒ 'a AiF› (infixl ‹∧·› 60) where
  ‹(a ∧· b) T = a T ∩ b T›
| ‹(a ∧· b) F = a F ∪ b F›

fun or_AiF :: ‹'a AiF ⇒ 'a AiF ⇒ 'a AiF› (infixl ‹∨·› 59) where
  ‹(a ∨· b) T = a T ∪ b T›
| ‹(a ∨· b) F = a F ∩ b F›

fun not_AiF :: ‹'a AiF ⇒ 'a AiF› (‹¬· _›) where
  ‹(¬· a) T = a F›
| ‹(¬· a) F = a T›

fun univ_AiF :: ‹'a AiF› (‹T∙›) where
  ‹T∙ T = UNIV›
| ‹T∙ F = {}›

fun satisfying_AiF :: ‹'a ⇒ 'a state AiF› (‹sat∙›) where
  ‹sat∙ x T = {state. x ∈ L state}›
| ‹sat∙ x F = {state. x ∉ L state}›

section ‹Example: Propositional logic›

datatype (atoms_plogic: 'a) plogic =
    True_plogic                               (‹true⇩p›)
  | Prop_plogic ‹'a›                            (‹prop⇩p'(_')›)
  | Not_plogic ‹'a plogic›                    (‹not⇩p _› [85] 85)
  | Or_plogic  ‹'a plogic› ‹'a plogic›        (‹_ or⇩p _› [82,82] 81)
  | And_plogic ‹'a plogic› ‹'a plogic›        (‹_ and⇩p _› [82,82] 81)

fun plogic_semantics :: ‹'a plogic ⇒ 'a state AiF› (‹⟦_⟧⇩p›) where
  ‹⟦ true⇩p    ⟧⇩p = T∙›
| ‹⟦ not⇩p φ   ⟧⇩p = ¬· ⟦φ⟧⇩p›
| ‹⟦ prop⇩p(a) ⟧⇩p = sat∙ a›
| ‹⟦ φ or⇩p ψ  ⟧⇩p = ⟦φ⟧⇩p ∨· ⟦ψ⟧⇩p›
| ‹⟦ φ and⇩p ψ ⟧⇩p = ⟦φ⟧⇩p ∧· ⟦ψ⟧⇩p›

definition false_p (‹false⇩p›) where
false_p_def [simp]: ‹false⇩p = not⇩p true⇩p›

definition implies_p :: ‹'a plogic ⇒ 'a plogic ⇒ 'a plogic› (‹_ implies⇩p _› [81,81] 80)  where
implies_p_def[simp]: ‹φ implies⇩p ψ = (not⇩p φ or⇩p ψ)›

subsection ‹Propositional logic lemmas›

lemma AiF_cases:  
  assumes ‹A T = B T› and ‹A F = B F›
  shows ‹A = B›
proof (rule ext)
  fix x show ‹A x = B x› by (cases ‹x›; simp add: assms) 
qed

lemma or_and_negation: ‹⟦ φ or⇩p ψ ⟧⇩p = ⟦ not⇩p ((not⇩p φ) and⇩p (not⇩p ψ)) ⟧⇩p›
  by (rule AiF_cases; simp)

lemma and_or_negation: ‹⟦ φ and⇩p ψ⟧⇩p = ⟦ not⇩p ((not⇩p φ) or⇩p (not⇩p ψ)) ⟧⇩p›
  by (rule AiF_cases; simp)

lemma de_morgan_1: ‹⟦ not⇩p (φ and⇩p ψ) ⟧⇩p = ⟦ (not⇩p φ) or⇩p (not⇩p ψ) ⟧⇩p›
  by (rule AiF_cases; simp)

lemma de_morgan_2: ‹⟦ not⇩p (φ or⇩p ψ)  ⟧⇩p = ⟦ (not⇩p φ) and⇩p (not⇩p ψ) ⟧⇩p›
  by (rule AiF_cases; simp)

subsection ‹Propositional logic equivalence›

fun plogic_semantics' :: ‹'a state ⇒ 'a plogic ⇒ bool› (infix ‹⊨⇩p› 60) where
  ‹Γ ⊨⇩p true⇩p = True›
| ‹Γ ⊨⇩p not⇩p φ = (¬ Γ ⊨⇩p φ)›
| ‹Γ ⊨⇩p prop⇩p(a) = (a ∈ L Γ)›
| ‹Γ ⊨⇩p φ or⇩p ψ = (Γ ⊨⇩p φ ∨ Γ ⊨⇩p ψ)›
| ‹Γ ⊨⇩p φ and⇩p ψ = (Γ ⊨⇩p φ ∧ Γ ⊨⇩p ψ)›

lemma plogic_equivalence:
  shows ‹(  Γ  ⊨⇩p φ ⟷ Γ ∈ ⟦φ⟧⇩p T)›
  and   ‹(¬ Γ  ⊨⇩p φ ⟷ Γ ∈ ⟦φ⟧⇩p F)›
proof (induct ‹φ›)
qed (auto)

end