Session Incredible_Proof_Machine

Theory Indexed_FSet

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

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

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

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

Theory Abstract_Rules

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: "xssset rules. consequent xs  []"

  assumes no_local_consts_in_consequences: "xssset 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

Theory Abstract_Rules_To_Incredible

theory Abstract_Rules_To_Incredible
imports
  Main 
  "HOL-Library.FSet"
  "HOL-Library.Stream"
  Incredible_Deduction
  Abstract_Rules
begin

text ‹In this theory, the abstract rules given in @{theory Incredible_Proof_Machine.Abstract_Rules} are used to
create a proper signature.›

text ‹Besides the rules given there, we have nodes for assumptions, conclusions, and the helper
block.›

datatype ('form, 'rule) graph_node = Assumption 'form | Conclusion 'form | Rule 'rule | Helper

type_synonym ('form, 'var) in_port = "('form, 'var) antecedent"
type_synonym 'form reg_out_port = "'form"
type_synonym 'form hyp = "'form"
datatype ('form, 'var) out_port = Reg "'form reg_out_port" | Hyp "'form hyp" "('form, 'var) in_port"
type_synonym ('v, 'form, 'var) edge' = "(('v × ('form, 'var) out_port) × ('v × ('form, 'var) in_port))"

context Abstract_Task
begin
  definition nodes :: "('form, 'rule) graph_node stream" where
    "nodes = Helper ## shift (map Assumption assumptions) (shift (map Conclusion conclusions) (smap Rule rules))"

  lemma Helper_in_nodes[simp]:
    "Helper  sset nodes" by (simp add: nodes_def)
  lemma Assumption_in_nodes[simp]:
    "Assumption a  sset nodes  a  set assumptions" by (auto simp add: nodes_def stream.set_map)
  lemma Conclusion_in_nodes[simp]:
    "Conclusion c  sset nodes  c  set conclusions" by (auto simp add: nodes_def stream.set_map)
  lemma Rule_in_nodes[simp]:
    "Rule r  sset nodes  r  sset rules" by (auto simp add: nodes_def stream.set_map)

  fun inPorts' :: "('form, 'rule) graph_node  ('form, 'var) in_port list"  where
    "inPorts' (Rule r) = antecedent r"
   |"inPorts' (Assumption r) = []"
   |"inPorts' (Conclusion r) = [ plain_ant r ]"
   |"inPorts' Helper  = [ plain_ant anyP ]"

  fun inPorts :: "('form, 'rule) graph_node  ('form, 'var) in_port fset"  where
    "inPorts (Rule r) = f_antecedent r"
   |"inPorts (Assumption r) = {||}"
   |"inPorts (Conclusion r) = {| plain_ant r |}"
   |"inPorts Helper  = {| plain_ant anyP |}"

  lemma inPorts_fset_of:
    "inPorts n = fset_from_list (inPorts' n)"
    by (cases n rule: inPorts.cases) (auto simp: fmember.rep_eq f_antecedent_def)

  definition outPortsRule where
    "outPortsRule r = ffUnion ((λ a. (λ h. Hyp h a) |`| a_hyps a) |`| f_antecedent r) |∪| Reg |`| f_consequent r"

  lemma Reg_in_outPortsRule[simp]:  "Reg c |∈| outPortsRule r  c |∈| f_consequent r"
    by (auto simp add: outPortsRule_def fmember.rep_eq ffUnion.rep_eq)
  lemma Hyp_in_outPortsRule[simp]:  "Hyp h c |∈| outPortsRule r  c |∈| f_antecedent r  h |∈| a_hyps c"
    by (auto simp add: outPortsRule_def fmember.rep_eq ffUnion.rep_eq)

  fun outPorts where
    "outPorts (Rule r) = outPortsRule r"
   |"outPorts (Assumption r) = {|Reg r|}"
   |"outPorts (Conclusion r) = {||}"
   |"outPorts Helper  = {| Reg anyP |}"

  fun labelsIn where
    "labelsIn _ p = a_conc p"

  fun labelsOut where
    "labelsOut _ (Reg p) = p"
   | "labelsOut _ (Hyp h c) = h"

  fun hyps where 
     "hyps (Rule r) (Hyp h a) = (if a |∈| f_antecedent r  h |∈| a_hyps a then Some a else None)"
   | "hyps _ _ = None"

  fun local_vars :: "('form, 'rule) graph_node  ('form, 'var) in_port  'var set"  where
     "local_vars _ a = a_fresh a"


  sublocale Labeled_Signature nodes inPorts outPorts hyps labelsIn labelsOut
  proof(standard,goal_cases)
    case (1 n p1 p2)
    thus ?case by(induction n p1 rule: hyps.induct) (auto  split: if_splits)
  qed

  lemma hyps_for_conclusion[simp]: "hyps_for (Conclusion n) p = {||}"
    using hyps_for_subset by auto
  lemma hyps_for_Helper[simp]: "hyps_for Helper p = {||}"
    using hyps_for_subset by auto
  lemma hyps_for_Rule[simp]: "ip |∈| f_antecedent r  hyps_for (Rule r) ip = (λ h. Hyp h ip) |`| a_hyps ip"
    by (auto elim!: hyps.elims split: if_splits)
end

text ‹Finally, a given proof graph solves the task at hand if all the given conclusions are present
as conclusion blocks in the graph.›

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

    and assumptions :: "'form list" 
    and conclusions :: "'form list" 

    and vertices :: "'vertex fset" 
    and nodeOf :: "'vertex  ('form, 'rule) graph_node" 
    and edges :: "('vertex, 'form, 'var) edge' set" 
    and vidx :: "'vertex  nat"
    and inst :: "'vertex  'subst"  +
  assumes conclusions_present: "set (map Conclusion conclusions)  nodeOf ` fset vertices"

end

Theory Entailment

theory Entailment
imports Main "HOL-Library.FSet"
begin

type_synonym 'form entailment = "('form fset × 'form)"

abbreviation entails :: "'form fset  'form  'form entailment" (infix "" 50)
  where "a  c  (a, c)"

fun add_ctxt :: "'form fset  'form entailment  'form entailment" where
  "add_ctxt Δ (Γ  c) = (Γ |∪| Δ  c)"

end

Theory Natural_Deduction

theory Natural_Deduction
imports
  Abstract_Completeness.Abstract_Completeness
  Abstract_Rules
  Entailment
begin

text ‹Our formalization of natural deduction builds on @{theory Abstract_Completeness.Abstract_Completeness} and refines and
concretizes the structure given there as follows
  The judgements are entailments consisting of a finite set of assumptions and a conclusion, which
   are abstract formulas in the sense of @{theory Incredible_Proof_Machine.Abstract_Formula}.
  The abstract rules given in @{theory Incredible_Proof_Machine.Abstract_Rules} are used to decide the validity of a
   step in the derivation.
›

text ‹A single setep in the derivation can either be the axiom rule, the cut rule, or one
of the given rules in @{theory Incredible_Proof_Machine.Abstract_Rules}.›

datatype 'rule NatRule = Axiom | NatRule 'rule | Cut


text ‹The following locale is still abstract in the set of rules (nat_rule›), but implements
the bookkeeping logic for assumptions, the @{term Axiom} rule and the @{term Cut} rule.›

locale ND_Rules_Inst =
  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 nat_rule :: "'rule  'form  ('form, 'var) antecedent fset  bool"
  and rules :: "'rule stream"
begin

  text  An application of the @{term Axiom} rule is valid if the conclusion is among the assumptions.
   An application of a @{term NatRule} is more complicated. This requires some natural number
    a› to rename local variables, and some instantiation s›. It checks that
      none of the local variables occur in the context of the judgement.
      none of the local variables occur in the instantiation.
    Together, this implements the usual freshness side-conditions.
    Furthermore, for every antecedent of the rule, the (correctly renamed and instantiated)
    hypotheses need to be added to the context.
   The @{term Cut} rule is again easy.
  ›
  inductive eff :: "'rule NatRule  'form entailment  'form entailment fset  bool" where
    "con |∈| Γ
     eff Axiom (Γ  con) {||}"
   |"nat_rule rule c ants
     ( ant f. ant |∈| ants  f |∈| Γ  freshenLC a ` (a_fresh ant)  lconsts f = {})
     ( ant. ant |∈| ants  freshenLC a ` (a_fresh ant)  subst_lconsts s = {})
     eff (NatRule rule)
        (Γ  subst s (freshen a c))
        ((λant. ((λp. subst s (freshen a p)) |`| a_hyps ant |∪| Γ  subst s (freshen a (a_conc ant)))) |`| ants) "
   |"eff Cut (Γ  c') {| (Γ  c')|}"

  inductive_simps eff_Cut_simps[simp]: "eff Cut (Γ  c) S"

  sublocale RuleSystem_Defs where
    eff = eff and rules = "Cut ## Axiom ## smap NatRule rules".
end

text ‹Now we instantiate the above locale. We duplicate each abstract rule (which can have multiple
consequents) for each consequent, as the natural deduction formulation can only handle a single
consequent per rule›

context Abstract_Task 
begin           
  inductive natEff_Inst where
    "c  set (consequent r)  natEff_Inst (r,c) c (f_antecedent r)"

  definition n_rules where
    "n_rules = flat (smap (λr. map (λc. (r,c)) (consequent r)) rules)"
  
  sublocale ND_Rules_Inst _ _ _ _ _ _ _ _ natEff_Inst n_rules ..
 
  text ‹A task is solved if for every conclusion, there is a well-formed and finite tree that proves
  this conclusion, using only assumptions given in the task.›
  
  definition solved where
    "solved  ( c. c |∈| conc_forms  ( Γ t. fst (root t) = (Γ  c)  Γ |⊆| ass_forms  wf t  tfinite t))"
end

end

Theory Incredible_Correctness

theory Incredible_Correctness
imports
  Abstract_Rules_To_Incredible
  Natural_Deduction
begin

text ‹
In this theory, we prove that if we have a graph that proves a given abstract task (which is
represented as the context @{term Tasked_Proof_Graph}), then we can prove @{term solved}.
›

context Tasked_Proof_Graph
begin

definition adjacentTo :: "'vertex  ('form, 'var) in_port  ('vertex × ('form, 'var) out_port)" where
 "adjacentTo v p = (SOME ps. (ps, (v,p))  edges)"

fun isReg where
  "isReg v p = (case p of Hyp h c  False | Reg  c 
      (case nodeOf v of
        Conclusion a  False
      | Assumption a  False
      | Rule r  True
      | Helper  True
      ))"

fun toNatRule  where
  "toNatRule v p = (case p of Hyp h c  Axiom | Reg  c 
      (case nodeOf v of
        Conclusion a  Axiom ― ‹a lie›
      | Assumption a  Axiom
      | Rule r  NatRule (r,c)
      | Helper  Cut
      ))"


inductive_set global_assms' :: "'var itself  'form set" for i  where
  "v |∈| vertices  nodeOf v = Assumption p  labelAtOut v (Reg p)  global_assms' i"

lemma finite_global_assms': "finite (global_assms' i)"
proof-
  have "finite (fset vertices)" by (rule finite_fset)
  moreover
  have "global_assms' i  (λ v. case nodeOf v of Assumption p   labelAtOut v (Reg p)) ` fset vertices"
    by (force simp add: global_assms'.simps fmember.rep_eq image_iff )
  ultimately
  show ?thesis by (rule finite_surj)
qed

context includes fset.lifting
begin
  lift_definition global_assms :: "'var itself  'form fset" is global_assms' by (rule finite_global_assms')
  lemmas global_assmsI = global_assms'.intros[Transfer.transferred]
  lemmas global_assms_simps = global_assms'.simps[Transfer.transferred]
end

fun extra_assms :: "('vertex × ('form, 'var) in_port)  'form fset" where
  "extra_assms (v, p) = (λ p. labelAtOut v p) |`| hyps_for (nodeOf v) p"

fun hyps_along :: "('vertex, 'form, 'var) edge' list  'form fset" where
  "hyps_along pth = ffUnion (extra_assms |`| snd |`| fset_from_list pth) |∪| global_assms TYPE('var)"

lemma hyps_alongE[consumes 1, case_names Hyp Assumption]:
  assumes "f |∈| hyps_along pth"
  obtains v p h where "(v,p)  snd ` set pth" and "f = labelAtOut v h " and "h |∈| hyps_for (nodeOf v) p"
  | v pf  where "v |∈| vertices" and "nodeOf v = Assumption pf" "f = labelAtOut v (Reg pf)"
  using assms
  apply (auto simp add: fmember.rep_eq ffUnion.rep_eq  global_assms_simps[unfolded fmember.rep_eq])
  apply (metis image_iff snd_conv)
  done

text ‹Here we build the natural deduction tree, by walking the graph.›

primcorec tree :: "'vertex  ('form, 'var) in_port  ('vertex, 'form, 'var) edge' list   (('form entailment), ('rule × 'form) NatRule) dtree" where
 "root (tree v p pth) =
    ((hyps_along ((adjacentTo v p,(v,p))#pth)  labelAtIn v p),
    (case adjacentTo v p of (v', p')  toNatRule v' p'
    ))"
 | "cont (tree v p pth) =
    (case adjacentTo v p of (v', p') 
    (if isReg v' p' then ((λ p''. tree v' p'' ((adjacentTo v p,(v,p))#pth)) |`| inPorts (nodeOf v')) else {||}
    ))"


lemma fst_root_tree[simp]: "fst (root (tree v p pth)) = (hyps_along ((adjacentTo v p,(v,p))#pth)  labelAtIn v p)" by simp

lemma out_port_cases[consumes 1, case_names Assumption Hyp Rule Helper]:
  assumes "p |∈| outPorts n"
  obtains
    a where "n = Assumption a" and "p = Reg a"
    | r h c where "n = Rule r" and "p = Hyp h c"
    | r f where "n = Rule r" and "p = Reg f"
    | "n = Helper" and "p = Reg anyP"
  using assms by (atomize_elim, cases p; cases n) auto

lemma hyps_for_fimage: "hyps_for (Rule r) x = (if x |∈| f_antecedent r then (λ f. Hyp f x) |`| (a_hyps x) else {||})"
  apply (rule fset_eqI)
  apply (rename_tac p')
  apply (case_tac p')
  apply (auto simp add:  split: if_splits out_port.splits)
  done

text ‹Now we prove that the thus produced tree is well-formed.›

theorem wf_tree:
  assumes "valid_in_port (v,p)"
  assumes "terminal_path v t pth"
  shows "wf (tree v p pth)"
using assms
proof (coinduction arbitrary: v p pth)
case (wf v p pth)
  let ?t = "tree v p pth"
  from saturated[OF wf(1)]
  obtain v' p'
  where e:"((v',p'),(v,p))  edges" and [simp]: "adjacentTo v p = (v',p')"
    by (auto simp add: adjacentTo_def, metis (no_types, lifting) eq_fst_iff tfl_some)

  let ?e = "((v',p'),(v,p))"
  let ?pth' = "?e#pth"
  let  = "hyps_along ?pth'"
  let ?l = "labelAtIn v p"

  from e valid_edges have "v' |∈| vertices" and "p' |∈| outPorts (nodeOf v')" by auto
  hence "nodeOf v'  sset nodes" using valid_nodes by (meson image_eqI notin_fset subsetD)

  from ?e  edges
  have s: "labelAtOut v' p' = labelAtIn v p"  by (rule solved)

  from p' |∈| outPorts (nodeOf v')
  show ?case
  proof (cases rule: out_port_cases)
    case (Hyp r h c)

    from Hyp p' |∈| outPorts (nodeOf v')
    have "h |∈| a_hyps c" and "c |∈| f_antecedent r" by auto
    hence "hyps (nodeOf v') (Hyp h c) = Some c" using Hyp by simp

    from well_scoped[OF _  edges[unfolded Hyp] this]
    have "(v, p) = (v', c)  v  scope (v', c)".
    hence "(v', c)  insert (v, p) (snd ` set pth)"
    proof
      assume "(v, p) = (v', c)"
      thus ?thesis by simp
    next
      assume "v  scope (v', c)"
      from this terminal_path_end_is_terminal[OF wf(2)] terminal_path_is_path[OF wf(2)]
      have "(v', c)  snd ` set pth" by (rule scope_find)
      thus ?thesis by simp
    qed
    moreover


    from ‹hyps (nodeOf v') (Hyp h c) = Some c
    have "Hyp h c |∈| hyps_for (nodeOf v') c" by simp
    hence "labelAtOut v' (Hyp h c) |∈| extra_assms (v',c)" by auto
    ultimately

    have "labelAtOut v' (Hyp h c) |∈| "
      by (fastforce simp add: fmember.rep_eq ffUnion.rep_eq)

    hence "labelAtIn v p |∈| " by (simp add: s[symmetric] Hyp fmember.rep_eq)
    thus ?thesis
      using Hyp
      apply (auto intro: exI[where x = ?t] simp add: eff.simps simp del: hyps_along.simps)
      done
  next
    case (Assumption f)

    from v' |∈| vertices nodeOf v' = Assumption f
    have "labelAtOut v' (Reg f) |∈| global_assms TYPE('var)"
      by (rule global_assmsI)
    hence "labelAtOut v' (Reg f) |∈| " by auto
    hence "labelAtIn v p |∈| " by (simp add: s[symmetric] Assumption fmember.rep_eq)
    thus ?thesis using Assumption
      by (auto intro: exI[where x = ?t] simp add: eff.simps)
  next
    case (Rule r f)
    with nodeOf v'  sset nodes›
    have "r  sset rules"
      by (auto simp add: nodes_def stream.set_map)

    from Rule
    have "hyps (nodeOf v') p' = None" by simp
    with e ‹terminal_path v t pth
    have "terminal_path v' t ?pth'"..

    from Rule  p' |∈| outPorts (nodeOf v')
    have "f |∈| f_consequent r" by simp
    hence "f  set (consequent r)" by (simp add: f_consequent_def)
    with r  sset rules
    have "NatRule (r, f)  sset (smap NatRule n_rules)"
      by (auto simp add: stream.set_map n_rules_def no_empty_conclusions)
    moreover

    {
    from f |∈| f_consequent r
    have "f  set (consequent r)" by (simp add: f_consequent_def)
    hence "natEff_Inst (r, f) f (f_antecedent r)"
      by (rule natEff_Inst.intros)
    hence "eff (NatRule (r, f)) (  subst (inst v') (freshen (vidx v') f))
           ((λant. ((λp. subst (inst v') (freshen (vidx v') p)) |`| a_hyps ant |∪|   subst (inst v') (freshen (vidx v') (a_conc ant)))) |`| f_antecedent r)"
           (is "eff _ _ ?ants")
    proof (rule eff.intros)
      fix ant f
      assume "ant |∈| f_antecedent r"
      from  v' |∈| vertices ant |∈| f_antecedent r
      have "valid_in_port (v',ant)" by (simp add: Rule)

      assume "f |∈| "
      thus "freshenLC (vidx v') ` a_fresh ant  lconsts f = {}"
      proof(induct rule: hyps_alongE)
        case (Hyp v'' p'' h'')

        from Hyp(1) snd_set_path_verties[OF terminal_path_is_path[OF ‹terminal_path v' t ?pth']]
        have "v'' |∈| vertices" by (force simp add: fmember.rep_eq)

        from ‹terminal_path v' t ?pth' Hyp(1)
        have "v''  scope (v', ant)" by (rule hyps_free_path_not_in_scope)
        with ‹valid_in_port (v',ant) v'' |∈| vertices
        have "freshenLC (vidx v') ` local_vars (nodeOf v') ant  subst_lconsts (inst v'') = {}"
         by (rule out_of_scope)
        moreover
        from hyps_free_vertices_distinct'[OF ‹terminal_path v' t ?pth'] Hyp.hyps(1)
        have "v''  v'" by (metis distinct.simps(2) fst_conv image_eqI list.set_map)
        hence "vidx v''  vidx v'" using v' |∈| vertices v'' |∈| vertices by (meson vidx_inj inj_onD notin_fset)
        hence "freshenLC (vidx v') ` a_fresh ant  freshenLC (vidx v'') ` lconsts (labelsOut (nodeOf v'') h'') = {}"by auto
        moreover
        have "lconsts f  lconsts (freshen (vidx v'') (labelsOut (nodeOf v'') h''))  subst_lconsts (inst v'') " using f = _
          by (simp add: labelAtOut_def fv_subst)
        ultimately
        show ?thesis
          by (fastforce simp add:  lconsts_freshen)
      next
        case (Assumption v pf)
        hence "f = subst (inst v) (freshen (vidx v) pf)" by (simp add: labelAtOut_def)
        moreover
        from Assumption have "Assumption pf  sset nodes" using valid_nodes by (auto simp add: fmember.rep_eq)
        hence "pf  set assumptions" unfolding nodes_def by (auto simp add: stream.set_map)
        hence "closed pf" by (rule assumptions_closed)
        ultimately
        have "lconsts f = {}" by (simp add: closed_no_lconsts lconsts_freshen subst_closed freshen_closed)
        thus ?thesis by simp
      qed
    next
      fix ant
      assume "ant |∈| f_antecedent r"
      from  v' |∈| vertices ant |∈| f_antecedent r
      have "valid_in_port (v',ant)" by (simp add: Rule)
      moreover
      note v' |∈| vertices
      moreover
      hence "v'  scope (v', ant)" by (rule scopes_not_refl)
      ultimately
      have "freshenLC (vidx v') ` local_vars (nodeOf v') ant  subst_lconsts (inst v') = {}"
        by (rule out_of_scope)
      thus "freshenLC (vidx v') ` a_fresh ant  subst_lconsts (inst v') = {}" by simp
    qed
    also
    have "subst (inst v') (freshen (vidx v') f) = labelAtOut v' p'" using Rule by (simp add: labelAtOut_def)
    also
    note ‹labelAtOut v' p' = labelAtIn v p
    also
    have "?ants = ((λx. (extra_assms (v',x) |∪| hyps_along ?pth'  labelAtIn  v' x)) |`| f_antecedent r)"
      by (rule fimage_cong[OF refl])
        (auto simp add: labelAtIn_def labelAtOut_def Rule hyps_for_fimage fmember.rep_eq ffUnion.rep_eq)
    finally
    have "eff (NatRule (r, f))
        (, labelAtIn v p)
        ((λx. extra_assms (v',x) |∪|   labelAtIn v' x) |`| f_antecedent r)".
    }
    moreover

    { fix x
      assume "x |∈| cont ?t"
      then obtain a where "x = tree v' a ?pth'" and "a |∈| f_antecedent r"
        by (auto simp add: Rule)
      note this(1)
      moreover

      from  v' |∈| vertices a |∈| f_antecedent r
      have "valid_in_port (v',a)" by (simp add: Rule)
      moreover

      note ‹terminal_path v' t ?pth'
      ultimately

      have "v p pth. x = tree v p pth  valid_in_port (v,p)   terminal_path v t pth"
        by blast
    }
    ultimately

    show ?thesis using Rule
      by (auto intro!: exI[where x = ?t]  simp add: comp_def funion_assoc)
  next
    case Helper
    from Helper
    have "hyps (nodeOf v') p' = None" by simp
    with e ‹terminal_path v t pth
    have "terminal_path v' t ?pth'"..

    have "labelAtIn v' (plain_ant anyP) = labelAtIn v p"
      unfolding s[symmetric]
      using Helper by (simp add: labelAtIn_def labelAtOut_def)
    moreover
    { fix x
      assume "x |∈| cont ?t"

      hence "x = tree v' (plain_ant anyP) ?pth'"
        by (auto simp add: Helper)
      note this(1)
      moreover

      from  v' |∈| vertices
      have "valid_in_port (v',plain_ant anyP)" by (simp add: Helper)
      moreover

      note ‹terminal_path v' t ?pth'
      ultimately

      have "v p pth. x = tree v p pth  valid_in_port (v,p)   terminal_path v t pth"
        by blast
    }
    ultimately

    show ?thesis using Helper
      by (auto intro!: exI[where x = ?t]  simp add: comp_def funion_assoc )
  qed
qed

lemma global_in_ass: "global_assms TYPE('var) |⊆| ass_forms"
proof
  fix x
  assume "x |∈| global_assms TYPE('var)"
  then obtain v pf where "v |∈| vertices" and "nodeOf v = Assumption pf" and "x = labelAtOut v (Reg pf)"
    by (auto simp add: global_assms_simps)
  from this (1,2) valid_nodes
  have "Assumption pf  sset nodes" by (auto simp add: fmember.rep_eq)
  hence "pf  set assumptions" by (auto simp add: nodes_def stream.set_map)
  hence "closed pf" by (rule  assumptions_closed)
  with x = labelAtOut v (Reg pf)
  have "x = pf" by (auto simp add: labelAtOut_def lconsts_freshen closed_no_lconsts freshen_closed subst_closed)
  thus "x |∈| ass_forms" using pf  set assumptions by (auto simp add: ass_forms_def)
qed

primcorec edge_tree :: "'vertex  ('form, 'var) in_port  ('vertex, 'form, 'var) edge' tree" where
 "root (edge_tree v p) = (adjacentTo v p, (v,p))"
 | "cont (edge_tree v p) =
    (case adjacentTo v p of (v', p') 
    (if isReg v' p' then ((λ p. edge_tree  v' p) |`| inPorts (nodeOf v')) else {||}
    ))"

lemma tfinite_map_tree: "tfinite (map_tree f t)  tfinite t"
proof
  assume "tfinite (map_tree f t)"
  thus "tfinite t"
    by (induction "map_tree f t" arbitrary: t rule: tfinite.induct)
       (fastforce intro:  tfinite.intros simp add:  tree.map_sel)
next
  assume "tfinite t"
  thus "tfinite (map_tree f t)"
    by (induction t rule: tfinite.induct)
       (fastforce intro:  tfinite.intros simp add:  tree.map_sel)
qed


lemma finite_tree_edge_tree:
  "tfinite (tree v p pth)  tfinite (edge_tree v p)"
proof-
  have "map_tree (λ _. ())  (tree v p pth) = map_tree (λ _. ()) (edge_tree v p)"
   by(coinduction arbitrary: v p pth)
     (fastforce simp add: tree.map_sel rel_fset_def rel_set_def split: prod.split out_port.split graph_node.split option.split)
  thus ?thesis by (metis tfinite_map_tree)
qed

coinductive forbidden_path :: "'vertex  ('vertex, 'form, 'var) edge' stream  bool"   where
    forbidden_path: "((v1,p1),(v2,p2))  edges  hyps (nodeOf v1) p1 = None  forbidden_path v1 pth  forbidden_path v2 (((v1,p1),(v2,p2))##pth)"

lemma path_is_forbidden:
  assumes "valid_in_port (v,p)"
  assumes "ipath (edge_tree v p) es"
  shows "forbidden_path v es"
using assms
proof(coinduction arbitrary: v p es)
  case forbidden_path

  let ?es' = "stl es"

  from forbidden_path(2)
  obtain t' where "root (edge_tree v p) = shd es" and "t' |∈| cont (edge_tree v p)" and "ipath t' ?es'"
    by rule blast

  from ‹root (edge_tree v p) = shd es
  have [simp]: "shd es = (adjacentTo v p, (v,p))" by simp

  from saturated[OF ‹valid_in_port (v,p)]
  obtain v' p'
  where e:"((v',p'),(v,p))  edges" and [simp]: "adjacentTo v p = (v',p')"
    by (auto simp add: adjacentTo_def, metis (no_types, lifting) eq_fst_iff tfl_some)
  let ?e = "((v',p'),(v,p))"

  from e have "p' |∈| outPorts (nodeOf v')" using valid_edges by auto
  thus ?case
  proof(cases rule: out_port_cases)
    case Hyp
    with  t' |∈| cont (edge_tree v p)
    have False by auto
    thus ?thesis..
  next
    case Assumption
    with  t' |∈| cont (edge_tree v p)
    have False by auto
    thus ?thesis..
  next
    case (Rule r f)
    from t' |∈| cont (edge_tree v p) Rule
    obtain a where [simp]: "t' = edge_tree v' a" and "a |∈| f_antecedent r"  by auto

    have "es = ?e ## ?es'" by (cases es rule: stream.exhaust_sel) simp
    moreover

    have "?e  edges" using e by simp
    moreover

    from p' = Reg f nodeOf v' = Rule r
    have "hyps (nodeOf v') p' = None" by simp
    moreover

    from e valid_edges have "v' |∈| vertices"  by auto
    with nodeOf v' = Rule r a |∈| f_antecedent r
    have "valid_in_port (v', a)" by simp
    moreover

    have "ipath (edge_tree v' a) ?es'" using ‹ipath t' _ by simp
    ultimately

    show ?thesis by metis
  next
    case Helper
    from t' |∈| cont (edge_tree v p) Helper
    have [simp]: "t' = edge_tree v' (plain_ant anyP)" by simp

    have "es = ?e ## ?es'" by (cases es rule: stream.exhaust_sel) simp
    moreover

    have "?e  edges" using e by simp
    moreover

    from p' = Reg anyP nodeOf v' = Helper›
    have "hyps (nodeOf v') p' = None" by simp
    moreover

    from e valid_edges have "v' |∈| vertices"  by auto
    with nodeOf v' = Helper›
    have "valid_in_port (v', plain_ant anyP)" by simp
    moreover

    have "ipath (edge_tree v' (plain_ant anyP)) ?es'" using ‹ipath t' _ by simp
    ultimately

    show ?thesis by metis
  qed
qed

lemma forbidden_path_prefix_is_path:
  assumes "forbidden_path v es"
  obtains v' where  "path v' v (rev (stake n es))"
  using assms
  apply (atomize_elim)
  apply (induction n arbitrary: v es)
  apply simp
  apply (simp add: path_snoc)
  apply (subst (asm) (2) forbidden_path.simps)
  apply auto
  done

lemma forbidden_path_prefix_is_hyp_free:
  assumes "forbidden_path v es"
  shows "hyps_free (rev (stake n es))"
  using assms
  apply (induction n arbitrary: v es)
  apply (simp add: hyps_free_def)
  apply (subst (asm) (2) forbidden_path.simps)
  apply (force simp add: hyps_free_def)
  done


text ‹And now we prove that the tree is finite, which requires the above notion of a
@{term forbidden_path}, i.e.\@ an infinite path.›

theorem finite_tree:
  assumes "valid_in_port (v,p)"
  assumes "terminal_vertex v"
  shows "tfinite (tree v p pth)"
proof(rule ccontr)
  let ?n = "Suc (fcard vertices)"
  assume "¬ tfinite (tree v p pth)"
  hence "¬ tfinite (edge_tree v p)" unfolding finite_tree_edge_tree.
  then obtain es  :: "('vertex, 'form, 'var) edge' stream"
    where "ipath (edge_tree v p) es" using Konig by blast
  with ‹valid_in_port (v,p)
  have "forbidden_path v es" by (rule path_is_forbidden)
  from forbidden_path_prefix_is_path[OF this] forbidden_path_prefix_is_hyp_free[OF this]
  obtain v' where "path v' v (rev (stake ?n es))" and "hyps_free (rev (stake ?n es))"
    by blast
  from this ‹terminal_vertex v
  have "terminal_path  v' v (rev (stake ?n es))" by (rule terminal_pathI)
  hence "length (rev (stake ?n es))  fcard vertices"
    by (rule hyps_free_limited)
  thus False by simp
qed

text ‹The main result of this theory.›

theorem solved
unfolding solved_def
proof(intro ballI allI conjI impI)
  fix c
  assume "c |∈| conc_forms"
  hence "c  set conclusions"  by (auto simp add: conc_forms_def)
  from this(1) conclusions_present
  obtain v where "v |∈| vertices" and "nodeOf v = Conclusion c"
    by (auto, metis (no_types, lifting) image_iff image_subset_iff notin_fset)

  have "valid_in_port (v, (plain_ant c))"
    using v |∈| vertices nodeOf _ = _  by simp

  have "terminal_vertex v" using v |∈| vertices nodeOf v = Conclusion c by auto

  let ?t = "tree v (plain_ant c) []"

  have "fst (root ?t) = (global_assms TYPE('var), c)"
    using c  set conclusions nodeOf _ = _
    by (auto simp add: labelAtIn_def conclusions_closed closed_no_lconsts  freshen_def rename_closed subst_closed)
  moreover

  have "global_assms TYPE('var) |⊆| ass_forms" by (rule global_in_ass)
  moreover

  from  ‹terminal_vertex v
  have "terminal_path v v []" by (rule terminal_path_empty)
  with ‹valid_in_port (v, (plain_ant c))
  have "wf ?t" by (rule wf_tree)
  moreover

  from ‹valid_in_port (v, plain_ant c) ‹terminal_vertex v
  have "tfinite ?t" by (rule finite_tree)
  ultimately

  show "Γ t. fst (root t) = (Γ  c)  Γ |⊆| ass_forms  wf t  tfinite t" by blast
qed

end

end

Theory Rose_Tree

theory Rose_Tree
imports Main "HOL-Library.Sublist"
begin

text ‹For theory Incredible_Trees› we need rose trees; this theory contains
the generally useful part of that development.›

subsubsection ‹The rose tree data type›


datatype 'a rose_tree = RNode (root: 'a) (children:  "'a rose_tree list")

subsubsection ‹The set of paths in a rose tree›

text ‹Too bad that @{command inductive_set} does not allow for varying parameters...›

inductive it_pathsP :: "'a rose_tree  nat list  bool"  where
   it_paths_Nil: "it_pathsP t []"
 | it_paths_Cons: "i < length (children t)  children t ! i = t'  it_pathsP t' is  it_pathsP t (i#is)"

inductive_cases it_pathP_ConsE: "it_pathsP t (i#is)"

inductive_cases it_pathP_RNodeE: "it_pathsP (RNode r ants) is"

definition it_paths:: "'a rose_tree  nat list set"  where
  "it_paths t = Collect (it_pathsP t)"

lemma it_paths_eq [pred_set_conv]: "it_pathsP t = (λx. x  it_paths t)"
 by(simp add: it_paths_def)

lemmas it_paths_intros [intro?] = it_pathsP.intros[to_set]
lemmas it_paths_induct [consumes 1, induct set: it_paths] = it_pathsP.induct[to_set]
lemmas it_paths_cases [consumes 1, cases set: it_paths] = it_pathsP.cases[to_set]
lemmas it_paths_ConsE = it_pathP_ConsE[to_set]
lemmas it_paths_RNodeE = it_pathP_RNodeE[to_set]
lemmas it_paths_simps = it_pathsP.simps[to_set]

lemmas it_paths_intros(1)[simp]

lemma it_paths_RNode_Nil[simp]: "it_paths (RNode r []) = {[]}"
  by (auto elim: it_paths_cases)

lemma it_paths_Union: "it_paths t  insert [] (Union (((λ (i,t). ((#) i) ` it_paths t) ` set (List.enumerate (0::nat) (children t)))))"
  apply (rule)
  apply (erule it_paths_cases)
  apply (auto intro!: bexI simp add: in_set_enumerate_eq)
  done

lemma finite_it_paths[simp]: "finite (it_paths t)"
  by (induction t) (auto intro!:  finite_subset[OF it_paths_Union]  simp add: in_set_enumerate_eq)

subsubsection ‹Indexing into a rose tree›

fun tree_at :: "'a rose_tree  nat list  'a rose_tree" where
  "tree_at t [] = t"
| "tree_at t (i#is) = tree_at (children t ! i) is"

lemma it_paths_SnocE[elim_format]:
  assumes "is @ [i]  it_paths t"
  shows "is  it_paths t  i < length (children (tree_at t is))"
using assms
by (induction "is" arbitrary: t)(auto intro!: it_paths_intros elim!: it_paths_ConsE)


lemma it_paths_strict_prefix:
  assumes "is  it_paths t"
  assumes "strict_prefix is' is"
  shows "is'  it_paths t"
proof-
  from assms(2)
  obtain is'' where "is = is' @ is''" using strict_prefixE' by blast
  from assms(1)[unfolded this]
  show ?thesis
    by(induction is' arbitrary: t) (auto elim!: it_paths_ConsE intro!: it_paths_intros)
qed

lemma it_paths_prefix:
  assumes "is  it_paths t"
  assumes "prefix is' is"
  shows "is'  it_paths t"
using assms it_paths_strict_prefix strict_prefixI by fastforce

lemma it_paths_butlast:
  assumes "is  it_paths t"
  shows "butlast is  it_paths t"
using assms prefixeq_butlast by (rule it_paths_prefix)

lemma it_path_SnocI:
  assumes "is  it_paths t" 
  assumes "i < length (children (tree_at t is))"
  shows "is @ [i]  it_paths t"
  using assms
  by (induction t arbitrary: "is" i)
     (auto 4 4  elim!: it_paths_RNodeE intro: it_paths_intros)


end

Theory Incredible_Trees

theory Incredible_Trees
imports
  "HOL-Library.Sublist" 
  "HOL-Library.Countable"
  Entailment
  Rose_Tree
  Abstract_Rules_To_Incredible
begin

text ‹This theory defines incredible trees, which carry roughly the same information
as a (tree-shaped) incredible graph, but where the structure is still given by the data type, 
and not by a set of edges etc.›


text ‹
Tree-shape, but incredible-graph-like content (port names, explicit annotation and substitution)
›

datatype ('form,'rule,'subst,'var) itnode =
    I (iNodeOf': "('form, 'rule) graph_node")
      (iOutPort': "'form reg_out_port")
      (iAnnot': "nat")
      (iSubst': "'subst")
  | H (iAnnot': "nat")
      (iSubst': "'subst")

abbreviation "INode n p i s ants  RNode (I n p i s) ants"
abbreviation "HNode i s ants  RNode (H i s) ants"

type_synonym ('form,'rule,'subst,'var) itree = "('form,'rule,'subst,'var) itnode rose_tree"

fun iNodeOf where
   "iNodeOf (INode n p i s ants) = n"
 | "iNodeOf (HNode i s ants) = Helper"

context Abstract_Formulas begin
fun iOutPort where
   "iOutPort (INode n p i s ants) = p"
 | "iOutPort (HNode i s ants) = anyP"
end

fun iAnnot where "iAnnot it = iAnnot' (root it)"
fun iSubst where "iSubst it = iSubst' (root it)"
fun iAnts where "iAnts it = children it"

type_synonym ('form, 'rule, 'subst) fresh_check = "('form, 'rule) graph_node  nat  'subst  'form entailment  bool"

context  Abstract_Task
begin

  text ‹The well-formedness of the tree. The first argument can be varied, depending on whether we
  are interested in the local freshness side-conditions or not.›

  inductive iwf :: "('form, 'rule, 'subst) fresh_check  ('form,'rule,'subst,'var) itree  'form entailment  bool"
    for fc
    where
    iwf: "
       n  sset nodes;
       Reg p |∈| outPorts n;
       list_all2 (λ ip t. iwf fc t ((λ h . subst s (freshen i (labelsOut n h))) |`| hyps_for n ip |∪| Γ  subst s (freshen i (labelsIn n ip))))
                (inPorts' n) ants;
       fc n i s (Γ  c);
       c = subst s (freshen i p)
        iwf fc (INode n p i s ants) (Γ  c)"  
  | iwfH: "
       c |∉| ass_forms;
       c |∈| Γ;
       c = subst s (freshen i anyP)
        iwf fc (HNode i s []) (Γ  c)"  

lemma iwf_subst_freshen_outPort:
  "iwf lc ts ent 
  snd ent = subst (iSubst ts) (freshen (iAnnot ts) (iOutPort ts))"
  by (auto elim: iwf.cases)

definition all_local_vars :: "('form, 'rule) graph_node  'var set" where
  "all_local_vars n = (local_vars n ` fset (inPorts n))"

lemma all_local_vars_Helper[simp]:
  "all_local_vars Helper = {}"
  unfolding all_local_vars_def by simp

lemma all_local_vars_Assumption[simp]:
  "all_local_vars (Assumption c) = {}"
  unfolding all_local_vars_def by simp

text ‹Local freshness side-conditions, corresponding what we have in the
theory Natural_Deduction›.›

inductive local_fresh_check :: "('form, 'rule, 'subst) fresh_check" where
  " f. f |∈| Γ  freshenLC i ` (all_local_vars n)  lconsts f = {};
    freshenLC i ` (all_local_vars n)  subst_lconsts s = {}
     local_fresh_check n i s (Γ  c)"

abbreviation "local_iwf  iwf local_fresh_check"

text ‹No freshness side-conditions. Used with the tree that comes out of
globalize›, where we establish the (global) freshness conditions
separately.›

inductive no_fresh_check :: "('form, 'rule, 'subst) fresh_check" where
  "no_fresh_check n i s (Γ  c)"

abbreviation "plain_iwf  iwf no_fresh_check"

fun isHNode where
  "isHNode (HNode _ _ _ ) = True"
 |"isHNode _ = False"

lemma iwf_edge_match:
  assumes "iwf fc t ent"
  assumes "is@[i]  it_paths t"
  shows "subst (iSubst (tree_at t (is@[i]))) (freshen (iAnnot (tree_at t (is@[i]))) (iOutPort (tree_at t (is@[i]))))
     = subst (iSubst (tree_at t is)) (freshen (iAnnot (tree_at t is)) (a_conc (inPorts' (iNodeOf (tree_at t is)) ! i)))"
  using assms
  apply (induction arbitrary: "is" i)
   apply (auto elim!: it_paths_SnocE)[1]
   apply (rename_tac "is" i)
   apply (case_tac "is")
    apply (auto dest!: list_all2_nthD2)[1]
    using iwf_subst_freshen_outPort
    apply (solves ‹(auto)[1])
   apply (auto elim!: it_paths_ConsE dest!: list_all2_nthD2)[1]
   using it_path_SnocI
   apply (solves blast)
  apply (solves auto)
  done

lemma iwf_length_inPorts:
  assumes "iwf fc t ent"
  assumes "is  it_paths t"
  shows "length (iAnts (tree_at t is))  length (inPorts' (iNodeOf (tree_at t is)))"
  using assms
  by (induction arbitrary: "is" rule: iwf.induct)
     (auto elim!: it_paths_RNodeE dest: list_all2_lengthD list_all2_nthD2)

lemma iwf_local_not_in_subst:
  assumes "local_iwf t ent"
  assumes "is  it_paths t"
  assumes "var  all_local_vars (iNodeOf (tree_at t is))"
  shows "freshenLC (iAnnot (tree_at t is)) var  subst_lconsts (iSubst (tree_at t is))"
  using assms
  by (induction arbitrary: "is" rule: iwf.induct)
     (auto 4 4 elim!: it_paths_RNodeE local_fresh_check.cases dest: list_all2_lengthD list_all2_nthD2)
  
lemma iwf_length_inPorts_not_HNode:
  assumes "iwf fc t ent"
  assumes "is  it_paths t"
  assumes "¬ (isHNode (tree_at t is))"
  shows "length (iAnts (tree_at t is)) = length (inPorts' (iNodeOf (tree_at t is)))"
  using assms
  by (induction arbitrary: "is" rule: iwf.induct)
     (auto 4 4 elim!: it_paths_RNodeE  dest: list_all2_lengthD list_all2_nthD2)

lemma iNodeOf_outPorts:
  "iwf fc t ent  is  it_paths t  outPorts (iNodeOf (tree_at t is)) = {||}  False"
  by (induction arbitrary: "is" rule: iwf.induct)
     (auto 4 4 elim!: it_paths_RNodeE  dest: list_all2_lengthD list_all2_nthD2)

lemma iNodeOf_tree_at:
  "iwf fc t ent  is  it_paths t  iNodeOf (tree_at t is)  sset nodes"
  by (induction arbitrary: "is" rule: iwf.induct)
     (auto 4 4 elim!: it_paths_RNodeE  dest: list_all2_lengthD list_all2_nthD2)

lemma iwf_outPort: 
  assumes "iwf fc t ent"
  assumes "is  it_paths t"
  shows "Reg (iOutPort (tree_at t is)) |∈| outPorts (iNodeOf (tree_at t is))"
  using assms
  by (induction arbitrary: "is" rule: iwf.induct)
     (auto 4 4 elim!: it_paths_RNodeE  dest: list_all2_lengthD list_all2_nthD2)

inductive_set hyps_along for t "is" where
 "prefix (is'@[i]) is 
  i < length (inPorts' (iNodeOf (tree_at t is'))) 
  hyps (iNodeOf (tree_at t is')) h = Some (inPorts' (iNodeOf (tree_at t is')) ! i) 
  subst (iSubst (tree_at t is')) (freshen (iAnnot (tree_at t is')) (labelsOut (iNodeOf (tree_at t is')) h))  hyps_along t is"

lemma hyps_along_Nil[simp]: "hyps_along t [] = {}"
  by (auto simp add: hyps_along.simps)

lemma prefix_app_Cons_elim:
  assumes "prefix (xs@[y]) (z#zs)"
  obtains "xs = []" and "y = z"
   | xs' where "xs = z#xs'" and "prefix (xs'@[y]) zs"
using assms by (cases xs) auto

lemma hyps_along_Cons:
  assumes "iwf fc t ent"
  assumes "i#is  it_paths t"
  shows "hyps_along t (i#is) =
    (λh. subst (iSubst t) (freshen (iAnnot t) (labelsOut (iNodeOf t) h))) ` fset (hyps_for (iNodeOf t) (inPorts' (iNodeOf t) ! i))
     hyps_along (iAnts t ! i) is" (is "?S1 = ?S2  ?S3")
proof-
  from assms
  have "i < length (iAnts t)" and "is  it_paths (iAnts t ! i)" 
    by (auto elim: it_paths_ConsE)
  let "?t'" = "iAnts t ! i"

  show ?thesis
  proof (rule; rule)
    fix x
    assume "x  hyps_along t (i # is)"
    then obtain is' i' h where
      "prefix (is'@[i']) (i#is)"
      and "i' < length (inPorts' (iNodeOf (tree_at t is')))"
      and "hyps (iNodeOf (tree_at t is')) h = Some (inPorts' (iNodeOf (tree_at t is')) ! i')"
      and [simp]: "x = subst (iSubst (tree_at t is')) (freshen (iAnnot (tree_at t is')) (labelsOut (iNodeOf (tree_at t is')) h))"
    by (auto elim!: hyps_along.cases)
    from this(1)
    show "x  ?S2  ?S3"
    proof(cases rule: prefix_app_Cons_elim)
      assume "is' = []" and "i' = i"
      with ‹hyps (iNodeOf (tree_at t is')) h = Some _
      have "x  ?S2" by auto
      thus ?thesis..
    next
      fix is''
      assume [simp]: "is' = i # is''" and "prefix (is'' @ [i']) is"
      have "tree_at t is' = tree_at ?t' is''" by simp

      note ‹prefix (is'' @ [i']) is
           i' < length (inPorts' (iNodeOf (tree_at t is')))
           ‹hyps (iNodeOf (tree_at t is')) h = Some (inPorts' (iNodeOf (tree_at t is')) ! i')
      from this[unfolded ‹tree_at t is' = tree_at ?t' is'']
      have "subst (iSubst (tree_at (iAnts t ! i) is'')) (freshen (iAnnot (tree_at (iAnts t ! i) is'')) (labelsOut (iNodeOf (tree_at (iAnts t ! i) is'')) h))
           hyps_along (iAnts t ! i) is" by (rule hyps_along.intros)
      hence "x  ?S3" by simp
      thus ?thesis..
    qed
  next
    fix x
    assume "x  ?S2  ?S3"
    thus "x  ?S1"
    proof
      have "prefix ([]@[i]) (i#is)" by simp
      moreover
      from ‹iwf _ t _
      have "length (iAnts t)  length (inPorts' (iNodeOf (tree_at t []))) "
        by cases (auto dest: list_all2_lengthD)
      with i < _
      have "i < length (inPorts' (iNodeOf (tree_at t [])))" by simp
      moreover
      assume "x  ?S2"
      then obtain h where "h |∈| hyps_for (iNodeOf t) (inPorts' (iNodeOf t) ! i)"
        and [simp]: "x = subst (iSubst t) (freshen (iAnnot t) (labelsOut (iNodeOf t) h))" by auto
      from this(1)
      have "hyps (iNodeOf (tree_at t [])) h = Some (inPorts' (iNodeOf (tree_at t [])) ! i)" by simp
      ultimately
      have "subst (iSubst (tree_at t [])) (freshen (iAnnot (tree_at t [])) (labelsOut (iNodeOf (tree_at t [])) h))  hyps_along t (i # is)"
        by (rule hyps_along.intros)
      thus "x  hyps_along t (i # is)" by simp
    next
      assume "x  ?S3"
      thus "x  ?S1"
        apply (auto simp add: hyps_along.simps)
        apply (rule_tac x = "i#is'" in exI)
        apply auto
        done
    qed
  qed
qed

lemma iwf_hyps_exist:
  assumes "iwf lc it ent"
  assumes "is  it_paths it"
  assumes "tree_at it is = (HNode i s ants')"
  assumes "fst ent |⊆| ass_forms"
  shows "subst s (freshen i anyP)  hyps_along it is"
proof-
  from assms(1,2,3)
  have "subst s (freshen i anyP)  hyps_along it is 
      subst s (freshen i anyP) |∈| fst ent
        subst s (freshen i anyP) |∉| ass_forms"
  proof(induction arbitrary: "is" rule: iwf.induct)
    case (iwf n p  s' a' Γ ants c "is")

    have "iwf lc (INode n p a' s' ants) (Γ  c)"
      using iwf(1,2,3,4,5)
      by (auto intro!: iwf.intros elim!: list_all2_mono)

    show ?case
    proof(cases "is")
      case Nil
      with ‹tree_at (INode n p a' s' ants) is = HNode i s ants'
      show ?thesis by auto
    next
      case (Cons i' "is'")
      with is  it_paths (INode n p a' s' ants)
      have "i' < length ants" and "is'  it_paths (ants ! i')"
        by (auto elim: it_paths_ConsE)

      let ?Γ' = "(λh. subst s' (freshen a' (labelsOut n h))) |`| hyps_for n (inPorts' n ! i')"

      from ‹tree_at (INode n p a' s' ants) is = HNode i s ants'
      have "tree_at (ants ! i') is' = HNode i s ants'" using Cons by simp

      from  iwf.IH i' < length ants  is'  it_paths (ants ! i') this
      have  "subst s (freshen i anyP)  hyps_along (ants ! i') is'
         subst s (freshen i anyP) |∈| ?Γ' |∪| Γ  subst s (freshen i anyP) |∉| ass_forms"
        by (auto dest: list_all2_nthD2)
      moreover
      from  is  it_paths (INode n p a' s' ants)
      have "hyps_along (INode n p a' s' ants) is = fset ?Γ'  hyps_along (ants ! i') is'"
        using is = _
        by (simp add: hyps_along_Cons[OF ‹iwf lc (INode n p a' s' ants) (Γ  c)])
      ultimately
      show ?thesis by auto
    qed
  next
    case (iwfH c  Γ s' i' "is")
    hence [simp]: "is = []" "i' = i" "s' = s" by simp_all
    from c = subst s' (freshen i' anyP) c |∈| Γ c |∉| ass_forms›
    show ?case by simp
  qed
  with assms(4)
  show ?thesis by blast
qed

definition hyp_port_for' :: "('form, 'rule, 'subst, 'var) itree  nat list  'form  nat list × nat × ('form, 'var) out_port" where
  "hyp_port_for' t is f = (SOME x.
   (case x of (is', i, h)  
      prefix (is' @ [i]) is 
      i < length (inPorts' (iNodeOf (tree_at t is'))) 
      hyps (iNodeOf (tree_at t is')) h =  Some (inPorts' (iNodeOf (tree_at t is')) ! i) 
      f = subst (iSubst  (tree_at t is')) (freshen (iAnnot (tree_at t is')) (labelsOut (iNodeOf (tree_at t is')) h))
   ))"

lemma hyp_port_for_spec':
  assumes "f  hyps_along t is"
  shows "(case hyp_port_for' t is f of (is', i, h)  
      prefix (is' @ [i]) is 
      i < length (inPorts' (iNodeOf (tree_at t is'))) 
      hyps (iNodeOf (tree_at t is')) h =  Some (inPorts' (iNodeOf (tree_at t is')) ! i) 
      f = subst (iSubst  (tree_at t is')) (freshen (iAnnot (tree_at t is')) (labelsOut (iNodeOf (tree_at t is')) h)))"
using assms unfolding hyps_along.simps hyp_port_for'_def by -(rule someI_ex, blast)

definition hyp_port_path_for :: "('form, 'rule, 'subst, 'var) itree  nat list  'form  nat list"
  where "hyp_port_path_for t is f = fst (hyp_port_for' t is f)"
definition hyp_port_i_for ::  "('form, 'rule, 'subst, 'var) itree  nat list  'form  nat"
  where "hyp_port_i_for t is f = fst (snd (hyp_port_for' t is f))"
definition hyp_port_h_for :: "('form, 'rule, 'subst, 'var) itree  nat list  'form  ('form, 'var) out_port"
  where "hyp_port_h_for t is f = snd (snd (hyp_port_for' t is f))"

lemma hyp_port_prefix:
  assumes "f  hyps_along t is"
  shows "prefix (hyp_port_path_for t is f@[hyp_port_i_for t is f]) is"
using hyp_port_for_spec'[OF assms] unfolding hyp_port_path_for_def hyp_port_i_for_def by auto

lemma hyp_port_strict_prefix:
  assumes "f  hyps_along t is"
  shows "strict_prefix (hyp_port_path_for t is f) is"
using hyp_port_prefix[OF assms] by (simp add: strict_prefixI' prefix_order.dual_order.strict_trans1)

lemma hyp_port_it_paths:
  assumes "is  it_paths t"
  assumes "f  hyps_along t is"
  shows "hyp_port_path_for t is f  it_paths t"
using assms by (rule it_paths_strict_prefix[OF _ hyp_port_strict_prefix] )


lemma hyp_port_hyps:
  assumes "f  hyps_along t is"
  shows "hyps (iNodeOf (tree_at t (hyp_port_path_for t is f))) (hyp_port_h_for t is f) = Some (inPorts' (iNodeOf (tree_at t (hyp_port_path_for t is f))) ! hyp_port_i_for t is f)"
using hyp_port_for_spec'[OF assms] unfolding hyp_port_path_for_def hyp_port_i_for_def hyp_port_h_for_def by auto

lemma hyp_port_outPort:
  assumes "f  hyps_along t is"
  shows "(hyp_port_h_for t is f) |∈| outPorts (iNodeOf (tree_at t (hyp_port_path_for t is f)))"
using hyps_correct[OF hyp_port_hyps[OF assms]]..

lemma hyp_port_eq:
  assumes "f  hyps_along t is"
  shows "f = subst (iSubst (tree_at t (hyp_port_path_for t is f))) (freshen (iAnnot (tree_at t (hyp_port_path_for t is f))) (labelsOut (iNodeOf (tree_at t (hyp_port_path_for t is f))) (hyp_port_h_for t is f)))"
using hyp_port_for_spec'[OF assms] unfolding hyp_port_path_for_def hyp_port_i_for_def hyp_port_h_for_def by auto


definition isidx :: "nat list  nat" where "isidx xs = to_nat (Some xs)"
definition v_away :: "nat" where "v_away = to_nat (None :: nat list option)"
lemma isidx_inj[simp]: "isidx xs = isidx ys  xs = ys"
  unfolding isidx_def by simp
lemma isidx_v_away[simp]: "isidx xs  v_away"
  unfolding isidx_def v_away_def by simp


definition mapWithIndex where "mapWithIndex f xs = map (λ (i,t) . f i t) (List.enumerate 0 xs)"
lemma mapWithIndex_cong [fundef_cong]:
  "xs = ys  (x i. x  set ys  f i x = g i x)  mapWithIndex f xs = mapWithIndex g ys"
unfolding mapWithIndex_def by (auto simp add: in_set_enumerate_eq)

lemma mapWithIndex_Nil[simp]: "mapWithIndex f [] = []"
  unfolding mapWithIndex_def by simp

lemma length_mapWithIndex[simp]: "length (mapWithIndex f xs) = length xs"
  unfolding mapWithIndex_def by simp

lemma nth_mapWithIndex[simp]: "i < length xs  mapWithIndex f xs ! i = f i (xs ! i)"
  unfolding mapWithIndex_def by (auto simp add: nth_enumerate_eq)

lemma list_all2_mapWithIndex2E:
  assumes "list_all2 P as bs"
  assumes " i a b . i < length bs  P a b  Q a (f i b)"
  shows "list_all2 Q as (mapWithIndex f bs)"
using assms(1)
by (auto simp add: list_all2_conv_all_nth mapWithIndex_def nth_enumerate_eq intro: assms(2) split: prod.split)

text ‹The globalize function, which renames all local constants so that they cannot clash with 
local constants occurring anywhere else in the tree.›


fun globalize_node :: "nat list  ('var  'var)  ('form,'rule,'subst,'var) itnode   ('form,'rule,'subst,'var) itnode"  where
  "globalize_node is f (I n p i s) =  I n p (isidx is) (subst_renameLCs f s)"
  | "globalize_node is f (H i s) = H (isidx is) (subst_renameLCs f s)"

fun globalize :: "nat list  ('var  'var)  ('form,'rule,'subst,'var) itree  ('form,'rule,'subst,'var) itree" where
  "globalize is f (RNode r ants) = RNode 
    (globalize_node is f r)
    (mapWithIndex (λ i' t.
      globalize (is@[i'])
                (rerename (a_fresh (inPorts' (iNodeOf (RNode r ants)) ! i'))
                          (iAnnot (RNode r ants)) (isidx is) f)
                t
      ) ants)"

lemma iAnnot'_globalize_node[simp]: "iAnnot' (globalize_node is f n) = isidx is"
  by (cases n) auto

lemma iAnnot_globalize:
  assumes "is'  it_paths (globalize is f t)"
  shows  "iAnnot (tree_at (globalize is f t) is') = isidx (is@is')"
  using assms
  by (induction t arbitrary: f "is" is') (auto elim!: it_paths_RNodeE)

lemma all_local_consts_listed':
  assumes "n  sset nodes"
  assumes "p |∈| inPorts n"
  shows "lconsts (a_conc p)  ((lconsts ` fset (a_hyps p)))  a_fresh p "
  using assms
  by (auto simp add: nodes_def stream.set_map lconsts_anyP closed_no_lconsts conclusions_closed fmember.rep_eq f_antecedent_def dest!: all_local_consts_listed)

lemma no_local_consts_in_consequences':
  "n  sset nodes  Reg p |∈| outPorts n   lconsts p = {}"
  using no_local_consts_in_consequences
  by (auto simp add: nodes_def lconsts_anyP closed_no_lconsts assumptions_closed stream.set_map f_consequent_def)

lemma iwf_globalize:
  assumes "local_iwf t (Γ  c)"
  shows "plain_iwf (globalize is f t) (renameLCs f |`| Γ  renameLCs f c)"
using assms
proof (induction t "Γ  c" arbitrary: "is" f Γ c rule: iwf.induct)
  case (iwf n p s i Γ ants c "is" f)

  note n  sset nodes›
  moreover
  note ‹Reg p |∈| outPorts n
  moreover
  { fix i' 
    let ?V = "a_fresh (inPorts' n ! i')"
    let ?f' = "rerename ?V i (isidx is) f"
    let ?t = "globalize (is @ [i']) ?f' (ants ! i')"
    let ?ip = "inPorts' n ! i'"
    let ?Γ' = "(λh. subst (subst_renameLCs f s) (freshen (isidx is) (labelsOut n h))) |`| hyps_for n ?ip"
    let ?c' = "subst (subst_renameLCs f s) (freshen (isidx is) (labelsIn n ?ip))"

    assume "i' < length (inPorts' n)"
    hence "(inPorts' n ! i') |∈| inPorts n" by (simp add: inPorts_fset_of)

    from i' < length (inPorts' n)
    have subset_V: "?V  all_local_vars n"
      unfolding all_local_vars_def
      by (auto simp add: inPorts_fset_of set_conv_nth)

    from ‹local_fresh_check n i s (Γ  c) 
    have "freshenLC i ` all_local_vars n  subst_lconsts s = {}" 
      by (rule local_fresh_check.cases) simp
    hence "freshenLC i ` ?V  subst_lconsts s = {}" 
      using subset_V  by auto
    hence rerename_subst: "subst_renameLCs ?f' s = subst_renameLCs f s"
      by (rule rerename_subst_noop)

    from all_local_consts_listed'[OF n  sset nodes› (inPorts' n ! i') |∈| inPorts n]
    have subset_conc: "lconsts (a_conc (inPorts' n ! i'))  ?V"
      and subset_hyp': " hyp . hyp |∈| a_hyps (inPorts' n ! i')  lconsts hyp  ?V"
      by (auto simp add: fmember.rep_eq)
      
    from List.list_all2_nthD[OF ‹list_all2 _ _ _ i' < length (inPorts' n),simplified]
    have "plain_iwf ?t
           (renameLCs ?f' |`| ((λh. subst s (freshen i (labelsOut n h))) |`| hyps_for n ?ip |∪|  Γ) 
            renameLCs ?f' (subst s (freshen i (a_conc ?ip))))"
         by simp
    also have "renameLCs ?f' |`| ((λh. subst s (freshen i (labelsOut n h))) |`| hyps_for n ?ip |∪|  Γ)
      = (λx. subst (subst_renameLCs ?f' s) (renameLCs ?f' (freshen i (labelsOut n x)))) |`|  hyps_for n ?ip |∪| renameLCs ?f' |`| Γ"
     by (simp add: fimage_fimage fimage_funion comp_def rename_subst)
    also have "renameLCs ?f' |`| Γ =  renameLCs f |`| Γ"
    proof(rule fimage_cong[OF refl])
      fix x
      assume "x |∈| Γ"
      with ‹local_fresh_check n i s (Γ  c)
      have "freshenLC i ` all_local_vars n  lconsts x = {}" 
        by (elim local_fresh_check.cases) simp
      hence "freshenLC i ` ?V  lconsts x = {}" 
        using subset_V  by auto
      thus "renameLCs ?f' x = renameLCs f x"
        by (rule rerename_rename_noop)
    qed
    also have "(λx. subst (subst_renameLCs ?f' s) (renameLCs ?f' (freshen i (labelsOut n x)))) |`|  hyps_for n ?ip = ?Γ'"
    proof(rule fimage_cong[OF refl])
      fix hyp
      assume "hyp |∈| hyps_for n (inPorts' n ! i')"
      hence "labelsOut n hyp |∈| a_hyps (inPorts' n ! i')"
        apply (cases hyp)
        apply (solves simp)
        apply (cases n)
        apply (auto split: if_splits)
        done
      from subset_hyp'[OF this]
      have subset_hyp: "lconsts (labelsOut n hyp)  ?V".
      
      show "subst (subst_renameLCs ?f' s) (renameLCs ?f' (freshen i (labelsOut n hyp))) =
            subst (subst_renameLCs f s)  (freshen (isidx is) (labelsOut n hyp))"
        apply (simp add: freshen_def rename_rename  rerename_subst)
        apply (rule arg_cong[OF renameLCs_cong])
        apply (auto dest: subsetD[OF subset_hyp])
        done
    qed
    also have "renameLCs ?f' (subst s (freshen i (a_conc ?ip))) = subst (subst_renameLCs ?f' s) (renameLCs ?f' (freshen i (a_conc ?ip)))" by (simp add: rename_subst)
    also have "... = ?c'"
        apply (simp add: freshen_def rename_rename  rerename_subst)
        apply (rule arg_cong[OF renameLCs_cong])
        apply (auto dest: subsetD[OF subset_conc])
        done
    finally
    have "plain_iwf ?t (?Γ' |∪| renameLCs f |`| Γ  ?c')".
  }
  with list_all2_lengthD[OF ‹list_all2 _ _ _]
  have "list_all2
     (λip t. plain_iwf t ((λh. subst (subst_renameLCs f s)
       (freshen (isidx is) (labelsOut n h))) |`| hyps_for n ip |∪|  renameLCs f |`| Γ  subst (subst_renameLCs f s) (freshen (isidx is) (labelsIn n ip))))
     (inPorts' n)
     (mapWithIndex (λ i' t. globalize (is@[i']) (rerename (a_fresh (inPorts' n ! i')) i (isidx is) f) t) ants)"
   by (auto simp add: list_all2_conv_all_nth)
  moreover
  have "no_fresh_check n (isidx is) (subst_renameLCs f s) (renameLCs f |`| Γ  renameLCs f c)"..
  moreover
  from n  sset nodes› ‹Reg p |∈| outPorts n
  have "lconsts p = {}" by (rule no_local_consts_in_consequences')
  with c = subst s (freshen i p)
  have "renameLCs f c = subst (subst_renameLCs f s) (freshen (isidx is) p)"
    by (simp add: rename_subst rename_closed freshen_closed)
  ultimately
  show ?case
    unfolding globalize.simps globalize_node.simps iNodeOf.simps iAnnot.simps itnode.sel rose_tree.sel  Let_def 
    by (rule iwf.intros(1))
next
  case (iwfH c Γ s i "is" f)
  from c |∉| ass_forms›
  have "renameLCs f c |∉| ass_forms"
    using assumptions_closed closed_no_lconsts lconsts_renameLCs rename_closed by fastforce
  moreover
  from c |∈| Γ
  have "renameLCs f c |∈| renameLCs f |`| Γ"  by auto
  moreover
  from c = subst s (freshen i anyP)
  have "renameLCs f c = subst (subst_renameLCs f s)  (freshen (isidx is) anyP)"
    by (metis freshen_closed lconsts_anyP rename_closed rename_subst)
  ultimately 
  show "plain_iwf (globalize is f (HNode i s [])) (renameLCs f |`| Γ  renameLCs f c)" 
    unfolding globalize.simps globalize_node.simps  mapWithIndex_Nil  Let_def 
    by (rule iwf.intros(2))
qed

definition fresh_at where
  "fresh_at t xs =
   (case rev xs of []  {}
                 | (i#is')  freshenLC (iAnnot (tree_at t (rev is'))) ` (a_fresh (inPorts' (iNodeOf (tree_at t (rev is'))) ! i)))"

lemma fresh_at_Nil[simp]:
  "fresh_at t [] = {}"
  unfolding fresh_at_def by simp

lemma fresh_at_snoc[simp]:
  "fresh_at t (is@[i]) = freshenLC (iAnnot (tree_at t is)) ` (a_fresh (inPorts' (iNodeOf (tree_at t is)) ! i))"
  unfolding fresh_at_def by simp

lemma fresh_at_def':
  "fresh_at t is =
   (if is = [] then {}
    else freshenLC (iAnnot (tree_at t (butlast is))) ` (a_fresh (inPorts' (iNodeOf (tree_at t (butlast is))) ! last is)))"
  unfolding fresh_at_def by (auto split: list.split)

lemma fresh_at_Cons[simp]:
  "fresh_at t (i#is) = (if is = [] then freshenLC (iAnnot t) ` (a_fresh (inPorts' (iNodeOf t) ! i)) else (let t' = iAnts t ! i in fresh_at t' is))"
  unfolding fresh_at_def'
  by (auto simp add: Let_def)

definition fresh_at_path where
  "fresh_at_path t is = (fresh_at t ` set (prefixes is))"

lemma fresh_at_path_Nil[simp]:
  "fresh_at_path t [] = {}"
  unfolding fresh_at_path_def by simp

lemma fresh_at_path_Cons[simp]:
  "fresh_at_path t (i#is) = fresh_at t [i]  fresh_at_path (iAnts t ! i) is"
  unfolding fresh_at_path_def
  by (fastforce split: if_splits)
  
lemma globalize_local_consts:
  assumes "is'  it_paths (globalize is f t)"
  shows "subst_lconsts (iSubst (tree_at (globalize is f t) is')) 
    fresh_at_path (globalize is f t) is'  range f"
  using assms
  apply (induction "is" f t  arbitrary: is' rule:globalize.induct)
  apply (rename_tac "is" f r ants is')
  apply (case_tac r)
   apply (auto simp add: subst_lconsts_subst_renameLCs  elim!: it_paths_RNodeE)
   apply (solves force dest!: subsetD[OF range_rerename])
  apply (solves force dest!: subsetD[OF range_rerename])
  done
  
lemma iwf_globalize':
  assumes "local_iwf t ent"
  assumes " x. x |∈| fst ent  closed x"
  assumes "closed (snd ent)"
  shows "plain_iwf (globalize is (freshenLC v_away) t) ent"
using assms
proof(induction ent rule: prod.induct)
  case (Pair Γ c)
  have "plain_iwf (globalize is (freshenLC v_away) t) (renameLCs (freshenLC v_away) |`| Γ  renameLCs (freshenLC v_away) c)"
    by (rule iwf_globalize[OF Pair(1)])
  also
  from Pair(3) have "closed c" by simp
  hence "renameLCs (freshenLC v_away) c = c" by (simp add: closed_no_lconsts rename_closed)
  also
  from Pair(2)
  have "renameLCs (freshenLC v_away) |`| Γ = Γ"
    by (auto simp add: closed_no_lconsts rename_closed fmember.rep_eq image_iff)
  finally show ?case.
qed
end   

end

Theory Build_Incredible_Tree

theory Build_Incredible_Tree
imports Incredible_Trees Natural_Deduction
begin

text ‹
This theory constructs an incredible tree (with freshness checked only locally) from a natural
deduction tree.
›

lemma image_eq_to_f:
  assumes  "f1 ` S1 = f2 ` S2"
  obtains f where " x. x  S2  f x  S1  f1 (f x) = f2 x"
proof (atomize_elim)
  from assms
  have "x. x  S2  ( y. y  S1  f1 y = f2 x)" by (metis image_iff)
  thus "f. x. x  S2  f x  S1  f1 (f x) = f2 x" by metis
qed

context includes fset.lifting
begin
lemma fimage_eq_to_f:
  assumes  "f1 |`| S1 = f2 |`| S2"
  obtains f where " x. x |∈| S2  f x |∈| S1  f1 (f x) = f2 x"
using assms apply transfer using image_eq_to_f by metis
end

context Abstract_Task
begin

lemma build_local_iwf:
  fixes t :: "('form entailment × ('rule × 'form) NatRule) tree"
  assumes "tfinite t"
  assumes "wf t"
  shows " it. local_iwf it (fst (root t))"
using assms
proof(induction)
  case (tfinite t)
  from ‹wf t
  have "snd (root t)  R" using wf.simps by blast

  from ‹wf t
  have "eff (snd (root t)) (fst (root t)) ((fst  root) |`| cont t)" using wf.simps by blast

  from ‹wf t
  have " t'. t' |∈| cont t  wf t'" using wf.simps by blast
  hence IH: " Γ' t'. t' |∈| cont t  (it'. local_iwf it' (fst (root t')))" using tfinite(2) by blast
  then obtain its where its: " t'. t' |∈| cont t  local_iwf (its t') (fst (root t'))" by metis

  from ‹eff _ _ _
  show ?case               
  proof(cases rule: eff.cases[case_names Axiom NatRule Cut])
  case (Axiom c Γ)
    show ?thesis
    proof (cases "c |∈| ass_forms")
      case True (* Global assumption *)
      then  have "c  set assumptions"  by (auto simp add:  ass_forms_def)

      let "?it" = "INode (Assumption c) c undefined undefined [] ::  ('form, 'rule, 'subst, 'var) itree"

      from c  set assumptions
      have "local_iwf ?it (Γ  c)"
        by (auto intro!: iwf local_fresh_check.intros)

      thus ?thesis unfolding Axiom..
    next
      case False
      obtain s where "subst s anyP = c" by atomize_elim (rule anyP_is_any)
      hence [simp]: "subst s (freshen undefined anyP) = c" by (simp add: lconsts_anyP freshen_closed)
  
      let "?it" = "HNode undefined s [] ::  ('form, 'rule, 'subst, 'var) itree"
  
      from  c |∈| Γ False
      have "local_iwf ?it (Γ  c)" by (auto intro: iwfH)
      thus ?thesis unfolding Axiom..
    qed
  next
  case (NatRule rule c ants Γ i s)
    from ‹natEff_Inst rule c ants
    have "snd rule = c"  and [simp]: "ants = f_antecedent (fst rule)" and "c  set (consequent (fst rule))"
      by (auto simp add: natEff_Inst.simps)  

    from (fst  root) |`| cont t = (λant. (λp. subst s (freshen i p)) |`| a_hyps ant |∪| Γ  subst s (freshen i (a_conc ant))) |`| ants
    obtain to_t where " ant. ant |∈| ants  to_t ant |∈| cont t  (fst  root) (to_t ant) = ((λp. subst s (freshen i p)) |`| a_hyps ant |∪| Γ  subst s (freshen i (a_conc ant)))"
      by (rule fimage_eq_to_f) (rule that)
    hence to_t_in_cont: " ant. ant |∈| ants  to_t ant |∈| cont t"
      and to_t_root: " ant. ant |∈| ants   fst (root (to_t ant)) = ((λp. subst s (freshen i p)) |`| a_hyps ant |∪| Γ  subst s (freshen i (a_conc ant)))"
      by auto

    let ?ants' = "map (λ ant. its (to_t ant)) (antecedent (fst rule))"
    let "?it" = "INode (Rule (fst rule)) c i s ?ants' ::  ('form, 'rule, 'subst, 'var) itree"

    from ‹snd (root t)  R›
    have "fst rule  sset rules"
      unfolding NatRule
      by (auto simp add: stream.set_map n_rules_def no_empty_conclusions )
    moreover
    from c  set (consequent (fst rule))
    have "c |∈| f_consequent (fst rule)" by (simp add: f_consequent_def)
    moreover
    { fix ant
      assume "ant  set (antecedent (fst rule))"
      hence "ant |∈| ants" by (simp add: f_antecedent_def)
      from its[OF to_t_in_cont[OF this]]
      have "local_iwf (its (to_t ant)) (fst (root (to_t ant)))".
      also have "fst (root (to_t ant)) =
        ((λp. subst s (freshen i p)) |`| a_hyps ant |∪| Γ  subst s (freshen i (a_conc ant)))"
        by (rule to_t_root[OF ant |∈| ants])
      also have " =
        ((λh. subst s (freshen i (labelsOut (Rule (fst rule)) h))) |`| hyps_for (Rule (fst rule)) ant |∪| Γ
          subst s (freshen i (a_conc ant)))" 
         using ant |∈| ants
         by auto
      finally
      have "local_iwf (its (to_t ant))
           ((λh. subst s (freshen i (labelsOut (Rule (fst rule)) h))) |`| hyps_for (Rule (fst rule)) ant |∪|
            Γ   subst s (freshen i (a_conc ant)))".
    }
    moreover
    from NatRule(5,6)
    have "local_fresh_check (Rule (fst rule)) i s (Γ  subst s (freshen i c))"
      by (fastforce intro!: local_fresh_check.intros simp add: all_local_vars_def fmember.rep_eq)
    ultimately
    have "local_iwf ?it ((Γ  subst s (freshen i c)))"
      by (intro iwf ) (auto simp add: list_all2_map2 list_all2_same)
    thus ?thesis unfolding NatRule..
  next
  case (Cut Γ con)
    obtain s where "subst s anyP = con" by atomize_elim (rule anyP_is_any)
    hence  [simp]: "subst s (freshen undefined anyP) = con" by (simp add: lconsts_anyP freshen_closed)

    from (fst  root) |`| cont t = {|Γ  con|}
    obtain t'  where "t' |∈| cont t" and [simp]: "fst (root t') = (Γ  con)"
      by (cases "cont t") auto
    
    from t' |∈| cont t obtain "it'" where "local_iwf it' (Γ  con)" using IH by force

    let "?it" = "INode Helper anyP undefined s [it'] ::  ('form, 'rule, 'subst, 'var) itree"

    from ‹local_iwf it' (Γ  con)
    have "local_iwf ?it (Γ  con)" by (auto intro!: iwf local_fresh_check.intros)
    thus ?thesis unfolding Cut..
  qed 
qed

definition to_it :: "('form entailment × ('rule × 'form) NatRule) tree  ('form,'rule,'subst,'var) itree" where
  "to_it t = (SOME it. local_iwf it (fst (root t)))"

lemma iwf_to_it:
  assumes "tfinite t" and "wf t"
  shows "local_iwf (to_it t) (fst (root t))"
unfolding to_it_def using build_local_iwf[OF assms] by (rule someI2_ex)
end
end

Theory Incredible_Completeness

theory Incredible_Completeness
imports Natural_Deduction Incredible_Deduction Build_Incredible_Tree
begin

text ‹
This theory takes the tree produced in @{theory Incredible_Proof_Machine.Build_Incredible_Tree}, globalizes it using
@{term globalize}, and then builds the incredible proof graph out of it.
›

type_synonym 'form vertex = "('form × nat list)"
type_synonym ('form, 'var) edge'' = "('form vertex, 'form, 'var) edge'"

locale Solved_Task =
  Abstract_Task  freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP antecedent consequent rules assumptions conclusions
   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" 
    and assumptions :: "'form list" 
    and conclusions :: "'form list" +
  assumes solved: solved
begin

text ‹Let us get our hand on concrete trees.›

definition ts :: "'form  (('form entailment) × ('rule × 'form) NatRule) tree" where
  "ts c = (SOME t. snd (fst (root t)) = c  fst (fst (root t)) |⊆| ass_forms  wf t  tfinite t)"

lemma
  assumes "c |∈| conc_forms"
  shows ts_conc: "snd (fst (root (ts c))) = c"
  and   ts_context: "fst (fst (root (ts c))) |⊆| ass_forms"
  and   ts_wf: "wf (ts c)"
  and   ts_finite[simp]: "tfinite (ts c)"
  unfolding atomize_conj conj_assoc ts_def
  apply (rule someI_ex)
  using solved assms
  by (force simp add: solved_def)

abbreviation it' where
  "it' c  globalize [fidx conc_forms c, 0] (freshenLC v_away) (to_it (ts c))"

lemma iwf_it:
  assumes "c  set conclusions"
  shows "plain_iwf (it' c) (fst (root (ts c)))"
  using assms
  apply (auto simp add: ts_conc conclusions_closed intro!: iwf_globalize' iwf_to_it ts_finite ts_wf)
  by (meson assumptions_closed fset_mp mem_ass_forms mem_conc_forms ts_context)

definition vertices :: "'form vertex fset"  where
  "vertices = Abs_fset (Union ( set (map (λ c. insert (c, []) ((λ p. (c, 0 # p)) ` (it_paths (it' c))))  conclusions)))"

lemma mem_vertices: "v |∈| vertices   (fst v  set conclusions  (snd v = []  snd v  ((#) 0) ` it_paths (it' (fst v))))"
  unfolding vertices_def fmember.rep_eq ffUnion.rep_eq 
  by (cases v)(auto simp add: Abs_fset_inverse Bex_def )

lemma prefixeq_vertices: "(c,is) |∈| vertices  prefix is' is  (c, is') |∈| vertices"
  by (cases is') (auto simp add: mem_vertices intro!: imageI elim: it_paths_prefix)

lemma none_vertices[simp]: "(c, []) |∈| vertices  c  set conclusions"
  by (simp add: mem_vertices)

lemma some_vertices[simp]: "(c, i#is) |∈| vertices  c  set conclusions  i = 0  is  it_paths (it' c)"
  by (auto simp add: mem_vertices)

lemma vertices_cases[consumes 1, case_names None Some]:
  assumes "v |∈| vertices"
  obtains c where "c  set conclusions" and "v = (c, [])"
      |   c "is" where "c  set conclusions" and "is  it_paths (it' c)" and "v = (c, 0#is)"
using assms by (cases v; rename_tac "is"; case_tac "is"; auto)

lemma vertices_induct[consumes 1, case_names None Some]:
  assumes "v |∈| vertices"
  assumes " c. c  set conclusions  P (c, [])"
  assumes " c is . c  set conclusions  is  it_paths (it' c)  P (c, 0#is)"
  shows "P v"
using assms by (cases v; rename_tac "is"; case_tac "is"; auto)

fun nodeOf :: "'form vertex  ('form, 'rule) graph_node" where
  "nodeOf (pf, []) = Conclusion pf"
| "nodeOf (pf, i#is) = iNodeOf (tree_at (it' pf) is)"

fun inst where
  "inst (c,[]) = empty_subst"
 |"inst (c, i#is) = iSubst (tree_at (it' c) is)" 

lemma terminal_is_nil[simp]: "v |∈| vertices  outPorts (nodeOf v) = {||}  snd v = []"
 by (induction v rule: nodeOf.induct)
    (auto elim: iNodeOf_outPorts[rotated] iwf_it)

sublocale Vertex_Graph nodes inPorts outPorts vertices nodeOf.

definition edge_from :: "'form  nat list => ('form vertex × ('form,'var) out_port)" where 
  "edge_from c is = ((c, 0 # is),  Reg (iOutPort (tree_at (it' c) is)))"

lemma fst_edge_from[simp]: "fst (edge_from c is) = (c, 0 # is)"
  by (simp add: edge_from_def)

fun in_port_at :: "('form × nat list)  nat  ('form,'var) in_port" where
    "in_port_at (c, [])  _  = plain_ant c"
  | "in_port_at (c, _#is) i = inPorts' (iNodeOf (tree_at (it' c) is)) ! i"

definition edge_to :: "'form  nat list => ('form vertex × ('form,'var) in_port)"  where
 "edge_to c is =
    (case rev is of   []    ((c, []),           in_port_at (c, []) 0)
                    | i#is  ((c, 0 # (rev is)), in_port_at (c, (0#rev is)) i))"

lemma edge_to_Nil[simp]: "edge_to c [] = ((c, []), plain_ant c)"
  by (simp add: edge_to_def)

lemma edge_to_Snoc[simp]: "edge_to c (is@[i]) = ((c, 0 # is), in_port_at ((c, 0 # is)) i)"
  by (simp add: edge_to_def)

definition edge_at :: "'form  nat list => ('form, 'var) edge''"  where
   "edge_at c is = (edge_from c is, edge_to c is)"

lemma fst_edge_at[simp]: "fst (edge_at c is) = edge_from c is" by (simp add: edge_at_def)
lemma snd_edge_at[simp]: "snd (edge_at c is) = edge_to c is" by (simp add: edge_at_def)


lemma hyps_exist':
  assumes "c  set conclusions"
  assumes "is  it_paths (it' c)"
  assumes "tree_at (it' c) is = (HNode i s ants)"
  shows "subst s (freshen i anyP)  hyps_along (it' c) is"
proof-
  from assms(1)
  have "plain_iwf (it' c) (fst (root (ts c)))" by (rule iwf_it)
  moreover
  note assms(2,3)
  moreover
  have "fst (fst (root (ts c))) |⊆| ass_forms"
    by (simp add: assms(1) ts_context)
  ultimately
  show ?thesis by (rule iwf_hyps_exist)
qed


definition hyp_edge_to :: "'form  nat list => ('form vertex × ('form,'var) in_port)" where
  "hyp_edge_to c is = ((c, 0 # is),  plain_ant anyP)"

(* TODO: Replace n and s by "subst s (freshen n anyP)" *)
definition hyp_edge_from :: "'form  nat list => nat  'subst  ('form vertex × ('form,'var) out_port)" where
  "hyp_edge_from c is n s = 
    ((c, 0 # hyp_port_path_for (it' c) is (subst s (freshen n anyP))),
     hyp_port_h_for (it' c) is (subst s (freshen n anyP)))"

definition hyp_edge_at  :: "'form  nat list => nat  'subst  ('form, 'var) edge''" where
  "hyp_edge_at c is n s = (hyp_edge_from c is n s, hyp_edge_to c is)"

lemma fst_hyp_edge_at[simp]:
  "fst (hyp_edge_at c is n s) = hyp_edge_from c is n s" by (simp add:hyp_edge_at_def) 
lemma snd_hyp_edge_at[simp]:
  "snd (hyp_edge_at c is n s) = hyp_edge_to c is" by (simp add:hyp_edge_at_def)

inductive_set edges where
  regular_edge: "c  set conclusions  is  it_paths (it' c)  edge_at c is  edges"
  | hyp_edge: "c  set conclusions  is  it_paths (it' c)  tree_at (it' c) is = HNode n s ants  hyp_edge_at c is n s  edges"

sublocale Pre_Port_Graph nodes inPorts outPorts vertices nodeOf edges.

lemma edge_from_valid_out_port:
  assumes "p  it_paths (it' c)"
  assumes "c  set conclusions"
  shows "valid_out_port (edge_from c p)"
using assms
by (auto simp add: edge_from_def intro: iwf_outPort iwf_it)

lemma edge_to_valid_in_port:
  assumes "p  it_paths (it' c)"
  assumes "c  set conclusions"
  shows "valid_in_port (edge_to c p)"
  using assms
  apply (auto simp add: edge_to_def inPorts_fset_of split: list.split elim!: it_paths_SnocE)
  apply (rule nth_mem)
  apply (drule (1) iwf_length_inPorts[OF iwf_it])
  apply auto
  done

lemma hyp_edge_from_valid_out_port:
  assumes "is  it_paths (it' c)"
  assumes "c  set conclusions"
  assumes "tree_at (it' c) is = HNode n s ants"
  shows "valid_out_port (hyp_edge_from c is n s)"
using assms
by(auto simp add: hyp_edge_from_def intro: hyp_port_outPort it_paths_strict_prefix hyp_port_strict_prefix hyps_exist')

lemma hyp_edge_to_valid_in_port:
  assumes "is  it_paths (it' c)"
  assumes "c  set conclusions"
  assumes "tree_at (it' c) is = HNode n s ants"
  shows "valid_in_port (hyp_edge_to c is)"
using assms by (auto simp add: hyp_edge_to_def)


inductive scope' :: "'form vertex  ('form,'var) in_port  'form × nat list  bool" where
  "c  set conclusions 
   is'  ((#) 0) ` it_paths (it' c) 
   prefix (is@[i]) is'  
   ip = in_port_at (c,is) i 
   scope' (c, is) ip (c, is')"

inductive_simps scope_simp: "scope' v i v'"
inductive_cases scope_cases: "scope' v i v'"

lemma scope_valid:
  "scope' v i v'  v' |∈| vertices"
by (auto elim: scope_cases)

lemma scope_valid_inport:
  "v' |∈| vertices  scope' v ip  v'  ( i. fst v = fst v'  prefix (snd v@[i]) (snd v')  ip = in_port_at v i)"
by (cases v; cases v')  (auto simp add: scope'.simps mem_vertices)

definition terminal_path_from :: "'form  nat list => ('form, 'var) edge'' list" where
   "terminal_path_from c is = map (edge_at c) (rev (prefixes is))"

lemma terminal_path_from_Nil[simp]:
  "terminal_path_from c [] = [edge_at c []]"
  by (simp add: terminal_path_from_def)

lemma terminal_path_from_Snoc[simp]:
  "terminal_path_from c (is @ [i]) = edge_at  c (is@[i]) # terminal_path_from c is"
  by (simp add: terminal_path_from_def)

lemma path_terminal_path_from:
  "c  set conclusions 
  is  it_paths (it' c) 
  path (c, 0 # is) (c, []) (terminal_path_from c is)"
by (induction "is" rule: rev_induct)
   (auto simp add: path_cons_simp intro!: regular_edge elim: it_paths_SnocE)

lemma edge_step:
  assumes "(((a, b), ba), ((aa, bb), bc))  edges"
  obtains 
    i where "a = aa" and "b = bb@[i]" and "bc = in_port_at (aa,bb) i"  and "hyps (nodeOf (a, b)) ba = None"
  | i where "a = aa" and "prefix (b@[i]) bb" and "hyps (nodeOf (a, b)) ba = Some (in_port_at (a,b) i)"
using assms
proof(cases rule: edges.cases[consumes 1, case_names Reg Hyp])
  case (Reg c "is")
  then obtain i where  "a = aa" and "b = bb@[i]" and "bc = in_port_at (aa,bb) i"  and "hyps (nodeOf (a, b)) ba = None"
    by (auto elim!: edges.cases simp add: edge_at_def edge_from_def edge_to_def split: list.split list.split_asm)
  thus thesis by (rule that)
next
  case (Hyp c "is" n s)
  let ?i = "hyp_port_i_for (it' c) is (subst s (freshen n anyP))"
  from Hyp have "a = aa" and "prefix (b@[?i]) bb" and
    "hyps (nodeOf (a, b)) ba = Some (in_port_at (a,b) ?i)"
  by (auto simp add: edge_at_def edge_from_def edge_to_def hyp_edge_at_def hyp_edge_to_def hyp_edge_from_def
      intro: hyp_port_prefix hyps_exist' hyp_port_hyps)
  thus thesis by (rule that)
qed

lemma path_has_prefixes:
  assumes "path v v' pth"
  assumes "snd v' = []"
  assumes "prefix (is' @ [i]) (snd v)"
  shows "((fst v, is'), (in_port_at (fst v, is') i))  snd ` set pth"
  using assms
  by (induction rule: path.induct)(auto elim!: edge_step dest: prefix_snocD)
  
lemma in_scope: "valid_in_port (v', p')  v  scope (v', p')  scope' v' p' v"
proof
  assume "v  scope (v', p')"
  hence "v |∈| vertices" and " pth t.  path v t pth  terminal_vertex t  (v', p')  snd ` set pth"
    by (auto simp add: scope.simps)
  from this
  show "scope' v' p' v"
  proof (induction  rule: vertices_induct)
    case (None c)
    from None(2)[of "(c, [])" "[]", simplified, OF None(1)]
    have False.
    thus "scope' v' p' (c, [])"..
  next
    case (Some c "is")

    from c  set conclusions is  it_paths (it' c)
    have "path (c, 0#is) (c, []) (terminal_path_from c is)"
      by (rule path_terminal_path_from)
    moreover
    from c  set conclusions
    have "terminal_vertex (c, [])" by simp
    ultimately
    have "(v', p')  snd ` set (terminal_path_from c is)"
      by (rule Some(3))
    hence "(v',p')  set (map (edge_to c) (prefixes is))"
      unfolding terminal_path_from_def by auto
    then obtain is' where "prefix is' is" and "(v',p') = edge_to c is'"
      by auto
    show "scope' v' p' (c, 0#is)"
    proof(cases "is'" rule: rev_cases)
      case Nil
      with (v',p') = edge_to c is'
      have "v' = (c, [])" and "p' = plain_ant c"
        by (auto simp add: edge_to_def)
      with c  set conclusions is  it_paths (it' c)
      show ?thesis  by (auto intro!: scope'.intros)
    next
      case (snoc is'' i)
      with (v',p') = edge_to c is'
      have "v' = (c, 0 # is'')" and "p' = in_port_at v' i"
        by (auto simp add: edge_to_def)
      with c  set conclusions is  it_paths (it' c) ‹prefix is' is[unfolded snoc]
      show ?thesis
        by (auto intro!: scope'.intros)
    qed
  qed
next
  assume "valid_in_port (v', p')"
  assume "scope' v' p' v"
  then obtain c is' i "is" where
    "v' = (c, is')" and "v = (c, is)" and "c  set conclusions" and
    "p' = in_port_at v' i" and
    "is  (#) 0 ` it_paths (it' c)" and  "prefix (is' @ [i]) is"
    by (auto simp add: scope'.simps)

  from ‹scope' v' p' v
  have "(c, is) |∈| vertices" unfolding v = _ by (rule scope_valid)
  hence "(c, is)  scope ((c, is'), p')"
  proof(rule scope.intros)
    fix pth t
    assume "path (c,is) t pth"
    
    assume "terminal_vertex t"
    hence "snd t = []" by auto

    from path_has_prefixes[OF ‹path (c,is) t pth ‹snd t = [], simplified, OF ‹prefix (is' @ [i]) is]
    show "((c, is'), p')  snd ` set pth" unfolding p' = _ v' = _.
  qed
  thus "v  scope (v', p')" using v =_ v' = _ by simp
qed

sublocale Port_Graph nodes inPorts outPorts vertices nodeOf edges
proof
  show "nodeOf ` fset vertices  sset nodes"
    apply (auto simp add: fmember.rep_eq[symmetric] mem_vertices)
    apply (auto simp add: stream.set_map dest: iNodeOf_tree_at[OF iwf_it])
    done
  next

  have " e  edges. valid_out_port (fst e)  valid_in_port (snd e)"
    by (auto elim!: edges.cases simp add: edge_at_def
        dest: edge_from_valid_out_port edge_to_valid_in_port
        dest: hyp_edge_from_valid_out_port hyp_edge_to_valid_in_port)
    
  thus "(ps1, ps2)edges. valid_out_port ps1  valid_in_port ps2" by auto
qed
  

sublocale Scoped_Graph nodes inPorts outPorts vertices nodeOf edges hyps..

lemma hyps_free_path_length:
  assumes "path v v' pth"
  assumes "hyps_free pth"
  shows "length pth + length (snd v') = length (snd v)"
using assms by induction (auto elim!: edge_step )

fun vidx :: "'form vertex  nat" where
   "vidx (c, [])   = isidx [fidx conc_forms c]"
  |"vidx (c, _#is) = iAnnot (tree_at (it' c) is)"

lemma my_vidx_inj: "inj_on vidx (fset vertices)"
  by (rule inj_onI)
     (auto simp add:  mem_vertices[unfolded fmember.rep_eq] iAnnot_globalize simp del: iAnnot.simps)

lemma vidx_not_v_away[simp]: "v |∈| vertices  vidx v  v_away"
  by (cases v rule:vidx.cases) (auto simp add: iAnnot_globalize  simp del: iAnnot.simps)

sublocale Instantiation inPorts outPorts nodeOf hyps  nodes edges vertices labelsIn labelsOut freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP vidx inst
proof
  show "inj_on vidx (fset vertices)" by (rule my_vidx_inj)
qed

sublocale  Well_Scoped_Graph nodes inPorts outPorts vertices nodeOf edges hyps
proof
  fix v1 p1 v2 p2 p'
  assume assms: "((v1, p1), (v2, p2))  edges" "hyps (nodeOf v1) p1 = Some p'"
  from assms(1) hyps_correct[OF assms(2)]
  have "valid_out_port (v1, p1)" and "valid_in_port (v2, p2)" and "valid_in_port (v1, p')" and "v2 |∈| vertices"
    using valid_edges by auto

  from assms
  have " i. fst v1 = fst v2  prefix (snd v1@[i]) (snd v2)  p' = in_port_at v1 i"
    by (cases v1; cases v2; auto elim!: edge_step)
  hence "scope' v1 p' v2"
    unfolding scope_valid_inport[OF v2 |∈| vertices›].
  hence "v2  scope (v1, p')"
    unfolding in_scope[OF ‹valid_in_port (v1, p')].
  thus "(v2, p2) = (v1, p')  v2  scope (v1, p')" ..
qed

sublocale Acyclic_Graph nodes inPorts outPorts vertices nodeOf edges hyps 
proof
  fix v pth
  assume "path v v pth" and "hyps_free pth"
  from hyps_free_path_length[OF this]
  show "pth = []" by simp
qed

sublocale Saturated_Graph nodes inPorts outPorts vertices nodeOf edges
proof
  fix v p
  assume "valid_in_port (v, p)"
  thus "eedges. snd e = (v, p)"
  proof(induction v)
    fix c cis
    assume "valid_in_port ((c, cis), p)"
    hence "c  set conclusions" by (auto simp add: mem_vertices)

    show "eedges. snd e = ((c, cis), p)"
    proof(cases cis)
      case Nil
      with ‹valid_in_port ((c, cis), p)
      have [simp]: "p = plain_ant c" by simp

      have "[]  it_paths (it' c)" by simp
      with c  set conclusions
      have "edge_at c []  edges" by (rule regular_edge)
      moreover
      have "snd (edge_at c []) = ((c, []), plain_ant c)"
        by (simp add: edge_to_def)
      ultimately
      show ?thesis by (auto simp add: Nil simp del: snd_edge_at)
    next
      case (Cons c' "is")
      with ‹valid_in_port ((c, cis), p)
      have [simp]: "c' = 0" and "is  it_paths (it' c)"
        and "p |∈| inPorts (iNodeOf (tree_at (it' c) is))" by auto
       
      from this(3) obtain i where
        "i < length (inPorts' (iNodeOf (tree_at (it' c) is)))" and
        "p = inPorts' (iNodeOf (tree_at (it' c) is)) ! i"
          by (auto simp add: inPorts_fset_of in_set_conv_nth)

      show ?thesis
      proof (cases "tree_at (it' c) is")
        case [simp]: (RNode r ants)
        show ?thesis
        proof(cases r)
          case I
          hence "¬ isHNode (tree_at (it' c) is)" by simp
          from iwf_length_inPorts_not_HNode[OF iwf_it[OF c  set conclusions]  is  it_paths (it' c) this]
               i < length (inPorts' (iNodeOf (tree_at (it' c) is)))
          have "i < length (children (tree_at (it' c) is))" by simp
          with is  it_paths (it' c)
          have "is@[i]  it_paths (it' c)" by (rule it_path_SnocI)
          from c  set conclusions this
          have "edge_at c (is@[i])  edges" by (rule regular_edge)
          moreover
          have "snd (edge_at c (is@[i])) = ((c, 0 # is),  inPorts' (iNodeOf (tree_at (it' c) is)) ! i)"
            by (simp add: edge_to_def)
          ultimately
          show ?thesis by (auto simp add: Cons p = _ simp del: snd_edge_at)
        next
          case (H n s)
          hence "tree_at (it' c) is = HNode n s ants" by simp
          from c  set conclusions is  it_paths (it' c)  this
          have "hyp_edge_at c is n s  edges"..
          moreover
          from H p |∈| inPorts (iNodeOf (tree_at (it' c) is))
          have [simp]: "p = plain_ant anyP" by simp
  
          have "snd (hyp_edge_at c is n s) = ((c, 0 # is), p)"
            by (simp add: hyp_edge_to_def)
          ultimately
          show ?thesis by (auto simp add: Cons simp del: snd_hyp_edge_at)
        qed
      qed
     qed
   qed
qed

sublocale Pruned_Port_Graph nodes inPorts outPorts vertices nodeOf edges
proof
  fix v 
  assume "v |∈| vertices"
  thus "pth v'. path v v' pth  terminal_vertex v'"
  proof(induct rule: vertices_induct)
    case (None c)
    hence "terminal_vertex (c,[])" by simp
    with path.intros(1)
    show ?case by blast
  next
    case (Some c "is")
    hence "path (c, 0 # is) (c, []) (terminal_path_from c is)"
      by (rule path_terminal_path_from)
    moreover
    have "terminal_vertex (c,[])" using Some(1) by simp
    ultimately
    show ?case by blast
  qed
qed

sublocale Well_Shaped_Graph  nodes inPorts outPorts vertices nodeOf edges hyps..

sublocale sol:Solution inPorts outPorts nodeOf hyps nodes vertices  labelsIn labelsOut freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP vidx inst edges
proof
  fix v1 p1 v2 p2
  assume "((v1, p1), (v2, p2))  edges"
  thus "labelAtOut v1 p1 = labelAtIn v2 p2"
  proof(cases rule:edges.cases)
    case (regular_edge c "is")
   
    from ((v1, p1), v2, p2) = edge_at c is
    have "(v1,p1) = edge_from c is" using fst_edge_at by (metis fst_conv)
    hence [simp]: "v1 = (c, 0 # is)" by (simp add: edge_from_def)

    show ?thesis
    proof(cases "is" rule:rev_cases)
      case Nil
      let "?t'" = "it' c"
      have "labelAtOut v1 p1 = subst (iSubst ?t') (freshen (vidx v1) (iOutPort ?t'))"
        using regular_edge Nil by (simp add: labelAtOut_def edge_at_def edge_from_def)
      also have "vidx v1 = iAnnot ?t'" by (simp add:  Nil)
      also have "subst (iSubst ?t') (freshen (iAnnot ?t') (iOutPort ?t')) = snd (fst (root (ts c)))"
        unfolding iwf_subst_freshen_outPort[OF iwf_it[OF c  set conclusions]]..
      also have " = c" using c  set conclusions by (simp add: ts_conc)
      also have " = labelAtIn v2 p2"
        using  c  set conclusions  regular_edge Nil
        by (simp add: labelAtIn_def edge_at_def freshen_closed conclusions_closed closed_no_lconsts)
      finally show ?thesis.
    next
      case (snoc is' i)
      let "?t1" = "tree_at (it' c) (is'@[i])"
      let "?t2" = "tree_at (it' c) is'"
      have "labelAtOut v1 p1 = subst (iSubst ?t1) (freshen (vidx v1) (iOutPort ?t1))"
        using regular_edge snoc by (simp add: labelAtOut_def edge_at_def edge_from_def)
      also have "vidx v1 = iAnnot ?t1" using snoc regular_edge(3) by simp
      also have "subst (iSubst ?t1) (freshen (iAnnot ?t1) (iOutPort ?t1))
          = subst (iSubst ?t2) (freshen (iAnnot ?t2) (a_conc (inPorts' (iNodeOf ?t2) ! i)))"
        by (rule iwf_edge_match[OF iwf_it[OF c  set conclusions] is  it_paths (it' c)[unfolded snoc]])
      also have "iAnnot ?t2 = vidx (c, 0 # is')" by simp
      also have "subst (iSubst ?t2) (freshen (vidx (c, 0 # is')) (a_conc (inPorts' (iNodeOf ?t2) ! i))) = labelAtIn v2 p2"
        using regular_edge snoc by (simp add: labelAtIn_def edge_at_def)
      finally show ?thesis.
  qed
  next
    case (hyp_edge c "is" n s ants)
    let ?f = "subst s (freshen n anyP)"
    let ?h = "hyp_port_h_for (it' c) is ?f"
    let ?his = "hyp_port_path_for (it' c) is ?f"
    let "?t1" = "tree_at (it' c) ?his"
    let "?t2" = "tree_at (it' c) is"

    from c  set conclusions is  it_paths (it' c) ‹tree_at (it' c) is = HNode n s ants
    have "?f  hyps_along (it' c) is"
      by (rule hyps_exist')

    from ((v1, p1), v2, p2) = hyp_edge_at c is n s
    have "(v1,p1) = hyp_edge_from c is n s" using fst_hyp_edge_at by (metis fst_conv)
    hence [simp]: "v1 = (c, 0 # ?his)" by (simp add: hyp_edge_from_def)


    have "labelAtOut v1 p1 = subst (iSubst ?t1) (freshen (vidx v1) (labelsOut (iNodeOf ?t1) ?h))"
      using hyp_edge by (simp add: hyp_edge_at_def hyp_edge_from_def labelAtOut_def)
    also have "vidx v1 = iAnnot ?t1" by simp
    also have "subst (iSubst ?t1) (freshen (iAnnot ?t1) (labelsOut (iNodeOf ?t1) ?h)) = ?f" using ?f  hyps_along (it' c) is by (rule local.hyp_port_eq[symmetric])
    also have " = subst (iSubst ?t2) (freshen (iAnnot ?t2) anyP)"  using hyp_edge by simp
    also have "subst (iSubst ?t2) (freshen (iAnnot ?t2) anyP) = labelAtIn v2 p2"
        using hyp_edge by (simp add: labelAtIn_def  hyp_edge_at_def hyp_edge_to_def)
    finally show ?thesis.
  qed
qed


lemma node_disjoint_fresh_vars:
  assumes "n  sset nodes"
  assumes "i < length (inPorts' n)"
  assumes "i' < length (inPorts' n)"
  shows "a_fresh (inPorts' n ! i)  a_fresh (inPorts' n ! i') = {}  i = i'"
  using assms no_multiple_local_consts
  by (fastforce simp add: nodes_def stream.set_map)

sublocale 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
proof
  fix v p var v'
  assume "valid_in_port (v, p)"
  hence "v |∈| vertices" by simp
  
  obtain c "is" where "v = (c,is)"  by (cases v, auto)

  from ‹valid_in_port (v, p) v= _
  have "(c,is) |∈| vertices"  and "p |∈| inPorts (nodeOf (c, is))"  by simp_all
  hence "c  set conclusions" by (simp add: mem_vertices)
  
  from p |∈| _ obtain i where
    "i < length (inPorts' (nodeOf (c, is)))" and
    "p = inPorts' (nodeOf (c, is)) ! i" by (auto simp add: inPorts_fset_of in_set_conv_nth)
  hence "p = in_port_at (c, is) i" by (cases "is") auto

  assume "v' |∈| vertices"
  then obtain c' is' where "v' = (c',is')" by (cases v', auto)

  assume "var  local_vars (nodeOf v) p"
  hence "var  a_fresh p" by simp

  assume "freshenLC (vidx v) var  subst_lconsts (inst v')"
  then obtain is'' where "is' = 0#is''" and "is''  it_paths (it' c')"
    using v' |∈| vertices›
    by (cases is') (auto simp add: v'=_)

  note freshenLC (vidx v) var  subst_lconsts (inst v')
  also
  have "subst_lconsts (inst v') = subst_lconsts (iSubst (tree_at (it' c') is''))"
    by (simp add: v'=_ is'=_)
  also
  from is''  it_paths (it' c')
  have "  fresh_at_path (it' c') is''  range (freshenLC v_away)"
    by (rule globalize_local_consts)
  finally
  have "freshenLC (vidx v) var  fresh_at_path (it' c') is''"
    using v |∈| vertices› by auto
  then obtain is''' where "prefix is''' is''"  and "freshenLC (vidx v) var  fresh_at (it' c') is'''"
    unfolding fresh_at_path_def by auto
  then obtain i' is'''' where "prefix (is''''@[i']) is''" 
      and "freshenLC (vidx v) var  fresh_at (it' c') (is''''@[i'])"
    using append_butlast_last_id[where xs = is''', symmetric]
    apply (cases "is''' = []")
    apply (auto simp del: fresh_at_snoc append_butlast_last_id)
    apply metis
    done

  from  is''  it_paths (it' c') ‹prefix (is''''@[i']) is''
  have "(is''''@[i'])  it_paths (it' c')" by (rule it_paths_prefix)
  hence "is''''  it_paths (it' c')" using append_prefixD it_paths_prefix by blast

  from this freshenLC (vidx v) var  fresh_at (it' c') (is''''@[i'])
  have "c = c'  is = 0 # is''''  var  a_fresh (inPorts' (iNodeOf (tree_at (it' c') is'''')) ! i')"
    unfolding fresh_at_def' using v |∈| vertices›  v' |∈| vertices›
    apply (cases "is")
    apply (auto split: if_splits simp add:  iAnnot_globalize it_paths_butlast v=_ v'=_ is'=_ simp del: iAnnot.simps)
    done
  hence "c' = c" and "is = 0 # is''''" and "var  a_fresh (inPorts' (iNodeOf (tree_at (it' c') is'''')) ! i')" by simp_all

  from (is''''@[i'])  it_paths (it' c')
  have "i' < length (inPorts' (nodeOf (c, is)))"
    using iwf_length_inPorts[OF iwf_it[OF c  set conclusions]]
    by (auto elim!: it_paths_SnocE simp add: is=_ c' = _ order.strict_trans2)

  have "nodeOf (c, is)  sset nodes"
    unfolding is = _ c' = _ nodeOf.simps
    by (rule iNodeOf_tree_at[OF iwf_it[OF c  set conclusions]  is''''  it_paths (it' c')[unfolded c' = _]])
    
  from var  a_fresh (inPorts' (iNodeOf (tree_at (it' c') is'''')) ! i')
       var  a_fresh p p = inPorts' (nodeOf (c, is)) ! i
       node_disjoint_fresh_vars[OF
          ‹nodeOf (c, is)  sset nodes›
          i < length (inPorts' (nodeOf (c, is))) i' < length (inPorts' (nodeOf (c, is)))]
  have "i' = i" by (auto simp add: is=_ c'=c)
   
  from  ‹prefix (is''''@[i']) is''
  have "prefix (is @ [i']) is'" by (simp add: is'=_ is=_)

 
  from c  set conclusions  is''  it_paths (it' c') ‹prefix (is @ [i']) is'
      p = in_port_at (c, is) i
  have "scope' v p v'"
  unfolding v=_ v'=_ c' = _ is' = _  i'=_ by (auto intro: scope'.intros)
  thus "v'  scope (v, p)" using ‹valid_in_port (v, p) by (simp add: in_scope)
qed

sublocale Scoped_Proof_Graph freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP  inPorts outPorts nodeOf hyps nodes vertices labelsIn labelsOut vidx inst edges local_vars..

(* interpretation of @{term Tasked_Proof_Graph} has to be named to avoid name clashes in @{term Abstract_Task}. *)
sublocale tpg:Tasked_Proof_Graph freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP antecedent consequent rules assumptions conclusions
  vertices nodeOf edges vidx inst
proof
  show "set (map Conclusion conclusions)  nodeOf ` fset vertices"
  proof-
  {
    fix c
    assume "c  set conclusions"
    hence "(c, []) |∈| vertices" by simp
    hence "nodeOf (c, [])  nodeOf ` fset vertices"
      unfolding fmember.rep_eq by (rule imageI)
    hence "Conclusion c  nodeOf ` fset vertices"  by simp
  } thus ?thesis by auto
  qed
qed  

end

end

Theory Incredible_Everything

(*<*)
theory Incredible_Everything
imports Incredible_Correctness Incredible_Completeness
begin

(* This file depends on all theory, to have a single entry point. *)

(* It can be used to pretty-print Isabelle output into the proof document.
   This is not used at the moment. *)

end
(*>*)

Theory Propositional_Formulas

theory Propositional_Formulas
imports
  Abstract_Formula
  "HOL-Library.Countable"
  "HOL-Library.Infinite_Set"
begin

class infinite =
  assumes infinite_UNIV: "infinite (UNIV::'a set)"

instance nat :: infinite
  by (intro_classes) simp
instance prod :: (infinite, type) infinite
  by intro_classes (simp add: finite_prod infinite_UNIV)
instance list :: (type) infinite
  by intro_classes (simp add: infinite_UNIV_listI)

lemma countable_infinite_ex_bij: "f::('a::{countable,infinite}'b::{countable,infinite}). bij f"
proof -
  have "infinite (range (to_nat::'a  nat))"
    using finite_imageD infinite_UNIV by blast
  moreover have "infinite (range (to_nat::'b  nat))"
    using finite_imageD infinite_UNIV by blast
  ultimately have "f. bij_betw f (range (to_nat::'a  nat)) (range (to_nat::'b  nat))"
    by (meson bij_betw_inv bij_betw_trans bij_enumerate)
  then obtain f where f_def: "bij_betw f (range (to_nat::'a  nat)) (range (to_nat::'b  nat))" ..
  then have f_range_trans: "f ` (range (to_nat::'a  nat)) = range (to_nat::'b  nat)"
    unfolding bij_betw_def by simp
  have "surj ((from_nat::nat  'b)  f  (to_nat::'a  nat))"
  proof (rule surjI)
    fix a
    obtain b where [simp]: "to_nat (a::'b) = b" by blast
    hence "b  range (to_nat::'b  nat)" by blast
    with f_range_trans have "b  f ` (range (to_nat::'a  nat))" by simp
    from imageE [OF this] obtain c where [simp]:"f c = b" and "c  range (to_nat::'a  nat)"
      by auto
    with f_def have [simp]: "inv_into (range (to_nat::'a  nat)) f b = c"
      by (meson bij_betw_def inv_into_f_f)
    then obtain d where cd: "from_nat c = (d::'a)" by blast
    with c  range to_nat› have [simp]:"to_nat d = c" by auto
    from ‹to_nat a = b have [simp]: "from_nat b = a"
      using from_nat_to_nat by blast
    show "(from_nat  f  to_nat) (((from_nat::nat  'a)  inv_into (range (to_nat::'a  nat)) f  (to_nat::'b  nat)) a) = a"
      by (clarsimp simp: cd)
  qed
  moreover have "inj ((from_nat::nat  'b)  f  (to_nat::'a  nat))"
    apply (rule injI)
    apply auto
    apply (metis bij_betw_inv_into_left f_def f_inv_into_f f_range_trans from_nat_def image_eqI rangeI to_nat_split)
    done
  ultimately show ?thesis by (blast intro: bijI)
qed
  

text ‹Propositional formulas are either a variable from an infinite but countable set,
  or a function given by a name and the arguments.›

datatype ('var,'cname) pform =
    Var "'var::{countable,infinite}"
  | Fun (name:'cname) (params: "('var,'cname) pform list")

text ‹Substitution on and closedness of propositional formulas is straight forward.›

fun subst :: "('var::{countable,infinite}  ('var,'cname) pform)  ('var,'cname) pform  ('var,'cname) pform"
  where "subst s (Var v) = s v"
  | "subst s (Fun n ps) = Fun n (map (subst s) ps)"

fun closed :: "('var::{countable,infinite},'cname) pform  bool"
  where "closed (Var v)  False"
  | "closed (Fun n ps)  list_all closed ps"

text ‹Now we can interpret @{term Abstract_Formulas}.
  As there are no locally fixed constants in propositional formulas, most of the locale parameters 
  are dummy values›

interpretation propositional: Abstract_Formulas
  ― ‹No need to freshen locally fixed constants›
  "curry (SOME f. bij f):: nat  'var  'var"
  ― ‹also no renaming needed as there are no locally fixed constants›
  "λ_. id" "λ_. {}"
  ― ‹closedness and substitution as defined above›
  "closed :: ('var::{countable,infinite},'cname) pform  bool" subst
  ― ‹no substitution and renaming of locally fixed constants›
  "λ_. {}" "λ_. id"
  ― ‹most generic formula›
  "Var undefined"
proof
  fix a v a' v'
  from countable_infinite_ex_bij obtain f where "bij (f::nat × 'var  'var)" by blast
  then show "(curry (SOME f. bij (f::nat × 'var  'var)) (a::nat) (v::'var) = curry (SOME f. bij f) (a'::nat) (v'::'var)) =
       (a = a'  v = v')"
  apply (rule someI2 [where Q="λf. curry f a v = curry f a' v'  a = a'  v = v'"])
  by auto (metis bij_pointE prod.inject)+
next
  fix f s
  assume "closed (f::('var, 'cname) pform)"
  then show "subst s f = f"
  proof (induction s f rule: subst.induct)
    case (2 s n ps)
    thus ?case by (induction ps) auto
  qed auto
next
  have "subst Var f = f" for f :: "('var,'cname) pform"
    by (induction f) (auto intro: map_idI)
  then show "s. (f. subst s (f::('var,'cname) pform) = f)  {} = {}"
    by (rule_tac x=Var in exI; clarsimp)
qed auto

declare propositional.subst_lconsts_empty_subst [simp del]

end

Theory Incredible_Propositional

theory Incredible_Propositional imports
  Abstract_Rules_To_Incredible
  Propositional_Formulas
begin

text ‹Our concrete interpretation with propositional logic will cover conjunction and implication
  as well as constant symbols. The type for variables will be @{typ string}.›

datatype prop_funs = "and" | imp | Const "string"

text ‹The rules are introduction and elimination of conjunction and implication.›
datatype prop_rule = andI | andE | impI | impE

definition prop_rules :: "prop_rule stream"
  where "prop_rules = cycle [andI, andE, impI, impE]"

lemma iR_prop_rules [simp]: "sset prop_rules = {andI, andE, impI, impE}"
  unfolding prop_rules_def by simp

text ‹Just some short notation.›
abbreviation X :: "(string,'a) pform"
  where "X  Var ''X''"
abbreviation Y :: "(string,'a) pform"
  where "Y  Var ''Y''"

text ‹Finally the right- and left-hand sides of the rules.›

fun consequent :: "prop_rule  (string, prop_funs) pform list"
  where "consequent andI = [Fun and [X, Y]]"
  | "consequent andE = [X, Y]"
  | "consequent impI = [Fun imp [X, Y]]"
  | "consequent impE = [Y]"

fun antecedent :: "prop_rule  ((string,prop_funs) pform,string) antecedent list"
  where "antecedent andI = [plain_ant X, plain_ant Y]"
  | "antecedent andE = [plain_ant (Fun and [X, Y])]"
  | "antecedent impI = [Antecedent {|X|} Y {}]"
  | "antecedent impE = [plain_ant (Fun imp [X, Y]), plain_ant X]"


interpretation propositional: Abstract_Rules
  "curry (SOME f. bij f):: nat  string  string"
  "λ_. id"
  "λ_. {}"
  "closed :: (string, prop_funs) pform  bool"
  subst
  "λ_. {}"
  "λ_. id"
  "Var undefined"
  antecedent
  consequent
  prop_rules
proof
  show "xssset prop_rules. consequent xs  []"
    unfolding prop_rules_def
    using consequent.elims by blast
next
  show "xssset prop_rules. ((λ_. {}) ` set (consequent xs)) = {}"
    by clarsimp
next
  fix i' r i ia
  assume "r  sset prop_rules"
    and "ia < length (antecedent r)"
    and "i' < length (antecedent r)"
  then show "a_fresh (antecedent r ! ia)  a_fresh (antecedent r ! i') = {}  ia = i'"
    by (cases i'; auto)
next
  fix p
  show "{}  ((λ_. {}) ` fset (a_hyps p))  a_fresh p"  by clarsimp
qed

end

Theory Incredible_Propositional_Tasks

theory Incredible_Propositional_Tasks
imports
  Incredible_Completeness
  Incredible_Propositional
begin

context ND_Rules_Inst begin
lemma eff_NatRuleI:
  "nat_rule rule c ants
     entail = (Γ  subst s (freshen a c))
     hyps = ((λant. ((λp. subst s (freshen a p)) |`| a_hyps ant |∪| Γ  subst s (freshen a (a_conc ant)))) |`| ants)
     ( ant f. ant |∈| ants  f |∈| Γ  freshenLC a ` (a_fresh ant)  lconsts f = {})
     ( ant. ant |∈| ants  freshenLC a ` (a_fresh ant)  subst_lconsts s = {})
     eff (NatRule rule) entail hyps"
  by (drule eff.intros(2)) simp_all
end

context Abstract_Task begin
lemma  natEff_InstI:
  "rule = (r,c)
   c  set (consequent r)
   antec = f_antecedent r
   natEff_Inst rule c antec"
  by (metis natEff_Inst.intros)
end

context begin

subsubsection ‹Task 1.1›

text ‹This is the very first task of the Incredible Proof Machine: @{term "A  A"}

abbreviation A :: "(string,prop_funs) pform"
  where "A  Fun (Const ''A'') []"

text ‹First the task is defined as an @{term Abstract_Task}.›

interpretation task1_1: Abstract_Task
  "curry (SOME f. bij f):: nat  string  string"
  "λ_. id"
  "λ_. {}"
  "closed :: (string, prop_funs) pform  bool"
  subst
  "λ_. {}"
  "λ_. id"
  "Var undefined"
  antecedent
  consequent
  prop_rules
  "[A]"
  "[A]"
by unfold_locales simp

text ‹Then we show, that this task has a proof within our formalization of natural deduction
  by giving a concrete proof tree.›

lemma "task1_1.solved"
  unfolding task1_1.solved_def
apply clarsimp
apply (rule_tac x="{|A|}" in exI)
apply clarsimp
apply (rule_tac x="Node ({|A|}  A, Axiom) {||}" in exI)
apply clarsimp
apply (rule conjI)
 apply (rule task1_1.wf)
   apply (solves clarsimp)
  apply clarsimp
  apply (rule task1_1.eff.intros(1))
  apply (solves simp)
 apply (solves clarsimp)
by (auto intro: tfinite.intros)


print_locale Vertex_Graph
interpretation task1_1: Vertex_Graph task1_1.nodes task1_1.inPorts task1_1.outPorts "{|0::nat,1|}"
  "undefined(0 := Assumption A, 1 := Conclusion A)"
.

print_locale Pre_Port_Graph
interpretation task1_1: Pre_Port_Graph task1_1.nodes task1_1.inPorts task1_1.outPorts "{|0::nat,1|}"
  "undefined(0 := Assumption A, 1 := Conclusion A)"
  "{((0,Reg A),(1,plain_ant A))}"
.

print_locale Instantiation
interpretation task1_1: Instantiation
  task1_1.inPorts
  task1_1.outPorts
  "undefined(0 := Assumption A, 1 := Conclusion A)"
  task1_1.hyps
  task1_1.nodes
  "{((0,Reg A),(1,plain_ant A))}"
  "{|0::nat,1|}"
  task1_1.labelsIn
  task1_1.labelsOut
  "curry (SOME f. bij f):: nat  string  string"
  "λ_. id"
  "λ_. {}"
  "closed :: (string, prop_funs) pform  bool"
  subst
  "λ_. {}"
  "λ_. id"
  "Var undefined"
  "id"
  "undefined"
by unfold_locales simp

declare One_nat_def [simp del]

lemma path_one_edge[simp]:
  "task1_1.path v1 v2 pth 
    (v1 = 0  v2 = 1  pth = [((0,Reg A),(1,plain_ant A))] 
    pth = []  v1 = v2)"
  apply (cases pth)
  apply (auto simp add: task1_1.path_cons_simp')
  apply (rename_tac list, case_tac list, auto simp add: task1_1.path_cons_simp')+
  done

text ‹Finally we can also show that there is a proof graph for this task.›

interpretation Tasked_Proof_Graph
  "curry (SOME f. bij f):: nat  string  string"
  "λ_. id"
  "λ_. {}"
  "closed :: (string, prop_funs) pform  bool"
  subst
  "λ_. {}"
  "λ_. id"
  "Var undefined"
  antecedent
  consequent
  prop_rules
  "[A]"
  "[A]"
  "{|0::nat,1|}"
  "undefined(0 := Assumption A, 1 := Conclusion A)"
  "{((0,Reg A),(1,plain_ant A))}"
  "id"
  "undefined"
apply unfold_locales
        apply (solves simp)
       apply (solves clarsimp)
      apply (solves clarsimp)
     apply (solves clarsimp)
    apply (solves fastforce)
   apply (solves fastforce)
  apply (solves clarsimp simp add: task1_1.labelAtOut_def task1_1.labelAtIn_def›)
 apply (solves clarsimp)
apply (solves clarsimp)
done

subsubsection ‹Task 2.11›

text ‹This is a slightly more interesting task as it involves both our connectives: @{term "P  Q  R  P  (Q  R)"}

abbreviation B :: "(string,prop_funs) pform"
  where "B  Fun (Const ''B'') []"
abbreviation C :: "(string,prop_funs) pform"
  where "C  Fun (Const ''C'') []"

interpretation task2_11: Abstract_Task
  "curry (SOME f. bij f):: nat  string  string"
  "λ_. id"
  "λ_. {}"
  "closed :: (string, prop_funs) pform  bool"
  subst
  "λ_. {}"
  "λ_. id"
  "Var undefined"
  antecedent
  consequent
  prop_rules
  "[Fun imp [Fun and [A,B],C]]"
  "[Fun imp [A,Fun imp [B,C]]]"
by unfold_locales simp_all

abbreviation "n_andI  task2_11.n_rules !! 0"
abbreviation "n_andE1  task2_11.n_rules !! 1"
abbreviation "n_andE2  task2_11.n_rules !! 2"
abbreviation "n_impI  task2_11.n_rules !! 3"
abbreviation "n_impE  task2_11.n_rules !! 4"

lemma n_andI [simp]: "n_andI = (andI, Fun and [X,Y])"
  unfolding task2_11.n_rules_def by (simp add: prop_rules_def)
lemma n_andE1 [simp]: "n_andE1 = (andE, X)"
  unfolding task2_11.n_rules_def One_nat_def by (simp add: prop_rules_def)
lemma n_andE2 [simp]: "n_andE2 = (andE, Y)"
  unfolding task2_11.n_rules_def numeral_2_eq_2 by (simp add: prop_rules_def)
lemma n_impI [simp]: "n_impI = (impI, Fun imp [X,Y])"
  unfolding task2_11.n_rules_def numeral_3_eq_3 by (simp add: prop_rules_def)
lemma n_impE [simp]: "n_impE = (impE, Y)"
proof -
  have "n_impE = task2_11.n_rules !! Suc 3" by simp
  also have "... = (impE, Y)"
  unfolding task2_11.n_rules_def numeral_3_eq_3 by (simp add: prop_rules_def)
  finally show ?thesis .
qed


lemma subst_Var_eq_id [simp]: "subst Var = id"
  by (rule ext) (induct_tac x; auto simp: map_idI)

lemma xy_update: "f = undefined(''X'' := x, ''Y'' := y)  x = f ''X''  y = f ''Y''" by force
lemma y_update: "f = undefined(''Y'':=y)  y = f ''Y''" by force

declare snth.simps(1) [simp del]

text ‹By interpreting @{term Solved_Task} we show that there is a proof tree for the task.
  We get the existence of the proof graph for free by using the completeness theorem.›

interpretation task2_11: Solved_Task
  "curry (SOME f. bij f):: nat  string  string"
  "λ_. id"
  "λ_. {}"
  "closed :: (string, prop_funs) pform  bool"
  subst
  "λ_. {}"
  "λ_. id"
  "Var undefined"
  antecedent
  consequent
  prop_rules
  "[Fun imp [Fun and [A,B],C]]"
  "[Fun imp [A,Fun imp [B,C]]]"
apply unfold_locales
  unfolding task2_11.solved_def
apply clarsimp
apply (rule_tac x="{|Fun imp [Fun and [A,B],C]|}" in exI)
apply clarsimp
― ‹The actual proof tree for this task.›
apply (rule_tac x="Node ({|Fun imp [Fun and [A, B], C]|}  Fun imp [A, Fun imp [B, C]],NatRule n_impI)
  {|Node ({|Fun imp [Fun and [A, B], C], A|}  Fun imp [B,C],NatRule n_impI)
    {|Node ({|Fun imp [Fun and [A, B], C], A, B|}  C,NatRule n_impE)
      {|Node ({|Fun imp [Fun and [A, B], C], A, B|}  Fun imp [Fun and [A,B], C],Axiom) {||},
        Node ({|Fun imp [Fun and [A, B], C], A, B|}  Fun and [A,B],NatRule n_andI) 
          {|Node ({|Fun imp [Fun and [A, B], C], A, B|}  A,Axiom) {||},
            Node ({|Fun imp [Fun and [A, B], C], A, B|}  B,Axiom) {||}
          |}
      |}
    |}
  |}" in exI)
apply clarsimp
apply (rule conjI)

 apply (rule task1_1.wf)
   apply (solves clarsimp; metis n_impI snth_smap snth_sset›)
  apply clarsimp
  apply (rule task1_1.eff_NatRuleI [unfolded propositional.freshen_def, simplified]) apply simp_all[4]
    apply (rule task2_11.natEff_InstI)
      apply (solves simp)
     apply (solves simp)
    apply (solves simp)
   apply (intro conjI; simp; rule xy_update)
   apply (solves simp)
  apply (solves fastforce simp: propositional.f_antecedent_def›)

 apply (rule task1_1.wf)
   apply (solves clarsimp; metis n_impI snth_smap snth_sset›)
  apply clarsimp
  apply (rule task1_1.eff_NatRuleI [unfolded propositional.freshen_def, simplified]) apply simp_all[4]
    apply (rule task2_11.natEff_InstI)
      apply (solves simp)
     apply (solves simp)
    apply (solves simp)
   apply (intro conjI; simp; rule xy_update)
   apply (solves simp)
  apply (solves fastforce simp: propositional.f_antecedent_def›)

 apply (rule task1_1.wf)
   apply (solves clarsimp; metis n_impE snth_smap snth_sset›)