Theory Incredible_Signatures

theory Incredible_Signatures
imports
  Main 
  "HOL-Library.FSet"
  "HOL-Library.Stream"
  Abstract_Formula
begin

text ‹This theory contains the definition for proof graph signatures, in the variants
▪ Plain port graph
▪ Port graph with local hypotheses
▪ Labeled port graph
▪ Port graph with local constants
›

locale Port_Graph_Signature =
  fixes nodes :: "'node stream"
  fixes inPorts :: "'node ⇒ 'inPort fset"
  fixes outPorts :: "'node ⇒ 'outPort fset"

locale Port_Graph_Signature_Scoped =
  Port_Graph_Signature +
  fixes hyps :: "'node ⇒ 'outPort ⇀ 'inPort"
  assumes hyps_correct: "hyps n p1 = Some p2 ⟹ p1 |∈| outPorts n ∧ p2 |∈| inPorts n"
begin
  inductive_set hyps_for' :: "'node ⇒ 'inPort ⇒ 'outPort set" for n p
    where "hyps n h = Some p ⟹ h ∈ hyps_for' n p"

  lemma hyps_for'_subset: "hyps_for' n p ⊆ fset (outPorts n)"
    using hyps_correct by (meson hyps_for'.cases subsetI)
 
  context includes fset.lifting
  begin
  lift_definition hyps_for  :: "'node ⇒ 'inPort ⇒ 'outPort fset" is hyps_for'
    by (meson finite_fset hyps_for'_subset rev_finite_subset)
  lemma hyps_for_simp[simp]: "h |∈| hyps_for n p ⟷ hyps n h = Some p"
    by transfer (simp add: hyps_for'.simps)
  lemma hyps_for_simp'[simp]: "h ∈ fset (hyps_for n p) ⟷ hyps n h = Some p"
    by transfer (simp add: hyps_for'.simps)
  lemma hyps_for_collect: "fset (hyps_for n p) = {h . hyps n h = Some p}"
    by auto
  end
  lemma hyps_for_subset: "hyps_for n p |⊆| outPorts n"
    using hyps_for'_subset
    by (fastforce simp add: hyps_for.rep_eq simp del: hyps_for_simp hyps_for_simp')
end

locale Labeled_Signature = 
  Port_Graph_Signature_Scoped +
  fixes labelsIn :: "'node ⇒ 'inPort ⇒ 'form" 
  fixes labelsOut :: "'node ⇒ 'outPort ⇒ 'form" 


locale Port_Graph_Signature_Scoped_Vars =
  Port_Graph_Signature nodes inPorts outPorts +
  Abstract_Formulas freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP
  for nodes :: "'node stream" and inPorts :: "'node ⇒ 'inPort fset"  and outPorts :: "'node ⇒ 'outPort fset"
  and  freshenLC :: "nat ⇒ 'var ⇒ 'var" 
    and renameLCs :: "('var ⇒ 'var) ⇒ 'form ⇒ 'form" 
    and lconsts :: "'form ⇒ 'var set" 
    and closed :: "'form ⇒ bool"
    and subst :: "'subst ⇒ 'form ⇒ 'form" 
    and subst_lconsts :: "'subst ⇒ 'var set" 
    and subst_renameLCs :: "('var ⇒ 'var) ⇒ ('subst ⇒ 'subst)"
    and anyP :: "'form" +

  fixes local_vars :: "'node ⇒ 'inPort ⇒ 'var set"

end