Theory Incredible_Deduction

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

text This theory contains the definition for actual proof graphs, and their various possible
properties.

text The following locale first defines graphs, without edges.

locale Vertex_Graph = 
  Port_Graph_Signature nodes inPorts outPorts
    for nodes :: "'node stream"
    and inPorts :: "'node  'inPort fset"
    and outPorts :: "'node  'outPort fset" +
  fixes vertices :: "'v fset"
  fixes nodeOf :: "'v  'node"
begin
  fun valid_out_port where "valid_out_port (v,p)  v |∈| vertices  p |∈| outPorts (nodeOf v)"
  fun valid_in_port  where "valid_in_port (v,p)  v |∈| vertices  p |∈| inPorts (nodeOf v)" 

  fun terminal_node where
    "terminal_node n  outPorts n = {||}"
  fun terminal_vertex where
    "terminal_vertex v  v |∈| vertices  terminal_node (nodeOf v)"
end

text And now we add the edges. This allows us to define paths and scopes.

type_synonym ('v, 'outPort, 'inPort) edge = "(('v × 'outPort) × ('v × 'inPort))"

locale Pre_Port_Graph =
  Vertex_Graph nodes inPorts outPorts vertices nodeOf
    for nodes :: "'node stream"
    and inPorts :: "'node  'inPort fset"
    and outPorts :: "'node  'outPort fset"
    and vertices :: "'v fset"
    and nodeOf :: "'v  'node" +
  fixes edges :: "('v, 'outPort, 'inPort) edge set"
begin
  fun edge_begin :: "(('v × 'outPort) × ('v × 'inPort))  'v" where
    "edge_begin ((v1,p1),(v2,p2)) = v1"
  fun edge_end :: "(('v × 'outPort) × ('v × 'inPort))  'v" where
    "edge_end ((v1,p1),(v2,p2)) = v2"

  lemma edge_begin_tup: "edge_begin x = fst (fst x)" by (metis edge_begin.simps prod.collapse)
  lemma edge_end_tup: "edge_end x = fst (snd x)" by (metis edge_end.simps prod.collapse)

  inductive path :: "'v  'v  ('v, 'outPort, 'inPort) edge list  bool"   where
    path_empty: "path v v []" |
    path_cons: "e  edges  path (edge_end e) v' pth  path (edge_begin e) v' (e#pth)"

  inductive_simps path_cons_simp': "path v v' (e#pth)"
  inductive_simps path_empty_simp[simp]: "path v v' []"
  lemma path_cons_simp: "path v v' (e # pth)  fst (fst e) = v  e  edges  path (fst (snd e)) v' pth"
    by(auto simp add: path_cons_simp', metis prod.collapse)

  lemma path_appendI: "path v v' pth1  path v' v'' pth2  path v v'' (pth1@pth2)"
    by (induction pth1 arbitrary: v) (auto simp add: path_cons_simp )

  lemma path_split: "path v v' (pth1@[e]@pth2)  path v (edge_end e) (pth1@[e])  path (edge_end e) v' pth2"
    by (induction pth1 arbitrary: v) (auto simp add: path_cons_simp edge_end_tup intro: path_empty)

  lemma path_split2: "path v v' (pth1@(e#pth2))  path v (edge_begin e) pth1  path (edge_begin e) v' (e#pth2)"
    by (induction pth1 arbitrary: v) (auto simp add: path_cons_simp edge_begin_tup intro: path_empty)

  lemma path_snoc: "path v v' (pth1@[e])  e  edges  path v (edge_begin e) pth1  edge_end e = v'"
    by (auto simp add: path_split2 path_cons_simp edge_end_tup edge_begin_tup)

  inductive_set scope :: "'v × 'inPort  'v set" for ps where
    "v |∈| vertices  ( pth v'.  path v v' pth  terminal_vertex v'  ps  snd ` set pth)
     v  scope ps"

  lemma scope_find:
    assumes "v  scope ps"
    assumes "terminal_vertex v'"
    assumes "path v v' pth"
    shows "ps  snd ` set pth"
  using assms by (auto simp add: scope.simps)

  lemma snd_set_split:
    assumes "ps  snd ` set pth"
    obtains pth1 pth2 e  where "pth = pth1@[e]@pth2" and "snd e = ps" and "ps  snd ` set pth1"
    using assms
    proof (atomize_elim, induction pth)
      case Nil thus ?case by simp
    next
      case (Cons e pth)
      show ?case
      proof(cases "snd e = ps")
        case True
        hence "e # pth = [] @ [e] @ pth  snd e = ps  ps  snd ` set []" by auto
        thus ?thesis by (intro exI)
      next
        case False
        with Cons(2)
        have "ps  snd ` set pth" by auto
        from Cons.IH[OF this this] 
        obtain pth1 e' pth2 where "pth = pth1 @ [e'] @ pth2  snd e' = ps  ps  snd ` set pth1" by auto
        with False
        have "e#pth = (e# pth1) @ [e'] @ pth2  snd e' = ps  ps  snd ` set (e#pth1)" by auto
        thus ?thesis by blast
      qed
    qed

  lemma scope_split:
    assumes "v  scope ps"
    assumes "path v v' pth"
    assumes "terminal_vertex v'"
    obtains pth1 e pth2
    where "pth = (pth1@[e])@pth2" and "path v (fst ps) (pth1@[e])" and "path (fst ps) v' pth2" and "snd e = ps" and "ps  snd ` set pth1"
  proof-
    from assms
    have "ps  snd ` set pth" by (auto simp add: scope.simps)
    then obtain pth1 pth2 e  where "pth = pth1@[e]@pth2" and "snd e = ps" and "ps  snd ` set pth1" by (rule snd_set_split)
    
    from path _ _ _ and pth = pth1@[e]@pth2
    have "path v (edge_end e) (pth1@[e])" and "path (edge_end e) v' pth2" by (metis path_split)+
    show thesis
    proof(rule that)
      show "pth = (pth1@[e])@pth2" using pth= _ by simp
      show "path v (fst ps) (pth1@[e])" using path v (edge_end e) (pth1@[e])  snd e = ps by (simp add: edge_end_tup)
      show "path (fst ps) v' pth2" using path (edge_end e) v' pth2  snd e = ps by (simp add: edge_end_tup)
      show "ps  snd ` set pth1" by fact
      show "snd e = ps" by fact
    qed
  qed  
end

text This adds well-formedness conditions to the edges and vertices.

locale Port_Graph = Pre_Port_Graph +
  assumes valid_nodes: "nodeOf ` fset vertices   sset nodes"
  assumes valid_edges: " (ps1,ps2)  edges. valid_out_port ps1  valid_in_port ps2"
begin
  lemma snd_set_path_verties: "path v v' pth  fst ` snd ` set pth  fset vertices"
    apply (induction rule: path.induct)
    apply auto
    apply (metis valid_in_port.elims(2) edge_end.simps notin_fset case_prodD valid_edges)
    done

  lemma fst_set_path_verties: "path v v' pth  fst ` fst ` set pth  fset vertices"
    apply (induction rule: path.induct)
    apply auto
    apply (metis valid_out_port.elims(2) edge_begin.simps notin_fset case_prodD valid_edges)
    done
end

text A pruned graph is one where every node has a path to a terminal node (which will be the conclusions).

locale Pruned_Port_Graph = Port_Graph +
  assumes pruned: "v.  v |∈| vertices  (pth v'. path v v' pth  terminal_vertex v')"
begin
  lemma scopes_not_refl:
    assumes "v |∈| vertices"
    shows "v  scope (v,p)"
  proof(rule notI)
    assume "v  scope (v,p)"

    from pruned[OF assms]
    obtain pth t where "terminal_vertex t" and "path v t pth" and least: " pth'. path v t pth'  length pth  length pth'"
      by atomize_elim (auto simp del: terminal_vertex.simps elim: ex_has_least_nat)
        
    from scope_split[OF v  scope (v,p) path v t pth terminal_vertex t]
    obtain pth1 e pth2 where "pth = (pth1 @ [e]) @ pth2" "path v t pth2" by (metis fst_conv)

    from this(2) least
    have "length pth  length pth2" by auto
    with pth = _
    show False by auto
  qed

  text This lemma can be found in \cite{incredible}, but it is otherwise inconsequential.
  lemma scopes_nest:
    fixes ps1 ps2
    shows "scope ps1  scope ps2  scope ps2  scope ps1  scope ps1  scope ps2 = {}"
  proof(cases "ps1 = ps2")
    assume "ps1  ps2"
    {
    fix v
    assume "v  scope ps1  scope ps2"
    hence "v |∈| vertices" using scope.simps by auto
    then obtain pth t where "path v t pth" and "terminal_vertex t" using pruned by blast
  
    from path v t pth and terminal_vertex t and v  scope ps1  scope ps2
    obtain pth1a e1 pth1b  where "pth = (pth1a@[e1])@pth1b" and "path v (fst ps1) (pth1a@[e1])" and "snd e1 = ps1" and "ps1  snd ` set pth1a"
      by (auto elim: scope_split)
  
    from path v t pth and terminal_vertex t and v  scope ps1  scope ps2
    obtain pth2a e2 pth2b  where "pth = (pth2a@[e2])@pth2b" and "path v (fst ps2) (pth2a@[e2])" and "snd e2 = ps2" and "ps2  snd ` set pth2a"
      by (auto elim: scope_split)
   
    from pth = (pth1a@[e1])@pth1b pth = (pth2a@[e2])@pth2b
    have "set pth1a  set pth2a  set pth2a  set pth1a" by (auto simp add: append_eq_append_conv2)
    hence "scope ps1  scope ps2  scope ps2  scope ps1"
    proof
      assume "set pth1a  set pth2a" with ps2  _
      have "ps2  snd ` set (pth1a@[e1])" using ps1  ps2 snd e1 = ps1 by auto
  
      have "scope ps1  scope ps2"
      proof
        fix v'
        assume "v'  scope ps1"
        hence "v' |∈| vertices" using scope.simps by auto
        thus "v'  scope ps2"
        proof(rule scope.intros)
          fix pth' t'
          assume "path v' t' pth'" and "terminal_vertex t'"
          with v'  scope ps1
          obtain pth3a e3 pth3b where "pth' = (pth3a@[e3])@pth3b" and "path (fst ps1) t' pth3b"
            by (auto elim: scope_split)
  
          have "path v t' ((pth1a@[e1]) @ pth3b)" using path v (fst ps1) (pth1a@[e1]) and path (fst ps1) t' pth3b
            by (rule path_appendI)
          with terminal_vertex t' v  _
          have "ps2  snd ` set ((pth1a@[e1]) @ pth3b)" by (meson IntD2 scope.cases)
          hence "ps2  snd ` set pth3b" using ps2  snd ` set (pth1a@[e1]) by auto
          thus "ps2  snd ` set pth'" using pth'=_ by auto
        qed
      qed
      thus ?thesis by simp
    next
      assume "set pth2a  set pth1a" with ps1  _
      have "ps1  snd ` set (pth2a@[e2])" using ps1  ps2 snd e2 = ps2 by auto
  
      have "scope ps2  scope ps1"
      proof
        fix v'
        assume "v'  scope ps2"
        hence "v' |∈| vertices" using scope.simps by auto
        thus "v'  scope ps1"
        proof(rule scope.intros)
          fix pth' t'
          assume "path v' t' pth'" and "terminal_vertex t'"
          with v'  scope ps2
          obtain pth3a e3 pth3b where "pth' = (pth3a@[e3])@pth3b" and "path (fst ps2) t' pth3b" 
            by (auto elim: scope_split)
  
          have "path v t' ((pth2a@[e2]) @ pth3b)" using path v (fst ps2) (pth2a@[e2]) and path (fst ps2) t' pth3b
            by (rule path_appendI)
          with terminal_vertex t' v  _
          have "ps1  snd ` set ((pth2a@[e2]) @ pth3b)" by (meson IntD1 scope.cases)
          hence "ps1  snd ` set pth3b" using ps1  snd ` set (pth2a@[e2]) by auto
          thus "ps1  snd ` set pth'" using pth'=_ by auto
        qed
      qed
      thus ?thesis by simp
    qed
    }
    thus ?thesis by blast
  qed simp
end

text A well-scoped graph is one where a port marked to be a local hypothesis is only connected to
the corresponding input port, either directly or via a path. It must not be, however, that there is
a a path from such a hypothesis to a terminal node that does not pass by the dedicated input port;
this is expressed via scopes.


locale Scoped_Graph = Port_Graph + Port_Graph_Signature_Scoped
locale Well_Scoped_Graph = Scoped_Graph +
  assumes well_scoped: "((v1,p1),(v2,p2))  edges  hyps (nodeOf v1) p1 = Some p'  (v2,p2) = (v1,p')  v2  scope (v1,p')"

context Scoped_Graph
begin

definition hyps_free where
  "hyps_free pth = ( v1 p1 v2 p2. ((v1,p1),(v2,p2))  set pth  hyps (nodeOf v1) p1 = None)"

lemma hyps_free_Nil[simp]: "hyps_free []" by (simp add: hyps_free_def)

lemma hyps_free_Cons[simp]: "hyps_free (e#pth)  hyps_free pth  hyps (nodeOf (fst (fst e))) (snd (fst e)) = None"
  by (auto simp add: hyps_free_def) (metis prod.collapse)

lemma path_vertices_shift:
  assumes "path v v' pth"
  shows "map fst (map fst pth)@[v'] = v#map fst (map snd pth)"
using assms by induction auto

inductive terminal_path where
    terminal_path_empty: "terminal_vertex v  terminal_path v v []" |
    terminal_path_cons: "((v1,p1),(v2,p2))  edges  terminal_path v2 v' pth  hyps (nodeOf v1) p1 = None  terminal_path v1 v' (((v1,p1),(v2,p2))#pth)"

lemma terminal_path_is_path:
  assumes "terminal_path v v' pth"
  shows "path v v' pth"
using assms by induction (auto simp add: path_cons_simp)

lemma terminal_path_is_hyps_free:
  assumes "terminal_path v v' pth"
  shows "hyps_free pth"
using assms by induction (auto simp add: hyps_free_def)

lemma terminal_path_end_is_terminal:
  assumes "terminal_path v v' pth"
  shows "terminal_vertex v'"
using assms by induction

lemma terminal_pathI:
  assumes "path v v' pth"
  assumes "hyps_free pth"
  assumes "terminal_vertex v'"
  shows "terminal_path v v' pth"
using assms
by induction (auto intro: terminal_path.intros)
end

text An acyclic graph is one where there are no non-trivial cyclic paths (disregarding
edges that are local hypotheses -- these are naturally and benignly cyclic).

locale Acyclic_Graph = Scoped_Graph +
  assumes hyps_free_acyclic: "path v v pth  hyps_free pth  pth = []"
begin
lemma hyps_free_vertices_distinct:
  assumes "terminal_path v v' pth"
  shows "distinct (map fst (map fst pth)@[v'])"
using assms
proof(induction v v' pth)
  case terminal_path_empty
  show ?case by simp
next
  case (terminal_path_cons v1 p1 v2 p2 v' pth)
  note terminal_path_cons.IH
  moreover
  have "v1  fst ` fst ` set pth"
  proof
    assume "v1  fst ` fst ` set pth"
    then obtain pth1 e' pth2 where "pth = pth1@[e']@pth2" and "v1 = fst (fst e')"
      apply (atomize_elim)
      apply (induction pth)
      apply (solves simp)
      apply (auto)
      apply (solves rule exI[where x = "[]"]; simp)
      apply (metis Cons_eq_appendI image_eqI prod.sel(1))
      done
    with terminal_path_is_path[OF terminal_path v2 v' pth]
    have "path v2 v1 pth1" by (simp add:  path_split2 edge_begin_tup)
    with ((v1, p1), (v2, p2))  _
    have "path v1 v1 (((v1, p1), (v2, p2)) # pth1)" by (simp add: path_cons_simp)
    moreover
    from terminal_path_is_hyps_free[OF terminal_path v2 v' pth]
         hyps (nodeOf v1) p1 = None
         pth = pth1@[e']@pth2
    have "hyps_free(((v1, p1), (v2, p2)) # pth1)"
      by (auto simp add: hyps_free_def)
    ultimately
    show False  using hyps_free_acyclic by blast
  qed
  moreover
  have "v1  v'"
    using hyps_free_acyclic path_cons terminal_path_cons.hyps(1) terminal_path_cons.hyps(2) terminal_path_cons.hyps(3) terminal_path_is_hyps_free terminal_path_is_path by fastforce
  ultimately
  show ?case by (auto simp add: comp_def)
qed

lemma hyps_free_vertices_distinct':
  assumes "terminal_path v v' pth"
  shows "distinct (v # map fst (map snd pth))"
  using hyps_free_vertices_distinct[OF assms]
  unfolding path_vertices_shift[OF terminal_path_is_path[OF assms]]
  .

lemma hyps_free_limited:
  assumes "terminal_path v v' pth"
  shows "length pth  fcard vertices"
proof-
  have "length pth = length (map fst (map fst pth))" by simp
  also
  from hyps_free_vertices_distinct[OF assms]
  have "distinct (map fst (map fst pth))" by simp
  hence "length (map fst (map fst pth)) = card (set (map fst (map fst pth)))"
    by (rule distinct_card[symmetric])
  also have "  card (fset vertices)"
  proof (rule card_mono[OF finite_fset])    
    from assms(1) 
    show "set (map fst (map fst pth))  fset vertices"
      by (induction v v' pth) (auto, metis valid_edges notin_fset case_prodD valid_out_port.simps)
  qed
  also have " = fcard vertices" by (simp add: fcard.rep_eq)
  finally show ?thesis.
qed

lemma hyps_free_path_not_in_scope:
  assumes "terminal_path v t pth"
  assumes "(v',p')  snd ` set pth"
  shows   "v'  scope (v, p)"
proof
  assume "v'  scope (v,p)"

  from (v',p')  snd ` set pth
  obtain pth1 pth2 e  where "pth = pth1@[e]@pth2" and "snd e = (v',p')" by (rule snd_set_split)
  from terminal_path_is_path[OF assms(1), unfolded pth = _ ] snd e = _
  have "path v v' (pth1@[e])" and "path v' t pth2" unfolding path_split by (auto simp add: edge_end_tup)
  
  from v'  scope (v,p) terminal_path_end_is_terminal[OF assms(1)] path v' t pth2
  have "(v,p)  snd ` set pth2" by (rule scope_find)
  then obtain pth2a e' pth2b  where "pth2 = pth2a@[e']@pth2b" and "snd e' = (v,p)"  by (rule snd_set_split)
  from path v' t pth2[unfolded pth2 = _ ] snd e' = _
  have "path v' v (pth2a@[e'])" and "path v t pth2b" unfolding path_split by (auto simp add: edge_end_tup)
  
  from path v v' (pth1@[e]) path v' v (pth2a@[e'])
  have "path v v ((pth1@[e])@(pth2a@[e']))" by (rule path_appendI)
  moreover
  from terminal_path_is_hyps_free[OF assms(1)] pth = _ pth2 = _
  have "hyps_free ((pth1@[e])@(pth2a@[e']))" by (auto simp add: hyps_free_def)
  ultimately
  have "((pth1@[e])@(pth2a@[e'])) = []" by (rule hyps_free_acyclic)
  thus False by simp
qed

end

text A saturated graph is one where every input port is incident to an edge.

locale Saturated_Graph = Port_Graph +
  assumes saturated: "valid_in_port (v,p)   e  edges . snd e = (v,p)"

text These four conditions make up a well-shaped graph.

locale Well_Shaped_Graph =  Well_Scoped_Graph + Acyclic_Graph + Saturated_Graph + Pruned_Port_Graph

text Next we demand an instantiation. This consists of a unique natural number per vertex,
in order to rename the local constants apart, and furthermore a substitution per block
which instantiates the schematic formulas given in @{term Labeled_Signature}.

locale Instantiation =
  Vertex_Graph nodes _ _ vertices _ +
  Labeled_Signature nodes  _ _ _ labelsIn labelsOut +
  Abstract_Formulas freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP
  for nodes :: "'node stream" and edges :: "('vertex, 'outPort, 'inPort) edge set" and vertices :: "'vertex fset" and labelsIn :: "'node  'inPort  'form" and labelsOut :: "'node  'outPort  'form" 
  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 vidx :: "'vertex  nat"
    and inst :: "'vertex  'subst"
  assumes vidx_inj: "inj_on vidx (fset vertices)"
begin
  definition labelAtIn :: "'vertex  'inPort  'form"  where
    "labelAtIn v p = subst (inst v) (freshen (vidx v) (labelsIn (nodeOf v) p))"
  definition labelAtOut :: "'vertex  'outPort  'form"  where
    "labelAtOut v p = subst (inst v) (freshen (vidx v) (labelsOut (nodeOf v) p))"
end

text A solution is an instantiation where on every edge, both incident ports are labeld with
the same formula.

locale Solution =
  Instantiation _ _ _ _ _ edges for edges :: "(('vertex × 'outPort) × 'vertex × 'inPort) set" +
  assumes solved: "((v1,p1),(v2,p2))  edges  labelAtOut v1 p1 = labelAtIn v2 p2"

locale Proof_Graph =  Well_Shaped_Graph + Solution

text If we have locally scoped constants, we demand that only blocks in the scope of the 
corresponding input port may mention such a locally scoped variable in its substitution.

locale Well_Scoped_Instantiation =
   Pre_Port_Graph  nodes inPorts outPorts vertices nodeOf edges +
   Instantiation  inPorts outPorts nodeOf hyps nodes edges  vertices labelsIn labelsOut freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP vidx inst +
   Port_Graph_Signature_Scoped_Vars nodes inPorts outPorts freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP local_vars
   for 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"
    and inPorts :: "'node  'inPort fset" 
    and outPorts :: "'node  'outPort fset" 
    and nodeOf :: "'vertex  'node" 
    and hyps :: "'node  'outPort  'inPort option" 
    and nodes :: "'node stream" 
    and vertices :: "'vertex fset" 
    and labelsIn :: "'node  'inPort  'form" 
    and labelsOut :: "'node  'outPort  'form" 
    and vidx :: "'vertex  nat" 
    and inst :: "'vertex  'subst" 
    and edges :: "('vertex, 'outPort, 'inPort) edge set" 
    and local_vars :: "'node  'inPort  'var set" +
  assumes well_scoped_inst:
    "valid_in_port (v,p) 
     var  local_vars (nodeOf v) p 
     v' |∈| vertices 
     freshenLC (vidx v) var  subst_lconsts (inst v') 
     v'  scope (v,p)"
begin
  lemma out_of_scope: "valid_in_port (v,p)  v' |∈| vertices  v'  scope (v,p)  freshenLC (vidx v) ` local_vars (nodeOf v) p  subst_lconsts (inst v') = {}"
    using well_scoped_inst by auto
end

text The following locale assembles all these conditions.
  
locale Scoped_Proof_Graph =
  Instantiation  inPorts outPorts nodeOf hyps nodes edges  vertices labelsIn labelsOut freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP vidx inst +
  Well_Shaped_Graph  nodes inPorts outPorts vertices nodeOf edges hyps  +
  Solution inPorts outPorts nodeOf hyps nodes vertices  labelsIn labelsOut freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP vidx inst edges +
  Well_Scoped_Instantiation  freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP inPorts outPorts nodeOf hyps  nodes vertices labelsIn labelsOut vidx inst edges local_vars
   for 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"
    and inPorts :: "'node  'inPort fset" 
    and outPorts :: "'node  'outPort fset" 
    and nodeOf :: "'vertex  'node" 
    and hyps :: "'node  'outPort  'inPort option" 
    and nodes :: "'node stream" 
    and vertices :: "'vertex fset" 
    and labelsIn :: "'node  'inPort  'form" 
    and labelsOut :: "'node  'outPort  'form" 
    and vidx :: "'vertex  nat" 
    and inst :: "'vertex  'subst" 
    and edges :: "('vertex, 'outPort, 'inPort) edge  set" 
    and local_vars :: "'node  'inPort  'var set"

end