theory SelectionSort

imports String

begin


lemma 1:
"
[|
  (min_int <= 0) ;
  (0 < max_int) ;
  (min_int <= 0) ;
  (0 < max_int) ;
  (Max_Length > 0) ;
  is_initial min1 ;
  (length Q) <= Max_Length ;
  (length Q) ~= 0 ;
 Q = <min1> o Q1
|]
==>
(IsPermutation ((empty_string o Q1) o <min1>) Q)
"
apply auto
done

lemma 2:
"
[|
min_int <= 0 ;
(0 < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(is_initial(min1));
(length Q <= Max_Length);
length Q ~= 0;
Q = (<min1> o Q1)
|]
==>
IsASmallest (empty_string o <min1>) min1

"
apply auto
done


lemma 3:
"
[|
(min_int <= (0::int)) ;
((0::int) < max_int) ;
(min_int <= 0) ;
(0 < max_int) ;
(Max_Length > 0) ;
(is_initial min1);
(length Q) <= Max_Length;
(length Q) ~= 0 ;
Q = (<min2> o Q3);
IsPermutation ( temp1 o ( Q2 o <min1>)) Q;
IsASmallest (temp1 o <min1>) min1 ;
(length Q2) ~= 0 ;
Q2 = (<x1> o Q1) ;
x1 <= min1
|]
==>
(length temp1) < length Q
"
defer
apply auto
done


lemma 4:
"
[|
(min_int <= (0::int));
((0::int) < max_int) ;
(min_int <= 0);
(0 < max_int) ;
(Max_Length > 0);
is_initial min;
(length Q <= Max_Length);
length Q ~= 0;
Q = (<min2> o Q3);
IsPermutation ((temp1 o Q2) o <min1>) Q;
IsASmallest (temp1 o <min1>) min1;
(length Q2 ~= 0);
Q2 = (<x1> o Q1);
x1 <= min1
|]
==>
IsPermutation (((temp1 o <min1>) o Q1) o <x1>) Q
"
defer

apply auto
(* Case 1  *)
apply (unfold IsPermutation_def)
apply (auto)
apply (drule_tac x=x in spec) 
apply auto
done

lemma 5:
"
[|
(min_int <= (0::int));
((0::int) < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
is_initial min1;
(length Q <= Max_Length);
length Q ~= 0;
Q = (<min2> o Q3);
IsPermutation ((temp1 o Q2) o <min1>) Q;
IsASmallest (temp1 o <min1>) min1;
length Q2 ~= 0;
Q2 = (<x1> o Q1);
x1 <= min1
|]
==>
IsASmallest ((temp1 o <min1>) o <x1>) x1
"
apply auto
done

lemma 6:
"
[|
min_int <= 0;
(0 < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(is_initial min);
(length Q <= Max_Length);
length Q ~= 0;
Q = (<min2> o Q3);
(IsPermutation ((temp1 o Q2) o <min1>) Q);
(IsASmallest (temp1 o <min1>) min1);
length Q2 ~= 0;
Q2 = (<x1> o Q1);
x1 <= min1
|]
==>
(length Q1 < length Q2)

"
apply auto
(* apply (auto simp add: Stringleton1 JLength)*)
done


lemma 11:
"
[|
min_int <= 0;
(0 < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(is_initial min0);
(length Q <= Max_Length);
length Q ~= 0;
Q = (<min2> o Q3)
|]
==>
IsPermutation ((empty_string o Q3) o <min2>) Q
"
apply auto
(* apply (auto simp add: JPER2)*)
(*apply (auto simp add: JCat1)*)
done

lemma 12:
"
[|
min_int <= 0;
0 < max_int;
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(is_initial min0);
(length Q <= Max_Length);
length Q ~= 0;
Q = (<min2> o Q3)
|]
==>
IsASmallest (empty_string o <min2>) min2
"
apply auto
(*apply (simp only: JCat1)
apply (simp only: JSmallStringleton)*)
done


lemma 13:
"
[|
min_int <= 0;
(0 < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(is_initial min0);
length Q <= Max_Length;
length Q ~= 0;
Q = (<min2> o Q3);
(IsPermutation (temp1 o (Q2 o <min1>)) Q);
(IsASmallest (temp1 o <min1>) min1);
length Q2 ~= 0;
Q2 = (<x1> o Q1);
~(x1 <=  min1)
|]
==>
length temp1 < Max_Length
"
apply auto
(*apply (auto simp del: JPER4 CatProp3 dest: JPER41)*)

(*
apply (drule JPER41)
apply auto *)
done

lemma 14:
"
[|
min_int <= 0;
(0 < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(is_initial min0);
(length Q <= Max_Length);
length Q ~= 0;
Q = (<min2> o Q3);
(IsPermutation ((temp1 o Q2) o <min1>) Q);
(IsASmallest (temp1 o <min1>) min1);
length Q2 ~= 0;
Q2 = (<x1> o Q1);
~ x1 <=  min1
|]
==>
( IsPermutation (((temp1 o <x1>) o Q1) o <min1>) Q)
"
apply auto

(*apply (auto simp add: IsPermutation_def OccursCtProp1) *)
(*apply (drule_tac x=x in spec)
apply auto *)
done

lemma 15:
"
[|
(min_int <= (0::int));
((0::int) < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(is_initial min0);
(length Q <= Max_Length);
length Q ~= 0;
Q = (<min2> o Q3);
(IsPermutation ((temp1 o Q2) o <min1>) Q);
(IsASmallest (temp1 o <min1>) min1);
(length Q2 ~= 0);
Q2 = (<x1> o Q1);
~ x1 <=  min1
|]
==>
(IsASmallest ((temp1 o <x1>) o <min1>) min1)
"

apply auto
(*
apply (rule IsASmallestProp01)
apply auto
*)
done


lemma 16:
"
[|
(min_int <= 0);
(0 < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(is_initial min0);
length Q <= Max_Length;
length Q ~= 0;
Q = (<min2> o Q3);
(IsPermutation ((temp1 o Q2) o <min1>) Q);
(IsASmallest (temp1 o <min1>) min1);
(length Q2  ~= 0);
Q2 = (<x1> o Q1);
~(x1 <= min1)
|]
==>
(length Q1 < length Q2)
"
apply auto
(*apply (auto  simp add: Stringleton1 JLength)*)
done

lemma 21:
"
[|
(min_int <= 0);
(0 < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(is_initial min0);
length Q <= Max_Length;
length Q ~= 0;
Q = (<min2> o Q2);
(IsPermutation ((temp1 o Q1) o <min1>) Q);
(IsASmallest (temp1 o <min1>) min1);
length Q1 = 0
|]
==>
IsPermutation (temp1 o <min1>) Q
"
apply auto
(*apply clarify
apply (drule JLengthEmpty2)
apply (clarify)
apply (auto simp add: JCat1)*)
done

lemma 22:
"
[|
(min_int <= 0);
(0 < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(is_initial min0);
length Q <= Max_Length;
length Q ~= 0;
Q = (<min2> o Q2);
(IsPermutation ((temp1 o Q1) o <min1>) Q);
(IsASmallest (temp1 o <min1>) min1);
length Q1 = 0
|]
==>
(IsASmallest Q min1)
"

apply auto
(*
apply (simp only: JCat1)
apply (drule JLengthEmpty2)
apply (clarify)
apply (simp only: JCat2)
apply (simp only: JPER8)
*)
done

lemma 31:
"
[|
(min_int <= 0);
(0 < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(length Q <= Max_Length)
|]
==>
IsPermutation (Q o empty_string) Q
"
apply auto
(*
apply (simp only: JCat1 JCat2 JPER5)
*)
done

lemma 32:
"
[|
(min_int <= 0);
(0 < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(length Q <= Max_Length)
|]
==>
IsNondecreasing empty_string
"

apply auto
done

lemma 33:
"
[|
(min_int <= 0);
(0 < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(length Q <= Max_Length)
|]
==>
ALL y. (IsSubstring <y> Q) -->  (IsNondecreasing (empty_string o <y>))
"
apply auto
(* apply (auto simp add: IsNondecreasing.simps)*)
done

lemma 34:
"
[|
(min_int <= 0);
(0 < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(length Q <= Max_Length);
(IsPermutation (Q2 o sorted1) Q);
(IsNondecreasing sorted1);
(ALL y. (IsSubstring <y> Q2) --> (IsNondecreasing (sorted1 o <y>)));
(length Q2 ~= 0);
(IsPermutation (Q1 o <min1>) Q2);
IsASmallest Q2 min1
|]
==>
(length sorted1 < Max_Length)
"

apply auto
done

lemma 35:
"
[|
min_int <= 0;
(0 < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(length Q <= Max_Length);
(IsPermutation (Q2 o sorted1) Q);
(IsNondecreasing sorted1);

ALL y. IsSubstring <y> Q2 --> (IsNondecreasing (sorted1 o <y>));
(length Q2 ~= 0);
(IsPermutation(Q1 o <min1>) Q2);
IsASmallest Q2 min1
|]
==>
IsPermutation (Q1 o (sorted1 o <min1>)) Q
"
apply auto
(* Case 1 again *)
apply (unfold IsPermutation_def)
apply auto
apply (drule_tac x=x in spec)
apply (drule_tac x=x in spec)
apply (drule_tac x=x in spec)
apply auto
done

lemma 36:
"
[|
(min_int <= 0);
(0 < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(length Q <= Max_Length);
(IsPermutation (Q2 o sorted1) Q);
(IsNondecreasing sorted1);

ALL y. Is_SubString <y> Q2 --> (IsNondecreasing (sorted1 o <y>));
(length Q2 ~= 0);
(IsPermutation (Q1 o <min1>) Q2);
(IsASmallest Q2 min1)
|]
==>
IsNondecreasing (sorted1 o <min1>)
"
apply auto
done

lemma 37:
"
[|
min_int <= 0;
(0 < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(length Q <= Max_Length);
(IsPermutation (Q2 o sorted1) Q);
(IsNondecreasing sorted1);
ALL y. Is_SubString <y> Q2 --> (IsNondecreasing (sorted1 o <y>));
(length Q2 ~= 0);
(IsPermutation (Q1 o <min1>) Q2);
(IsASmallest Q2 min1)
|]
==>
ALL y. Is_SubString <y> Q1 --> (IsNondecreasing ((sorted1 o <min1>) o <y>))
"

apply auto
(* Case 2 *)
(* apply (rule ND4) *) (*Adding Cut to the ND4 rule fixes this*)
(* apply auto *)
done

lemma 38:
"
[|
min_int <= 0;
(0 < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(length Q <= Max_Length);
(IsPermutation (Q2 o sorted1) Q);
(IsNondecreasing sorted1);
ALL y. Is_SubString <y> Q2 --> (IsNondecreasing (sorted1 o <y>));
(length Q2 ~= 0);
(IsPermutation (Q1 o <min1>) Q2);
(IsASmallest Q2 min1)
|]
==>
(length Q1 < length Q2)
"
apply auto
done

lemma 41:
"
[|
(min_int <= 0);
(0 < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(length Q <= Max_Length);
(IsPermutation (Q1 o sorted1) Q);
IsNondecreasing sorted1;
ALL y. Is_SubString <y> Q1 --> IsNondecreasing (sorted1 o <y>);
length Q1 = 0
|]
==>
IsNondecreasing(sorted1)
"
apply auto
done

lemma 42:
"
[|
(min_int <= 0);
(0 < max_int);
(min_int <= 0);
(0 < max_int);
(Max_Length > 0);
(length Q <= Max_Length);
(IsPermutation (Q1 o sorted1) Q);
IsNondecreasing sorted1;
ALL y. Is_SubString <y> Q1 --> (IsNondecreasing (sorted1 o <y>));
length Q1 = 0
|]
==>
IsPermutation Q sorted1
"
apply auto
done

end