Theory EquivRelationalDenotFSet

section "Relational and denotational views are equivalent"

theory EquivRelationalDenotFSet
  imports RelationalSemFSet DeclSemAsDenotFSet
begin
    
lemma denot_implies_rel: "(v ∈ E e ρ) ⟹ (ρ ⊢ e ⇒ v)"
proof (induction e arbitrary: v ρ)
 case (EIf e1 e2 e3)
  then show ?case 
    apply simp apply clarify apply (rename_tac n) apply (case_tac n) apply force apply simp
    apply (rule rifnz) apply force+ done
qed auto

lemma rel_implies_denot: "ρ ⊢ e ⇒ v ⟹ v ∈ E e ρ" 
  by (induction ρ e v rule: rel_sem.induct) auto

theorem equivalence_relational_denotational: "(v ∈ E e ρ) = (ρ ⊢ e ⇒ v)"
  using denot_implies_rel rel_implies_denot by blast
  
end