Theory attic

section‹Attic›
theory attic
imports Main "Lib/FiniteGraph"
begin

text‹old lemma, mainly unused.›

lemma exists_x1x2_x1notoffending_natLeq: 
  fixes 
    G::"'v graph" and
    f and
    p::"'v ⇒ nat"
  assumes
    "wf_graph G"
    "∃(e1, e2)∈(edges G). ¬ (p e1 ≤ p e2)" and
    "f ⊆ edges G ∧ (∀(e1, e2)∈f. ¬ p e1 ≤ p e2)" and
    "∀(e1, e2)∈(edges G) - f. p e1 ≤ p e2"
  shows "∃ x1 x2. (x1,x2)∈(edges G) ∧ (x1,x2)∈ f ∧ x1 ∈ fst ` f ∧ x1 ∉ snd ` f ∧ ((p x1) = Max (p`fst` f))"
proof -
   from assms have a2: "∃x∈(edges G). ¬ (case x of (e1, e2) ⇒ p e1 ≤ p e2)" by auto
   from assms have a3: "f ⊆(edges G) ∧ (∀(e1, e2)∈f. ¬ p e1 ≤ p e2)" by simp
   from assms have a4: "∀(e1, e2)∈(edges G) - f. p e1 ≤ p e2" by simp
   from assms(1) have finiteE: "finite (edges G)" using wf_graph.finiteE by fast
   from finiteE conjunct1[OF a3] have  finiteF: "finite f" by (metis rev_finite_subset)

   ― ‹Find a suitable x1, it is the Max of the firsts›
   from finiteF have x12: "∀ x ∈ f. Max (p`fst` f) ≥ p (fst x)" by (metis Max_ge finite_imageI image_eqI)
   from a2 a4 have x14: "∃ x1. (p x1) ∈ p`fst` f ∧ x1 ∈ fst` f" by fast
   from finiteF have "(p`fst` f) ≠ {} ⟹ Max (p`fst` f) ∈ (p`fst` f)" by simp
   hence x15: "Max (p`fst` f) ∈ (p`fst` f)" using x14 by fastforce
   hence "∃ x1. ((p x1) = Max (p`fst` f)) ∧ x1 ∈ fst` f" by force
   from this x14 obtain x1 where x1Cond: "((p x1) = Max (p`fst` f)) ∧ x1 ∈ fst` f" by blast
   
   ― ‹Thus x1 is not in the seconds, not offending›
   from x1Cond x15 have x1ImportantProp3: "(p x1) ∈ p`fst` f" by presburger
   from x1Cond conjunct2[OF a3] x12 have "∀(e1, e2) ∈ f. p x1 > p e2" by fastforce

   from x1Cond this a2 a3 a4 have x1ImportantProp1: "(p x1) ∉ p`snd` f" by force
   hence x1ImportantProp2: "x1 ∉ snd` f" by blast

   ― ‹Obtain x2›
   from x1ImportantProp3 x1Cond have x1ImportantProp4: "x1 ∈ fst` f" by presburger
   from this x1ImportantProp2 have  "∃ x1 x2. (x1,x2) ∈ f ∧ x1 ∉ snd` f" by fastforce
   from this x1Cond x1ImportantProp2 obtain x2 where x2Cond:"(x1,x2) ∈ f ∧ x1 ∉ snd` f" by force
   
   from a3 have "⋀ x. x ∈ f ⟹ x ∈ (edges G)" by blast
   from this x2Cond have x1x2Cond: "(x1,x2) ∈ (edges G)" by blast

   from x1x2Cond x2Cond x1Cond show ?thesis by auto
qed


lemma exCasePairSimp: "(∃x. x ∈ A ∧ (case x of (e1, e2) ⇒ P e1 e2)) = (∃(e1, e2) ∈ A. (P e1 e2))"
  by auto

lemma exCasePairNotSimp: "(∃x. x ∈ A ∧ ¬ (case x of (e1, e2) ⇒ P e1 e2)) = (∃(e1, e2) ∈ A. ¬ (P e1 e2))"
  by auto


(* moved here from FiniteGraph.thy. Currently unused *)
subsection ‹Paths›
  text ‹A path is represented by a list of adjacent edges.›
  type_synonym 'v path = "('v × 'v) list"

  context wf_graph
  begin
    text ‹The following predicate describes a valid path:›
    (* is-path src [src, ...., dst] dst *)
    fun is_path :: "'v ⇒ 'v path ⇒ 'v ⇒ bool" where
      "is_path v [] v' ⟷ v=v' ∧ v'∈V" |
      "is_path v ((v1,v2)#p) v' ⟷ v=v1 ∧ (v1,v2)∈E ∧ is_path v2 p v'"
  
    lemma is_path_simps[simp, intro!]:
      "is_path v [] v ⟷ v∈V"
      "is_path v [(v,v')] v' ⟷ (v,v')∈E"
      by (auto dest: E_wfD)
    
    lemma is_path_memb[simp]:
      "is_path v p v' ⟹ v∈V ∧ v'∈V"
      apply (induction p arbitrary: v) 
       apply (auto dest: E_wfD)
      done

    lemma is_path_split:
      "is_path v (p1@p2) v' ⟷ (∃u. is_path v p1 u ∧ is_path u p2 v')"
      by (induct p1 arbitrary: v) auto

    lemma is_path_split'[simp]: 
      "is_path v (p1@(u,u')#p2) v' 
        ⟷ is_path v p1 u ∧ (u,u')∈E ∧ is_path u' p2 v'"
      by (auto simp add: is_path_split)
  end

  text ‹Set of intermediate vertices of a path. These are all vertices but
    the last one. Note that, if the last vertex also occurs earlier on the path,
    it is contained in ‹int_vertices›.›
  definition int_vertices :: "'v path ⇒ 'v set" where
    "int_vertices p ≡ set (map fst p)"

  lemma int_vertices_simps[simp]:
    "int_vertices [] = {}"
    "int_vertices (vv#p) = insert (fst vv) (int_vertices p)"
    "int_vertices (p1@p2) = int_vertices p1 ∪ int_vertices p2"
    by (auto simp add: int_vertices_def)
  
  lemma (in wf_graph) int_vertices_subset: 
    "is_path v p v' ⟹ int_vertices p ⊆ V"
    apply (induct p arbitrary: v)
     apply (simp) 
    apply (force dest: E_wfD)
    done

  lemma int_vertices_empty[simp]: "int_vertices p = {} ⟷ p=[]"
    by (cases p) auto

subsubsection ‹Splitting Paths›
  text ‹Split a path at the point where it first leaves the set ‹W›:›
  lemma (in wf_graph) path_split_set:
    assumes "is_path v p v'" and "v∈W" and "v'∉W"
    obtains p1 p2 u w u' where
    "p=p1@(u,u')#p2" and
    "int_vertices p1 ⊆ W" and "u∈W" and "u'∉W"
    using assms
  proof (induct p arbitrary: v thesis)
    case Nil thus ?case by auto
  next
    case (Cons vv p)
    note [simp, intro!] = ‹v∈W› ‹v'∉W›
    from Cons.prems obtain u' where 
      [simp]: "vv=(v,u')" and
        REST: "is_path u' p v'"
      by (cases vv) auto
    
    txt ‹Distinguish wether the second node ‹u'› of the path is 
      in ‹W›. If yes, the proposition follows by the 
      induction hypothesis, otherwise it is straightforward, as
      the split takes place at the first edge of the path.›
    {
      assume A [simp, intro!]: "u'∈W"
      from Cons.hyps[OF _ REST] obtain p1 uu uu' p2 where
        "p=p1@(uu,uu')#p2" "int_vertices p1 ⊆ W" "uu ∈ W" "uu' ∉ W"
        by blast
      with Cons.prems(1)[of "vv#p1" uu uu' p2] have thesis by auto
    } moreover {
      assume "u'∉W"
      with Cons.prems(1)[of "[]" v u' p] have thesis by auto
    } ultimately show thesis by blast
  qed
  
  text ‹Split a path at the point where it first enters the set ‹W›:›
  lemma (in wf_graph) path_split_set':
    assumes "is_path v p v'" and "v'∈W"
    obtains p1 p2 u where
    "p=p1@p2" and
    "is_path v p1 u" and
    "is_path u p2 v'" and
    "int_vertices p1 ⊆ -W" and "u∈W"
    using assms
  proof (cases "v∈W")
    case True with that[of "[]" p] assms show ?thesis
      by auto
  next
    case False with assms that show ?thesis
    proof (induct p arbitrary: v thesis)
      case Nil thus ?case by auto
    next
      case (Cons vv p)
      note [simp, intro!] = ‹v'∈W› ‹v∉W›
      from Cons.prems obtain u' where 
        [simp]: "vv=(v,u')" and [simp]: "(v,u')∈E" and
          REST: "is_path u' p v'"
        by (cases vv) auto
    
      txt ‹Distinguish wether the second node ‹u'› of the path is 
        in ‹W›. If yes, the proposition is straightforward, otherwise,
        it follows by the induction hypothesis.
›
      {
        assume A [simp, intro!]: "u'∈W"
        from Cons.prems(3)[of "[vv]" p u'] REST have ?case by auto
      } moreover {
        assume [simp, intro!]: "u'∉W"
        from Cons.hyps[OF REST] obtain p1 p2 u'' where
          [simp]: "p=p1@p2" and 
            "is_path u' p1 u''" and 
            "is_path u'' p2 v'" and
            "int_vertices p1 ⊆ -W" and
            "u''∈W" by blast
        with Cons.prems(3)[of "vv#p1"] have ?case by auto
      } ultimately show ?case by blast
    qed
  qed

  text ‹Split a path at the point where a given vertex is first visited:›
  lemma (in wf_graph) path_split_vertex:
    assumes "is_path v p v'" and "u∈int_vertices p"
    obtains p1 p2 where
    "p=p1@p2" and
    "is_path v p1 u" and
    "u ∉ int_vertices p1"
    using assms
  proof (induct p arbitrary: v thesis)
    case Nil thus ?case by auto
  next
    case (Cons vv p)
    from Cons.prems obtain u' where 
      [simp]: "vv=(v,u')" "v∈V" "(v,u')∈E" and
        REST: "is_path u' p v'"
      by (cases vv) auto
    
    {
      assume "u=v"
      with Cons.prems(1)[of "[]" "vv#p"] have thesis by auto
    } moreover {
      assume [simp]: "u≠v"
      with Cons.hyps(1)[OF _ REST] Cons.prems(3) obtain p1 p2 where
        "p=p1@p2" "is_path u' p1 u" "u∉int_vertices p1"
        by auto
      with Cons.prems(1)[of "vv#p1" p2] have thesis
        by auto
    } ultimately show ?case by blast
  qed


end