# Theory PRecList

Up to index of Isabelle/HOL/Recursion-Theory-I

theory PRecList
imports PRecFun
`(*  Title:       Primitive recursive coding of lists of natural numbers    Author:      Michael Nedzelsky <MichaelNedzelsky at yandex.ru>, 2008    Maintainer:  Michael Nedzelsky <MichaelNedzelsky at yandex.ru>*)header {* Primitive recursive coding of lists of natural numbers *}theory PRecListimports PRecFunbegintext {*  We introduce a particular coding @{text "list_to_nat"} from lists of  natural numbers to natural numbers.*}definition  c_len :: "nat => nat" where  "c_len = (λ (u::nat). (sgn1 u) * (c_fst(u-(1::nat))+1))"lemma c_len_1: "c_len u = (case u of 0 => 0 | Suc v => c_fst(v)+1)" by (unfold c_len_def, cases u, auto)lemma c_len_is_pr: "c_len ∈ PrimRec1" unfolding c_len_def by preclemma [simp]: "c_len 0 = 0" by (simp add: c_len_def)lemma c_len_2: "u ≠ 0 ==> c_len u = c_fst(u-(1::nat))+1" by (simp add: c_len_def)lemma c_len_3: "u>0 ==> c_len u > 0" by (simp add: c_len_2)lemma c_len_4: "c_len u = 0 ==> u = 0"proof cases  assume A1: "u = 0"  thus ?thesis by simpnext  assume A1: "c_len u = 0" and A2: "u ≠ 0"  from A2 have "c_len u > 0" by (simp add: c_len_3)  from A1 this show "u=0" by simpqedlemma c_len_5: "c_len u > 0 ==> u > 0"proof cases  assume A1: "c_len u > 0" and A2: "u=0"  from A2 have "c_len u = 0" by simp  from A1 this show ?thesis by simpnext  assume A1: "u ≠ 0"  from A1 show "u>0" by simpqedfun c_fold :: "nat list => nat" where    "c_fold [] = 0"  | "c_fold [x] = x"  | "c_fold (x#ls) = c_pair x (c_fold ls)"lemma c_fold_0: "ls ≠ [] ==> c_fold (x#ls) = c_pair x (c_fold ls)"proof -  assume A1: "ls ≠ []"  then have S1: "ls = (hd ls)#(tl ls)" by simp  then have S2: "x#ls = x#(hd ls)#(tl ls)" by simp  have S3: "c_fold (x#(hd ls)#(tl ls)) = c_pair x (c_fold ((hd ls)#(tl ls)))" by simp  from S1 S2 S3 show ?thesis by simpqedprimrec  c_unfold :: "nat => nat => nat list"where  "c_unfold 0 u = []"| "c_unfold (Suc k) u = (if k = 0 then [u] else ((c_fst u) # (c_unfold k (c_snd u))))"lemma c_fold_1: "c_unfold 1 (c_fold [x]) = [x]" by simplemma c_fold_2: "c_fold (c_unfold 1 u) = u" by simplemma c_unfold_1: "c_unfold 1 u = [u]" by simplemma c_unfold_2: "c_unfold (Suc 1) u = (c_fst u) # (c_unfold 1 (c_snd u))" by simplemma c_unfold_3: "c_unfold (Suc 1) u = [c_fst u, c_snd u]" by simplemma c_unfold_4: "k > 0 ==> c_unfold (Suc k) u = (c_fst u) # (c_unfold k (c_snd u))" by simplemma c_unfold_4_1: "k > 0 ==> c_unfold (Suc k) u ≠ []" by (simp add: c_unfold_4)lemma two: "(2::nat) = Suc 1" by simplemma c_unfold_5: "c_unfold 2 u = [c_fst u, c_snd u]" by (simp add: two)lemma c_unfold_6: "k>0 ==> c_unfold k u ≠ []"proof -  assume A1: "k>0"  let ?k1 = "k-(1::nat)"  from A1 have S1: "k = Suc ?k1" by simp  have S2: "?k1 = 0 ==> ?thesis"  proof -    assume A2_1: "?k1=0"    from A1 A2_1 have S2_1: "k=1" by simp    from S2_1 show ?thesis by (simp add: c_unfold_1)  qed  have S3: "?k1 > 0 ==> ?thesis"  proof -    assume A3_1: "?k1 > 0"    from A3_1 have S3_1: "c_unfold (Suc ?k1) u ≠ []" by (rule c_unfold_4_1)    from S1 S3_1 show ?thesis by simp  qed  from S2 S3 show ?thesis by arithqedlemma th_lm_1: "k=1 ==> (∀ u. c_fold (c_unfold k u) = u)" by (simp add: c_fold_2)lemma th_lm_2: "[|k>0; (∀ u. c_fold (c_unfold k u) = u)|] ==> (∀ u. c_fold (c_unfold (Suc k) u) = u)"proof  assume A1: "k>0"  assume A2: "∀ u. c_fold (c_unfold k u) = u"  fix u  from A1 have S1: "c_unfold (Suc k) u = (c_fst u) # (c_unfold k (c_snd u))" by (rule c_unfold_4)  let ?ls = "c_unfold k (c_snd u)"  from A1 have S2: "?ls ≠ []" by (rule c_unfold_6)  from S2 have S3: "c_fold ( (c_fst u) # ?ls) = c_pair (c_fst u) (c_fold ?ls)" by (rule c_fold_0)  from A2 have S4: "c_fold ?ls = c_snd u" by simp  from S3 S4 have S5: "c_fold ( (c_fst u) # ?ls) = c_pair (c_fst u) (c_snd u)" by simp  from S5 have S6: "c_fold ( (c_fst u) # ?ls) = u" by simp  from S1 S6 have S7: "c_fold (c_unfold (Suc k) u) = u" by simp  thus "c_fold (c_unfold (Suc k) u) = u" .qedlemma th_lm_3: "(∀ u. c_fold (c_unfold (Suc k) u) = u)==> (∀ u. c_fold (c_unfold (Suc (Suc k)) u) = u)"proof -  assume A1: "∀ u. c_fold (c_unfold (Suc k) u) = u"  let ?k1 = "Suc k"  have S1: "?k1 > 0" by simp  from S1 A1 have S2: "∀ u. c_fold (c_unfold (Suc ?k1) u) = u" by (rule th_lm_2)  thus ?thesis by simpqedtheorem th_1: "∀ u. c_fold (c_unfold (Suc k) u) = u"apply(induct k)apply(simp add: c_fold_2)apply(rule th_lm_3)apply(assumption)donetheorem th_2: "k > 0 ==> (∀ u. c_fold (c_unfold k u) = u)"proof -  assume A1: "k>0"  let ?k1 = "k-(1::nat)"  from A1 have S1: "Suc ?k1 = k" by simp  have S2: "∀ u. c_fold (c_unfold (Suc ?k1) u) = u" by (rule th_1)  from S1 S2 show ?thesis by simpqedlemma c_fold_3: "c_unfold 2 (c_fold [x, y]) = [x, y]" by (simp add: two)theorem c_unfold_len: "ALL u. length (c_unfold k u) = k"apply(induct k)apply(simp)apply(subgoal_tac "n=(0::nat) ∨ n>0")apply(drule disjE)prefer 3apply(simp_all)apply(auto)donelemma th_3_lm_0: "[|c_unfold (length ls) (c_fold ls) = ls; ls = a # ls1; ls1 = aa # list|] ==> c_unfold (length (x # ls)) (c_fold (x # ls)) = x # ls"proof -  assume A1: "c_unfold (length ls) (c_fold ls) = ls"  assume A2: "ls = a # ls1"  assume A3: "ls1 = aa # list"  from A2 have S1: "ls ≠ []" by simp  from S1 have S2: "c_fold (x#ls) = c_pair x (c_fold ls)" by (rule c_fold_0)  have S3: "length (x#ls) = Suc (length ls)" by simp  from S3 have S4: "c_unfold (length (x # ls)) (c_fold (x # ls)) = c_unfold (Suc (length ls)) (c_fold (x # ls))" by simp  from A2 have S5: "length ls > 0" by simp  from S5 have S6: "c_unfold (Suc (length ls)) (c_fold (x # ls)) = c_fst (c_fold (x # ls))#(c_unfold (length ls) (c_snd (c_fold (x#ls))))" by (rule c_unfold_4)  from S2 have S7: "c_fst (c_fold (x#ls)) = x" by simp  from S2 have S8: "c_snd (c_fold (x#ls)) = c_fold ls" by simp  from S6 S7 S8 have S9: "c_unfold (Suc (length ls)) (c_fold (x # ls)) = x # (c_unfold (length ls) (c_fold ls))" by simp  from A1 have S10: "x # (c_unfold (length ls) (c_fold ls)) = x # ls" by simp  from S9 S10 have S11: "c_unfold (Suc (length ls)) (c_fold (x # ls)) = (x # ls)" by simp  thus ?thesis by simpqedlemma th_3_lm_1: "[|c_unfold (length ls) (c_fold ls) = ls; ls = a # ls1|] ==> c_unfold (length (x # ls)) (c_fold (x # ls)) = x # ls"apply(cases ls1)apply(simp add: c_fold_1)apply(simp)donelemma th_3_lm_2: "c_unfold (length ls) (c_fold ls) = ls ==> c_unfold (length (x # ls)) (c_fold (x # ls)) = x # ls"apply(cases ls)apply(simp add: c_fold_1)apply(rule th_3_lm_1)apply(assumption+)donetheorem th_3: "c_unfold (length ls) (c_fold ls) = ls"apply(induct ls)apply(simp)apply(rule th_3_lm_2)apply(assumption)donedefinition  list_to_nat :: "nat list => nat" where  "list_to_nat = (λ ls. if ls=[] then 0 else (c_pair ((length ls) - 1) (c_fold ls))+1)"definition  nat_to_list :: "nat => nat list" where  "nat_to_list = (λ u. if u=0 then [] else (c_unfold (c_len u) (c_snd (u-(1::nat)))))"lemma nat_to_list_of_pos: "u>0 ==> nat_to_list u = c_unfold (c_len u) (c_snd (u-(1::nat)))" by (simp add: nat_to_list_def)theorem list_to_nat_th [simp]: "list_to_nat (nat_to_list u) = u"proof -  have S1: "u=0 ==> ?thesis" by (simp add: list_to_nat_def nat_to_list_def)  have S2: "u>0 ==> ?thesis"  proof -    assume A1: "u>0"    def D1: ls == "nat_to_list u"    from D1 A1 have S2_1: "ls = c_unfold (c_len u) (c_snd (u-(1::nat)))" by (simp add: nat_to_list_def)    let ?k = "c_len u"    from A1 have S2_2: "?k > 0" by (rule c_len_3)    from S2_1 have S2_3: "length ls = ?k" by (simp add: c_unfold_len)    from S2_2 S2_3 have S2_4: "length ls > 0" by simp    from S2_4 have S2_5: "ls ≠ []" by simp    from S2_5 have S2_6: "list_to_nat ls = c_pair ((length ls)-(1::nat)) (c_fold ls)+1" by (simp add: list_to_nat_def)    have S2_7: "c_fold ls = c_snd(u-(1::nat))"    proof -      from S2_1 have S2_7_1: "c_fold ls = c_fold (c_unfold (c_len u) (c_snd (u-(1::nat))))" by simp      from S2_2 S2_7_1 show ?thesis by (simp add: th_2)    qed    have S2_8: "(length ls)-(1::nat) = c_fst (u-(1::nat))"    proof -      from S2_3 have S2_8_1: "length ls = c_len u" by simp      from A1 S2_8_1 have S2_8_2: "length ls = c_fst(u-(1::nat)) + 1" by (simp add: c_len_2)      from S2_8_2 show ?thesis by simp    qed    from S2_7 S2_8 have S2_9: "c_pair ((length ls)-(1::nat)) (c_fold ls) = c_pair (c_fst (u-(1::nat))) (c_snd (u-(1::nat)))" by simp     from S2_9 have S2_10: "c_pair ((length ls)-(1::nat)) (c_fold ls) = u - (1::nat)" by simp    from S2_6 S2_10 have S2_11: "list_to_nat ls = (u - (1::nat))+1" by simp    from A1 have S2_12: "(u - (1::nat))+1 = u" by simp    from D1 S2_11 S2_12 show ?thesis by simp  qed  from S1 S2 show ?thesis by arithqedtheorem nat_to_list_th [simp]: "nat_to_list (list_to_nat ls) = ls"proof -  have S1: "ls=[] ==> ?thesis" by (simp add: nat_to_list_def list_to_nat_def)  have S2: "ls ≠ [] ==> ?thesis"  proof -    assume A1: "ls ≠ []"    def D1: u == "list_to_nat ls"    from D1 A1 have S2_1: "u = (c_pair ((length ls)-(1::nat)) (c_fold ls))+1" by (simp add: list_to_nat_def)    let ?k = "length ls"    from A1 have S2_2: "?k > 0" by simp    from S2_1 have S2_3: "u>0" by simp    from S2_3 have S2_4: "nat_to_list u = c_unfold (c_len u) (c_snd (u-(1::nat)))" by (simp add: nat_to_list_def)    have S2_5: "c_len u = length ls"    proof -      from S2_1 have S2_5_1: "u-(1::nat) = c_pair ((length ls)-(1::nat)) (c_fold ls)" by simp      from S2_5_1 have S2_5_2: "c_fst (u-(1::nat)) = (length ls)-(1::nat)" by simp      from S2_2 S2_5_2 have "c_fst (u-(1::nat))+1 = length ls" by simp      from S2_3 this show ?thesis by (simp add: c_len_2)    qed    have S2_6: "c_snd (u-(1::nat)) = c_fold ls"    proof -      from S2_1 have S2_6_1: "u-(1::nat) = c_pair ((length ls)-(1::nat)) (c_fold ls)" by simp      from S2_6_1 show ?thesis by simp    qed    from S2_4 S2_5 S2_6 have S2_7:"nat_to_list u = c_unfold (length ls) (c_fold ls)" by simp    from S2_7 have "nat_to_list u = ls" by (simp add: th_3)    from D1 this show ?thesis by simp  qed  have S3: "ls = [] ∨ ls ≠ []" by simp  from S1 S2 S3 show ?thesis by autoqedlemma [simp]: "list_to_nat [] = 0" by (simp add: list_to_nat_def)lemma [simp]: "nat_to_list 0 = []" by (simp add: nat_to_list_def)theorem c_len_th_1: "c_len (list_to_nat ls) = length ls"proof (cases)  assume "ls=[]"  from this show ?thesis by simpnext  assume S1: "ls ≠ []"  then have S2: "list_to_nat ls = c_pair ((length ls)-(1::nat)) (c_fold ls)+1" by (simp add: list_to_nat_def)  let ?u = "list_to_nat ls"  from S2 have u_not_zero: "?u > 0" by simp  from S2 have S3: "?u-(1::nat) = c_pair ((length ls)-(1::nat)) (c_fold ls)" by simp  then have S4: "c_fst(?u-(1::nat)) = (length ls)-(1::nat)" by simp  from S1 this have S5: "c_fst(?u-(1::nat))+1=length ls" by simp  from u_not_zero S5 have S6: "c_len (?u) = length ls" by (simp add: c_len_2)  from S1 S6 show ?thesis by simpqedtheorem "length (nat_to_list u) = c_len u"proof -  let ?ls = "nat_to_list u"  have S1: "u = list_to_nat ?ls" by (rule list_to_nat_th [THEN sym])  from c_len_th_1 have S2: "length ?ls = c_len (list_to_nat ?ls)" by (rule sym)  from S1 S2 show ?thesis by (rule ssubst)qeddefinition  c_hd :: "nat => nat" where  "c_hd = (λ u. if u=0 then 0 else hd (nat_to_list u))"definition  c_tl :: "nat => nat" where  "c_tl = (λ u. list_to_nat (tl (nat_to_list u)))"definition  c_cons :: "nat => nat => nat" where  "c_cons = (λ x u. list_to_nat (x # (nat_to_list u)))"lemma [simp]: "c_hd 0 = 0" by (simp add: c_hd_def)lemma c_hd_aux0: "c_len u = 1 ==> nat_to_list u = [c_snd (u-(1::nat))]" by (simp add: nat_to_list_def c_len_5)lemma c_hd_aux1: "c_len u = 1 ==> c_hd u = c_snd (u-(1::nat))"proof -  assume A1: "c_len u = 1"  then have S1: "nat_to_list u = [c_snd (u-(1::nat))]" by (simp add: nat_to_list_def c_len_5)  from A1 have "u > 0" by (simp add: c_len_5)  with S1 show ?thesis by (simp add: c_hd_def)qedlemma c_hd_aux2: "c_len u > 1 ==> c_hd u = c_fst (c_snd (u-(1::nat)))"proof -  assume A1: "c_len u > 1"  let ?k = "(c_len u) - 1"  from A1 have S1: "c_len u = Suc ?k" by simp  from A1 have S2: "c_len u > 0" by simp  from S2 have S3: "u > 0" by (rule c_len_5)  from S3 have S4: "c_hd u = hd (nat_to_list u)" by (simp add: c_hd_def)  from S3 have S5: "nat_to_list u = c_unfold (c_len u) (c_snd (u-(1::nat)))" by (rule nat_to_list_of_pos)  from S1 S5 have S6: "nat_to_list u = c_unfold (Suc ?k) (c_snd (u-(1::nat)))" by simp  from A1 have S7: "?k > 0" by simp  from S7 have S8: "c_unfold (Suc ?k) (c_snd (u-(1::nat))) = (c_fst (c_snd (u-(1::nat)))) # (c_unfold ?k (c_snd (c_snd (u-(1::nat)))))" by (rule c_unfold_4)  from S6 S8 have S9: "nat_to_list u = (c_fst (c_snd (u-(1::nat)))) # (c_unfold ?k (c_snd (c_snd (u-(1::nat)))))" by simp  from S9 have S10: "hd (nat_to_list u) = c_fst (c_snd (u-(1::nat)))" by simp  from S4 S10 show ?thesis by simpqedlemma c_hd_aux3: "u > 0 ==> c_hd u = (if (c_len u) = 1 then c_snd (u-(1::nat)) else c_fst (c_snd (u-(1::nat))))"proof -  assume A1: "u > 0"  from A1 have "c_len u > 0" by (rule c_len_3)  then have S1: "c_len u = 1 ∨ c_len u > 1" by arith  let ?tmp = "if (c_len u) = 1 then c_snd (u-(1::nat)) else c_fst (c_snd (u-(1::nat)))"  have S2: "c_len u = 1 ==> ?thesis"  proof -    assume A2_1: "c_len u = 1"    then have S2_1: "c_hd u = c_snd (u-(1::nat))" by (rule c_hd_aux1)    from A2_1 have S2_2: "?tmp = c_snd(u-(1::nat))" by simp    from S2_1 this show ?thesis by simp  qed  have S3: "c_len u > 1 ==> ?thesis"  proof -    assume A3_1: "c_len u > 1"    from A3_1 have S3_1: "c_hd u = c_fst (c_snd (u-(1::nat)))" by (rule c_hd_aux2)    from A3_1 have S3_2: "?tmp = c_fst (c_snd (u-(1::nat)))" by simp    from S3_1 this show ?thesis by simp  qed  from S1 S2 S3 show ?thesis by autoqedlemma c_hd_aux4: "c_hd u = (if u=0 then 0 else (if (c_len u) = 1 then c_snd (u-(1::nat)) else c_fst (c_snd (u-(1::nat)))))"proof cases  assume "u=0" then show ?thesis by simpnext  assume "u ≠ 0" then have A1: "u > 0" by simp  then show ?thesis by (simp add: c_hd_aux3)qedlemma c_hd_is_pr: "c_hd ∈ PrimRec1"proof -  have "c_hd = (%u. (if u=0 then 0 else (if (c_len u) = 1 then c_snd (u-(1::nat)) else c_fst (c_snd (u-(1::nat))))))" (is "_ = ?R")  by (simp add: c_hd_aux4 ext)  moreover have "?R ∈ PrimRec1"  proof (rule if_is_pr)    show "(λ x. x) ∈ PrimRec1" by (rule pr_id1_1)    next show "(λ x. 0) ∈ PrimRec1" by (rule pr_zero)    next show "(λx. if c_len x = 1 then c_snd (x - 1) else c_fst (c_snd (x - 1))) ∈ PrimRec1"    proof (rule if_eq_is_pr)      show "c_len ∈ PrimRec1" by (rule c_len_is_pr)      next show "(λ x. 1) ∈ PrimRec1" by (rule const_is_pr)      next show "(λx. c_snd (x - 1)) ∈ PrimRec1" by prec      next show "(λx. c_fst (c_snd (x - 1))) ∈ PrimRec1" by prec    qed  qed  ultimately show ?thesis by simpqedlemma [simp]: "c_tl 0 = 0" by (simp add: c_tl_def)lemma c_tl_eq_tl: "c_tl (list_to_nat ls) = list_to_nat (tl ls)" by (simp add: c_tl_def)lemma tl_eq_c_tl: "tl (nat_to_list x) = nat_to_list (c_tl x)" by (simp add: c_tl_def)lemma c_tl_aux1: "c_len u = 1 ==> c_tl u = 0" by (unfold c_tl_def, simp add: c_hd_aux0)lemma c_tl_aux2: "c_len u > 1 ==> c_tl u = (c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) + 1"proof -  assume A1: "c_len u > 1"  let ?k = "(c_len u) - 1"  from A1 have S1: "c_len u = Suc ?k" by simp  from A1 have S2: "c_len u > 0" by simp  from S2 have S3: "u > 0" by (rule c_len_5)  from S3 have S4: "nat_to_list u = c_unfold (c_len u) (c_snd (u-(1::nat)))" by (rule nat_to_list_of_pos)  from A1 have S5: "?k > 0" by simp  from S5 have S6: "c_unfold (Suc ?k) (c_snd (u-(1::nat))) = (c_fst (c_snd (u-(1::nat)))) # (c_unfold ?k (c_snd (c_snd (u-(1::nat)))))" by (rule c_unfold_4)  from S6 have S7: "tl (c_unfold (Suc ?k) (c_snd (u-(1::nat)))) = c_unfold ?k (c_snd (c_snd (u-(1::nat))))" by simp  from S2 S4 S7 have S8: "tl (nat_to_list u) = c_unfold ?k (c_snd (c_snd (u-(1::nat))))" by simp  def D1: ls == "tl (nat_to_list u)"  from D1 S8 have S9: "length ls = ?k" by (simp add: c_unfold_len)  from D1 have S10: "c_tl u = list_to_nat ls" by (simp add: c_tl_def)  from S5 S9 have S11: "length ls > 0" by simp  from S11 have S12: "ls ≠ []" by simp  from S12 have S13: "list_to_nat ls = (c_pair ((length ls) - 1) (c_fold ls))+1" by (simp add: list_to_nat_def)  from S10 S13 have S14: "c_tl u = (c_pair ((length ls) - 1) (c_fold ls))+1" by simp  from S9 have S15: "(length ls)-(1::nat) = ?k-(1::nat)" by simp  from A1 have S16: "?k-(1::nat) = c_len u - (2::nat)" by arith  from S15 S16 have S17: "(length ls)-(1::nat) = c_len u - (2::nat)" by simp  from D1 S8 have S18: "ls = c_unfold ?k (c_snd (c_snd (u-(1::nat))))" by simp  from S5 have S19: "c_fold (c_unfold ?k (c_snd (c_snd (u-(1::nat))))) = c_snd (c_snd (u-(1::nat)))" by (simp add: th_2)  from S18 S19 have S20: "c_fold ls = c_snd (c_snd (u-(1::nat)))" by simp  from S14 S17 S20 show ?thesis by simpqedlemma c_tl_aux3: "c_tl u = (sgn1 ((c_len u) - 1))*((c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) + 1)" (is "_ = ?R")proof -  have S1: "u=0 ==> ?thesis" by simp  have S2: "u>0 ==> ?thesis"  proof -    assume A1: "u>0"    have S2_1: "c_len u = 1 ==> ?thesis" by (simp add: c_tl_aux1)    have S2_2: "c_len u ≠ 1 ==> ?thesis"    proof -      assume A2_2_1: "c_len u ≠ 1"      from A1 have S2_2_1: "c_len u > 0" by (rule c_len_3)      from A2_2_1 S2_2_1 have S2_2_2: "c_len u > 1" by arith      from this have S2_2_3: "c_len u - 1 > 0" by simp      from this have S2_2_4: "sgn1 (c_len u - 1)=1" by simp      from S2_2_4 have S2_2_5: "?R = (c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) + 1" by simp      from S2_2_2 have S2_2_6: "c_tl u = (c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) + 1" by (rule c_tl_aux2)      from S2_2_5 S2_2_6 show ?thesis by simp    qed  from S2_1 S2_2 show ?thesis by blast  qed  from S1 S2 show ?thesis by arithqedlemma c_tl_less: "u > 0 ==> c_tl u < u"proof -  assume A1: "u > 0"  then have S1: "c_len u > 0" by (rule c_len_3)  then show ?thesis  proof cases    assume "c_len u = 1"    from this A1 show ?thesis by (simp add: c_tl_aux1)  next    assume "¬ c_len u = 1" with S1 have A2: "c_len u > 1" by simp    then have S2: "c_tl u = (c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) + 1" by (rule c_tl_aux2)    from A1 have S3: "c_len u = c_fst(u-(1::nat))+1" by (simp add: c_len_def)    from A2 S3 have S4: "c_len u - (2::nat) < c_fst(u-(1::nat))" by simp    then have S5: "(c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) < (c_pair (c_fst(u-(1::nat))) (c_snd (c_snd (u-(1::nat)))))" by (rule c_pair_strict_mono1)    have S6: "c_snd (c_snd (u-(1::nat))) ≤ c_snd (u-(1::nat))" by (rule c_snd_le_arg)    then have S7: "(c_pair (c_fst(u-(1::nat))) (c_snd (c_snd (u-(1::nat))))) ≤ (c_pair (c_fst(u-(1::nat))) (c_snd (u-(1::nat))))" by (rule c_pair_mono2)    then have S8: "(c_pair (c_fst(u-(1::nat))) (c_snd (c_snd (u-(1::nat))))) ≤ u-(1::nat)" by simp    with S5 have "(c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) < u - (1::nat)" by simp    with S2 have "c_tl u < (u-(1::nat))+1" by simp    with A1 show ?thesis by simp  qedqedlemma c_tl_le: "c_tl u ≤ u"proof (cases u)  assume "u=0"  then show ?thesis by simpnext  fix v assume A1: "u = Suc v"  then have S1: "u > 0" by simp  then have S2: "c_tl u < u" by (rule c_tl_less)  with A1 show "c_tl u ≤ u" by simpqedtheorem c_tl_is_pr: "c_tl ∈ PrimRec1"proof -  have "c_tl = (λ u. (sgn1 ((c_len u) - 1))*((c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) + 1))" (is "_ = ?R") by (simp add: c_tl_aux3 ext)  moreover from c_len_is_pr c_pair_is_pr have "?R ∈ PrimRec1" by prec  ultimately show ?thesis by simpqedlemma c_cons_aux1: "c_cons x 0 = (c_pair 0 x) + 1"apply(unfold c_cons_def)apply(simp)apply(unfold list_to_nat_def)apply(simp)donelemma c_cons_aux2: "u > 0 ==> c_cons x u = (c_pair (c_len u) (c_pair x (c_snd (u-(1::nat))))) + 1"proof -  assume A1: "u > 0"  from A1 have S1: "c_len u > 0" by (rule c_len_3)  from A1 have S2: "nat_to_list u = c_unfold (c_len u) (c_snd (u-(1::nat)))" by (rule nat_to_list_of_pos)  def D1: ls == "nat_to_list u"  from D1 S2 have S3: "ls = c_unfold (c_len u) (c_snd (u-(1::nat)))" by simp  from S3 have S4: "length ls = c_len u" by (simp add: c_unfold_len)  from S4 S1 have S5: "length ls > 0" by simp  from S5 have S6: "ls ≠ []" by simp  from D1 have S7: "c_cons x u = list_to_nat (x # ls)" by (simp add: c_cons_def)  have S8: "list_to_nat (x # ls) = (c_pair ((length (x#ls))-(1::nat)) (c_fold (x#ls)))+1" by (simp add: list_to_nat_def)  have S9: "(length (x#ls))-(1::nat) = length ls" by simp  from S9 S4 S8 have S10: "list_to_nat (x # ls) = (c_pair (c_len u) (c_fold (x#ls)))+1" by simp  have S11: "c_fold (x#ls) = c_pair x (c_snd (u-(1::nat)))"  proof -    from S6 have S11_1: "c_fold (x#ls) = c_pair x (c_fold ls)" by (rule c_fold_0)    from S3 have S11_2: "c_fold ls = c_fold (c_unfold (c_len u) (c_snd (u-(1::nat))))" by simp    from S1 S11_2 have S11_3: "c_fold ls = c_snd (u-(1::nat))" by (simp add: th_2)    from S11_1 S11_3 show ?thesis by simp  qed  from S7 S10 S11 show ?thesis by simpqedlemma c_cons_aux3: "c_cons = (λ x u. (sgn2 u)*((c_pair 0 x)+1) + (sgn1 u)*((c_pair (c_len u) (c_pair x (c_snd (u-(1::nat))))) + 1))"proof (rule ext, rule ext)  fix x u show "c_cons x u = (sgn2 u)*((c_pair 0 x)+1) + (sgn1 u)*((c_pair (c_len u) (c_pair x (c_snd (u-(1::nat))))) + 1)" (is "_ = ?R")  proof cases    assume A1: "u=0"    then have "?R = (c_pair 0 x)+1" by simp    moreover from A1 have "c_cons x u = (c_pair 0 x)+1" by (simp add: c_cons_aux1)    ultimately show ?thesis by simp  next    assume A1: "u≠0"    then have S1: "?R = (c_pair (c_len u) (c_pair x (c_snd (u-(1::nat))))) + 1" by simp    from A1 have S2: "c_cons x u = (c_pair (c_len u) (c_pair x (c_snd (u-(1::nat))))) + 1" by (simp add: c_cons_aux2)    from S1 S2 have "c_cons x u = ?R" by simp    then show ?thesis .  qedqedlemma c_cons_pos: "c_cons x u > 0"proof cases  assume "u=0"  then show "c_cons x u > 0" by (simp add: c_cons_aux1)next  assume "¬ u=0" then have "u>0" by simp  then show "c_cons x u > 0" by (simp add: c_cons_aux2)qedtheorem c_cons_is_pr: "c_cons ∈ PrimRec2"proof -  have "c_cons = (λ x u. (sgn2 u)*((c_pair 0 x)+1) + (sgn1 u)*((c_pair (c_len u) (c_pair x (c_snd (u-(1::nat))))) + 1))" (is "_ = ?R") by (simp add: c_cons_aux3)  moreover from c_pair_is_pr c_len_is_pr have "?R ∈ PrimRec2" by prec  ultimately show ?thesis by simpqeddefinition  c_drop :: "nat => nat => nat" where  "c_drop = PrimRecOp (λ x. x) (λ x y z. c_tl y)"lemma c_drop_at_0 [simp]: "c_drop 0 x = x" by (simp add: c_drop_def)lemma c_drop_at_Suc: "c_drop (Suc y) x = c_tl (c_drop y x)" by (simp add: c_drop_def)theorem c_drop_is_pr: "c_drop ∈ PrimRec2"proof -  have "(λ x. x) ∈ PrimRec1" by (rule pr_id1_1)  moreover from c_tl_is_pr have "(λ x y z. c_tl y) ∈ PrimRec3" by prec  ultimately show ?thesis by (simp add: c_drop_def pr_rec)qedlemma c_tl_c_drop: "c_tl (c_drop y x) = c_drop y (c_tl x)"apply(induct y)apply(simp)apply(simp add: c_drop_at_Suc)donelemma c_drop_at_Suc1: "c_drop (Suc y) x = c_drop y (c_tl x)"apply(simp add: c_drop_at_Suc c_tl_c_drop)donelemma c_drop_df: "∀ ls. drop n ls = nat_to_list (c_drop n (list_to_nat ls))"proof (induct n)  show "∀ ls. drop 0 ls = nat_to_list (c_drop 0 (list_to_nat ls))" by (simp add: c_drop_def)next  fix n assume A1: "∀ ls. drop n ls = nat_to_list (c_drop n (list_to_nat ls))"  then show "∀ ls. drop (Suc n) ls = nat_to_list (c_drop (Suc n) (list_to_nat ls))"  proof -    {    fix ls::"nat list"    have S1: "drop (Suc n) ls = drop n (tl ls)" by (rule drop_Suc)    from A1 have S2: "drop n (tl ls) = nat_to_list (c_drop n (list_to_nat (tl ls)))" by simp    also have "… = nat_to_list (c_drop n (c_tl (list_to_nat ls)))" by  (simp add: c_tl_eq_tl)    also have "… = nat_to_list (c_drop (Suc n) (list_to_nat ls))" by  (simp add: c_drop_at_Suc1)    finally have "drop n (tl ls) = nat_to_list (c_drop (Suc n) (list_to_nat ls))" by simp    with S1 have "drop (Suc n) ls = nat_to_list (c_drop (Suc n) (list_to_nat ls))" by simp        }    then show ?thesis by blast  qedqeddefinition  c_nth :: "nat => nat => nat" where  "c_nth = (λ x n. c_hd (c_drop n x))"lemma c_nth_is_pr: "c_nth ∈ PrimRec2"proof (unfold c_nth_def)  from c_hd_is_pr c_drop_is_pr show "(λx n. c_hd (c_drop n x)) ∈ PrimRec2" by precqedlemma c_nth_at_0: "c_nth x 0 = c_hd x" by (simp add: c_nth_def)lemma c_hd_c_cons [simp]: "c_hd (c_cons x y) = x"proof -  have "c_cons x y > 0" by (rule c_cons_pos)  then show ?thesis by (simp add: c_hd_def c_cons_def)qedlemma c_tl_c_cons [simp]: "c_tl (c_cons x y) = y" by (simp add: c_tl_def c_cons_def)definition  c_f_list :: "(nat => nat => nat) => nat => nat => nat" where  "c_f_list = (λ f.    let g = (%x. c_cons (f 0 x) 0); h = (%a b c. c_cons (f (Suc a) c) b) in PrimRecOp g h)"lemma c_f_list_at_0: "c_f_list f 0 x = c_cons (f 0 x) 0" by (simp add: c_f_list_def Let_def)lemma c_f_list_at_Suc: "c_f_list f (Suc y) x = c_cons (f (Suc y) x) (c_f_list f y x)" by ((simp add: c_f_list_def Let_def))lemma c_f_list_is_pr: "f ∈ PrimRec2 ==> c_f_list f ∈ PrimRec2"proof -  assume A1: "f ∈ PrimRec2"  let ?g = "(%x. c_cons (f 0 x) 0)"  from A1 c_cons_is_pr have S1: "?g ∈ PrimRec1" by prec  let ?h = "(%a b c. c_cons (f (Suc a) c) b)"  from A1 c_cons_is_pr have S2: "?h ∈ PrimRec3" by prec  from S1 S2 show ?thesis by (simp add: pr_rec c_f_list_def Let_def)qedlemma c_f_list_to_f_0: "f y x = c_hd (c_f_list f y x)"apply(induct y)apply(simp add: c_f_list_at_0)apply(simp add: c_f_list_at_Suc)donelemma c_f_list_to_f: "f = (λ y x. c_hd (c_f_list f y x))"apply(rule ext, rule ext)apply(rule c_f_list_to_f_0)donelemma c_f_list_f_is_pr: "c_f_list f ∈ PrimRec2 ==> f ∈ PrimRec2"proof -  assume A1: "c_f_list f ∈ PrimRec2"  have S1: "f = (λ y x. c_hd (c_f_list f y x))" by (rule c_f_list_to_f)  from A1 c_hd_is_pr have S2: "(λ y x. c_hd (c_f_list f y x)) ∈ PrimRec2" by prec  with S1 show ?thesis by simpqedlemma c_f_list_lm_1: "c_nth (c_cons x y) (Suc z) = c_nth y z" by (simp add: c_nth_def c_drop_at_Suc1)lemma c_f_list_lm_2: " z < Suc n ==> c_nth (c_f_list f (Suc n) x) (Suc n - z) = c_nth (c_f_list f n x) (n - z)"proof -  assume "z < Suc n"  then have "Suc n - z = Suc (n-z)" by arith  then have "c_nth (c_f_list f (Suc n) x) (Suc n - z) = c_nth (c_f_list f (Suc n) x) (Suc (n - z))" by simp  also have "… = c_nth (c_cons (f (Suc n) x) (c_f_list f n x)) (Suc (n - z))" by (simp add: c_f_list_at_Suc)  also have "… = c_nth (c_f_list f n x) (n - z)" by (simp add: c_f_list_lm_1)  finally show ?thesis by simpqedlemma c_f_list_nth: "z ≤ y --> c_nth (c_f_list f y x) (y-z) = f z x"proof (induct y)  show "z ≤ 0 --> c_nth (c_f_list f 0 x) (0 - z) = f z x"  proof    assume "z ≤ 0" then have A1: "z=0" by simp    then have "c_nth (c_f_list f 0 x) (0 - z) = c_nth (c_f_list f 0 x) 0" by simp    also have "… = c_hd (c_f_list f 0 x)" by (simp add: c_nth_at_0)    also have "… = c_hd (c_cons (f 0 x) 0)" by (simp add: c_f_list_at_0)    also have "… = f 0 x" by simp    finally show "c_nth (c_f_list f 0 x) (0 - z) = f z x" by (simp add: A1)  qednext  fix n assume A2: " z ≤ n --> c_nth (c_f_list f n x) (n - z) = f z x" show "z ≤ Suc n --> c_nth (c_f_list f (Suc n) x) (Suc n - z) = f z x"  proof    assume A3: "z ≤ Suc n"    show " z ≤ Suc n ==> c_nth (c_f_list f (Suc n) x) (Suc n - z) = f z x"    proof cases      assume AA1: "z ≤ n"      then have AA2: "z < Suc n" by simp      from A2 this have S1: "c_nth (c_f_list f n x) (n - z) = f z x" by auto      from AA2 have "c_nth (c_f_list f (Suc n) x) (Suc n - z) = c_nth (c_f_list f n x) (n - z)" by (rule c_f_list_lm_2)      with S1 show "c_nth (c_f_list f (Suc n) x) (Suc n - z) = f z x" by simp    next      assume "¬ z ≤ n"      from A3 this have S1: "z = Suc n" by simp      then have S2: "Suc n - z = 0" by simp      then have "c_nth (c_f_list f (Suc n) x) (Suc n - z) = c_nth (c_f_list f (Suc n) x) 0" by simp      also have "… = c_hd (c_f_list f (Suc n) x)" by (simp add: c_nth_at_0)      also have "… = c_hd (c_cons (f (Suc n) x) (c_f_list f n x))" by (simp add: c_f_list_at_Suc)      also have "… = f (Suc n) x" by simp      finally show "c_nth (c_f_list f (Suc n) x) (Suc n - z) = f z x" by (simp add: S1)    qed  qedqedtheorem th_pr_rec: "[| g ∈ PrimRec1; h ∈ PrimRec3; (∀ x. (f 0 x) = (g x)); (∀ x y. (f (Suc y) x) = h y (f y x) x) |] ==> f ∈ PrimRec2"proof -  assume g_is_pr: "g ∈ PrimRec1"  assume h_is_pr: "h ∈ PrimRec3"  assume f_0: "∀ x. f 0 x = g x"  assume f_1: "∀ x y. (f (Suc y) x) = h y (f y x) x"  let ?f = "PrimRecOp g h"  from g_is_pr h_is_pr have S1: "?f ∈ PrimRec2" by (rule pr_rec)  have f_2:"∀ x. ?f 0 x = g x" by simp  have f_3: "∀ x y. (?f (Suc y) x) = h y (?f y x) x" by simp  have S2: "f = ?f"  proof -    have "!! x y. f y x = ?f y x"    apply(induct_tac y)    apply(insert f_0 f_1)    apply(auto)    done    then show "f = ?f" by (simp add: ext)  qed  from S1 S2 show ?thesis by simpqedtheorem th_rec: "[| g ∈ PrimRec1; α ∈ PrimRec2; h ∈ PrimRec3; (∀ x y. α y x ≤ y); (∀ x. (f 0 x) = (g x)); (∀ x y. (f (Suc y) x) = h y (f (α y x) x) x) |] ==> f ∈ PrimRec2"proof -  assume g_is_pr: "g ∈ PrimRec1"  assume a_is_pr: "α ∈ PrimRec2"  assume h_is_pr: "h ∈ PrimRec3"  assume a_le: "(∀ x y. α y x ≤ y)"  assume f_0: "∀ x. f 0 x = g x"  assume f_1: "∀ x y. (f (Suc y) x) = h y (f (α y x) x) x"  let ?g' = "λ x. c_cons (g x) 0"  let ?h' = "λ a b c. c_cons (h a (c_nth b (a - (α a c))) c) b"  let ?r = "c_f_list f"  from g_is_pr c_cons_is_pr have g'_is_pr: "?g' ∈ PrimRec1" by prec  from h_is_pr c_cons_is_pr c_nth_is_pr a_is_pr have h'_is_pr: "?h' ∈ PrimRec3" by prec  have S1: "∀ x. ?r 0 x = ?g' x"  proof    fix x have "?r 0 x = c_cons (f 0 x) 0" by (rule c_f_list_at_0)    with f_0 have "?r 0 x = c_cons (g x) 0" by simp    then show "?r 0 x = ?g' x" by simp  qed  have S2: "∀ x y. ?r (Suc y) x = ?h' y (?r y x) x"  proof (rule allI, rule allI)    fix x y show "?r (Suc y) x = ?h' y (?r y x) x"    proof -      have S2_1: "?r (Suc y) x = c_cons (f (Suc y) x) (?r y x)" by (rule c_f_list_at_Suc)      with f_1 have S2_2: "f (Suc y) x = h y (f (α y x) x) x" by simp      from a_le have S2_3: "α y x ≤ y" by simp      then have S2_4: "f (α y x) x = c_nth (?r y x) (y-(α y x))" by (simp add: c_f_list_nth)      from S2_1 S2_2 S2_4 show ?thesis by simp    qed  qed  from g'_is_pr h'_is_pr S1 S2 have S3: "?r ∈ PrimRec2" by (rule th_pr_rec)  then show "f ∈ PrimRec2" by (rule c_f_list_f_is_pr)qeddeclare c_tl_less [termination_simp]fun c_assoc_have_key :: "nat => nat => nat" where  c_assoc_have_key_df [simp del]: "c_assoc_have_key y x = (if y = 0 then 1 else    (if c_fst (c_hd y) = x then 0 else c_assoc_have_key (c_tl y) x))"lemma c_assoc_have_key_lm_1: "y ≠ 0 ==> c_assoc_have_key y x = (if c_fst (c_hd y) = x then 0 else c_assoc_have_key (c_tl y) x)" by (simp add: c_assoc_have_key_df)theorem c_assoc_have_key_is_pr: "c_assoc_have_key ∈ PrimRec2"proof -  let ?h = "λ a b c. if c_fst (c_hd (Suc a)) = c then 0 else b"  let ?a = "λ y x. c_tl (Suc y)"  let ?g = "λ x. (1::nat)"  have g_is_pr: "?g ∈ PrimRec1" by (rule const_is_pr)  from c_tl_is_pr have a_is_pr: "?a ∈ PrimRec2" by prec  have h_is_pr: "?h ∈ PrimRec3"  proof (rule if_eq_is_pr3)    from c_fst_is_pr c_hd_is_pr show "(λx y z. c_fst (c_hd (Suc x))) ∈ PrimRec3" by prec  next    show "(λx y z. z) ∈ PrimRec3" by (rule pr_id3_3)  next    show "(λx y z. 0) ∈ PrimRec3" by prec  next    show "(λx y z. y) ∈ PrimRec3" by (rule pr_id3_2)  qed  have a_le: "∀ x y. ?a y x ≤ y"  proof (rule allI, rule allI)    fix x y show "?a y x ≤ y"    proof -      have "Suc y > 0" by simp      then have "?a y x < Suc y" by (rule c_tl_less)      then show ?thesis by simp    qed  qed  have f_0: "∀ x. c_assoc_have_key 0 x = ?g x" by (simp add: c_assoc_have_key_df)  have f_1: "∀ x y. c_assoc_have_key (Suc y) x = ?h y (c_assoc_have_key (?a y x) x) x" by (simp add: c_assoc_have_key_df)  from g_is_pr a_is_pr h_is_pr a_le f_0 f_1 show ?thesis by (rule th_rec)qedfun c_assoc_value :: "nat => nat => nat" where  c_assoc_value_df [simp del]: "c_assoc_value y x = (if y = 0 then 0 else    (if c_fst (c_hd y) = x then c_snd (c_hd y) else c_assoc_value (c_tl y) x))"lemma c_assoc_value_lm_1: "y ≠ 0 ==> c_assoc_value y x = (if c_fst (c_hd y) = x then c_snd (c_hd y) else c_assoc_value (c_tl y) x)" by (simp add: c_assoc_value_df)theorem c_assoc_value_is_pr: "c_assoc_value ∈ PrimRec2"proof -  let ?h = "λ a b c. if c_fst (c_hd (Suc a)) = c then c_snd (c_hd (Suc a)) else b"  let ?a = "λ y x. c_tl (Suc y)"  let ?g = "λ x. (0::nat)"  have g_is_pr: "?g ∈ PrimRec1" by (rule const_is_pr)  from c_tl_is_pr have a_is_pr: "?a ∈ PrimRec2" by prec  have h_is_pr: "?h ∈ PrimRec3"  proof (rule if_eq_is_pr3)    from c_fst_is_pr c_hd_is_pr show "(λx y z. c_fst (c_hd (Suc x))) ∈ PrimRec3" by prec  next    show "(λx y z. z) ∈ PrimRec3" by (rule pr_id3_3)  next    from c_snd_is_pr c_hd_is_pr show "(λx y z. c_snd (c_hd (Suc x))) ∈ PrimRec3" by prec  next    show "(λx y z. y) ∈ PrimRec3" by (rule pr_id3_2)  qed  have a_le: "∀ x y. ?a y x ≤ y"  proof (rule allI, rule allI)    fix x y show "?a y x ≤ y"    proof -      have "Suc y > 0" by simp      then have "?a y x < Suc y" by (rule c_tl_less)      then show ?thesis by simp    qed  qed  have f_0: "∀ x. c_assoc_value 0 x = ?g x" by (simp add: c_assoc_value_df)  have f_1: "∀ x y. c_assoc_value (Suc y) x = ?h y (c_assoc_value (?a y x) x) x" by (simp add: c_assoc_value_df)  from g_is_pr a_is_pr h_is_pr a_le f_0 f_1 show ?thesis by (rule th_rec)qedlemma c_assoc_lm_1: "c_assoc_have_key (c_cons (c_pair x y) z) x = 0"apply(simp add: c_assoc_have_key_df)apply(simp add: c_cons_pos)donelemma c_assoc_lm_2: "c_assoc_value (c_cons (c_pair x y) z) x = y"apply(simp add: c_assoc_value_df)apply(rule impI)apply(insert c_cons_pos [where x="(c_pair x y)" and u="z"])apply(auto)donelemma c_assoc_lm_3: "x1 ≠ x ==> c_assoc_have_key (c_cons (c_pair x y) z) x1 = c_assoc_have_key z x1"proof -  assume A1: "x1 ≠ x"  let ?ls = "(c_cons (c_pair x y) z)"  have S1: "?ls ≠ 0" by (simp add: c_cons_pos)  then have S2: "c_assoc_have_key ?ls x1 = (if c_fst (c_hd ?ls) = x1 then 0 else c_assoc_have_key (c_tl ?ls) x1)" (is "_ = ?R")  by (rule c_assoc_have_key_lm_1)  have S3: "c_fst (c_hd ?ls) = x" by simp  with A1 have S4: "¬ (c_fst (c_hd ?ls) = x1)" by simp  from S4 have S5: "?R = c_assoc_have_key (c_tl ?ls) x1" by (rule if_not_P)  from S2 S5 show ?thesis by simpqedlemma c_assoc_lm_4: "x1 ≠ x ==> c_assoc_value (c_cons (c_pair x y) z) x1 = c_assoc_value z x1"proof -  assume A1: "x1 ≠ x"  let ?ls = "(c_cons (c_pair x y) z)"  have S1: "?ls ≠ 0" by (simp add: c_cons_pos)  then have S2: "c_assoc_value ?ls x1 = (if c_fst (c_hd ?ls) = x1 then c_snd (c_hd ?ls) else c_assoc_value (c_tl ?ls) x1)" (is "_ = ?R")  by (rule c_assoc_value_lm_1)  have S3: "c_fst (c_hd ?ls) = x" by simp  with A1 have S4: "¬ (c_fst (c_hd ?ls) = x1)" by simp  from S4 have S5: "?R = c_assoc_value (c_tl ?ls) x1" by (rule if_not_P)  from S2 S5 show ?thesis by simpqedend`