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 notin_fset 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: fmember.rep_eq 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