theory SelectionSort

imports String Main

begin

lemma SelectionSort01:
"[| (((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & (EntryIsInitial & (( |Q|  <= Max_Length) &  |Q|  ~= 0))) & Q = (<min2> o Q3)) |] ==> (IsPermutation ((empty_string o Q3) o <min2>) Q)
"
apply (auto simp add: PerCon)
done

lemma SelectionSort02:
"
[| (((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & (EntryIsInitial(min) & (( |Q|  <= Max_Length) &  |Q|  ~= 0))) & Q = (<min2> o Q3)) |] ==> (IsPreceding <min2> empty_string)
"
apply (auto simp add: URT1)
done

lemma SelectionSort03:
"
[| ((((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & (EntryIsInitial(min) & (( |Q|  <= Max_Length) &  |Q|  ~= 0))) & Q = (<min2> o Q3)) & (((IsPermutation ((NewQ1 o Q2) o <min1>) Q) & (IsPreceding <min1> NewQ1)) & ( |Q2|  ~= 0 & (Q2 = (<E1> o Q1) & (LEQV E1 min1))))) |] ==> ( |NewQ1|  < Max_Length)
"

apply (auto dest!: PermCATSMT2)
apply (auto simp add: length_def)
done


lemma SelectionSort04:
"
[| ((((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & (EntryIsInitial(min) & (( |Q|  <= Max_Length) &  |Q|  ~= 0))) & Q = (<min2> o Q3)) & (((IsPermutation ((NewQ1 o Q2) o <min1>) Q) & (IsPreceding <min1> NewQ1)) & ( |Q2|  ~= 0 & (Q2 = (<E1> o Q1) & (LEQV E1 min1))))) |] ==> (IsPermutation (((NewQ1 o <min1>) o Q1) o <E1>) Q)
"
apply auto
(* Comutativity *)
apply (unfold IsPermutation_def)
apply (simp add: OCCat)
apply auto
apply (drule_tac x=x in spec)
apply auto
done

lemma SelectionSort05:
"
[| ((((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & (EntryIsInitial(min) & (( |Q|  <= Max_Length) &  |Q|  ~= 0))) & Q = (<min2> o Q3)) & (((IsPermutation ((NewQ1 o Q2) o <min1>) Q) & (IsPreceding <min1> NewQ1)) & ( |Q2|  ~= 0 & (Q2 = (<E1> o Q1) & (LEQV E1 min1))))) |] ==> (IsPreceding <E1> (NewQ1 o <min1>))
"

(* Stuck on URT(R,<x>,N) and R(y,x) ==> URT(R,<y>,N) *)

apply (auto intro!: JURT3hc simp add: SSExts intro: URTC3)
done

lemma SelectionSort06:
"
[| ((((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & (EntryIsInitial(min) & (( |Q|  <= Max_Length) &  |Q|  ~= 0))) & Q = (<min2> o Q3)) & (((IsPermutation ((NewQ1 o Q2) o <min1>) Q) & (IsPreceding <min1> NewQ1)) & ( |Q2|  ~= 0 & (Q2 = (<E1> o Q1) & (LEQV E1 min1))))) |] ==> ( |Q1|  <  |Q2| )
"
apply auto
done

lemma SelectionSort11:
"
[| (((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & (EntryIsInitial(min) & (( |Q|  <= Max_Length) &  |Q|  ~= 0))) & Q = (<min2> o Q3)) |] ==> (IsPermutation ((empty_string o Q3) o <min2>) Q)
"
apply (auto simp add: PerCon)
done

lemma SelectionSort12:
"
[| (((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & (EntryIsInitial(min) & (( |Q|  <= Max_Length) &  |Q|  ~= 0))) & Q = (<min2> o Q3)) |] ==> (IsPreceding <min2> empty_string)
"
apply (auto simp add: URT1)
done

lemma SelectionSort13:
"
[| ((((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & (EntryIsInitial(min) & (( |Q|  <= Max_Length) &  |Q|  ~= 0))) & Q = (<min2> o Q3)) & (((IsPermutation ((NewQ1 o Q2) o <min1>) Q) & (IsPreceding <min1> NewQ1)) & ( |Q2|  ~= 0 & (Q2 = (<E1> o Q1) & not((LEQV E1 min1)))))) |] ==> ( |NewQ1|  < Max_Length)
"

apply (erule conjE)+
apply (drule PerCom1)
apply (unfold CatProp3)
apply (drule PerComThree2)
apply (drule PermCATSMT2)
apply clarsimp
apply (simp only: length_def)
apply auto
done

lemma SelectionSort14:
"
[| ((((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & (EntryIsInitial(min) & (( |Q|  <= Max_Length) &  |Q|  ~= 0))) & Q = (<min2> o Q3)) & (((IsPermutation ((NewQ1 o Q2) o <min1>) Q) & (IsPreceding <min1> NewQ1)) & ( |Q2|  ~= 0 & (Q2 = (<E1> o Q1) & not((LEQV E1 min1)))))) |] ==> (IsPermutation (((NewQ1 o <E1>) o Q1) o <min1>) Q)
"
apply auto
done

lemma SelectionSort15:
"
[| ((((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & (EntryIsInitial(min) & (( |Q|  <= Max_Length) &  |Q|  ~= 0))) & Q = (<min2> o Q3)) & (((IsPermutation ((NewQ1 o Q2) o <min1>) Q) & (IsPreceding <min1> NewQ1)) & ( |Q2|  ~= 0 & (Q2 = (<E1> o Q1) & not((LEQV E1 min1)))))) |] ==> (IsPreceding <min1> (NewQ1 o <E1>)) 
"

apply (auto intro!: URT3b intro: URT4C4)
done

lemma SelectionSort16:
"
[| ((((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & (EntryIsInitial(min) & (( |Q|  <= Max_Length) &  |Q|  ~= 0))) & Q = (<min2> o Q3)) & (((IsPermutation ((NewQ1 o Q2) o <min1>) Q) & (IsPreceding <min1> NewQ1)) & ( |Q2|  ~= 0 & (Q2 = (<E1> o Q1) & not((LEQV E1 min1)))))) |] ==> ( |Q1|  <  |Q2| )
"
apply auto
done

lemma SelectionSort21:
"
[| (((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & (EntryIsInitial(min) & (( |Q|  <= Max_Length) &  |Q|  ~= 0))) & (Q = (<min2> o Q2) & (((IsPermutation ((NewQ1 o Q1) o <min1>) Q) & (IsPreceding <min1> NewQ1)) &  |Q1|  = 0))) |] ==> (IsPermutation (NewQ1 o <min1>) Q)
"

apply auto
done

lemma SelectionSort31:
"
[| ((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & ( |Q|  <= Max_Length)) |] ==> (IsPermutation (Q o empty_string) Q)
"
apply (auto simp add: PerReflect)
done

lemma SelectionSort32:
"
[| ((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & ( |Q|  <= Max_Length)) |] ==> (IsNonDecreasing empty_string)
"
apply (auto simp add: Con1)
done

lemma SelectionSort33:
"
[| ((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & ( |Q|  <= Max_Length)) |] ==> (IsPreceding empty_string Q)
"
apply (auto simp add: URT2)
done


lemma SelectionSort34:
"
[| (((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & ( |Q|  <= Max_Length)) & ((((IsPermutation (Q2 o sorted1) Q) & (IsNonDecreasing sorted1)) & (IsPreceding sorted1 Q2)) & ( |Q2|  ~= 0 & ((IsPermutation (Q1 o <min1>) Q2) & (IsPreceding <min1> Q1))))) |] ==> ( |sorted1|  < Max_Length)
"

apply (auto dest: PerCom1 PermCATSMT2)

apply (drule PermCATSMT2)
back
apply auto
apply (drule PerCom1)
apply (drule PermCATSMT2)
apply auto
done

lemma SelectionSort35:
"
[| (((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & ( |Q|  <= Max_Length)) & ((((IsPermutation (Q2 o sorted1) Q) & (IsNonDecreasing sorted1)) & (IsPreceding sorted1 Q2)) & ( |Q2|  ~= 0 & ((IsPermutation (Q1 o <min1>) Q2) & (IsPreceding <min1> Q1))))) |] ==> (IsPermutation (Q1 o (sorted1 o <min1>)) Q)
"

apply (auto dest: PerTransIn intro: PerComThree1)
done

lemma SelectionSort36:
"
[| (((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & ( |Q|  <= Max_Length)) & ((((IsPermutation (Q2 o sorted1) Q) & (IsNonDecreasing sorted1)) & (IsPreceding sorted1 Q2)) & ( |Q2|  ~= 0 & ((IsPermutation (Q1 o <min1>) Q2) & (IsPreceding <min1> Q1))))) |] ==> (IsNonDecreasing (sorted1 o <min1>))
"

apply (auto intro: Con8 URT5P2 PermSS SSCat3 dest: PerPer simp add: SSExts Con1P1)


apply (rule Con8)

apply auto
apply (simp add: Con1P1)
apply (drule PerPer)
back
apply (rule URT5P2)
apply auto

apply (rule PermSS)
apply auto
apply (rule SSCat3)
apply (auto simp add: SSExts)
done

lemma SelectionSort37:
"
[| (((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & ( |Q|  <= Max_Length)) & ((((IsPermutation (Q2 o sorted1) Q) & (IsNonDecreasing sorted1)) & (IsPreceding sorted1 Q2)) & ( |Q2|  ~= 0 & ((IsPermutation (Q1 o <min1>) Q2) & (IsPreceding <min1> Q1))))) |] ==> (IsPreceding (sorted1 o <min1>) Q1)
"

apply (auto intro: URT3 dest: PerPer USRT7P2 URT4C5)

apply (rule URT3)
apply auto
apply (drule PerPer)
back
apply (drule USRT7P2)
back
apply auto

apply (drule URT4C5)

apply auto
done

lemma SelectionSort38:
"
[| (((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & ( |Q|  <= Max_Length)) & ((((IsPermutation (Q2 o sorted1) Q) & (IsNonDecreasing sorted1)) & (IsPreceding sorted1 Q2)) & ( |Q2|  ~= 0 & ((IsPermutation (Q1 o <min1>) Q2) & (IsPreceding <min1> Q1))))) |] ==> ( |Q1|  <  |Q2| )
"

apply (auto dest: PermCATSMT)
done


lemma SelectionSort41:
"
[| ((((min_int <= 0) & (0 < max_int)) & (Max_Length > 0)) & (( |Q|  <= Max_Length) & ((((IsPermutation (Q1 o sorted1) Q) & (IsNonDecreasing sorted1)) & (IsPreceding sorted1 Q1)) &  |Q1|  = 0))) |] ==> (IsPermutation Q sorted1)
"
apply auto
done

end