Theory StandardModels

section ‹Standard Models›
text ‹We define the kind of models we are interested in here.
      In particular, we care about standard graphs.
      To allow some reuse, we distinguish a generic version called @{term standard},
      from an instantiated abbreviation @{term standard'}.
      There is little we can prove about these definition here, except for Lemma 2.›
theory StandardModels
imports LabeledGraphSemantics Main
begin

abbreviation "a_bot ≡ A_Lbl S_Bot"
abbreviation "a_top ≡ A_Lbl S_Top"
abbreviation "a_idt ≡ A_Lbl S_Idt"
notation a_bot ("⊥")
notation a_top ("⊤")
notation a_idt ("𝟭")
                                       
type_synonym 'v std_term = "'v Standard_Constant allegorical_term"
type_synonym 'v std_sentence = "'v std_term × 'v std_term"
type_synonym ('v,'a) std_graph = "('v Standard_Constant, ('v+'a)) labeled_graph"

abbreviation ident_rel where
"ident_rel idt G ≡ getRel idt G = (λ x.(x,x)) ` vertices G"

lemma ident_relI[intro]:
  assumes min:"⋀ x. x ∈ vertices G ⟹ (x,x) ∈ getRel idt G"
  and max1:"⋀ x y. (x,y) ∈ getRel idt G ⟹ x = y"
  and max2:"⋀ x y. (x,y) ∈ getRel idt G ⟹ x ∈ vertices G"
shows "ident_rel idt G"
proof
  from max1 max2 have "⋀ x y. (x,y) ∈ getRel idt G ⟹ (x = y ∧ x ∈ vertices G)" by simp
  thus "getRel idt G ⊆ (λx. (x, x)) ` vertices G" by auto
  show "(λx. (x, x)) ` vertices G ⊆ getRel idt G" using min by auto
qed


text ‹Definition 4, generically.›
definition standard :: "('l × 'v) set ⇒ 'l ⇒ 'l ⇒ 'l ⇒ ('l, 'v) labeled_graph ⇒ bool" where
"standard C b t idt G
   ≡ G = restrict G
   ∧ vertices G ≠ {}
   ∧ ident_rel idt G
   ∧ getRel b G = {}
   ∧ getRel t G = {(x,y). x∈vertices G ∧ y∈vertices G}
   ∧ (∀ (l,v) ∈ C. getRel l G = {(v,v)})"

text ‹Definition 4.›
abbreviation standard' :: "'v set ⇒ ('v,'a) std_graph ⇒ bool" where
"standard' C ≡ standard ((λ c. (S_Const c,Inl c)) ` C) S_Bot S_Top S_Idt"

text ‹Definition 5.›
definition model :: "'v set ⇒ ('v,'a) std_graph ⇒ ('v std_sentence) set ⇒ bool" where
"model C G T ≡ standard' C G ∧ (∀ S ∈ T. G ⊨ S)"

text ‹Definition 5.›
abbreviation consistent :: "'b itself ⇒ 'v set ⇒ ('v std_sentence) set ⇒ bool" where
"consistent _ C T ≡ ∃ (G::('v,'b) std_graph). model C G T"

text ‹Definition 6.›
definition entails :: "'b itself ⇒ 'v set ⇒ ('v std_sentence) set ⇒ 'v std_sentence ⇒ bool"  where
"entails _ C T S ≡ ∀ (G::('v,'b) std_graph). model C G T ⟶ G ⊨ S"

lemma standard_top_not_bot[intro]:
"standard' C G ⟹ :G:⟦⊥⟧ ≠ :G:⟦⊤⟧"
  unfolding standard_def by auto

text ‹Lemma 2.›
lemma consistent_iff_entails_nonsense:
"consistent t C T = (¬ entails t C T (⊥,⊤))"
proof
  show "consistent t C T ⟹ ¬ entails t C T (⊥, ⊤)"
    using standard_top_not_bot unfolding entails_def model_def
    by fastforce
qed (auto simp:entails_def model_def)

end