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

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"
lemma hyps_for_simp'[simp]: "h ∈ fset (hyps_for n p) ⟷ hyps n h = Some p"
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: "((v⇩1,p⇩1),(v⇩2,p⇩2)) ∈ edges ⟹ hyps (nodeOf v⇩1) p⇩1 = Some p' ⟹ (v⇩2,p⇩2) = (v⇩1,p') ∨ v⇩2 ∈ scope (v⇩1,p')"

context Scoped_Graph
begin

definition hyps_free where
"hyps_free pth = (∀ v⇩1 p⇩1 v⇩2 p⇩2. ((v⇩1,p⇩1),(v⇩2,p⇩2)) ∈ set pth ⟶ hyps (nodeOf v⇩1) p⇩1 = None)"

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

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

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

inductive terminal_path where
terminal_path_empty: "terminal_vertex v ⟹ terminal_path v v []" |
terminal_path_cons: "((v⇩1,p⇩1),(v⇩2,p⇩2)) ∈ edges ⟹ terminal_path v⇩2 v' pth ⟹ hyps (nodeOf v⇩1) p⇩1 = None ⟹ terminal_path v⇩1 v' (((v⇩1,p⇩1),(v⇩2,p⇩2))#pth)"

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

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

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

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

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

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

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

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

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

from ‹(v',p') ∈ snd  set pth›
obtain pth1 pth2 e  where "pth = pth1@[e]@pth2" and "snd e = (v',p')" by (rule snd_set_split)
from terminal_path_is_path[OF assms(1), unfolded ‹pth = _ ›] ‹snd e = _›
have "path v v' (pth1@[e])" and "path v' t pth2" unfolding path_split by (auto simp add: edge_end_tup)

from ‹v' ∈ scope (v,p)› terminal_path_end_is_terminal[OF assms(1)] ‹path v' t pth2›
have "(v,p) ∈ snd  set pth2" by (rule scope_find)
then obtain pth2a e' pth2b  where "pth2 = pth2a@[e']@pth2b" and "snd e' = (v,p)"  by (rule snd_set_split)
from ‹path v' t pth2›[unfolded ‹pth2 = _ ›] ‹snd e' = _›
have "path v' v (pth2a@[e'])" and "path v t pth2b" unfolding path_split by (auto simp add: edge_end_tup)

from ‹path v v' (pth1@[e])› ‹path v' v (pth2a@[e'])›
have "path v v ((pth1@[e])@(pth2a@[e']))" by (rule path_appendI)
moreover
from terminal_path_is_hyps_free[OF assms(1)] ‹pth = _› ‹pth2 = _›
have "hyps_free ((pth1@[e])@(pth2a@[e']))" by (auto simp add: hyps_free_def)
ultimately
have "((pth1@[e])@(pth2a@[e'])) = []" by (rule hyps_free_acyclic)
thus False by simp
qed

end

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

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

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

locale Well_Shaped_Graph =  Well_Scoped_Graph + Acyclic_Graph + Saturated_Graph + Pruned_Port_Graph

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

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

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

locale Solution =
Instantiation _ _ _ _ _ edges for edges :: "(('vertex × 'outPort) × 'vertex × 'inPort) set" +
assumes solved: "((v⇩1,p⇩1),(v⇩2,p⇩2)) ∈ edges ⟹ labelAtOut v⇩1 p⇩1 = labelAtIn v⇩2 p⇩2"

locale Proof_Graph =  Well_Shaped_Graph + Solution

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

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

text ‹The following locale assembles all these conditions.›

locale Scoped_Proof_Graph =
Instantiation  inPorts outPorts nodeOf hyps nodes edges  vertices labelsIn labelsOut freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP vidx inst +
Well_Shaped_Graph  nodes inPorts outPorts vertices nodeOf edges hyps  +
Solution inPorts outPorts nodeOf hyps nodes vertices  labelsIn labelsOut freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP vidx inst edges +
Well_Scoped_Instantiation  freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP inPorts outPorts nodeOf hyps  nodes vertices labelsIn labelsOut vidx inst edges local_vars
for freshenLC :: "nat ⇒ 'var ⇒ 'var"
and renameLCs :: "('var ⇒ 'var) ⇒ 'form ⇒ 'form"
and lconsts :: "'form ⇒ 'var set"
and closed :: "'form ⇒ bool"
and subst :: "'subst ⇒ 'form ⇒ 'form"
and subst_lconsts :: "'subst ⇒ 'var set"
and subst_renameLCs :: "('var ⇒ 'var) ⇒ ('subst ⇒ 'subst)"
and anyP :: "'form"
and inPorts :: "'node ⇒ 'inPort fset"
and outPorts :: "'node ⇒ 'outPort fset"
and nodeOf :: "'vertex ⇒ 'node"
and hyps :: "'node ⇒ 'outPort ⇒ 'inPort option"
and nodes :: "'node stream"
and vertices :: "'vertex fset"
and labelsIn :: "'node ⇒ 'inPort ⇒ 'form"
and labelsOut :: "'node ⇒ 'outPort ⇒ 'form"
and vidx :: "'vertex ⇒ nat"
and inst :: "'vertex ⇒ 'subst"
and edges :: "('vertex, 'outPort, 'inPort) edge  set"
and local_vars :: "'node ⇒ 'inPort ⇒ 'var set"

end


Theory Abstract_Rules

theory Abstract_Rules
imports
Abstract_Formula
begin

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

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

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

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

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

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

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

locale Abstract_Rules =
Abstract_Formulas freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP
for freshenLC :: "nat ⇒ 'var ⇒ 'var"
and renameLCs  :: "('var ⇒ 'var) ⇒ ('form ⇒ 'form)"
and lconsts :: "'form ⇒ 'var set"
and closed :: "'form ⇒ bool"
and subst :: "'subst ⇒ 'form ⇒ 'form"
and subst_lconsts :: "'subst ⇒ 'var set"
and subst_renameLCs :: "('var ⇒ 'var) ⇒ ('subst ⇒ 'subst)"
and anyP :: "'form" +

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

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

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

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

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

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"

lemma mem_conc_forms[simp]: "a |∈| conc_forms ⟷ a ∈ set conclusions"

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))"

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.›

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›

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}.
›

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')"

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 = _›
ultimately
show ?thesis
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"
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'"
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)"
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: "((v⇩1,p⇩1),(v⇩2,p⇩2)) ∈ edges ⟹ hyps (nodeOf v⇩1) p⇩1 = None ⟹ forbidden_path v⇩1 pth ⟹ forbidden_path v⇩2 (((v⇩1,p⇩1),(v⇩2,p⇩2))##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')"
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 (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 (subst (asm) (2) forbidden_path.simps)
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)"

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"

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 [] = {}"

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 (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"

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)"
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'

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

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))"

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'"

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

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"

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

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)"

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)"

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

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"
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 []]"

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

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"
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"
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"
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"

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 v⇩1 p⇩1 v⇩2 p⇩2 p'
assume assms: "((v⇩1, p⇩1), (v⇩2, p⇩2)) ∈ edges" "hyps (nodeOf v⇩1) p⇩1 = Some p'"
from assms(1) hyps_correct[OF assms(2)]
have "valid_out_port (v⇩1, p⇩1)" and "valid_in_port (v⇩2, p⇩2)" and "valid_in_port (v⇩1, p')" and "v⇩2 |∈| vertices"
using valid_edges by auto

from assms
have "∃ i. fst v⇩1 = fst v⇩2 ∧ prefix (snd v⇩1@[i]) (snd v⇩2) ∧ p' = in_port_at v⇩1 i"
by (cases v⇩1; cases v⇩2; auto elim!: edge_step)
hence "scope' v⇩1 p' v⇩2"
unfolding scope_valid_inport[OF ‹v⇩2 |∈| vertices›].
hence "v⇩2 ∈ scope (v⇩1, p')"
unfolding in_scope[OF ‹valid_in_port (v⇩1, p')›].
thus "(v⇩2, p⇩2) = (v⇩1, p') ∨ v⇩2 ∈ scope (v⇩1, 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 "∃e∈edges. 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 "∃e∈edges. 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)"
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)"
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)"
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 v⇩1 p⇩1 v⇩2 p⇩2
assume "((v⇩1, p⇩1), (v⇩2, p⇩2)) ∈ edges"
thus "labelAtOut v⇩1 p⇩1 = labelAtIn v⇩2 p⇩2"
proof(cases rule:edges.cases)
case (regular_edge c "is")

from ‹((v⇩1, p⇩1), v⇩2, p⇩2) = edge_at c is›
have "(v⇩1,p⇩1) = edge_from c is" using fst_edge_at by (metis fst_conv)
hence [simp]: "v⇩1 = (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 v⇩1 p⇩1 = subst (iSubst ?t') (freshen (vidx v⇩1) (iOutPort ?t'))"
using regular_edge Nil by (simp add: labelAtOut_def edge_at_def edge_from_def)
also have "vidx v⇩1 = 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 v⇩2 p⇩2"
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 v⇩1 p⇩1 = subst (iSubst ?t1) (freshen (vidx v⇩1) (iOutPort ?t1))"
using regular_edge snoc by (simp add: labelAtOut_def edge_at_def edge_from_def)
also have "vidx v⇩1 = 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 v⇩2 p⇩2"
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 ‹((v⇩1, p⇩1), v⇩2, p⇩2) = hyp_edge_at c is n s›
have "(v⇩1,p⇩1) = hyp_edge_from c is n s" using fst_hyp_edge_at by (metis fst_conv)
hence [simp]: "v⇩1 = (c, 0 # ?his)" by (simp add: hyp_edge_from_def)

have "labelAtOut v⇩1 p⇩1 = subst (iSubst ?t1) (freshen (vidx v⇩1) (labelsOut (iNodeOf ?t1) ?h))"
using hyp_edge by (simp add: hyp_edge_at_def hyp_edge_from_def labelAtOut_def)
also have "vidx v⇩1 = 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 v⇩2 p⇩2"
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''))"
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

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 "∀xs∈sset prop_rules. consequent xs ≠ []"
unfolding prop_rules_def
using consequent.elims by blast
next
show "∀xs∈sset 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
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

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

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'') []"

"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.›

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 (solves clarsimp)
apply clarsimp
apply (solves simp)
apply (solves clarsimp)
by (auto intro: tfinite.intros)

print_locale Vertex_Graph
"undefined(0 := Assumption A, 1 := Conclusion A)"
.

print_locale Pre_Port_Graph
"undefined(0 := Assumption A, 1 := Conclusion A)"
"{((0,Reg A),(1,plain_ant A))}"
.

print_locale Instantiation
"undefined(0 := Assumption A, 1 := Conclusion A)"
"{((0,Reg A),(1,plain_ant A))}"
"{|0::nat,1|}"
"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]:
(v1 = 0 ∧ v2 = 1 ∧ pth = [((0,Reg A),(1,plain_ant A))] ∨
pth = [] ∧ v1 = v2)"
apply (cases pth)
done

text ‹Finally we can also show that there is a proof graph for this 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]"
"{|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)
apply (solves clarsimp)
done

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'') []"

"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])"
lemma n_andE1 [simp]: "n_andE1 = (andE, X)"
lemma n_andE2 [simp]: "n_andE2 = (andE, Y)"
lemma n_impI [simp]: "n_impI = (impI, Fun imp [X,Y])"
lemma n_impE [simp]: "n_impE = (impE, Y)"
proof -
have "n_impE = task2_11.n_rules !! Suc 3" by simp
also have "... = (impE, Y)"
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.›

"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
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 (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 (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 (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]