theory Indexed_FSet
imports
  "HOL-Library.FSet"
begin

text ‹It is convenient to address the members of a finite set by a natural number, and
also to convert a finite set to a list.›

context includes fset.lifting
begin
lift_definition fset_from_list :: "'a list => 'a fset" is set by (rule finite_set)
lemma mem_fset_from_list[simp]: "x |∈| fset_from_list l  ⟷ x ∈ set l" by transfer rule
lemma fimage_fset_from_list[simp]: "f |`| fset_from_list l = fset_from_list (map f l)"  by transfer auto
lemma fset_fset_from_list[simp]: "fset (fset_from_list l) = set l"  by transfer auto
lemmas fset_simps[simp] = set_simps[Transfer.transferred]
lemma size_fset_from_list[simp]: "distinct l ⟹ size (fset_from_list l) = length l"
  by (induction l) auto

definition list_of_fset :: "'a fset ⇒ 'a list" where
  "list_of_fset s = (SOME l. fset_from_list l = s ∧ distinct l)"

lemma fset_from_list_of_fset[simp]: "fset_from_list (list_of_fset s) = s"
  and distinct_list_of_fset[simp]: "distinct (list_of_fset s)"
  unfolding atomize_conj list_of_fset_def 
  by (transfer, rule someI_ex, rule finite_distinct_list)

lemma length_list_of_fset[simp]: "length (list_of_fset s) = size s"
  by (metis distinct_list_of_fset fset_from_list_of_fset size_fset_from_list)

lemma nth_list_of_fset_mem[simp]: "i < size s ⟹ list_of_fset s ! i |∈| s"
  by (metis fset_from_list_of_fset length_list_of_fset mem_fset_from_list nth_mem)

inductive indexed_fmember :: "'a ⇒ nat ⇒ 'a fset ⇒ bool" ("_ |∈|⇘_⇙ _" [50,50,50] 50 ) where
  "i < size s ⟹ list_of_fset s ! i |∈|⇘i⇙ s"

lemma indexed_fmember_is_fmember: "x |∈|⇘i⇙ s ⟹ x |∈| s"
proof (induction rule: indexed_fmember.induct)
case (1 i s)
   hence "i < length (list_of_fset s)" by (metis length_list_of_fset)
   hence "list_of_fset s ! i ∈ set (list_of_fset s)" by (rule nth_mem)
   thus "list_of_fset s ! i |∈| s" by (metis mem_fset_from_list fset_from_list_of_fset)
qed 

lemma fmember_is_indexed_fmember:
  assumes "x |∈| s"
  shows "∃i. x |∈|⇘i⇙ s"
proof-
  from assms
  have "x ∈ set (list_of_fset s)" using mem_fset_from_list by fastforce
  then obtain i where "i < length (list_of_fset s)" and "x = list_of_fset s ! i" by (metis in_set_conv_nth)
  hence "x |∈|⇘i⇙ s"  by (simp add: indexed_fmember.simps)
  thus ?thesis..
qed


lemma indexed_fmember_unique: "x |∈|⇘i⇙ s ⟹ y |∈|⇘j⇙ s ⟹ x = y ⟷ i = j"
  by (metis distinct_list_of_fset indexed_fmember.cases length_list_of_fset nth_eq_iff_index_eq)

definition indexed_members :: "'a fset ⇒ (nat × 'a) list" where
  "indexed_members s = zip [0..<size s] (list_of_fset s)"

lemma mem_set_indexed_members:
  "(i,x) ∈ set (indexed_members s) ⟷ x |∈|⇘i⇙ s"
  unfolding indexed_members_def indexed_fmember.simps
  by (force simp add: set_zip)

lemma mem_set_indexed_members'[simp]:
  "t ∈ set (indexed_members s) ⟷ snd t |∈|⇘fst t⇙ s"
  by (cases t, simp add: mem_set_indexed_members)

definition fnth (infixl "|!|" 100)  where
  "s |!| n = list_of_fset s ! n"
lemma fnth_indexed_fmember: "i < size s ⟹ s |!| i |∈|⇘i⇙ s"
  unfolding fnth_def by (rule indexed_fmember.intros)
lemma indexed_fmember_fnth: "x |∈|⇘i⇙ s ⟷ (s |!| i = x ∧ i < size s)"
 unfolding fnth_def by (metis indexed_fmember.simps)
end

definition fidx :: "'a fset ⇒ 'a ⇒ nat" where
  "fidx s x = (SOME i. x |∈|⇘i⇙ s)"

lemma fidx_eq[simp]: "x |∈|⇘i⇙ s ⟹ fidx s x = i"
  unfolding fidx_def
  by (rule someI2)(auto simp add: indexed_fmember_fnth fnth_def nth_eq_iff_index_eq)

lemma fidx_inj[simp]: "x |∈| s ⟹ y |∈| s ⟹ fidx s x = fidx s y ⟷ x = y"
  by (auto dest!: fmember_is_indexed_fmember simp add: indexed_fmember_unique)

lemma inj_on_fidx: "inj_on (fidx vertices) (fset vertices)"
  by (rule inj_onI) (auto simp: fmember.rep_eq [symmetric])

end

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

text ‹
The following locale describes an abstract interface for a set of formulas, without fixing the
concret shape, or set of variables.

The variables mentioned in this locale are only the @{emph ‹locally fixed constants›} occurring in
formulas, e.g.\@ in the introduction rule for the universal quantifier. Normal variables are not
something we care about at this point; they are handled completely abstractly by the abstract notion
of a substitution.
›

locale Abstract_Formulas =
  ― ‹Variables can be renamed injectively›
  fixes freshenLC :: "nat ⇒ 'var ⇒ 'var"
  ― ‹A variable-changing function can be mapped over a formula›
  fixes renameLCs :: "('var ⇒ 'var) ⇒ ('form ⇒ 'form)"
  ― ‹The set of variables occurring in a formula›
  fixes lconsts :: "'form ⇒ 'var set"
  ― ‹A closed formula has no variables, and substitions do not affect it.›
  fixes closed :: "'form ⇒ bool"
  ― ‹A substitution can be applied to a formula.›
  fixes subst :: "'subst ⇒ 'form ⇒ 'form"
  ― ‹The set of variables occurring (in the image) of a substitution.›
  fixes subst_lconsts :: "'subst ⇒ 'var set"
  ― ‹A variable-changing function can be mapped over a substitution›
  fixes subst_renameLCs :: "('var ⇒ 'var) ⇒ ('subst ⇒ 'subst)"
  ― ‹A most generic formula, can be substitutied to anything.›
  fixes anyP :: "'form"

  assumes freshenLC_eq_iff[simp]: "freshenLC a v = freshenLC a' v' ⟷ a = a' ∧ v = v'"
  assumes lconsts_renameLCs: "lconsts (renameLCs p f) = p ` lconsts f"
  assumes rename_closed: "lconsts f = {} ⟹ renameLCs p f = f"
  assumes subst_closed: "closed f ⟹ subst s f = f"
  assumes closed_no_lconsts: "closed f ⟹ lconsts f = {}"
  assumes fv_subst: "lconsts (subst s f) ⊆ lconsts f ∪ subst_lconsts s"
  assumes rename_rename: "renameLCs p1 (renameLCs p2 f) = renameLCs (p1 ∘ p2) f"
  assumes rename_subst: "renameLCs p (subst s f) = subst (subst_renameLCs p s) (renameLCs p f)"
  assumes renameLCs_cong: "(⋀ x. x ∈ lconsts f ⟹ f1 x = f2 x) ⟹ renameLCs f1 f = renameLCs f2 f"
  assumes subst_renameLCs_cong: "(⋀ x. x ∈ subst_lconsts s ⟹ f1 x = f2 x) ⟹ subst_renameLCs f1 s = subst_renameLCs f2 s"
  assumes subst_lconsts_subst_renameLCs: "subst_lconsts (subst_renameLCs p s) = p ` subst_lconsts s"
  assumes lconsts_anyP: "lconsts anyP = {}"
  assumes empty_subst: "∃ s. (∀ f. subst s f = f) ∧ subst_lconsts s = {}"
  assumes anyP_is_any: "∃ s. subst s anyP = f"
begin
  definition freshen :: "nat ⇒ 'form ⇒ 'form" where
    "freshen n = renameLCs (freshenLC n)"

  definition empty_subst :: "'subst" where
    "empty_subst = (SOME s. (∀ f. subst s f = f) ∧ subst_lconsts s = {})"

  lemma empty_subst_spec:
    "(∀ f. subst empty_subst f = f) ∧ subst_lconsts empty_subst = {}"
    unfolding empty_subst_def using empty_subst by (rule someI_ex)
  lemma subst_empty_subst[simp]: "subst empty_subst f = f"
    by (metis empty_subst_spec)
  lemma subst_lconsts_empty_subst[simp]: "subst_lconsts empty_subst = {}"
    by (metis empty_subst_spec)

  lemma lconsts_freshen: "lconsts (freshen a f) = freshenLC a ` lconsts f"
    unfolding freshen_def by (rule lconsts_renameLCs)

  lemma freshen_closed: "lconsts f = {} ⟹ freshen a f = f"
    unfolding freshen_def by (rule rename_closed)
    
  lemma closed_eq:
    assumes "closed f1"
    assumes "closed f2"
    shows "subst s1 (freshen a1 f1) = subst s2 (freshen a2 f2) ⟷ f1 = f2"
  using assms
    by (auto simp add: closed_no_lconsts freshen_def lconsts_freshen subst_closed rename_closed)

  lemma freshenLC_range_eq_iff[simp]: "freshenLC a v ∈ range (freshenLC a') ⟷ a = a'"
    by auto

  definition rerename :: "'var set ⇒ nat ⇒ nat ⇒ ('var ⇒ 'var) ⇒ ('var ⇒ 'var)" where
    "rerename V from to f x = (if x ∈ freshenLC from ` V then freshenLC to (inv (freshenLC from) x) else f x)"
  
  lemma inj_freshenLC[simp]: "inj (freshenLC i)"
    by (rule injI) simp
  
  lemma rerename_freshen[simp]: "x ∈ V ⟹ rerename  V i (isidx is) f (freshenLC i x) = freshenLC (isidx is) x"
    unfolding rerename_def by simp

  lemma range_rerename: "range (rerename V  from to f) ⊆ freshenLC to ` V ∪ range f"
    by (auto simp add: rerename_def split: if_splits)

  lemma rerename_noop:
      "x ∉ freshenLC from ` V  ⟹ rerename V from to f x = f x"
    by (auto simp add: rerename_def split: if_splits)

  lemma rerename_rename_noop:
      "freshenLC from ` V ∩ lconsts form  = {}  ⟹ renameLCs (rerename V from to f) form = renameLCs f form"
      by (intro renameLCs_cong rerename_noop) auto

  lemma rerename_subst_noop:
      "freshenLC from ` V ∩ subst_lconsts s  = {}  ⟹ subst_renameLCs (rerename V from to f) s = subst_renameLCs f s"
      by (intro subst_renameLCs_cong rerename_noop) auto
end
end

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

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: "((v⇩1,p⇩1),(v⇩2,p⇩2)) ∈ edges ⟹ hyps (nodeOf v⇩1) p⇩1 = Some p' ⟹ (v⇩2,p⇩2) = (v⇩1,p') ∨ v⇩2 ∈ scope (v⇩1,p')"

context Scoped_Graph
begin

definition hyps_free where
  "hyps_free pth = (∀ v⇩1 p⇩1 v⇩2 p⇩2. ((v⇩1,p⇩1),(v⇩2,p⇩2)) ∈ set pth ⟶ hyps (nodeOf v⇩1) p⇩1 = 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: "((v⇩1,p⇩1),(v⇩2,p⇩2)) ∈ edges ⟹ terminal_path v⇩2 v' pth ⟹ hyps (nodeOf v⇩1) p⇩1 = None ⟹ terminal_path v⇩1 v' (((v⇩1,p⇩1),(v⇩2,p⇩2))#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 v⇩1 p⇩1 v⇩2 p⇩2 v' pth)
  note terminal_path_cons.IH
  moreover
  have "v⇩1 ∉ fst ` fst ` set pth"
  proof
    assume "v⇩1 ∈ fst ` fst ` set pth"
    then obtain pth1 e' pth2 where "pth = pth1@[e']@pth2" and "v⇩1 = 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 v⇩2 v' pth›]
    have "path v⇩2 v⇩1 pth1" by (simp add:  path_split2 edge_begin_tup)
    with ‹((v⇩1, p⇩1), (v⇩2, p⇩2)) ∈ _›
    have "path v⇩1 v⇩1 (((v⇩1, p⇩1), (v⇩2, p⇩2)) # pth1)" by (simp add: path_cons_simp)
    moreover
    from terminal_path_is_hyps_free[OF ‹terminal_path v⇩2 v' pth›]
         ‹hyps (nodeOf v⇩1) p⇩1 = None›
         ‹pth = pth1@[e']@pth2›
    have "hyps_free(((v⇩1, p⇩1), (v⇩2, p⇩2)) # pth1)"
      by (auto simp add: hyps_free_def)
    ultimately
    show False  using hyps_free_acyclic by blast
  qed
  moreover
  have "v⇩1 ≠ 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: "((v⇩1,p⇩1),(v⇩2,p⇩2)) ∈ edges ⟹ labelAtOut v⇩1 p⇩1 = labelAtIn v⇩2 p⇩2"

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

theory Abstract_Rules
imports
  Abstract_Formula
begin

text ‹
Next, we can define a logic, by giving a set of rules.

In order to connect to the AFP entry Abstract Completeness, the set of rules is a stream; the only
relevant effect of this is that the set is guaranteed to be non-empty and at most countable. This
has no further significance in our development.

Each antecedent of a rule consists of
 ▪ a set of fresh variables
 ▪ a set of hypotheses that may be used in proving the conclusion of the antecedent and
 ▪ the conclusion of the antecedent.

Our rules allow for multiple conclusions (but must have at least one).

In order to prove the completeness (but incidentally not to prove correctness) of the incredible
proof graphs, there are some extra conditions about the fresh variables in a rule. 
 ▪ These need to be disjoint for different antecedents.
 ▪ They need to list all local variables occurring in either the hypothesis and the conclusion.
 ▪ The conclusions of a rule must not contain any local variables.
›


datatype ('form, 'var) antecedent =
  Antecedent (a_hyps: "'form fset") (a_conc: "'form") (a_fresh: "'var set")

abbreviation plain_ant :: "'form ⇒ ('form, 'var) antecedent"
  where "plain_ant f ≡ Antecedent {||} f {}"

locale Abstract_Rules =
  Abstract_Formulas freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP
  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" +

  fixes antecedent :: "'rule ⇒ ('form, 'var) antecedent list"
    and consequent :: "'rule ⇒ 'form list"
    and rules :: "'rule stream"

  assumes no_empty_conclusions: "∀xs∈sset rules. consequent xs ≠ []"

  assumes no_local_consts_in_consequences: "∀xs∈sset rules. ⋃(lconsts ` (set (consequent xs))) = {}"
  assumes no_multiple_local_consts:
    "⋀ r i i' . r ∈ sset rules ⟹
                 i < length (antecedent r) ⟹
                 i' < length (antecedent r) ⟹
                 a_fresh (antecedent r ! i) ∩ a_fresh (antecedent r ! i') = {} ∨ i = i'"
  assumes all_local_consts_listed:
    "⋀ r p. r ∈ sset rules ⟹ p ∈ set (antecedent r) ⟹
        lconsts (a_conc p) ∪ (⋃(lconsts ` fset (a_hyps p))) ⊆ a_fresh p "
begin
  definition f_antecedent :: "'rule ⇒ ('form, 'var) antecedent fset"
    where "f_antecedent r = fset_from_list (antecedent r)"
  definition "f_consequent r = fset_from_list (consequent r)"
end

text ‹
Finally, an abstract task specifies what a specific proof should prove. In particular, it gives
a set of assumptions that may be used, and lists the conclusions that need to be proven.

Both assumptions and conclusions are closed expressions that may not be changed by substitutions. 
›

locale Abstract_Task =
  Abstract_Rules freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP  antecedent consequent rules
  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 antecedent :: "'rule ⇒ ('form, 'var) antecedent list"
    and consequent :: "'rule ⇒ 'form list" 
    and rules :: "'rule stream" +

  fixes assumptions :: "'form list"
  fixes conclusions :: "'form list"
  assumes assumptions_closed: "⋀ a. a ∈ set assumptions ⟹ closed a"
  assumes conclusions_closed: "⋀ c. c ∈ set conclusions ⟹ closed c"
begin
  definition ass_forms where "ass_forms = fset_from_list assumptions"
  definition conc_forms where "conc_forms = fset_from_list  conclusions"

  lemma mem_ass_forms[simp]: "a |∈| ass_forms ⟷ a ∈ set assumptions"
    by (auto simp add: ass_forms_def)
  
  lemma mem_conc_forms[simp]: "a |∈| conc_forms ⟷ a ∈ set conclusions"
    by (auto simp add: conc_forms_def)

  lemma subst_freshen_assumptions[simp]:
    assumes "pf ∈ set assumptions"
    shows "subst s (freshen a pf) = pf "
      using assms assumptions_closed 
      by (simp add: closed_no_lconsts freshen_def rename_closed subst_closed)

  lemma subst_freshen_conclusions[simp]:
    assumes "pf ∈ set conclusions"
    shows "subst s (freshen a pf) = pf "
      using assms conclusions_closed 
      by (simp add: closed_no_lconsts freshen_def rename_closed subst_closed)

  lemma subst_freshen_in_ass_formsI:
    assumes "pf ∈ set assumptions"
    shows "subst s (freshen a pf) |∈| ass_forms"
      using assms by simp

  lemma subst_freshen_in_conc_formsI:
    assumes "pf ∈ set conclusions"
    shows "subst s (freshen a pf) |∈| conc_forms"
      using assms by simp
end


end