27 lemma map2_Cons [simp, code]: |
27 lemma map2_Cons [simp, code]: |
28 "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys" |
28 "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys" |
29 unfolding map2_def by auto |
29 unfolding map2_def by auto |
30 |
30 |
31 |
31 |
32 subsection {* Operations on lists of booleans *} |
32 subsection \<open>Operations on lists of booleans\<close> |
33 |
33 |
34 primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" |
34 primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" |
35 where |
35 where |
36 Nil: "bl_to_bin_aux [] w = w" |
36 Nil: "bl_to_bin_aux [] w = w" |
37 | Cons: "bl_to_bin_aux (b # bs) w = |
37 | Cons: "bl_to_bin_aux (b # bs) w = |
64 | y # ys => y # takefill fill n ys)" |
64 | y # ys => y # takefill fill n ys)" |
65 |
65 |
66 |
66 |
67 subsection "Arithmetic in terms of bool lists" |
67 subsection "Arithmetic in terms of bool lists" |
68 |
68 |
69 text {* |
69 text \<open> |
70 Arithmetic operations in terms of the reversed bool list, |
70 Arithmetic operations in terms of the reversed bool list, |
71 assuming input list(s) the same length, and don't extend them. |
71 assuming input list(s) the same length, and don't extend them. |
72 *} |
72 \<close> |
73 |
73 |
74 primrec rbl_succ :: "bool list => bool list" |
74 primrec rbl_succ :: "bool list => bool list" |
75 where |
75 where |
76 Nil: "rbl_succ Nil = Nil" |
76 Nil: "rbl_succ Nil = Nil" |
77 | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)" |
77 | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)" |
81 Nil: "rbl_pred Nil = Nil" |
81 Nil: "rbl_pred Nil = Nil" |
82 | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)" |
82 | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)" |
83 |
83 |
84 primrec rbl_add :: "bool list => bool list => bool list" |
84 primrec rbl_add :: "bool list => bool list => bool list" |
85 where |
85 where |
86 -- "result is length of first arg, second arg may be longer" |
86 \<comment> "result is length of first arg, second arg may be longer" |
87 Nil: "rbl_add Nil x = Nil" |
87 Nil: "rbl_add Nil x = Nil" |
88 | Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in |
88 | Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in |
89 (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))" |
89 (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))" |
90 |
90 |
91 primrec rbl_mult :: "bool list => bool list => bool list" |
91 primrec rbl_mult :: "bool list => bool list => bool list" |
92 where |
92 where |
93 -- "result is length of first arg, second arg may be longer" |
93 \<comment> "result is length of first arg, second arg may be longer" |
94 Nil: "rbl_mult Nil x = Nil" |
94 Nil: "rbl_mult Nil x = Nil" |
95 | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in |
95 | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in |
96 if y then rbl_add ws x else ws)" |
96 if y then rbl_add ws x else ws)" |
97 |
97 |
98 lemma butlast_power: |
98 lemma butlast_power: |
127 lemma bin_to_bl_aux_Bit1_minus_simp [simp]: |
127 lemma bin_to_bl_aux_Bit1_minus_simp [simp]: |
128 "0 < n ==> bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = |
128 "0 < n ==> bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = |
129 bin_to_bl_aux (n - 1) (numeral w) (True # bl)" |
129 bin_to_bl_aux (n - 1) (numeral w) (True # bl)" |
130 by (cases n) auto |
130 by (cases n) auto |
131 |
131 |
132 text {* Link between bin and bool list. *} |
132 text \<open>Link between bin and bool list.\<close> |
133 |
133 |
134 lemma bl_to_bin_aux_append: |
134 lemma bl_to_bin_aux_append: |
135 "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)" |
135 "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)" |
136 by (induct bs arbitrary: w) auto |
136 by (induct bs arbitrary: w) auto |
137 |
137 |
1116 length (bin_rsplit_aux n nw v bs) = |
1116 length (bin_rsplit_aux n nw v bs) = |
1117 length (bin_rsplit_aux n nw w cs)" |
1117 length (bin_rsplit_aux n nw w cs)" |
1118 proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct) |
1118 proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct) |
1119 case (1 n m w cs v bs) show ?case |
1119 case (1 n m w cs v bs) show ?case |
1120 proof (cases "m = 0") |
1120 proof (cases "m = 0") |
1121 case True then show ?thesis using `length bs = length cs` by simp |
1121 case True then show ?thesis using \<open>length bs = length cs\<close> by simp |
1122 next |
1122 next |
1123 case False |
1123 case False |
1124 from "1.hyps" `m \<noteq> 0` `n \<noteq> 0` have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow> |
1124 from "1.hyps" \<open>m \<noteq> 0\<close> \<open>n \<noteq> 0\<close> have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow> |
1125 length (bin_rsplit_aux n (m - n) v bs) = |
1125 length (bin_rsplit_aux n (m - n) v bs) = |
1126 length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))" |
1126 length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))" |
1127 by auto |
1127 by auto |
1128 show ?thesis using `length bs = length cs` `n \<noteq> 0` |
1128 show ?thesis using \<open>length bs = length cs\<close> \<open>n \<noteq> 0\<close> |
1129 by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len |
1129 by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len |
1130 split: prod.split) |
1130 split: prod.split) |
1131 qed |
1131 qed |
1132 qed |
1132 qed |
1133 |
1133 |