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)
  case (7 t p)
  then have sc (E, F, G) (tp # 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)
  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, #?np # 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