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 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 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  scope ps1  scope ps2
          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  scope ps1  scope ps2
          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 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