Theory Soundness

section ‹Soundness›

theory Soundness imports "Abstract_Soundness.Finite_Proof_Soundness" Prover Semantics begin

lemma eff_sound:
  assumes ‹eff r (A, B) = Some ss› ‹∀A B. (A, B) |∈| ss ⟶ (∀(E :: _ ⇒ 'a). sc (E, F, G) (A, B))›
  shows ‹sc (E, F, G) (A, B)›
  using assms
proof (induct r ‹(A, B)› rule: eff.induct)
  case (5 p q)
  then have ‹sc (E, F, G) (A [÷] (p ❙⟶ q), p # B)› ‹sc (E, F, G) (q # A [÷] (p ❙⟶ q), B)›
    by (metis eff.simps(5) finsertCI option.inject option.simps(3))+
  then show ?case
    using "5.prems"(1) by (force split: if_splits)
next
  case (7 t p)
  then have ‹sc (E, F, G) (⟨t⟩p # A, B)›
    by (metis eff.simps(7) finsert_iff option.inject option.simps(3))
  then show ?case
    using "7.prems"(1) by (fastforce split: if_splits)
next
  case (8 p)
  let ?n = ‹fresh (A @ B)›
  have A: ‹∀p [∈] A. max_list (vars_fm p) < ?n› and B: ‹∀p [∈] B. max_list (vars_fm p) < ?n›
    unfolding fresh_def using max_list_vars_fms max_list_mono vars_fms_member
    by (metis Un_iff le_imp_less_Suc set_append)+
  from 8 have ‹sc (E(?n := x), F, G) (A, ⟨❙#?n⟩p # B [÷] ❙∀p)› for x
    by (metis eff.simps(8) finsert_iff option.inject option.simps(3))
  then have ‹(∀p [∈] A. ⟦E, F, G⟧ p) ⟶
      (∀x. ⟦(x ⨟ λm. (E(?n := x)) m), F, G⟧ p) ∨ (∃q [∈] B [÷] ❙∀p. ⟦E, F, G⟧ q)›
    using A B upd_vars_fm by fastforce
  then have ‹(∀p [∈] A. ⟦E, F, G⟧ p) ⟶
      (∀x. ⟦((x ⨟ E)(Suc ?n := x)), F, G⟧ p) ∨ (∃q [∈] B [÷] ❙∀p. ⟦E, F, G⟧ q)›
    unfolding add_upd_commute by blast
  moreover have ‹max_list (vars_fm p) < ?n›
    using B "8.prems"(1) by (metis eff.simps(8) option.distinct(1) vars_fm.simps(4))
  ultimately have ‹sc (E, F, G) (A, ❙∀p # (B [÷] ❙∀p))›
    by auto
  moreover have ‹❙∀p [∈] B›
    using "8.prems"(1) by (simp split: if_splits)
  ultimately show ?case
    by (metis (full_types) Diff_iff sc.simps set_ConsD set_removeAll)
qed (fastforce split: if_splits)+

interpretation Soundness ‹λr s ss. eff r s = Some ss› rules UNIV sc
  unfolding Soundness_def using eff_sound by fast

theorem prover_soundness:
  assumes ‹tfinite t› and ‹wf t›
  shows ‹sc (E, F, G) (fst (root t))›
  using assms soundness by fast

end