(* Automatic proof of the Kraft-Chatin theorem in the interative theorem prover Isabelle (http://isabelle.in.tum.de/).
   
   Author:  Nicholas Hay (nickhay@cs.auckland.ac.nz)
   Date:  2007-2008

   Thanks to Jeremy Dawson for help with Isabelle, and to Prof. Cris Calude for many useful discussions. *)


ML "add_path \"$ISABELLE_HOME/src/HOL\""
ML "add_path \"$ISABELLE_HOME/src/HOL/Real\""

theory KraftChaitin
imports Rational
begin



(* ----------------------------------------------------------------------- *)
(* Formalise the algorithm which constructively establishes the kc theorem *)
(* ----------------------------------------------------------------------- *)

fun extend :: "nat list => nat => nat list list"
where
  "extend l 0 = [l]"
| "extend l (Suc n) = (hd (extend l n) @ [0]) # (hd (extend l n) @ [1]) # tl (extend l n)" 

consts kcstep :: "nat list list => nat list list => nat => (nat list list * nat list list)"
primrec
  "kcstep A [] n       = (A, [])"   (* fail case *)
  "kcstep A (f # F) n  = (if length f <= n 
                             then ((hd (extend f (n - length f))) # A, (tl (extend f (n - length f))) @ F)
                             else (fst (kcstep A F n), f # snd (kcstep A F n)))"

consts kcloop :: "nat list => (nat list list * nat list list) => (nat list list * nat list list)"
primrec
  "kcloop [] X = X"
  "kcloop (l#ls) X = (kcstep (fst (kcloop ls X)) (snd (kcloop ls X)) l)"

fun kc :: "nat list => nat list list"
where
	"kc ls = (fst (kcloop ls ([],[[]])))"



(* Define the measure of a prefix-free set *)

consts expn2 :: "nat => rat"
primrec
  "expn2 0 = 1"
  "expn2 (Suc n) = (1/2) * expn2 n"

consts meas :: "nat list list => rat"		(* The measure of a prefix free set *)
primrec
  "meas [] = 0"
  "meas (x # xs) = expn2 (length x) + meas xs"




(* Define prefix-free set (list) *)

fun prefixes :: "nat list => nat list => bool"
where
  "prefixes [] x = True"
| "prefixes x [] = True"
| "prefixes (x#xs) (y#ys) = ((x=y) & (prefixes xs ys))"

consts incomparable :: "nat list => nat list list => bool"
primrec
  "incomparable x [] = True"
  "incomparable x (y # ys) = (~(prefixes x y) & (incomparable x ys))"

consts prefixfree :: "nat list list => bool"
primrec
  "prefixfree [] = True"
  "prefixfree (x # xs) = ((incomparable x xs) & (prefixfree xs))"




(* Define the invariants that kcloop maintains *)

fun strictlysorted :: "nat list list => bool"
where
  "strictlysorted [] = True"
| "strictlysorted [x] = True"
| "strictlysorted (x1 # x2 # xs) = ((length x1 > length x2) & (strictlysorted (x2 # xs)))" 


fun inv1 :: "nat list list * nat list list => bool"
where
  "inv1 X = strictlysorted (snd X)"

fun inv2 :: "nat list list * nat list list => bool"
where
  "inv2 X = prefixfree ((fst X) @ (snd X))"

fun inv :: "nat list list * nat list list => bool"
where
  "inv X = ((inv1 X) & (inv2 X))"


(* --------------------------------------------------------------------------- *)
(* Given these invariants, we prove that kcstep preserves them unconditionally *)
(* --------------------------------------------------------------------------- *)

(* First, inv1:  sorting is preserved *)

lemma strictlysorted_reduce: "strictlysorted (f # F) ==> strictlysorted F"
apply(case_tac F, simp_all)
done

lemma extend_length1: "length (hd (extend f k)) = length f + k"
apply(induct k, simp_all) 
done

lemma extend_length2: "k>0 ==> length (hd (tl (extend f k) @ as)) = length f + k"
apply(case_tac k, simp_all add: extend_length1)
done

lemma kcstep_hdlen2 : "length(hd(snd(kcstep A (f # F) n))) = 
  (if length f = n then length(hd F) else (if length f <= n then n else (length f)))"

apply(simp add: extend_length2)
done

lemma lem8: "[|strictlysorted (f # F); strictlysorted (tl (extend f n) @ F) |] ==> strictlysorted ((hd (extend f n) @ [Suc 0]) # tl (extend f n) @ F)"
apply(induct n, simp_all) apply(induct F, simp_all)
done

lemma lem9: "strictlysorted (f # F) ==> strictlysorted (tl (extend f n) @ F)"
apply(induct n, simp_all add:lem8)
 apply(induct F, simp_all)
done

lemma strictlysorted_expand: "strictlysorted (f # F) = (if F = [] then True else ((length (hd F) < length f) & strictlysorted F))"
apply(case_tac F, simp_all)
done

lemma extend_zero: "(tl (extend aa k) = []) = (k = 0)"
apply(case_tac k, simp_all)
done

lemma lemm11b: "length f <= n ==> (tl (extend f (n - length f)) = []) = (length f = n)"
apply(simp only: extend_zero) apply(arith)
done

lemma lem11a: "(snd (kcstep A (f # F) n) = []) = (length f = n & F = [])"
apply(safe) apply(simp_all) apply(subgoal_tac "length f <= n | ~ length f <= n") apply(erule disjE) apply(simp)
apply(simp_all add: lemm11b)  apply(subgoal_tac "length f <= n | ~ length f <= n") apply(erule disjE) apply(simp_all)
done

lemma lem11: "[| ~F = []; ~ length f <= n; strictlysorted (f # F); strictlysorted (snd (kcstep A F n))|] ==> strictlysorted (f # snd (kcstep A F n))"
apply(case_tac F) apply(simp) apply(simp_all only: kcstep_hdlen2 strictlysorted_expand) apply(simp only: lem11a) apply(auto)
done

lemma strictlysorted_preserved: "strictlysorted F --> strictlysorted (snd (kcstep A F n))"
apply(induct F, simp) apply(safe)  apply(drule strictlysorted_reduce, simp) apply(simp)
apply(rule conjI) apply(simp add: lem9) apply(case_tac F, simp) apply(rule impI) apply(rule lem11, simp_all) 
done



theorem kcstep_inv1: "[|inv (A, F)|] ==> inv1 (kcstep A F n)"
apply(simp) apply(insert strictlysorted_preserved [of F A n]) apply(auto)
done





(* Prefix-free *)

lemma prefix2: "incomparable a (A @ f # F) = (~ (prefixes a f) & incomparable a (A @ F))"
  apply(induct A, auto)
done

lemma prefix3: "incomparable a (A @ B) = ((incomparable a A) & (incomparable a B))"
  apply(induct A, simp_all)
done

lemma prefix4: "prefixes a []"
  apply(induct a, simp_all)
done



lemma prefix5: "~ prefixes a b ==> ~ prefixes a (b@[c])"
  apply(induct a b rule: prefixes.induct) apply(simp_all)
done


lemma extend1: "extend f k = (hd (extend f k)) # (tl (extend f k))"
  apply(induct k, auto)
done

lemma extend1b: "(hd (extend f k)) # (tl (extend f k)) = (extend f k)"
  apply(induct k, auto)
done


lemma prefix6: "~ prefixes a f ==> incomparable a (extend f k)"
  apply(subst extend1) apply(induct k, simp_all add: prefix5)
done

lemma prefix7: "~ prefixes a f ==> ~ prefixes a (hd (extend f k)) & (incomparable a (tl (extend f k)))"
  apply(induct k, simp_all add: prefix5)
done


lemma prefix8: "incomparable a (A@F) ==> incomparable a ((fst (kcstep A F n)) @ (snd (kcstep A F n)))"
  apply(induct F) apply(simp_all add: prefix2 prefix3 prefix7) 
done

lemma prefix9 : "prefixes a b = prefixes b a"
  apply(induct a b rule: prefixes.induct) apply(simp_all add: prefix4) apply(auto)
done


lemma prefix5b: "~ prefixes a b ==> ~ prefixes (a@[c]) b"
  apply(simp add: prefix5 prefix9)
done

lemma prefix10: "prefixfree (a # b # A @ B) = prefixfree (b # a # A @ B)"
  apply(induct A, auto) apply(induct a, simp_all add: prefix9 )
done

lemma prefix10b: "prefixfree (a # b # A) = prefixfree (b # a # A)"
  apply(induct A, auto) apply(simp_all add: prefix9)
done

lemma prefix11: "(incomparable aa (A @ a # F)) = (incomparable aa (a # (A @ F)))"
  apply(induct A, auto)
done

lemma prefix12: "prefixfree (A @ a # F) = prefixfree (a # (A @ F))"
  apply(induct A) apply(simp)  apply(simp del: prefixfree.simps) apply(simp only:prefix10)
  apply(simp (no_asm_simp) only: prefixfree.simps prefix11)
done

lemma strictlysorted1: "strictlysorted (a # A) = (strictlysorted A & (if A ~= [] then (length a) > (length (hd A)) else True))"
  apply(induct A, auto)
done

lemma prefix13: "(prefixfree (a # A)) ==> (prefixfree ((a @ [0]) # (a @ [1]) # A))"
  apply (induct A) apply(simp) apply(induct a, simp, simp) apply(simp) apply(simp add: prefix5b) 
done


lemma prefix14: "[|incomparable a A; prefixfree A |] ==> (prefixfree ((extend a k) @ A))"
  apply(induct k) apply(simp) apply(simp del: prefixfree.simps) apply(subst (asm) extend1) apply(simp del: prefixfree.simps) apply(drule prefix13) apply(simp)
done

lemma prefix15a: "(incomparable a (B@A@C)) = (incomparable a (A@B@C))"
  apply(induct A, simp_all) apply(subst prefix11) apply(auto)
done

lemma prefix15b: "(prefixfree (B@A@C)) = (prefixfree (A@B@C))"
  apply(induct A, simp_all) apply(subst prefix12) apply(simp add:prefix15a)
done


lemma prefix16: "prefixfree ((a#A)@B@C) ==> prefixfree (a#B@A@C)"
  apply(simp add: prefix3) apply(simp add: prefix15b)
done


theorem kcstep_inv2: "[|inv (A, F)|] ==> inv2 (kcstep A F n)"
	apply(simp)
	apply(induct F) apply(simp) apply(simp only: prefix12) apply(simp only: prefixfree.simps)
	apply(simp del: prefixfree.simps add: strictlysorted1)
	apply(rule conjI)
	apply(rule impI) apply(rule prefix16) apply(subst extend1b) apply(simp add: prefix14)
	apply(subst prefix12) apply(simp add: prefix8)
done



(* -------------------------------------- *)
(*            Measure invariant           *)
(* -------------------------------------- *)


(* 1.  Establish if our free space has an element of length <= n, then Kraft-chaitin can allocate a string of length n *)


lemma meas3: "expn2 (length (hd (extend a k))) + meas (tl (extend a k)) = meas (extend a k)"
  apply(induct a) apply(induct k, simp_all)
  apply(induct k, simp_all)
done

lemma meas4: "meas (extend (b # x) k) * 2 = meas (extend x k)"
  apply(induct k,simp_all add: meas3)
done

lemma meas_extend: "meas (extend a k) = expn2 (length a)"
  apply(induct a)
  apply(simp_all add: meas4)
  apply(induct k, simp_all add: meas3)
done

lemma meas6: "meas (A @ B) = (meas A) + (meas B)"
  apply(induct A, simp_all)
done

lemma meas7: "expn2 (length (hd (extend a k))) + meas (A @ tl (extend a k) @ F) = meas(A @ a # F)"
  apply(induct A) apply(simp_all) apply(induct k) apply(simp_all)
done

lemma meas8: "meas (A @ a # F) = expn2(length a) + meas A + meas F"
  apply(induct A, simp_all)
done


(* Harder case when we actually allocate*)
lemma kcstep_meas: "meas ((fst (kcstep A F n)) @ (snd (kcstep A F n))) = meas (A@F)"
  apply(induct F) apply(simp_all) apply(rule conjI) apply(simp add: meas7) apply(simp add: meas6 meas8)
done



(* Correctness of the kcloop inner loop:  if there is enough remaining measure we succeed in allocating a string of the requested length. *)
(* To prove this we will need some lemmas about how the measure of prefix-free sets behave, combining this with our old result *)


consts nrange :: "nat => nat => rat"
primrec
  "nrange 0 m = 0"
  "nrange (Suc n) m = (nrange n m) + (if m <= n then expn2 (Suc n) else 0)"

consts interp ::"nat list list => rat"
recdef interp "measure length"
  "interp [] = 0"
  "interp [x] = expn2 (length x)"
  "interp (x1#x2#xs) = nrange (length x1) (length x2) +  interp (x2#xs)"


lemma measb1: "0 <= expn2 n"
apply(induct n, simp_all)
done

lemma measb1b: "0 < expn2 n"
apply(induct n, simp_all)
done


(* need two for ease of simplication *)
lemma rat1: "[| a <= (b::rat); 0 <= (d::rat) |] ==> a <= b + d"
apply(simp_all)
done

lemma rat2: "[| a <= (b::rat); c <= (d::rat) |] ==> a + c <= b + d"
apply(simp_all)
done


lemma measb2: "0 <= nrange m n"
apply(induct m, simp_all add: measb1 rat1)
done

lemma measb3: "0 < k ==>  expn2 (length x1 + k) <= nrange (length x1 + k) (length x1)"
apply(induct k, simp_all del: expn2.simps) apply(case_tac k, simp add:measb2) apply(simp del: expn2.simps)
apply(erule rat1) apply(simp add: measb1)
done

lemma measb4: "length x2 < length x1 ==>  expn2 (length x1) <= nrange (length x1) (length x2)"
apply(insert measb3 [of "length x1 - length x2" x2], simp_all add: measb3)
done

lemma measb5: "strictlysorted A ==> meas A <= interp A"
apply(induct A rule: interp.induct) apply(simp_all add: measb4 rat2)
done

lemma measb6: "[| n <= m |] ==> nrange n m = 0"
apply(induct n, simp_all)
done

lemma measb7: "[| a <= b |] ==> nrange (b+k) b + nrange b a = nrange (b+k) a"
apply(induct k, simp_all add: measb6)
done

lemma measb8: "[| a <= b; b <= c |] ==> nrange c b + nrange b a = nrange c a"
apply(insert measb7 [of a b "c-b"], simp_all)
done

lemma lem2: "strictlysorted (a # as) ==> strictlysorted as"
apply(case_tac as, simp_all)
done

lemma lem10: "strictlysorted (a # A) = (if A = [] then True else ((length (hd A) < length a) & strictlysorted A))"
apply(case_tac A, simp_all)
done


lemma invlem1: "[| strictlysorted A; A ~= [] |] ==> length (last A) <= length (hd A)"
apply(induct A, simp_all) apply(rule impI) apply(simp add: lem2 lem10) 
done

lemma invlem2: "[| strictlysorted (x#xs); xs ~= [] |] ==> length (last xs) <= length x"
apply(insert invlem1 [of "x#xs"]) apply(simp)
done

lemma measb9: "[| strictlysorted A; A ~= []|] ==> interp A = nrange (length (hd A)) (length (last A)) + expn2 (length (last A))"
apply(induct A rule: interp.induct) apply(simp) apply(simp_all add: measb6)
apply(rule impI) apply(rule measb8) apply(simp_all add: invlem2)
done

lemma measb10: "nrange (n+k) n + expn2 (n + k) = expn2 n"
apply(induct k, simp_all add: measb6)
done

lemma measb11: "nrange (Suc n + k) (Suc n) + expn2 (Suc n) = nrange (Suc n + k) n"
apply(induct k, simp add: measb6) apply(simp del: expn2.simps)
done

lemma rat3: "[| (a::rat) + c = b; 0 < c  |] ==> a < b"
apply(simp)
done

lemma measb12: "nrange (Suc n + k) (Suc n) + expn2 (Suc n) < expn2 n"
apply(simp only: measb11) apply(insert measb10 [of "n" "Suc k"]) apply(drule rat3)
apply(simp_all add: measb1b)
done

lemma rat5: "[| (a::rat) <= b ; b < c |] ==> a < c"
apply(simp)
done

declare expn2.simps [simp del]		(* Bad form? *)

lemma add1: "(a::nat) <= b ==> b = a + (b-a)"
apply(simp)
done

lemma measb15: "[| strictlysorted A; A ~= []; length (last A) = Suc n |] ==> meas A < expn2 n"
apply(insert measb5 [of A], simp) apply(erule rat5)
apply(simp add: measb9) apply(insert invlem1 [of A]) apply(simp) apply(subst add1 [of "Suc n"]) apply(simp)
apply(rule measb12)
done

lemma expn2_1: "expn2 k <= 1"
apply(induct k) apply(simp_all add: expn2.simps)
done

lemma expn2_2: "expn2 (n+k) <= expn2 n"
apply(induct n) apply(simp_all add: expn2_1 expn2.simps)
done

lemma measb16: "[| strictlysorted A; A ~= []; length (last A) = Suc n + k |] ==> meas A < expn2 n"
apply(simp) apply(insert measb15 [of A "n+k"], simp)
apply(insert expn2_2 [of n k]) apply(simp)
done


lemma add2: "(a::nat) < b ==> (Suc a <= b)"
apply(simp)
done


lemma measb17: "[| A ~= []; n < length (last A); strictlysorted A |] ==> meas A < expn2 n"
apply(drule add2 [of n "length(last A)"]) apply(drule add1) apply(simp add: measb16) 
done


(* contrapositive of above *)
lemma meas13: "[| ~ meas A < expn2 n; A ~= []; strictlysorted A |] ==> ~ n < length (last A)"
apply(erule contrapos_nn) 
apply(simp add: measb17)
done


lemma add3: "[| (a::nat) <= b; b < a |] ==> False"
apply(arith)
done



theorem meas_alloc: "[| expn2 n <= meas F; strictlysorted F |] ==> length (last F) <= n"
apply(case_tac F) apply(insert measb1b [of n]) apply(simp add: add3) 
apply(insert meas13 [of F n]) apply(auto)
done


(* It really seems like there should be a shorter proof of the above *)


lemma kcstep2: "[|F~=[]; (length (last F)) <= n|] ==> (tl (fst (kcstep A F n)) = A)"
  apply(induct F, auto) apply(split split_if_asm) apply(auto)
done 

lemma kcstep3: "[|F~=[]; (length (last F)) <= n|] ==> (length (hd (fst (kcstep A F n))) = n)"
  apply(induct F, auto) apply(simp add: extend_length1) apply(split split_if_asm, simp_all)
done

lemma kcstep3b: "[|F~=[]; (length (last F)) <= n|] ==> fst (kcstep A F n) ~= []"
  apply(induct F, auto) apply(split split_if_asm, simp_all)
done

lemma kcstep4: "[|F~=[]; (length (last F)) <= n|] ==> meas (fst (kcstep A F n)) = meas A + expn2 n"
  apply(induct F, auto) apply(simp add: extend_length1) apply(split split_if_asm, simp_all)
done

lemma nonzero_meas: "expn2 n <= meas F ==> F ~= []"
  apply(case_tac F) apply(insert measb1b [of n]) apply(auto)
done


lemma kcstep_correct1: "[|inv (A, F); expn2 n <= meas F|] ==> (tl (fst (kcstep A F n)) = A) & (length (hd (fst (kcstep A F n))) = n)"
  apply(simp)  apply(frule meas_alloc, simp) apply(frule nonzero_meas) 
  apply(simp add: kcstep2 kcstep3)
done

lemma kcstep_correct1b: "[|inv (A, F); expn2 n <= meas F|] ==> fst (kcstep A F n) ~= []"
  apply(simp)  apply(frule meas_alloc, simp) apply(frule nonzero_meas) 
  apply(simp add: kcstep3b)
done


lemma kcstep_correct2: "[|inv (A,F); expn2 n <= meas F|] ==> meas (fst (kcstep A F n)) = meas A + expn2 n"
  apply(simp)  apply(frule meas_alloc, simp) apply(frule nonzero_meas) 
  apply(simp add: kcstep4)
done



(* Kraft-Chaitin theorem is correctness of the kc algorithm. *)

fun lengthsmatch :: "nat list list => nat list => bool"
where
  "lengthsmatch [] [] = True"
|  "lengthsmatch [] (l#ls) = False"
|  "lengthsmatch (x#xs) [] = False"
|  "lengthsmatch (x#xs) (l#ls) = ((length x = l) & (lengthsmatch xs ls))"

consts meas_nat :: "nat list => rat"
primrec
  "meas_nat [] = 0"
  "meas_nat (f#F) = (expn2 f + meas_nat F)"


lemma lem53: "[|(a+b) <= c; (0::rat) <= a |] ==> b<=c"
  apply(arith)
done 

lemma lem54: "(meas_nat (a#ls)) <= 1 ==> (meas_nat ls) <=1"
  apply(simp) apply(drule lem53) apply(auto) apply(induct a, simp_all add: expn2.simps)
done

lemma lem56: "[|X~=[]; Y~=[]; (length (hd X)) = (hd Y); lengthsmatch (tl X) (tl Y) |] ==> lengthsmatch X Y"
  apply(induct X Y rule: lengthsmatch.induct) apply(simp_all)
done

theorem kcstep_inv: "inv (A,F) ==> inv (kcstep A F n)"
  apply(simp del: inv1.simps inv2.simps add: kcstep_inv1 kcstep_inv2)
done

lemma kcloop1: "inv (A,F) ==> inv (kcloop ls (A,F))"
  apply(induct ls) apply(simp) apply(simp del: inv.simps add: kcstep_inv)
done

lemma kcloop2: "lengthsmatch X L ==> (meas X) = (meas_nat L)"
  apply(induct X L rule: lengthsmatch.induct) apply(simp_all)
done

lemma rat9: "((a::rat) = 1-b) = (b+a=1)"
  apply(arith)
done

lemma rat10: "((a::rat) <= c-b) = (a+b <= c)"
  apply(arith)
done

lemma kcloop3: "meas ((fst (kcloop ls X)) @ (snd (kcloop ls X))) = meas ((fst X) @ (snd X))"
  apply(induct ls) apply(simp) apply(simp) apply(simp add: kcstep_meas)
done

lemma meas6rev: "(meas A) + (meas B) = meas (A@B)"
  apply(induct A, simp_all)
done

lemma kcloop4: "meas (snd (kcloop ls ([],[[]]))) = 1 - meas (fst (kcloop ls ([],[[]])))"
  apply(subst rat9) apply(subst meas6rev) apply(subst kcloop3) apply(simp add: expn2.simps)
done


theorem kc_correct1: "meas_nat ls <= 1 ==> lengthsmatch (kc ls) ls"
  apply(induct ls, simp) apply(simp add: lem54)
  apply(subgoal_tac "(tl (fst (kcstep (fst (kcloop ls ([], [[]]))) (snd (kcloop ls ([], [[]]))) a))) = (fst (kcloop ls ([], [[]]))) & (length (hd (fst (kcstep (fst (kcloop ls ([], [[]]))) (snd (kcloop ls ([], [[]]))) a))) = a)")
  apply(rule lem56) apply(simp_all) defer
  apply(rule kcstep_correct1)
  apply(simp del: inv.simps) apply(rule kcloop1, simp) defer
  apply(rule kcstep_correct1b) apply(simp del: inv.simps) apply(rule kcloop1) apply(simp_all)
  apply(subst kcloop4) apply(subst rat10) apply(simp add: kcloop2)
  apply(subst kcloop4) apply(subst rat10) apply(simp add: kcloop2)
done


lemma prefixfree2: "prefixfree (A @ B) ==> prefixfree A"
  apply(induct A, simp_all add: prefix3)
done


theorem kc_correct2: "prefixfree (kc ls)"
  apply(insert kcloop1 [of "[]" "[[]]" "ls"]) apply(simp_all) apply(rule prefixfree2) apply(auto)
done



(* Show that kc does not modify previously allocated strings *)

fun extends :: "'A list => 'A list => bool"
where
  "extends [] [] = True"
| "extends [] (y#ys) = False"
| "extends x [] = True"
| "extends (x#xs) (y#ys) = ((x=y) & (extends xs ys))"


lemma extends0: "extends A A"
  apply(induct A, simp_all)
done

lemma extends1: "extends A []"
  apply(induct A) apply(simp_all)
done

lemma extends2: "extends (A@B) A"
  apply(induct A) apply(simp_all) apply(simp only: extends1)
done

lemma extends3: "extends A' A ==> extends (A' @ B) A"
  apply(induct A' A rule: extends.induct) apply(simp_all) apply(simp only: extends1)
done


lemma kcstep_extends: "extends (rev (fst (kcstep A F n))) (rev A)"
  apply(induct F, simp_all add: extends0 extends3)
done

lemma kcstep_extends1: "extends (rev A') (rev A) ==> extends (rev (fst (kcstep A' F n))) (rev A)"
  apply(induct F, simp_all add: extends1 extends3 extends0 kcstep_extends) 
done


theorem kc_extend: "extends (rev (kc (L1 @ L2) )) (rev (kc L2))"
  apply(induct L1) apply(simp_all add: kcstep_extends kcstep_extends1 extends1 extends0)
done