Theory Incredible_Correctness

theory Incredible_Correctness
imports Abstract_Rules_To_Incredible Natural_Deduction
theory Incredible_Correctness
imports
  Abstract_Rules_To_Incredible
  Natural_Deduction
begin

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

context Tasked_Proof_Graph
begin

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

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

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


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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

      note `terminal_path v' t ?pth'`
      ultimately

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

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

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

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

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

      note `terminal_path v' t ?pth'`
      ultimately

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

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

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

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

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


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

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

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

  let ?es' = "stl es"

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

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

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

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

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

    have "?e ∈ edges" using e by simp
    moreover

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

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

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

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

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

    have "?e ∈ edges" using e by simp
    moreover

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

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

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

    show ?thesis by metis
  qed
qed

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

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


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

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

text ‹The main result of this theory.›

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

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

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

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

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

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

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

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

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

end

end