# 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"
lemma hyps_for_simp'[simp]: "h ∈ fset (hyps_for n p) ⟷ hyps n h = Some p"
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
```