Theory PMLinHOL_faithfulness

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

theory PMLinHOL_faithfulness (* Christoph Benzmüller, 2025 *)
  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 φ)"  ―‹sledgehammer: Proof found; metis reconstruction timeout› oops
lemma Sound2: "⊨⇧m ψ ⟶ (∃φ. ψ=⟦φ⟧ ∧ ⊨⇧m ⟦φ⟧)" ―‹sledgehammer: Proof found; metis reconstruction timeout› oops
end