nodup.thy

(* Isabelle 2014 *)

theory InjVec imports "~~/src/HOL/Hoare/Hoare_Logic" begin

theorem "(ALL i j. i < length b & j < length b & i ~= j --> b!i ~= b!j)
= (ALL i. 1 <= i & i < length b --> (ALL j. j < i --> b!i ~= b!j))"
apply(auto)
by (metis Suc_le_eq gr0_conv_Suc linorder_neqE_nat old.nat.exhaust)

theorem "(ALL i j. i < length b & j < length b & i ~= j --> b!i ~= b!j)
= (ALL i. i < length b --> (ALL j. j < i --> b!i ~= b!j))"
apply(auto)
by (metis Suc_le_eq gr0_conv_Suc linorder_neqE_nat old.nat.exhaust)

fun mem :: "'a => 'a list => bool" where
  "mem x [] = False"
| "mem x (y#ys) = (if x=y then True else mem x ys)"

fun nodup :: "'a list => bool" where
  "nodup [] = True"
| "nodup (x#xs) = (~(mem x xs) & nodup xs)"

lemma mem1 [simp]: "ALL i. i < length v --> mem (v!i) v"
apply(induct_tac v)
apply(auto)
apply(case_tac i)
apply(auto)
done

lemma mem2 [rule_format]:
  "ALL x. mem x v --> (EX i. i < length v & x = v!i)"
apply(induct_tac v)
apply(auto)
apply(drule_tac x="x" in spec)
apply(auto)
done

theorem "(nodup b)
 = (ALL i j. i < length b & j < length b & i ~= j --> b!i ~= b!j)"
apply(induct_tac b)
apply(auto)
apply(case_tac i)
apply(case_tac j)
apply(auto)
apply(case_tac j)
apply(auto)
apply(drule mem2)
apply(auto)
apply (metis Suc_less_eq2 nth_Cons_0 nth_Cons_Suc zero_less_Suc)
apply(drule mem2)
apply(auto)
apply (metis Suc_less_eq nth_Cons_0 nth_Cons_Suc zero_less_Suc)
apply(drule_tac x="Suc ia" in spec)
apply(drule_tac x="Suc ja" in spec)
apply(auto)
done

theorem "VARS i j
{True}
i := 0; j := 0;
WHILE i < length b & (j < i --> b!i ~= b!j)
INV {
i <= length b &
j <= i &
(ALL k. k < i --> (ALL m. m < k --> b!k ~= b!m)) &
(ALL m. m < j --> b!i ~= b!m)
}
DO 
  IF j=i THEN
    i := i + 1; j := 0
  ELSE
    j := j + 1
  FI
OD
{
i <= length b &
(i = length b --> (ALL i. i < length b --> (ALL j. j < i --> b!i ~= b!j))) &
(i < length b --> j < i & b!i = b!j)
}"
apply(vcg)
apply(auto)
apply (metis less_antisym)
by (metis less_Suc_eq)

end