theory Recursive_Add_to_Realiz

imports Main

begin

lemma 1:
"
[| 
  ((min_int::int) <= 0);
  (0 < (max_int::int));
  (min_int <= (j::int));
  (j <= max_int) ;
  (min_int <= (i::int));
  (i <= max_int);
  (min_int <= (i + j));
  ((i + j) <= max_int);
  (j >= 0);
  P_val = abs(j);
  j ~= 0
  
|]
==>
(i + 1) <= max_int

"

apply auto
done

lemma 2:
"
[| 
  ((min_int::int) <= 0);
  (0 < (max_int::int));
  (min_int <= (j::int));
  (j <= max_int);
  (min_int <= (i::int));
  (i <= max_int);
  (min_int <= (i + j));
  ((i + j) <= max_int);
  (j >= 0);
  P_val = abs(j);
  j ~= 0

|]
==>
min_int <= (j - 1)
"
apply auto
done

lemma 3:
"
[| 
  ((min_int::int) <= 0);
  (0 < (max_int::int));
  (min_int <= (j::int));
  (j <= max_int);
  (min_int <= (i::int));
  (i <= max_int);
  (min_int <= (i + j));
  ((i + j) <= max_int);
  (j >= 0);
  P_val = abs(j);
  j ~= 0

|]
==>
(abs(j-(1::int))) < (abs(j))
"
apply auto
done

lemma 4:
"
[|  
  ((min_int::int) <= 0);
  (0 < (max_int::int));
  (min_int <= (j::int));
  (j <= max_int);
  (min_int <= (i::int));
  (i <= max_int);
  (min_int <= (i + j));
  ((i + j) <= max_int);
  (j >= 0);
  P_val = abs(j);
  j ~= 0
|]
==>
min_int <= ((i+(1::int)) + (j -(1::int))) 
"
apply auto
done

lemma 5:
"
[|  
  ((min_int::int) <= 0);
  (0 < (max_int::int));
  (min_int <= (j::int));
  (j <= max_int);
  (min_int <= (i::int));
  (i <= max_int);
  (min_int <= (i + j));
  ((i + j) <= max_int);
  (j >= 0);
  P_val = abs(j);
  j ~= 0
|]
==>
(((i + (1::int)) + (j - (1::int))) <= max_int)
"
apply auto
done

lemma 6:
"
[|  
  ((min_int::int) <= 0);
  (0 < (max_int::int));
  (min_int <= (j::int));
  (j <= max_int);
  (min_int <= (i::int));
  (i <= max_int);
  (min_int <= (i + j));
  ((i + j) <= max_int);
  (j >= 0);
  P_val = abs(j);
  j ~= 0
|]
==>
((j - (1::int)) >= 0)
"
apply auto
done

lemma 7:
"
[|  
  ((min_int::int) <= 0);
  (0 < (max_int::int));
  (min_int <= (j::int));
  (j <= max_int);
  (min_int <= (i::int));
  (i <= max_int);
  (min_int <= (i + j));
  ((i + j) <= max_int);
  (j >= 0);
  P_val = abs(j);
  j ~= 0
|]
==>
(( i + 1) + ( j - 1)) = (i +j)
"
apply auto
done

lemma 8:
"
[|  
  ((min_int::int) <= 0);
  (0 < (max_int::int));
  (min_int <= (j::int));
  (j <= max_int);
  (min_int <= (i::int));
  (i <= max_int);
  (min_int <= (i + j));
  ((i + j) <= max_int);
  (j >= 0);
  P_val = abs(j);
  j = 0
|]
==>
i = (i + j)
"
apply auto
done

end