Theory MinWeightBasis

theory MinWeightBasis
  imports "../../Sepreftime" "../../Refine_Foreach"
    "List-Index.List_Index" Matroids.Matroid     
begin
  
abbreviation "sorted_wrt_w w == sorted_wrt (λe1 e2. w e1 ≤ w e2)"
  
locale minWeightBasis = matroid carrier indep for carrier::"'a set" and indep  +
  fixes w :: "'a ⇒ 'b::{linorder, ordered_comm_monoid_add}"
begin
   
section ‹minWeightBasis algorithm›
   

subsection ‹Proof that it computes an minimum Basis›

definition minBasis where "minBasis B ≡ basis B ∧ (∀B'. basis B' ⟶ sum w B ≤ sum w B')"  
                                         
subsubsection ‹preparation›
     
fun in_sort_edge where
   "in_sort_edge x [] = [x]" 
 | "in_sort_edge x (y#ys) = (if w x ≤ w y then x#y#ys else y# in_sort_edge x ys)"  

lemma [simp]: "set (in_sort_edge x L) = insert x (set L)"
apply(induct L) by auto

lemma in_sort_edge: "sorted_wrt (λe1 e2. w e1 ≤ w e2) L ⟹ sorted_wrt (λe1 e2. w e1 ≤ w e2) (in_sort_edge x L)"
  apply(induct L ) by auto
   
lemma in_sort_edge_distinct: "x ∉ set L ⟹ distinct L ⟹ distinct (in_sort_edge x L)"    
apply(induct L) by auto 
    
lemma finite_sorted_edge_distinct:
  assumes "finite S" 
  obtains L where "distinct L" "sorted_wrt (λe1 e2. w e1 ≤ w e2) L" "S = set L"
proof -
  {
    have "∃L.  distinct L ∧ sorted_wrt (λe1 e2. w e1 ≤ w e2) L ∧ S = set L"
      using assms
      apply(induct S)
       apply(clarsimp)
      apply(clarsimp) 
      subgoal for x L apply(rule exI[where x="in_sort_edge x L"])
        by (auto simp: in_sort_edge in_sort_edge_distinct)
    done
  }
  with that show ?thesis by blast
qed    
    
abbreviation "wsorted == sorted_wrt_w w"
  
lemma sum_list_map_cons: "sum_list (map w (y # ys)) = w y + sum_list (map w ys)" by auto  
     
lemma exists_greater:
  assumes  len: "length F = length F'"
      and sum: "sum_list (map w F) > sum_list (map w F')"
    shows "∃i<length F. w (F ! i) > w (F' ! i)"
using len sum    
proof (induct rule: list_induct2) 
  case (Cons x xs y ys)    
  show ?case
  proof(cases "w y < w x")
    case True
    then show ?thesis by auto
  next
    case False
    from False Cons(3) have "sum_list (map w ys) < sum_list (map w xs)"
      apply(simp add: sum_list_map_cons) 
      by (meson add_mono leD le_less_linear)
    from Cons(2)[OF this] show ?thesis by auto
  qed
qed simp
 

  
lemma wsorted_Cons: "wsorted (x#xs) = (wsorted xs & (ALL y:set xs. w x <= w y))"
  by (induct xs arbitrary: x) auto 
  
   

lemma wsorted_nth_mono: assumes "wsorted L" "i≤j" "j<length L"
  shows "w (L!i) ≤ w (L!j)"
  using assms apply (induct L arbitrary: i j rule: list.induct) by (auto simp: nth_Cons' wsorted_Cons) 
 
(**
  limi T g is the set T restricted  
     to elements only with weight
    strictly smaller than g.
*)
definition "limi T g == {e. e∈T ∧ w e < g}"
  
lemma limi_subset: "limi T g ⊆ T" unfolding limi_def by auto  
  
lemma limi_mono: "A ⊆ B ⟹ limi A g ⊆ limi B g"
unfolding limi_def by auto


(*
  let F be a set of elements
  limi F g is the set F restricted to elements with weight smaller than g
  let E be a set of elements we want to exclude
    
  no_smallest_element_skipped E F says,
     that going greedyly over (carrier-E), every every element,
     that did not render the akkumulated set dependent, was added to the set F.
*)
definition "no_smallest_element_skipped E F = (∀e∈carrier - E. ∀g>w e. indep (insert e (limi F g)) ⟶ (e ∈ limi F g))"
  
lemma no_smallest_element_skipped_empty[simp]: "no_smallest_element_skipped carrier {}"
  by(auto simp: no_smallest_element_skipped_def)

lemma no_smallest_element_skippedD: "no_smallest_element_skipped E F ⟹ (⋀e g. e ∈carrier - E ⟹ w e < g ⟹ (indep (insert e (limi F g)) ⟹  e∈ limi F g))"
  by(auto simp: no_smallest_element_skipped_def)
 
subsubsection ‹the heart of the argument›


lemma greedy_approach_leads_to_minBasis: assumes "indep F"
  and "∀e∈carrier - F. ¬ indep (insert e F)"
  and "no_smallest_element_skipped {} F"
  shows "minBasis F"
proof (rule ccontr)
  ― ‹from our assumptions we have that F is a basis›  
  from assms have bF: "basis F" using indep_not_basis by blast
  ― ‹towards a contradiction, assume F is not a minimum Basis›
  assume notmin: "¬ minBasis F"    
  ― ‹then we can get a smaller Basis B›
  from bF notmin[unfolded minBasis_def] obtain B where bB: "basis B" and sum: "sum w B < sum w F"
    by force
  ― ‹lets us obtain two sorted lists for the bases F and B›
  from bF basis_finite finite_sorted_edge_distinct
    obtain FL where dF[simp]: "distinct FL" and wF[simp]: "wsorted FL" and sF[simp]: "F = set FL"
    by blast
  from bB basis_finite finite_sorted_edge_distinct
    obtain BL where dB[simp]: "distinct BL" and wB[simp]: "wsorted BL" and sB[simp]: "B = set BL"
      by blast
  ― ‹as basis F has more total weight than basis B ...›
  from sum have suml: "sum_list (map w BL) < sum_list (map w FL)"
    by(simp add: sum.distinct_set_conv_list[symmetric]) 
  from bB bF have "card B = card F"
    using basis_card by blast 
  then have l: "length FL = length BL"
    by (simp add: distinct_card) 
  ― ‹... there exists an index i such that the ith element of the BL is strictly smaller 
      than the ith element of FL ›
  from exists_greater[OF (*_ _ _ _*) l suml] obtain i where i: "i<length FL" and gr: "w (BL ! i) < w (FL ! i)"
    by auto
  let ?FL_restricted = "limi (set FL) (w (FL ! i))"

  ― ‹now let us look at the two independent sets X and Y:
        let X and Y be the set if we take the first i-1 elements of BL
         and the first i elements of FL respectively. 
      We want to use the augment property of Matroids in order to show that we must have skipped
      and optimal element, which then contradicts our assumption. ›
  let ?X = "take i FL"
  have X_size: "card (set ?X) = i" using i
    by (simp add: distinct_card)
  have X_indep: "indep (set ?X)" using bF
    using indep_iff_subset_basis set_take_subset by force

  let ?Y = "take (Suc i) BL"
  have Y_size: "card (set ?Y) = Suc i" using i l
    by (simp add: distinct_card)
  have Y_indep: "indep (set ?Y)" using bB
    using indep_iff_subset_basis set_take_subset by force 

  have "card (set ?X) < card (set ?Y)" using X_size Y_size by simp

  ― ‹X and Y are independent and X is smaller than Y, thus we can augment X with some element x›
  with Y_indep X_indep                                 
    obtain x where x: "x∈set (take (Suc i) BL) - set ?X" and indepX: "indep (insert x (set ?X))"
      using augment by auto

  ― ‹we know many things about x now, i.e. x weights strictly less than the ith element of FL ...›
  have "x∈carrier"  using indepX indep_subset_carrier by blast     
  from x have xs: "x∈set (take (Suc i) BL)" and xnX: "x ∉ set ?X" by auto
  from xs have "w x ≤ w (BL ! i)" using wB
    by (metis List.length_take Lists_Thms.nth_take Suc_leI Suc_le_mono dB distinct_Ex1 distinct_take i local.l min_Suc_gt(2) wsorted_nth_mono)
      (* FIXME *)
  then have k: "w x < w (FL ! i)" using gr by auto

  ― ‹... and that adding x to X gives us an independent set›
  have "?FL_restricted ⊆ set ?X"
    unfolding  limi_def apply auto
    by (smt dF i index_nth_id leD leI linorder_linear mem_Collect_eq set_conv_nth set_take_if_index wF wsorted_nth_mono) (* FIXME *) 
  have z': "insert x ?FL_restricted ⊆ insert x (set ?X)"
    using xnX `?FL_restricted ⊆ set (take i FL)` by auto 
  from indep_subset[OF indepX z'] have add_x_stay_indep: "indep (insert x ?FL_restricted)" .

  ― ‹... finally this means that we must have taken the element during our greedy algorithm›
  from `no_smallest_element_skipped {} F` `x∈carrier` `w x < w (FL ! i)` add_x_stay_indep
    have "x ∈ ?FL_restricted"  by (auto dest: no_smallest_element_skippedD)
  with `?FL_restricted ⊆ set ?X` have "x ∈ set ?X"  by auto

  ― ‹... but we actually didn't. This finishes our proof by contradiction.›  
  with xnX show "False" by auto              
qed

lemma assumes createsCycle: "¬ indep (insert e F)"
       and    I: "no_smallest_element_skipped (E∪{e}) F"
       and    sorted: "(∀x∈F.∀y∈(E∪{e}). w x ≤ w y)"
     shows I_preservation1': "no_smallest_element_skipped E F"
  unfolding no_smallest_element_skipped_def
proof (clarsimp)
  fix x g
  assume x: "x ∈ carrier"  "x ∉ E"  "w x < g"
  assume f: "indep (insert x (limi F g))" 
  show "(x ∈ limi F g)"  
  proof (cases "x=e")
    case True 
    from True have "limi F g = F"
      unfolding limi_def using ‹w x < g› sorted by fastforce  
    with createsCycle f True have "False" by auto  
    then show ?thesis by simp
  next
    case False
    show ?thesis 
    apply(rule I[THEN no_smallest_element_skippedD, OF _ ‹w x < g›])
    using x f False
    by (auto simp add: )
  qed
qed
 
lemma I_preservation2:       
    assumes "e ∈ E" "∀e∈carrier - E - F. ¬ indep (insert e F)"        
    shows  "(∀x∈carrier - (E - {e}) - insert e F. ¬ indep (insert x (insert e F)))"
using assms  by (smt Diff_insert Diff_insert2 indep_subset insert_Diff insert_commute subset_insertI)
 

lemma I_preservation3':
  assumes I: "no_smallest_element_skipped (E∪{e}) F"
  shows "no_smallest_element_skipped E (insert e F)"
  unfolding no_smallest_element_skipped_def
proof (clarsimp)
  fix x g
  assume xc: "x ∈ carrier"
  assume x: "x ∉ E"
  assume wx: "w x < g"
  assume f: "indep (insert x (limi (insert e F) g))"
  show "(x ∈ limi (insert e F) g)"
  proof(cases "x=e")
    case True   
    then show ?thesis unfolding limi_def
      using wx by blast 
  next
    case False
    have ind: "indep (insert x (limi F g))" apply(rule indep_subset[OF f]) using limi_mono by blast  
    have "indep (insert x (limi F g)) ⟹ x ∈ limi F g" 
      apply(rule I[THEN no_smallest_element_skippedD]) using False xc wx x by auto
    with ind show ?thesis using limi_mono by blast
  qed      
qed 
 
  
  
definition I_minWeightBasis_fine where
  "I_minWeightBasis_fine == λ(T,E). indep T 
                ∧ T ⊆ carrier
                 ∧ E ⊆ carrier  ∧ T ∩ E = {} 
                 ∧ (∀x∈T.∀y∈E. w x ≤ w y)
                ∧ (∀e∈carrier-E-T. ~indep (insert e T))
                 ∧ no_smallest_element_skipped E T"

lemma I_minWeightBasis_fineD: 
  assumes 
   "I_minWeightBasis_fine (T,E)"
 shows"indep T" "⋀e. e∈carrier-E-T ⟹ ~indep (insert e T)"
    "E ⊆ carrier" "⋀x y. x∈T ⟹ y∈E ⟹ w x ≤ w y" "T ∩ E = {}" "T ⊆ carrier"
    "no_smallest_element_skipped E T"
  using assms by(auto simp: no_smallest_element_skipped_def I_minWeightBasis_fine_def)

lemma I_minWeightBasis_fineI:
  assumes "indep T" "⋀e. e∈carrier-E-T ⟹ ~indep (insert e T)"
    "E ⊆ carrier" "⋀x y. x∈T ⟹ y∈E ⟹ w x ≤ w y" "T ∩ E = {}" "T ⊆ carrier"
    "no_smallest_element_skipped E T"
  shows "I_minWeightBasis_fine (T,E)"
  using assms by(auto simp: no_smallest_element_skipped_def I_minWeightBasis_fine_def)

lemma I_minWeightBasis_fineG: "I_minWeightBasis_fine (T,E) ⟹ no_smallest_element_skipped E T" by(auto simp: no_smallest_element_skipped_def I_minWeightBasis_fine_def)

lemma I_minWeightBasis_sorted: "I_minWeightBasis_fine (T,E) ⟹ (∀x∈T.∀y∈E. w x ≤ w y)" by(auto simp: no_smallest_element_skipped_def I_minWeightBasis_fine_def)
 
  
end

locale minWeightBasis_time = minWeightBasis +
  fixes sorted_carrier_time :: nat
    and  empty_basis_time indep_test_time insert_time :: nat
begin
subsection ‹Refinement to an algorithm using sorted lists› 

  definition (in -) "obtain_sorted_carrier_aux sct c w ≡ SPECT (emb (λL. sorted_wrt_w w L ∧ distinct L ∧ set L = c) sct)"

  abbreviation "obtain_sorted_carrier ≡ obtain_sorted_carrier_aux sorted_carrier_time carrier w"
      
section ‹minWeightBasis algorithm with nfoldi›

abbreviation "empty_basis ≡ {}"

 

definition (in -) minWeightBasis3_aux where 
  "minWeightBasis3_aux osc_t c we ebt itt it ind eb ≡ do {
        l ← obtain_sorted_carrier_aux osc_t c we ;
        ASSERT (set l = c);
        s ← SPECT [eb↦ebt];
        T ← nfoldli l (λ_. True)
        (λe T. do { 
            ASSERT (e∉T ∧ ind T ∧ e∈c ∧ T⊆c);
            b ← SPECT [ind (insert e T) ↦ itt];
            if b then
              SPECT [(insert e T)↦it]
            else 
              RETURNT T
        }) s;
        RETURNT T
      }"

abbreviation "minWeightBasis3 ≡ minWeightBasis3_aux sorted_carrier_time carrier w empty_basis_time
                                     indep_test_time insert_time indep empty_basis"



lemma I_minWeightBasis_fine_empty: "I_minWeightBasis_fine ({}, carrier)"
  by (auto simp: I_minWeightBasis_fine_def)

lemma I_minWeightBasis_fine_final: "I_minWeightBasis_fine (T, {}) ⟹ minBasis T"
  by(auto simp: greedy_approach_leads_to_minBasis I_minWeightBasis_fine_def)

lemma preservation_else: "set x = carrier ⟹
    x = l1 @ xa # l2 ⟹ I_minWeightBasis_fine (σ, set (xa # l2))
     ⟹ indep σ   ⟹ ¬ indep (insert xa σ) ⟹ I_minWeightBasis_fine (σ, set l2)"
  apply(rule I_minWeightBasis_fineI)
  subgoal by simp
  subgoal by (auto simp: DiffD2 I_minWeightBasis_fine_def)   
  subgoal by auto 
  subgoal by(auto simp: I_minWeightBasis_fine_def)   
  subgoal by(auto simp: I_minWeightBasis_fine_def)  
  subgoal by(auto simp: I_minWeightBasis_fine_def)  
  subgoal apply (rule I_preservation1')
    by(auto intro!:  simp: I_minWeightBasis_fine_def)  
  done

lemma I_preservation2':       
  assumes "e ∈ E" "∀e∈carrier - E - F. ¬ indep (insert e F)"        
    and "x∈carrier - (E - {e}) - insert e F"
    shows  "¬ indep (insert x (insert e F))"
  using assms I_preservation2 by auto

lemma preservation_if: "wsorted x ⟹ distinct x ⟹ set x = carrier ⟹
    x = l1 @ xa # l2 ⟹ I_minWeightBasis_fine (σ, set (xa # l2)) ⟹ True ⟹ xa ∉ σ  
   ⟹ xa ∈ carrier ⟹ indep (insert xa σ) ⟹ I_minWeightBasis_fine (insert xa σ, set l2)"
  apply(rule I_minWeightBasis_fineI)
  subgoal by simp      
  subgoal unfolding I_minWeightBasis_fine_def apply(rule I_preservation2'[where E="set (xa # l2)"]) 
    by simp_all 
  subgoal by auto        
  subgoal by (metis insert_iff list.set(2) I_minWeightBasis_sorted sorted_wrt_append wsorted_Cons)  
  subgoal by(auto simp: I_minWeightBasis_fine_def)  
  subgoal by(auto simp: I_minWeightBasis_fine_def)  
  subgoal apply (rule I_preservation3')
    by(auto intro!:  simp: I_minWeightBasis_fine_def)  
  done

definition "minBasis_time = sorted_carrier_time +  empty_basis_time
             +  card carrier * (indep_test_time + insert_time)"


lemma le_Id: "M ≤ M' ⟹ M ≤ ⇓ Id M'"
  by auto

theorem minWeightBasis3_refine: "minWeightBasis3 ≤ ⇓ Id (SPECT (emb minBasis minBasis_time))"
  unfolding minWeightBasis3_aux_def obtain_sorted_carrier_aux_def
  unfolding nfoldliIE_def[where E="indep_test_time + insert_time" and I="λl1 l2 s. I_minWeightBasis_fine (s,set l2)", symmetric]
  apply(rule le_Id)
  apply(rule T_specifies_I) 
  unfolding nfoldliIE'_def[symmetric]                      
  apply(vcg' ‹-› rules: nfoldliIE'_rule  )
  unfolding Some_le_emb'_conv
       apply (safe) 
  oops

lemmas f = nfoldliIE_rule[where  t="card carrier * (indep_test_time + insert_time)" and
                    P="λT. I_minWeightBasis_fine (T, {})", THEN T_specifies_rev, THEN T_conseq4]
theorem minWeightBasis3_refine: "minWeightBasis3 ≤ ⇓ Id (SPECT (emb minBasis minBasis_time))"
  unfolding minWeightBasis3_aux_def obtain_sorted_carrier_aux_def
  unfolding nfoldliIE_def[where E="indep_test_time + insert_time" and I="λl1 l2 s. I_minWeightBasis_fine (s,set l2)", symmetric]
  apply(rule le_Id)
    apply(rule T_specifies_I)             
  apply(vcg' ‹-› rules: f ) 

  subgoal by (auto simp: I_minWeightBasis_fine_empty) 
  subgoal (* loop body *)
    apply(rule T_specifies_I)
    apply(vcg' ‹-› rules: f ) 
      apply(simp_all add: Some_le_emb'_conv )

    subgoal apply(rule preservation_if) by (auto dest!: I_minWeightBasis_fineD(5))  
    subgoal apply(rule preservation_else) by (auto dest!: I_minWeightBasis_fineD(1))  

    (* asserts *)
    subgoal by (auto      simp: I_minWeightBasis_fine_def)  
    done
  subgoal by simp
  subgoal by simp

  subgoal by (auto  simp:  distinct_card Some_le_emb'_conv )
  subgoal by (auto  simp: I_minWeightBasis_fine_final minBasis_time_def vcg_simp_rules)
  subgoal by auto                      
  done
 



end
  
  
end