theory Incredible_Correctness imports Abstract_Rules_To_Incredible Natural_Deduction begin text ‹ In this theory, we prove that if we have a graph that proves a given abstract task (which is represented as the context @{term Tasked_Proof_Graph}), then we can prove @{term solved}. › context Tasked_Proof_Graph begin definition adjacentTo :: "'vertex ⇒ ('form, 'var) in_port ⇒ ('vertex × ('form, 'var) out_port)" where "adjacentTo v p = (SOME ps. (ps, (v,p)) ∈ edges)" fun isReg where "isReg v p = (case p of Hyp h c ⇒ False | Reg c ⇒ (case nodeOf v of Conclusion a ⇒ False | Assumption a ⇒ False | Rule r ⇒ True | Helper ⇒ True ))" fun toNatRule where "toNatRule v p = (case p of Hyp h c ⇒ Axiom | Reg c ⇒ (case nodeOf v of Conclusion a ⇒ Axiom ― ‹a lie› | Assumption a ⇒ Axiom | Rule r ⇒ NatRule (r,c) | Helper ⇒ Cut ))" inductive_set global_assms' :: "'var itself ⇒ 'form set" for i where "v |∈| vertices ⟹ nodeOf v = Assumption p ⟹ labelAtOut v (Reg p) ∈ global_assms' i" lemma finite_global_assms': "finite (global_assms' i)" proof- have "finite (fset vertices)" by (rule finite_fset) moreover have "global_assms' i ⊆ (λ v. case nodeOf v of Assumption p ⇒ labelAtOut v (Reg p)) ` fset vertices" by (force simp add: global_assms'.simps 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: ffUnion.rep_eq global_assms_simps) apply (metis image_iff snd_conv) done text ‹Here we build the natural deduction tree, by walking the graph.› primcorec tree :: "'vertex ⇒ ('form, 'var) in_port ⇒ ('vertex, 'form, 'var) edge' list ⇒ (('form entailment), ('rule × 'form) NatRule) dtree" where "root (tree v p pth) = ((hyps_along ((adjacentTo v p,(v,p))#pth) ⊢ labelAtIn v p), (case adjacentTo v p of (v', p') ⇒ toNatRule v' p' ))" | "cont (tree v p pth) = (case adjacentTo v p of (v', p') ⇒ (if isReg v' p' then ((λ p''. tree v' p'' ((adjacentTo v p,(v,p))#pth)) |`| inPorts (nodeOf v')) else {||} ))" lemma fst_root_tree[simp]: "fst (root (tree v p pth)) = (hyps_along ((adjacentTo v p,(v,p))#pth) ⊢ labelAtIn v p)" by simp lemma out_port_cases[consumes 1, case_names Assumption Hyp Rule Helper]: assumes "p |∈| outPorts n" obtains a where "n = Assumption a" and "p = Reg a" | r h c where "n = Rule r" and "p = Hyp h c" | r f where "n = Rule r" and "p = Reg f" | "n = Helper" and "p = Reg anyP" using assms by (atomize_elim, cases p; cases n) auto lemma hyps_for_fimage: "hyps_for (Rule r) x = (if x |∈| f_antecedent r then (λ f. Hyp f x) |`| (a_hyps x) else {||})" apply (rule fset_eqI) apply (rename_tac p') apply (case_tac p') apply (auto simp add: split: if_splits out_port.splits) done text ‹Now we prove that the thus produced tree is well-formed.› theorem wf_tree: assumes "valid_in_port (v,p)" assumes "terminal_path v t pth" shows "wf (tree v p pth)" using assms proof (coinduction arbitrary: v p pth) case (wf v p pth) let ?t = "tree v p pth" from saturated[OF wf(1)] obtain v' p' where e:"((v',p'),(v,p)) ∈ edges" and [simp]: "adjacentTo v p = (v',p')" by (auto simp add: adjacentTo_def, metis (no_types, lifting) eq_fst_iff tfl_some) let ?e = "((v',p'),(v,p))" let ?pth' = "?e#pth" let ?Γ = "hyps_along ?pth'" let ?l = "labelAtIn v p" from e valid_edges have "v' |∈| vertices" and "p' |∈| outPorts (nodeOf v')" by auto hence "nodeOf v' ∈ sset nodes" using valid_nodes by (meson image_eqI 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: ffUnion.rep_eq) hence "labelAtIn v p |∈| ?Γ" by (simp add: s[symmetric] Hyp) 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) 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:) 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) hence "freshenLC (vidx v') ` a_fresh ant ∩ freshenLC (vidx v'') ` lconsts (labelsOut (nodeOf v'') h'') = {}"by auto moreover have "lconsts f ⊆ lconsts (freshen (vidx v'') (labelsOut (nodeOf v'') h'')) ∪ subst_lconsts (inst v'') " using ‹f = _› by (simp add: labelAtOut_def fv_subst) ultimately show ?thesis by (fastforce simp add: lconsts_freshen) next case (Assumption v pf) hence "f = subst (inst v) (freshen (vidx v) pf)" by (simp add: labelAtOut_def) moreover from Assumption have "Assumption pf ∈ sset nodes" using valid_nodes by auto 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 ffUnion.rep_eq) finally have "eff (NatRule (r, f)) (?Γ, labelAtIn v p) ((λx. extra_assms (v',x) |∪| ?Γ ⊢ labelAtIn v' x) |`| f_antecedent r)". } moreover { fix x assume "x |∈| cont ?t" then obtain a where "x = tree v' a ?pth'" and "a |∈| f_antecedent r" by (auto simp add: Rule) note this(1) moreover from ‹v' |∈| vertices› ‹a |∈| f_antecedent r› have "valid_in_port (v',a)" by (simp add: Rule) moreover note ‹terminal_path v' t ?pth'› ultimately have "∃v p pth. x = tree v p pth ∧ valid_in_port (v,p) ∧ terminal_path v t pth" by blast } ultimately show ?thesis using Rule by (auto intro!: exI[where x = ?t] simp add: comp_def funion_assoc) next case Helper from Helper have "hyps (nodeOf v') p' = None" by simp with e ‹terminal_path v t pth› have "terminal_path v' t ?pth'".. have "labelAtIn v' (plain_ant anyP) = labelAtIn v p" unfolding s[symmetric] using Helper by (simp add: labelAtIn_def labelAtOut_def) moreover { fix x assume "x |∈| cont ?t" hence "x = tree v' (plain_ant anyP) ?pth'" by (auto simp add: Helper) note this(1) moreover from ‹v' |∈| vertices› have "valid_in_port (v',plain_ant anyP)" by (simp add: Helper) moreover note ‹terminal_path v' t ?pth'› ultimately have "∃v p pth. x = tree v p pth ∧ valid_in_port (v,p) ∧ terminal_path v t pth" by blast } ultimately show ?thesis using Helper by (auto intro!: exI[where x = ?t] simp add: comp_def funion_assoc ) qed qed lemma global_in_ass: "global_assms TYPE('var) |⊆| ass_forms" proof fix x assume "x |∈| global_assms TYPE('var)" then obtain v pf where "v |∈| vertices" and "nodeOf v = Assumption pf" and "x = labelAtOut v (Reg pf)" by (auto simp add: global_assms_simps) from this (1,2) valid_nodes have "Assumption pf ∈ sset nodes" by (auto simp add:) 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')" by (auto simp add: adjacentTo_def, metis (no_types, lifting) eq_fst_iff tfl_some) let ?e = "((v',p'),(v,p))" from e have "p' |∈| outPorts (nodeOf v')" using valid_edges by auto thus ?case proof(cases rule: out_port_cases) case Hyp with ‹t' |∈| cont (edge_tree v p)› have False by auto thus ?thesis.. next case Assumption with ‹t' |∈| cont (edge_tree v p)› have False by auto thus ?thesis.. next case (Rule r f) from ‹t' |∈| cont (edge_tree v p)› Rule obtain a where [simp]: "t' = edge_tree v' a" and "a |∈| f_antecedent r" by auto have "es = ?e ## ?es'" by (cases es rule: stream.exhaust_sel) simp moreover have "?e ∈ edges" using e by simp moreover from ‹p' = Reg f› ‹nodeOf v' = Rule r› have "hyps (nodeOf v') p' = None" by simp moreover from e valid_edges have "v' |∈| vertices" by auto with ‹nodeOf v' = Rule r› ‹a |∈| f_antecedent r› have "valid_in_port (v', a)" by simp moreover have "ipath (edge_tree v' a) ?es'" using ‹ipath t' _› by simp ultimately show ?thesis by metis next case Helper from ‹t' |∈| cont (edge_tree v p)› Helper have [simp]: "t' = edge_tree v' (plain_ant anyP)" by simp have "es = ?e ## ?es'" by (cases es rule: stream.exhaust_sel) simp moreover have "?e ∈ edges" using e by simp moreover from ‹p' = Reg anyP› ‹nodeOf v' = Helper› have "hyps (nodeOf v') p' = None" by simp moreover from e valid_edges have "v' |∈| vertices" by auto with ‹nodeOf v' = Helper› have "valid_in_port (v', plain_ant anyP)" by simp moreover have "ipath (edge_tree v' (plain_ant anyP)) ?es'" using ‹ipath t' _› by simp ultimately show ?thesis by metis qed qed lemma forbidden_path_prefix_is_path: assumes "forbidden_path v es" obtains v' where "path v' v (rev (stake n es))" using assms apply (atomize_elim) apply (induction n arbitrary: v es) apply simp apply (simp add: path_snoc) apply (subst (asm) (2) forbidden_path.simps) apply auto done lemma forbidden_path_prefix_is_hyp_free: assumes "forbidden_path v es" shows "hyps_free (rev (stake n es))" using assms apply (induction n arbitrary: v es) apply (simp add: hyps_free_def) apply (subst (asm) (2) forbidden_path.simps) apply (force simp add: hyps_free_def) done text ‹And now we prove that the tree is finite, which requires the above notion of a @{term forbidden_path}, i.e.\@ an infinite path.› theorem finite_tree: assumes "valid_in_port (v,p)" assumes "terminal_vertex v" shows "tfinite (tree v p pth)" proof(rule ccontr) let ?n = "Suc (fcard vertices)" assume "¬ tfinite (tree v p pth)" hence "¬ tfinite (edge_tree v p)" unfolding finite_tree_edge_tree. then obtain es :: "('vertex, 'form, 'var) edge' stream" where "ipath (edge_tree v p) es" using Konig by blast with ‹valid_in_port (v,p)› have "forbidden_path v es" by (rule path_is_forbidden) from forbidden_path_prefix_is_path[OF this] forbidden_path_prefix_is_hyp_free[OF this] obtain v' where "path v' v (rev (stake ?n es))" and "hyps_free (rev (stake ?n es))" by blast from this ‹terminal_vertex v› have "terminal_path v' v (rev (stake ?n es))" by (rule terminal_pathI) hence "length (rev (stake ?n es)) ≤ fcard vertices" by (rule hyps_free_limited) thus False by simp qed text ‹The main result of this theory.› theorem solved unfolding solved_def proof(intro ballI allI conjI impI) fix c assume "c |∈| conc_forms" hence "c ∈ set conclusions" by (auto simp add: conc_forms_def) from this(1) conclusions_present obtain v where "v |∈| vertices" and "nodeOf v = Conclusion c" by auto 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