Theory PMLinHOL_faithfulness

section‹Automated faithfulness proofs\label{sec:faithfulness}›

theory PMLinHOL_faithfulness 
  imports PMLinHOL_deep PMLinHOL_shallow PMLinHOL_shallow_minimal
begin 

―‹Mappings: deep to maximal shallow and deep to minimal shallow›
primrec DpToShMax ("⦇_⦈") where "⦇φ⇧^d⦈= φ⇧^s" | "⦇¬⇧^d φ⦈ = ¬⇧^s ⦇φ⦈" | "⦇φ ⊃⇧^d ψ⦈ = ⦇φ⦈ ⊃⇧^s ⦇ψ⦈" | "⦇□⇧^d φ⦈ = □⇧^s ⦇φ⦈" 
primrec DpToShMin ("⟦_⟧") where "⟦φ⇧^d⟧= φ⇧^m" | "⟦¬⇧^d φ⟧ = ¬⇧^m ⟦φ⟧" | "⟦φ ⊃⇧^d ψ⟧ = ⟦φ⟧ ⊃⇧^m ⟦ψ⟧" | "⟦□⇧^d φ⟧ = □⇧^m ⟦φ⟧" 

―‹Proving faithfulness between deep and maximal shallow›
theorem Faithful1a: "∀W R V. ∀w:W. ⟨W,R,V⟩,w ⊨⇧^d φ ⟷ ⟨W,R,V⟩,w ⊨⇧^s ⦇φ⦈" apply induct by auto
theorem Faithful1b: "⊨⇧^d φ ⟷ ⊨⇧^s ⦇φ⦈" using Faithful1a by auto

―‹Proving faithfulness between deep and minimal shallow›
theorem Faithful2: "∀w. ⟨(λx::𝗐. True),R,V⟩,w ⊨⇧^d φ ⟷ w ⊨⇧^m ⟦φ⟧" apply induct by auto

―‹Proving faithfulness maximal shallow and minimal shallow›
theorem Faithful3: "∀w. ⟨(λx::𝗐. True),R,V⟩,w ⊨⇧^s ⦇φ⦈ ⟷ w ⊨⇧^m ⟦φ⟧" apply induct by auto

―‹Additional check for soundness for the minimal shallow embedding›
lemma Sound1: "⊨⇧^m ψ ⟷ (∃φ. ψ=⟦φ⟧ ∧ ⊨⇧^d φ)" by (smt (z3) Faithful2 DefM DefD RelativeTruthD.simps ext[of ψ "⟦x⊃⇧^dx⟧"])   
lemma Sound2: "⊨⇧^m ψ ⟷ (∃φ. ψ=⟦φ⟧ ∧ ⊨⇧^m ⟦φ⟧)" using Sound1 by blast
end