1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Thu Sep 23 14:50:18 2010 +0200
1.3 @@ -0,0 +1,1488 @@
1.4 +theory Predicate_Compile_Tests
1.5 +imports Predicate_Compile_Alternative_Defs
1.6 +begin
1.7 +
1.8 +subsection {* Basic predicates *}
1.9 +
1.10 +inductive False' :: "bool"
1.11 +
1.12 +code_pred (expected_modes: bool) False' .
1.13 +code_pred [dseq] False' .
1.14 +code_pred [random_dseq] False' .
1.15 +
1.16 +values [expected "{}" pred] "{x. False'}"
1.17 +values [expected "{}" dseq 1] "{x. False'}"
1.18 +values [expected "{}" random_dseq 1, 1, 1] "{x. False'}"
1.19 +
1.20 +value "False'"
1.21 +
1.22 +inductive True' :: "bool"
1.23 +where
1.24 + "True ==> True'"
1.25 +
1.26 +code_pred True' .
1.27 +code_pred [dseq] True' .
1.28 +code_pred [random_dseq] True' .
1.29 +
1.30 +thm True'.equation
1.31 +thm True'.dseq_equation
1.32 +thm True'.random_dseq_equation
1.33 +values [expected "{()}" ]"{x. True'}"
1.34 +values [expected "{}" dseq 0] "{x. True'}"
1.35 +values [expected "{()}" dseq 1] "{x. True'}"
1.36 +values [expected "{()}" dseq 2] "{x. True'}"
1.37 +values [expected "{}" random_dseq 1, 1, 0] "{x. True'}"
1.38 +values [expected "{}" random_dseq 1, 1, 1] "{x. True'}"
1.39 +values [expected "{()}" random_dseq 1, 1, 2] "{x. True'}"
1.40 +values [expected "{()}" random_dseq 1, 1, 3] "{x. True'}"
1.41 +
1.42 +inductive EmptySet :: "'a \<Rightarrow> bool"
1.43 +
1.44 +code_pred (expected_modes: o => bool, i => bool) EmptySet .
1.45 +
1.46 +definition EmptySet' :: "'a \<Rightarrow> bool"
1.47 +where "EmptySet' = {}"
1.48 +
1.49 +code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
1.50 +
1.51 +inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
1.52 +
1.53 +code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel .
1.54 +
1.55 +inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
1.56 +for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
1.57 +
1.58 +code_pred
1.59 + (expected_modes: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool,
1.60 + (o => o => bool) => o => i => bool, (o => o => bool) => i => i => bool,
1.61 + (i => o => bool) => o => o => bool, (i => o => bool) => i => o => bool,
1.62 + (i => o => bool) => o => i => bool, (i => o => bool) => i => i => bool,
1.63 + (o => i => bool) => o => o => bool, (o => i => bool) => i => o => bool,
1.64 + (o => i => bool) => o => i => bool, (o => i => bool) => i => i => bool,
1.65 + (i => i => bool) => o => o => bool, (i => i => bool) => i => o => bool,
1.66 + (i => i => bool) => o => i => bool, (i => i => bool) => i => i => bool)
1.67 + EmptyClosure .
1.68 +
1.69 +thm EmptyClosure.equation
1.70 +
1.71 +(* TODO: inductive package is broken!
1.72 +inductive False'' :: "bool"
1.73 +where
1.74 + "False \<Longrightarrow> False''"
1.75 +
1.76 +code_pred (expected_modes: []) False'' .
1.77 +
1.78 +inductive EmptySet'' :: "'a \<Rightarrow> bool"
1.79 +where
1.80 + "False \<Longrightarrow> EmptySet'' x"
1.81 +
1.82 +code_pred (expected_modes: [1]) EmptySet'' .
1.83 +code_pred (expected_modes: [], [1]) [inductify] EmptySet'' .
1.84 +*)
1.85 +
1.86 +consts a' :: 'a
1.87 +
1.88 +inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
1.89 +where
1.90 +"Fact a' a'"
1.91 +
1.92 +code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact .
1.93 +
1.94 +inductive zerozero :: "nat * nat => bool"
1.95 +where
1.96 + "zerozero (0, 0)"
1.97 +
1.98 +code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero .
1.99 +code_pred [dseq] zerozero .
1.100 +code_pred [random_dseq] zerozero .
1.101 +
1.102 +thm zerozero.equation
1.103 +thm zerozero.dseq_equation
1.104 +thm zerozero.random_dseq_equation
1.105 +
1.106 +text {* We expect the user to expand the tuples in the values command.
1.107 +The following values command is not supported. *}
1.108 +(*values "{x. zerozero x}" *)
1.109 +text {* Instead, the user must type *}
1.110 +values "{(x, y). zerozero (x, y)}"
1.111 +
1.112 +values [expected "{}" dseq 0] "{(x, y). zerozero (x, y)}"
1.113 +values [expected "{(0::nat, 0::nat)}" dseq 1] "{(x, y). zerozero (x, y)}"
1.114 +values [expected "{(0::nat, 0::nat)}" dseq 2] "{(x, y). zerozero (x, y)}"
1.115 +values [expected "{}" random_dseq 1, 1, 2] "{(x, y). zerozero (x, y)}"
1.116 +values [expected "{(0::nat, 0:: nat)}" random_dseq 1, 1, 3] "{(x, y). zerozero (x, y)}"
1.117 +
1.118 +inductive nested_tuples :: "((int * int) * int * int) => bool"
1.119 +where
1.120 + "nested_tuples ((0, 1), 2, 3)"
1.121 +
1.122 +code_pred nested_tuples .
1.123 +
1.124 +inductive JamesBond :: "nat => int => code_numeral => bool"
1.125 +where
1.126 + "JamesBond 0 0 7"
1.127 +
1.128 +code_pred JamesBond .
1.129 +
1.130 +values [expected "{(0::nat, 0::int , 7::code_numeral)}"] "{(a, b, c). JamesBond a b c}"
1.131 +values [expected "{(0::nat, 7::code_numeral, 0:: int)}"] "{(a, c, b). JamesBond a b c}"
1.132 +values [expected "{(0::int, 0::nat, 7::code_numeral)}"] "{(b, a, c). JamesBond a b c}"
1.133 +values [expected "{(0::int, 7::code_numeral, 0::nat)}"] "{(b, c, a). JamesBond a b c}"
1.134 +values [expected "{(7::code_numeral, 0::nat, 0::int)}"] "{(c, a, b). JamesBond a b c}"
1.135 +values [expected "{(7::code_numeral, 0::int, 0::nat)}"] "{(c, b, a). JamesBond a b c}"
1.136 +
1.137 +values [expected "{(7::code_numeral, 0::int)}"] "{(a, b). JamesBond 0 b a}"
1.138 +values [expected "{(7::code_numeral, 0::nat)}"] "{(c, a). JamesBond a 0 c}"
1.139 +values [expected "{(0::nat, 7::code_numeral)}"] "{(a, c). JamesBond a 0 c}"
1.140 +
1.141 +
1.142 +subsection {* Alternative Rules *}
1.143 +
1.144 +datatype char = C | D | E | F | G | H
1.145 +
1.146 +inductive is_C_or_D
1.147 +where
1.148 + "(x = C) \<or> (x = D) ==> is_C_or_D x"
1.149 +
1.150 +code_pred (expected_modes: i => bool) is_C_or_D .
1.151 +thm is_C_or_D.equation
1.152 +
1.153 +inductive is_D_or_E
1.154 +where
1.155 + "(x = D) \<or> (x = E) ==> is_D_or_E x"
1.156 +
1.157 +lemma [code_pred_intro]:
1.158 + "is_D_or_E D"
1.159 +by (auto intro: is_D_or_E.intros)
1.160 +
1.161 +lemma [code_pred_intro]:
1.162 + "is_D_or_E E"
1.163 +by (auto intro: is_D_or_E.intros)
1.164 +
1.165 +code_pred (expected_modes: o => bool, i => bool) is_D_or_E
1.166 +proof -
1.167 + case is_D_or_E
1.168 + from is_D_or_E.prems show thesis
1.169 + proof
1.170 + fix xa
1.171 + assume x: "x = xa"
1.172 + assume "xa = D \<or> xa = E"
1.173 + from this show thesis
1.174 + proof
1.175 + assume "xa = D" from this x is_D_or_E(1) show thesis by simp
1.176 + next
1.177 + assume "xa = E" from this x is_D_or_E(2) show thesis by simp
1.178 + qed
1.179 + qed
1.180 +qed
1.181 +
1.182 +thm is_D_or_E.equation
1.183 +
1.184 +inductive is_F_or_G
1.185 +where
1.186 + "x = F \<or> x = G ==> is_F_or_G x"
1.187 +
1.188 +lemma [code_pred_intro]:
1.189 + "is_F_or_G F"
1.190 +by (auto intro: is_F_or_G.intros)
1.191 +
1.192 +lemma [code_pred_intro]:
1.193 + "is_F_or_G G"
1.194 +by (auto intro: is_F_or_G.intros)
1.195 +
1.196 +inductive is_FGH
1.197 +where
1.198 + "is_F_or_G x ==> is_FGH x"
1.199 +| "is_FGH H"
1.200 +
1.201 +text {* Compilation of is_FGH requires elimination rule for is_F_or_G *}
1.202 +
1.203 +code_pred (expected_modes: o => bool, i => bool) is_FGH
1.204 +proof -
1.205 + case is_F_or_G
1.206 + from is_F_or_G.prems show thesis
1.207 + proof
1.208 + fix xa
1.209 + assume x: "x = xa"
1.210 + assume "xa = F \<or> xa = G"
1.211 + from this show thesis
1.212 + proof
1.213 + assume "xa = F"
1.214 + from this x is_F_or_G(1) show thesis by simp
1.215 + next
1.216 + assume "xa = G"
1.217 + from this x is_F_or_G(2) show thesis by simp
1.218 + qed
1.219 + qed
1.220 +qed
1.221 +
1.222 +subsection {* Named alternative rules *}
1.223 +
1.224 +inductive appending
1.225 +where
1.226 + nil: "appending [] ys ys"
1.227 +| cons: "appending xs ys zs \<Longrightarrow> appending (x#xs) ys (x#zs)"
1.228 +
1.229 +lemma appending_alt_nil: "ys = zs \<Longrightarrow> appending [] ys zs"
1.230 +by (auto intro: appending.intros)
1.231 +
1.232 +lemma appending_alt_cons: "xs' = x # xs \<Longrightarrow> appending xs ys zs \<Longrightarrow> zs' = x # zs \<Longrightarrow> appending xs' ys zs'"
1.233 +by (auto intro: appending.intros)
1.234 +
1.235 +text {* With code_pred_intro, we can give fact names to the alternative rules,
1.236 + which are used for the code_pred command. *}
1.237 +
1.238 +declare appending_alt_nil[code_pred_intro alt_nil] appending_alt_cons[code_pred_intro alt_cons]
1.239 +
1.240 +code_pred appending
1.241 +proof -
1.242 + case appending
1.243 + from appending.prems show thesis
1.244 + proof(cases)
1.245 + case nil
1.246 + from alt_nil nil show thesis by auto
1.247 + next
1.248 + case cons
1.249 + from alt_cons cons show thesis by fastsimp
1.250 + qed
1.251 +qed
1.252 +
1.253 +
1.254 +inductive ya_even and ya_odd :: "nat => bool"
1.255 +where
1.256 + even_zero: "ya_even 0"
1.257 +| odd_plus1: "ya_even x ==> ya_odd (x + 1)"
1.258 +| even_plus1: "ya_odd x ==> ya_even (x + 1)"
1.259 +
1.260 +
1.261 +declare even_zero[code_pred_intro even_0]
1.262 +
1.263 +lemma [code_pred_intro odd_Suc]: "ya_even x ==> ya_odd (Suc x)"
1.264 +by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros)
1.265 +
1.266 +lemma [code_pred_intro even_Suc]:"ya_odd x ==> ya_even (Suc x)"
1.267 +by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros)
1.268 +
1.269 +code_pred ya_even
1.270 +proof -
1.271 + case ya_even
1.272 + from ya_even.prems show thesis
1.273 + proof (cases)
1.274 + case even_zero
1.275 + from even_zero even_0 show thesis by simp
1.276 + next
1.277 + case even_plus1
1.278 + from even_plus1 even_Suc show thesis by simp
1.279 + qed
1.280 +next
1.281 + case ya_odd
1.282 + from ya_odd.prems show thesis
1.283 + proof (cases)
1.284 + case odd_plus1
1.285 + from odd_plus1 odd_Suc show thesis by simp
1.286 + qed
1.287 +qed
1.288 +
1.289 +subsection {* Preprocessor Inlining *}
1.290 +
1.291 +definition "equals == (op =)"
1.292 +
1.293 +inductive zerozero' :: "nat * nat => bool" where
1.294 + "equals (x, y) (0, 0) ==> zerozero' (x, y)"
1.295 +
1.296 +code_pred (expected_modes: i => bool) zerozero' .
1.297 +
1.298 +lemma zerozero'_eq: "zerozero' x == zerozero x"
1.299 +proof -
1.300 + have "zerozero' = zerozero"
1.301 + apply (auto simp add: mem_def)
1.302 + apply (cases rule: zerozero'.cases)
1.303 + apply (auto simp add: equals_def intro: zerozero.intros)
1.304 + apply (cases rule: zerozero.cases)
1.305 + apply (auto simp add: equals_def intro: zerozero'.intros)
1.306 + done
1.307 + from this show "zerozero' x == zerozero x" by auto
1.308 +qed
1.309 +
1.310 +declare zerozero'_eq [code_pred_inline]
1.311 +
1.312 +definition "zerozero'' x == zerozero' x"
1.313 +
1.314 +text {* if preprocessing fails, zerozero'' will not have all modes. *}
1.315 +
1.316 +code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
1.317 +
1.318 +subsection {* Sets and Numerals *}
1.319 +
1.320 +definition
1.321 + "one_or_two = {Suc 0, (Suc (Suc 0))}"
1.322 +
1.323 +code_pred [inductify] one_or_two .
1.324 +
1.325 +code_pred [dseq] one_or_two .
1.326 +code_pred [random_dseq] one_or_two .
1.327 +thm one_or_two.dseq_equation
1.328 +values [expected "{Suc 0::nat, 2::nat}"] "{x. one_or_two x}"
1.329 +values [random_dseq 0,0,10] 3 "{x. one_or_two x}"
1.330 +
1.331 +inductive one_or_two' :: "nat => bool"
1.332 +where
1.333 + "one_or_two' 1"
1.334 +| "one_or_two' 2"
1.335 +
1.336 +code_pred one_or_two' .
1.337 +thm one_or_two'.equation
1.338 +
1.339 +values "{x. one_or_two' x}"
1.340 +
1.341 +definition one_or_two'':
1.342 + "one_or_two'' == {1, (2::nat)}"
1.343 +
1.344 +code_pred [inductify] one_or_two'' .
1.345 +thm one_or_two''.equation
1.346 +
1.347 +values "{x. one_or_two'' x}"
1.348 +
1.349 +subsection {* even predicate *}
1.350 +
1.351 +inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
1.352 + "even 0"
1.353 + | "even n \<Longrightarrow> odd (Suc n)"
1.354 + | "odd n \<Longrightarrow> even (Suc n)"
1.355 +
1.356 +code_pred (expected_modes: i => bool, o => bool) even .
1.357 +code_pred [dseq] even .
1.358 +code_pred [random_dseq] even .
1.359 +
1.360 +thm odd.equation
1.361 +thm even.equation
1.362 +thm odd.dseq_equation
1.363 +thm even.dseq_equation
1.364 +thm odd.random_dseq_equation
1.365 +thm even.random_dseq_equation
1.366 +
1.367 +values "{x. even 2}"
1.368 +values "{x. odd 2}"
1.369 +values 10 "{n. even n}"
1.370 +values 10 "{n. odd n}"
1.371 +values [expected "{}" dseq 2] "{x. even 6}"
1.372 +values [expected "{}" dseq 6] "{x. even 6}"
1.373 +values [expected "{()}" dseq 7] "{x. even 6}"
1.374 +values [dseq 2] "{x. odd 7}"
1.375 +values [dseq 6] "{x. odd 7}"
1.376 +values [dseq 7] "{x. odd 7}"
1.377 +values [expected "{()}" dseq 8] "{x. odd 7}"
1.378 +
1.379 +values [expected "{}" dseq 0] 8 "{x. even x}"
1.380 +values [expected "{0::nat}" dseq 1] 8 "{x. even x}"
1.381 +values [expected "{0::nat, 2}" dseq 3] 8 "{x. even x}"
1.382 +values [expected "{0::nat, 2}" dseq 4] 8 "{x. even x}"
1.383 +values [expected "{0::nat, 2, 4}" dseq 6] 8 "{x. even x}"
1.384 +
1.385 +values [random_dseq 1, 1, 0] 8 "{x. even x}"
1.386 +values [random_dseq 1, 1, 1] 8 "{x. even x}"
1.387 +values [random_dseq 1, 1, 2] 8 "{x. even x}"
1.388 +values [random_dseq 1, 1, 3] 8 "{x. even x}"
1.389 +values [random_dseq 1, 1, 6] 8 "{x. even x}"
1.390 +
1.391 +values [expected "{}" random_dseq 1, 1, 7] "{x. odd 7}"
1.392 +values [random_dseq 1, 1, 8] "{x. odd 7}"
1.393 +values [random_dseq 1, 1, 9] "{x. odd 7}"
1.394 +
1.395 +definition odd' where "odd' x == \<not> even x"
1.396 +
1.397 +code_pred (expected_modes: i => bool) [inductify] odd' .
1.398 +code_pred [dseq inductify] odd' .
1.399 +code_pred [random_dseq inductify] odd' .
1.400 +
1.401 +values [expected "{}" dseq 2] "{x. odd' 7}"
1.402 +values [expected "{()}" dseq 9] "{x. odd' 7}"
1.403 +values [expected "{}" dseq 2] "{x. odd' 8}"
1.404 +values [expected "{}" dseq 10] "{x. odd' 8}"
1.405 +
1.406 +
1.407 +inductive is_even :: "nat \<Rightarrow> bool"
1.408 +where
1.409 + "n mod 2 = 0 \<Longrightarrow> is_even n"
1.410 +
1.411 +code_pred (expected_modes: i => bool) is_even .
1.412 +
1.413 +subsection {* append predicate *}
1.414 +
1.415 +inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
1.416 + "append [] xs xs"
1.417 + | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
1.418 +
1.419 +code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix,
1.420 + i => o => i => bool as suffix, i => i => i => bool) append .
1.421 +code_pred (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as "concat", o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as "slice", o \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool as prefix,
1.422 + i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool) append .
1.423 +
1.424 +code_pred [dseq] append .
1.425 +code_pred [random_dseq] append .
1.426 +
1.427 +thm append.equation
1.428 +thm append.dseq_equation
1.429 +thm append.random_dseq_equation
1.430 +
1.431 +values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
1.432 +values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
1.433 +values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
1.434 +
1.435 +values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
1.436 +values [expected "{(([]::nat list), [Suc 0, 2, 3, 4, (5::nat)])}" dseq 1] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
1.437 +values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
1.438 +values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
1.439 +values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
1.440 +values [random_dseq 1, 1, 1] 10 "{(xs, ys, zs::int list). append xs ys zs}"
1.441 +values [random_dseq 1, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
1.442 +values [random_dseq 3, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
1.443 +values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
1.444 +values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}"
1.445 +
1.446 +value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
1.447 +value [code] "Predicate.the (slice ([]::int list))"
1.448 +
1.449 +
1.450 +text {* tricky case with alternative rules *}
1.451 +
1.452 +inductive append2
1.453 +where
1.454 + "append2 [] xs xs"
1.455 +| "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)"
1.456 +
1.457 +lemma append2_Nil: "append2 [] (xs::'b list) xs"
1.458 + by (simp add: append2.intros(1))
1.459 +
1.460 +lemmas [code_pred_intro] = append2_Nil append2.intros(2)
1.461 +
1.462 +code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool,
1.463 + i => o => i => bool, i => i => i => bool) append2
1.464 +proof -
1.465 + case append2
1.466 + from append2.prems show thesis
1.467 + proof
1.468 + fix xs
1.469 + assume "xa = []" "xb = xs" "xc = xs"
1.470 + from this append2(1) show thesis by simp
1.471 + next
1.472 + fix xs ys zs x
1.473 + assume "xa = x # xs" "xb = ys" "xc = x # zs" "append2 xs ys zs"
1.474 + from this append2(2) show thesis by fastsimp
1.475 + qed
1.476 +qed
1.477 +
1.478 +inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
1.479 +where
1.480 + "tupled_append ([], xs, xs)"
1.481 +| "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
1.482 +
1.483 +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
1.484 + i * o * i => bool, i * i * i => bool) tupled_append .
1.485 +
1.486 +code_pred (expected_modes: i \<times> i \<times> o \<Rightarrow> bool, o \<times> o \<times> i \<Rightarrow> bool, o \<times> i \<times> i \<Rightarrow> bool,
1.487 + i \<times> o \<times> i \<Rightarrow> bool, i \<times> i \<times> i \<Rightarrow> bool) tupled_append .
1.488 +
1.489 +code_pred [random_dseq] tupled_append .
1.490 +thm tupled_append.equation
1.491 +
1.492 +values "{xs. tupled_append ([(1::nat), 2, 3], [4, 5], xs)}"
1.493 +
1.494 +inductive tupled_append'
1.495 +where
1.496 +"tupled_append' ([], xs, xs)"
1.497 +| "[| ys = fst (xa, y); x # zs = snd (xa, y);
1.498 + tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)"
1.499 +
1.500 +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
1.501 + i * o * i => bool, i * i * i => bool) tupled_append' .
1.502 +thm tupled_append'.equation
1.503 +
1.504 +inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
1.505 +where
1.506 + "tupled_append'' ([], xs, xs)"
1.507 +| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
1.508 +
1.509 +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
1.510 + i * o * i => bool, i * i * i => bool) tupled_append'' .
1.511 +thm tupled_append''.equation
1.512 +
1.513 +inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
1.514 +where
1.515 + "tupled_append''' ([], xs, xs)"
1.516 +| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
1.517 +
1.518 +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
1.519 + i * o * i => bool, i * i * i => bool) tupled_append''' .
1.520 +thm tupled_append'''.equation
1.521 +
1.522 +subsection {* map_ofP predicate *}
1.523 +
1.524 +inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
1.525 +where
1.526 + "map_ofP ((a, b)#xs) a b"
1.527 +| "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
1.528 +
1.529 +code_pred (expected_modes: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP .
1.530 +thm map_ofP.equation
1.531 +
1.532 +subsection {* filter predicate *}
1.533 +
1.534 +inductive filter1
1.535 +for P
1.536 +where
1.537 + "filter1 P [] []"
1.538 +| "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)"
1.539 +| "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys"
1.540 +
1.541 +code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 .
1.542 +code_pred [dseq] filter1 .
1.543 +code_pred [random_dseq] filter1 .
1.544 +
1.545 +thm filter1.equation
1.546 +
1.547 +values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
1.548 +values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
1.549 +values [expected "{[0::nat, 2, 4]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
1.550 +
1.551 +inductive filter2
1.552 +where
1.553 + "filter2 P [] []"
1.554 +| "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)"
1.555 +| "\<not> P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys"
1.556 +
1.557 +code_pred (expected_modes: (i => bool) => i => i => bool, (i => bool) => i => o => bool) filter2 .
1.558 +code_pred [dseq] filter2 .
1.559 +code_pred [random_dseq] filter2 .
1.560 +
1.561 +thm filter2.equation
1.562 +thm filter2.random_dseq_equation
1.563 +
1.564 +inductive filter3
1.565 +for P
1.566 +where
1.567 + "List.filter P xs = ys ==> filter3 P xs ys"
1.568 +
1.569 +code_pred (expected_modes: (o => bool) => i => o => bool, (o => bool) => i => i => bool , (i => bool) => i => o => bool, (i => bool) => i => i => bool) [skip_proof] filter3 .
1.570 +
1.571 +code_pred filter3 .
1.572 +thm filter3.equation
1.573 +
1.574 +(*
1.575 +inductive filter4
1.576 +where
1.577 + "List.filter P xs = ys ==> filter4 P xs ys"
1.578 +
1.579 +code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .
1.580 +(*code_pred [depth_limited] filter4 .*)
1.581 +(*code_pred [random] filter4 .*)
1.582 +*)
1.583 +subsection {* reverse predicate *}
1.584 +
1.585 +inductive rev where
1.586 + "rev [] []"
1.587 + | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
1.588 +
1.589 +code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev .
1.590 +
1.591 +thm rev.equation
1.592 +
1.593 +values "{xs. rev [0, 1, 2, 3::nat] xs}"
1.594 +
1.595 +inductive tupled_rev where
1.596 + "tupled_rev ([], [])"
1.597 +| "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)"
1.598 +
1.599 +code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev .
1.600 +thm tupled_rev.equation
1.601 +
1.602 +subsection {* partition predicate *}
1.603 +
1.604 +inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
1.605 + for f where
1.606 + "partition f [] [] []"
1.607 + | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
1.608 + | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
1.609 +
1.610 +code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool,
1.611 + (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool)
1.612 + partition .
1.613 +code_pred [dseq] partition .
1.614 +code_pred [random_dseq] partition .
1.615 +
1.616 +values 10 "{(ys, zs). partition is_even
1.617 + [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
1.618 +values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
1.619 +values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
1.620 +
1.621 +inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool"
1.622 + for f where
1.623 + "tupled_partition f ([], [], [])"
1.624 + | "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)"
1.625 + | "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)"
1.626 +
1.627 +code_pred (expected_modes: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool,
1.628 + (i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition .
1.629 +
1.630 +thm tupled_partition.equation
1.631 +
1.632 +lemma [code_pred_intro]:
1.633 + "r a b \<Longrightarrow> tranclp r a b"
1.634 + "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
1.635 + by auto
1.636 +
1.637 +subsection {* transitive predicate *}
1.638 +
1.639 +text {* Also look at the tabled transitive closure in the Library *}
1.640 +
1.641 +code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,
1.642 + (o => i => bool) => i => i => bool, (o => i => bool) => o => i => bool as backwards_trancl, (o => o => bool) => i => i => bool, (o => o => bool) => i => o => bool,
1.643 + (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp
1.644 +proof -
1.645 + case tranclp
1.646 + from this converse_tranclpE[OF tranclp.prems] show thesis by metis
1.647 +qed
1.648 +
1.649 +
1.650 +code_pred [dseq] tranclp .
1.651 +code_pred [random_dseq] tranclp .
1.652 +thm tranclp.equation
1.653 +thm tranclp.random_dseq_equation
1.654 +
1.655 +inductive rtrancl' :: "'a => 'a => ('a => 'a => bool) => bool"
1.656 +where
1.657 + "rtrancl' x x r"
1.658 +| "r x y ==> rtrancl' y z r ==> rtrancl' x z r"
1.659 +
1.660 +code_pred [random_dseq] rtrancl' .
1.661 +
1.662 +thm rtrancl'.random_dseq_equation
1.663 +
1.664 +inductive rtrancl'' :: "('a * 'a * ('a \<Rightarrow> 'a \<Rightarrow> bool)) \<Rightarrow> bool"
1.665 +where
1.666 + "rtrancl'' (x, x, r)"
1.667 +| "r x y \<Longrightarrow> rtrancl'' (y, z, r) \<Longrightarrow> rtrancl'' (x, z, r)"
1.668 +
1.669 +code_pred rtrancl'' .
1.670 +
1.671 +inductive rtrancl''' :: "('a * ('a * 'a) * ('a * 'a => bool)) => bool"
1.672 +where
1.673 + "rtrancl''' (x, (x, x), r)"
1.674 +| "r (x, y) ==> rtrancl''' (y, (z, z), r) ==> rtrancl''' (x, (z, z), r)"
1.675 +
1.676 +code_pred rtrancl''' .
1.677 +
1.678 +
1.679 +inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
1.680 + "succ 0 1"
1.681 + | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
1.682 +
1.683 +code_pred (modes: i => i => bool, i => o => bool, o => i => bool, o => o => bool) succ .
1.684 +code_pred [random_dseq] succ .
1.685 +thm succ.equation
1.686 +thm succ.random_dseq_equation
1.687 +
1.688 +values 10 "{(m, n). succ n m}"
1.689 +values "{m. succ 0 m}"
1.690 +values "{m. succ m 0}"
1.691 +
1.692 +text {* values command needs mode annotation of the parameter succ
1.693 +to disambiguate which mode is to be chosen. *}
1.694 +
1.695 +values [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
1.696 +values [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
1.697 +values 20 "{(n, m). tranclp succ n m}"
1.698 +
1.699 +inductive example_graph :: "int => int => bool"
1.700 +where
1.701 + "example_graph 0 1"
1.702 +| "example_graph 1 2"
1.703 +| "example_graph 1 3"
1.704 +| "example_graph 4 7"
1.705 +| "example_graph 4 5"
1.706 +| "example_graph 5 6"
1.707 +| "example_graph 7 6"
1.708 +| "example_graph 7 8"
1.709 +
1.710 +inductive not_reachable_in_example_graph :: "int => int => bool"
1.711 +where "\<not> (tranclp example_graph x y) ==> not_reachable_in_example_graph x y"
1.712 +
1.713 +code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph .
1.714 +
1.715 +thm not_reachable_in_example_graph.equation
1.716 +thm tranclp.equation
1.717 +value "not_reachable_in_example_graph 0 3"
1.718 +value "not_reachable_in_example_graph 4 8"
1.719 +value "not_reachable_in_example_graph 5 6"
1.720 +text {* rtrancl compilation is strange! *}
1.721 +(*
1.722 +value "not_reachable_in_example_graph 0 4"
1.723 +value "not_reachable_in_example_graph 1 6"
1.724 +value "not_reachable_in_example_graph 8 4"*)
1.725 +
1.726 +code_pred [dseq] not_reachable_in_example_graph .
1.727 +
1.728 +values [dseq 6] "{x. tranclp example_graph 0 3}"
1.729 +
1.730 +values [dseq 0] "{x. not_reachable_in_example_graph 0 3}"
1.731 +values [dseq 0] "{x. not_reachable_in_example_graph 0 4}"
1.732 +values [dseq 20] "{x. not_reachable_in_example_graph 0 4}"
1.733 +values [dseq 6] "{x. not_reachable_in_example_graph 0 3}"
1.734 +values [dseq 3] "{x. not_reachable_in_example_graph 4 2}"
1.735 +values [dseq 6] "{x. not_reachable_in_example_graph 4 2}"
1.736 +
1.737 +
1.738 +inductive not_reachable_in_example_graph' :: "int => int => bool"
1.739 +where "\<not> (rtranclp example_graph x y) ==> not_reachable_in_example_graph' x y"
1.740 +
1.741 +code_pred not_reachable_in_example_graph' .
1.742 +
1.743 +value "not_reachable_in_example_graph' 0 3"
1.744 +(* value "not_reachable_in_example_graph' 0 5" would not terminate *)
1.745 +
1.746 +
1.747 +(*values [depth_limited 0] "{x. not_reachable_in_example_graph' 0 3}"*)
1.748 +(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
1.749 +(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"*)
1.750 +(*values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
1.751 +(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
1.752 +(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
1.753 +
1.754 +code_pred [dseq] not_reachable_in_example_graph' .
1.755 +
1.756 +(*thm not_reachable_in_example_graph'.dseq_equation*)
1.757 +
1.758 +(*values [dseq 0] "{x. not_reachable_in_example_graph' 0 3}"*)
1.759 +(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
1.760 +(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"
1.761 +values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
1.762 +(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
1.763 +(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
1.764 +
1.765 +subsection {* Free function variable *}
1.766 +
1.767 +inductive FF :: "nat => nat => bool"
1.768 +where
1.769 + "f x = y ==> FF x y"
1.770 +
1.771 +code_pred FF .
1.772 +
1.773 +subsection {* IMP *}
1.774 +
1.775 +types
1.776 + var = nat
1.777 + state = "int list"
1.778 +
1.779 +datatype com =
1.780 + Skip |
1.781 + Ass var "state => int" |
1.782 + Seq com com |
1.783 + IF "state => bool" com com |
1.784 + While "state => bool" com
1.785 +
1.786 +inductive tupled_exec :: "(com \<times> state \<times> state) \<Rightarrow> bool" where
1.787 +"tupled_exec (Skip, s, s)" |
1.788 +"tupled_exec (Ass x e, s, s[x := e(s)])" |
1.789 +"tupled_exec (c1, s1, s2) ==> tupled_exec (c2, s2, s3) ==> tupled_exec (Seq c1 c2, s1, s3)" |
1.790 +"b s ==> tupled_exec (c1, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
1.791 +"~b s ==> tupled_exec (c2, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
1.792 +"~b s ==> tupled_exec (While b c, s, s)" |
1.793 +"b s1 ==> tupled_exec (c, s1, s2) ==> tupled_exec (While b c, s2, s3) ==> tupled_exec (While b c, s1, s3)"
1.794 +
1.795 +code_pred tupled_exec .
1.796 +
1.797 +values "{s. tupled_exec (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))), [3, 5], s)}"
1.798 +
1.799 +subsection {* CCS *}
1.800 +
1.801 +text{* This example formalizes finite CCS processes without communication or
1.802 +recursion. For simplicity, labels are natural numbers. *}
1.803 +
1.804 +datatype proc = nil | pre nat proc | or proc proc | par proc proc
1.805 +
1.806 +inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
1.807 +where
1.808 +"tupled_step (pre n p, n, p)" |
1.809 +"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
1.810 +"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
1.811 +"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par q p2)" |
1.812 +"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par p1 q)"
1.813 +
1.814 +code_pred tupled_step .
1.815 +thm tupled_step.equation
1.816 +
1.817 +subsection {* divmod *}
1.818 +
1.819 +inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
1.820 + "k < l \<Longrightarrow> divmod_rel k l 0 k"
1.821 + | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
1.822 +
1.823 +code_pred divmod_rel .
1.824 +thm divmod_rel.equation
1.825 +value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
1.826 +
1.827 +subsection {* Transforming predicate logic into logic programs *}
1.828 +
1.829 +subsection {* Transforming functions into logic programs *}
1.830 +definition
1.831 + "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)"
1.832 +
1.833 +code_pred [inductify, skip_proof] case_f .
1.834 +thm case_fP.equation
1.835 +
1.836 +fun fold_map_idx where
1.837 + "fold_map_idx f i y [] = (y, [])"
1.838 +| "fold_map_idx f i y (x # xs) =
1.839 + (let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs
1.840 + in (y'', x' # xs'))"
1.841 +
1.842 +code_pred [inductify] fold_map_idx .
1.843 +
1.844 +subsection {* Minimum *}
1.845 +
1.846 +definition Min
1.847 +where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
1.848 +
1.849 +code_pred [inductify] Min .
1.850 +thm Min.equation
1.851 +
1.852 +subsection {* Lexicographic order *}
1.853 +
1.854 +declare lexord_def[code_pred_def]
1.855 +code_pred [inductify] lexord .
1.856 +code_pred [random_dseq inductify] lexord .
1.857 +
1.858 +thm lexord.equation
1.859 +thm lexord.random_dseq_equation
1.860 +
1.861 +inductive less_than_nat :: "nat * nat => bool"
1.862 +where
1.863 + "less_than_nat (0, x)"
1.864 +| "less_than_nat (x, y) ==> less_than_nat (Suc x, Suc y)"
1.865 +
1.866 +code_pred less_than_nat .
1.867 +
1.868 +code_pred [dseq] less_than_nat .
1.869 +code_pred [random_dseq] less_than_nat .
1.870 +
1.871 +inductive test_lexord :: "nat list * nat list => bool"
1.872 +where
1.873 + "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)"
1.874 +
1.875 +code_pred test_lexord .
1.876 +code_pred [dseq] test_lexord .
1.877 +code_pred [random_dseq] test_lexord .
1.878 +thm test_lexord.dseq_equation
1.879 +thm test_lexord.random_dseq_equation
1.880 +
1.881 +values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
1.882 +(*values [depth_limited 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"*)
1.883 +
1.884 +lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
1.885 +(*
1.886 +code_pred [inductify] lexn .
1.887 +thm lexn.equation
1.888 +*)
1.889 +(*
1.890 +code_pred [random_dseq inductify] lexn .
1.891 +thm lexn.random_dseq_equation
1.892 +
1.893 +values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
1.894 +*)
1.895 +inductive has_length
1.896 +where
1.897 + "has_length [] 0"
1.898 +| "has_length xs i ==> has_length (x # xs) (Suc i)"
1.899 +
1.900 +lemma has_length:
1.901 + "has_length xs n = (length xs = n)"
1.902 +proof (rule iffI)
1.903 + assume "has_length xs n"
1.904 + from this show "length xs = n"
1.905 + by (rule has_length.induct) auto
1.906 +next
1.907 + assume "length xs = n"
1.908 + from this show "has_length xs n"
1.909 + by (induct xs arbitrary: n) (auto intro: has_length.intros)
1.910 +qed
1.911 +
1.912 +lemma lexn_intros [code_pred_intro]:
1.913 + "has_length xs i ==> has_length ys i ==> r (x, y) ==> lexn r (Suc i) (x # xs, y # ys)"
1.914 + "lexn r i (xs, ys) ==> lexn r (Suc i) (x # xs, x # ys)"
1.915 +proof -
1.916 + assume "has_length xs i" "has_length ys i" "r (x, y)"
1.917 + from this has_length show "lexn r (Suc i) (x # xs, y # ys)"
1.918 + unfolding lexn_conv Collect_def mem_def
1.919 + by fastsimp
1.920 +next
1.921 + assume "lexn r i (xs, ys)"
1.922 + thm lexn_conv
1.923 + from this show "lexn r (Suc i) (x#xs, x#ys)"
1.924 + unfolding Collect_def mem_def lexn_conv
1.925 + apply auto
1.926 + apply (rule_tac x="x # xys" in exI)
1.927 + by auto
1.928 +qed
1.929 +
1.930 +code_pred [random_dseq] lexn
1.931 +proof -
1.932 + fix r n xs ys
1.933 + assume 1: "lexn r n (xs, ys)"
1.934 + assume 2: "\<And>r' i x xs' y ys'. r = r' ==> n = Suc i ==> (xs, ys) = (x # xs', y # ys') ==> has_length xs' i ==> has_length ys' i ==> r' (x, y) ==> thesis"
1.935 + assume 3: "\<And>r' i x xs' ys'. r = r' ==> n = Suc i ==> (xs, ys) = (x # xs', x # ys') ==> lexn r' i (xs', ys') ==> thesis"
1.936 + from 1 2 3 show thesis
1.937 + unfolding lexn_conv Collect_def mem_def
1.938 + apply (auto simp add: has_length)
1.939 + apply (case_tac xys)
1.940 + apply auto
1.941 + apply fastsimp
1.942 + apply fastsimp done
1.943 +qed
1.944 +
1.945 +values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
1.946 +
1.947 +code_pred [inductify, skip_proof] lex .
1.948 +thm lex.equation
1.949 +thm lex_def
1.950 +declare lenlex_conv[code_pred_def]
1.951 +code_pred [inductify, skip_proof] lenlex .
1.952 +thm lenlex.equation
1.953 +
1.954 +code_pred [random_dseq inductify] lenlex .
1.955 +thm lenlex.random_dseq_equation
1.956 +
1.957 +values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}"
1.958 +
1.959 +thm lists.intros
1.960 +code_pred [inductify] lists .
1.961 +thm lists.equation
1.962 +
1.963 +subsection {* AVL Tree *}
1.964 +
1.965 +datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
1.966 +fun height :: "'a tree => nat" where
1.967 +"height ET = 0"
1.968 +| "height (MKT x l r h) = max (height l) (height r) + 1"
1.969 +
1.970 +primrec avl :: "'a tree => bool"
1.971 +where
1.972 + "avl ET = True"
1.973 +| "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and>
1.974 + h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
1.975 +(*
1.976 +code_pred [inductify] avl .
1.977 +thm avl.equation*)
1.978 +
1.979 +code_pred [new_random_dseq inductify] avl .
1.980 +thm avl.new_random_dseq_equation
1.981 +
1.982 +values [new_random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
1.983 +
1.984 +fun set_of
1.985 +where
1.986 +"set_of ET = {}"
1.987 +| "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"
1.988 +
1.989 +fun is_ord :: "nat tree => bool"
1.990 +where
1.991 +"is_ord ET = True"
1.992 +| "is_ord (MKT n l r h) =
1.993 + ((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)"
1.994 +
1.995 +code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of .
1.996 +thm set_of.equation
1.997 +
1.998 +code_pred (expected_modes: i => bool) [inductify] is_ord .
1.999 +thm is_ord_aux.equation
1.1000 +thm is_ord.equation
1.1001 +
1.1002 +subsection {* Definitions about Relations *}
1.1003 +
1.1004 +term "converse"
1.1005 +code_pred (modes:
1.1006 + (i * i => bool) => i * i => bool,
1.1007 + (i * o => bool) => o * i => bool,
1.1008 + (i * o => bool) => i * i => bool,
1.1009 + (o * i => bool) => i * o => bool,
1.1010 + (o * i => bool) => i * i => bool,
1.1011 + (o * o => bool) => o * o => bool,
1.1012 + (o * o => bool) => i * o => bool,
1.1013 + (o * o => bool) => o * i => bool,
1.1014 + (o * o => bool) => i * i => bool) [inductify] converse .
1.1015 +
1.1016 +thm converse.equation
1.1017 +code_pred [inductify] rel_comp .
1.1018 +thm rel_comp.equation
1.1019 +code_pred [inductify] Image .
1.1020 +thm Image.equation
1.1021 +declare singleton_iff[code_pred_inline]
1.1022 +declare Id_on_def[unfolded Bex_def UNION_def singleton_iff, code_pred_def]
1.1023 +
1.1024 +code_pred (expected_modes:
1.1025 + (o => bool) => o => bool,
1.1026 + (o => bool) => i * o => bool,
1.1027 + (o => bool) => o * i => bool,
1.1028 + (o => bool) => i => bool,
1.1029 + (i => bool) => i * o => bool,
1.1030 + (i => bool) => o * i => bool,
1.1031 + (i => bool) => i => bool) [inductify] Id_on .
1.1032 +thm Id_on.equation
1.1033 +thm Domain_def
1.1034 +code_pred (modes:
1.1035 + (o * o => bool) => o => bool,
1.1036 + (o * o => bool) => i => bool,
1.1037 + (i * o => bool) => i => bool) [inductify] Domain .
1.1038 +thm Domain.equation
1.1039 +
1.1040 +thm Range_def
1.1041 +code_pred (modes:
1.1042 + (o * o => bool) => o => bool,
1.1043 + (o * o => bool) => i => bool,
1.1044 + (o * i => bool) => i => bool) [inductify] Range .
1.1045 +thm Range.equation
1.1046 +
1.1047 +code_pred [inductify] Field .
1.1048 +thm Field.equation
1.1049 +
1.1050 +thm refl_on_def
1.1051 +code_pred [inductify] refl_on .
1.1052 +thm refl_on.equation
1.1053 +code_pred [inductify] total_on .
1.1054 +thm total_on.equation
1.1055 +code_pred [inductify] antisym .
1.1056 +thm antisym.equation
1.1057 +code_pred [inductify] trans .
1.1058 +thm trans.equation
1.1059 +code_pred [inductify] single_valued .
1.1060 +thm single_valued.equation
1.1061 +thm inv_image_def
1.1062 +code_pred [inductify] inv_image .
1.1063 +thm inv_image.equation
1.1064 +
1.1065 +subsection {* Inverting list functions *}
1.1066 +
1.1067 +code_pred [inductify] size_list .
1.1068 +code_pred [new_random_dseq inductify] size_list .
1.1069 +thm size_listP.equation
1.1070 +thm size_listP.new_random_dseq_equation
1.1071 +
1.1072 +values [new_random_dseq 2,3,10] 3 "{xs. size_listP (xs::nat list) (5::nat)}"
1.1073 +
1.1074 +code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat .
1.1075 +thm concatP.equation
1.1076 +
1.1077 +values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
1.1078 +values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}"
1.1079 +
1.1080 +code_pred [dseq inductify] List.concat .
1.1081 +thm concatP.dseq_equation
1.1082 +
1.1083 +values [dseq 3] 3
1.1084 + "{xs. concatP xs ([0] :: nat list)}"
1.1085 +
1.1086 +values [dseq 5] 3
1.1087 + "{xs. concatP xs ([1] :: int list)}"
1.1088 +
1.1089 +values [dseq 5] 3
1.1090 + "{xs. concatP xs ([1] :: nat list)}"
1.1091 +
1.1092 +values [dseq 5] 3
1.1093 + "{xs. concatP xs [(1::int), 2]}"
1.1094 +
1.1095 +code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd .
1.1096 +thm hdP.equation
1.1097 +values "{x. hdP [1, 2, (3::int)] x}"
1.1098 +values "{(xs, x). hdP [1, 2, (3::int)] 1}"
1.1099 +
1.1100 +code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] tl .
1.1101 +thm tlP.equation
1.1102 +values "{x. tlP [1, 2, (3::nat)] x}"
1.1103 +values "{x. tlP [1, 2, (3::int)] [3]}"
1.1104 +
1.1105 +code_pred [inductify, skip_proof] last .
1.1106 +thm lastP.equation
1.1107 +
1.1108 +code_pred [inductify, skip_proof] butlast .
1.1109 +thm butlastP.equation
1.1110 +
1.1111 +code_pred [inductify, skip_proof] take .
1.1112 +thm takeP.equation
1.1113 +
1.1114 +code_pred [inductify, skip_proof] drop .
1.1115 +thm dropP.equation
1.1116 +code_pred [inductify, skip_proof] zip .
1.1117 +thm zipP.equation
1.1118 +
1.1119 +code_pred [inductify, skip_proof] upt .
1.1120 +code_pred [inductify, skip_proof] remdups .
1.1121 +thm remdupsP.equation
1.1122 +code_pred [dseq inductify] remdups .
1.1123 +values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
1.1124 +
1.1125 +code_pred [inductify, skip_proof] remove1 .
1.1126 +thm remove1P.equation
1.1127 +values "{xs. remove1P 1 xs [2, (3::int)]}"
1.1128 +
1.1129 +code_pred [inductify, skip_proof] removeAll .
1.1130 +thm removeAllP.equation
1.1131 +code_pred [dseq inductify] removeAll .
1.1132 +
1.1133 +values [dseq 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}"
1.1134 +
1.1135 +code_pred [inductify] distinct .
1.1136 +thm distinct.equation
1.1137 +code_pred [inductify, skip_proof] replicate .
1.1138 +thm replicateP.equation
1.1139 +values 5 "{(n, xs). replicateP n (0::int) xs}"
1.1140 +
1.1141 +code_pred [inductify, skip_proof] splice .
1.1142 +thm splice.simps
1.1143 +thm spliceP.equation
1.1144 +
1.1145 +values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
1.1146 +
1.1147 +code_pred [inductify, skip_proof] List.rev .
1.1148 +code_pred [inductify] map .
1.1149 +code_pred [inductify] foldr .
1.1150 +code_pred [inductify] foldl .
1.1151 +code_pred [inductify] filter .
1.1152 +code_pred [random_dseq inductify] filter .
1.1153 +
1.1154 +section {* Function predicate replacement *}
1.1155 +
1.1156 +text {*
1.1157 +If the mode analysis uses the functional mode, we
1.1158 +replace predicates that resulted from functions again by their functions.
1.1159 +*}
1.1160 +
1.1161 +inductive test_append
1.1162 +where
1.1163 + "List.append xs ys = zs ==> test_append xs ys zs"
1.1164 +
1.1165 +code_pred [inductify, skip_proof] test_append .
1.1166 +thm test_append.equation
1.1167 +
1.1168 +text {* If append is not turned into a predicate, then the mode
1.1169 + o => o => i => bool could not be inferred. *}
1.1170 +
1.1171 +values 4 "{(xs::int list, ys). test_append xs ys [1, 2, 3, 4]}"
1.1172 +
1.1173 +text {* If appendP is not reverted back to a function, then mode i => i => o => bool
1.1174 + fails after deleting the predicate equation. *}
1.1175 +
1.1176 +declare appendP.equation[code del]
1.1177 +
1.1178 +values "{xs::int list. test_append [1,2] [3,4] xs}"
1.1179 +values "{xs::int list. test_append (replicate 1000 1) (replicate 1000 2) xs}"
1.1180 +values "{xs::int list. test_append (replicate 2000 1) (replicate 2000 2) xs}"
1.1181 +
1.1182 +text {* Redeclaring append.equation as code equation *}
1.1183 +
1.1184 +declare appendP.equation[code]
1.1185 +
1.1186 +subsection {* Function with tuples *}
1.1187 +
1.1188 +fun append'
1.1189 +where
1.1190 + "append' ([], ys) = ys"
1.1191 +| "append' (x # xs, ys) = x # append' (xs, ys)"
1.1192 +
1.1193 +inductive test_append'
1.1194 +where
1.1195 + "append' (xs, ys) = zs ==> test_append' xs ys zs"
1.1196 +
1.1197 +code_pred [inductify, skip_proof] test_append' .
1.1198 +
1.1199 +thm test_append'.equation
1.1200 +
1.1201 +values "{(xs::int list, ys). test_append' xs ys [1, 2, 3, 4]}"
1.1202 +
1.1203 +declare append'P.equation[code del]
1.1204 +
1.1205 +values "{zs :: int list. test_append' [1,2,3] [4,5] zs}"
1.1206 +
1.1207 +section {* Arithmetic examples *}
1.1208 +
1.1209 +subsection {* Examples on nat *}
1.1210 +
1.1211 +inductive plus_nat_test :: "nat => nat => nat => bool"
1.1212 +where
1.1213 + "x + y = z ==> plus_nat_test x y z"
1.1214 +
1.1215 +code_pred [inductify, skip_proof] plus_nat_test .
1.1216 +code_pred [new_random_dseq inductify] plus_nat_test .
1.1217 +
1.1218 +thm plus_nat_test.equation
1.1219 +thm plus_nat_test.new_random_dseq_equation
1.1220 +
1.1221 +values [expected "{9::nat}"] "{z. plus_nat_test 4 5 z}"
1.1222 +values [expected "{9::nat}"] "{z. plus_nat_test 7 2 z}"
1.1223 +values [expected "{4::nat}"] "{y. plus_nat_test 5 y 9}"
1.1224 +values [expected "{}"] "{y. plus_nat_test 9 y 8}"
1.1225 +values [expected "{6::nat}"] "{y. plus_nat_test 1 y 7}"
1.1226 +values [expected "{2::nat}"] "{x. plus_nat_test x 7 9}"
1.1227 +values [expected "{}"] "{x. plus_nat_test x 9 7}"
1.1228 +values [expected "{(0::nat,0::nat)}"] "{(x, y). plus_nat_test x y 0}"
1.1229 +values [expected "{(0, Suc 0), (Suc 0, 0)}"] "{(x, y). plus_nat_test x y 1}"
1.1230 +values [expected "{(0, 5), (4, Suc 0), (3, 2), (2, 3), (Suc 0, 4), (5, 0)}"]
1.1231 + "{(x, y). plus_nat_test x y 5}"
1.1232 +
1.1233 +inductive minus_nat_test :: "nat => nat => nat => bool"
1.1234 +where
1.1235 + "x - y = z ==> minus_nat_test x y z"
1.1236 +
1.1237 +code_pred [inductify, skip_proof] minus_nat_test .
1.1238 +code_pred [new_random_dseq inductify] minus_nat_test .
1.1239 +
1.1240 +thm minus_nat_test.equation
1.1241 +thm minus_nat_test.new_random_dseq_equation
1.1242 +
1.1243 +values [expected "{0::nat}"] "{z. minus_nat_test 4 5 z}"
1.1244 +values [expected "{5::nat}"] "{z. minus_nat_test 7 2 z}"
1.1245 +values [expected "{16::nat}"] "{x. minus_nat_test x 7 9}"
1.1246 +values [expected "{16::nat}"] "{x. minus_nat_test x 9 7}"
1.1247 +values [expected "{0, Suc 0, 2, 3}"] "{x. minus_nat_test x 3 0}"
1.1248 +values [expected "{0::nat}"] "{x. minus_nat_test x 0 0}"
1.1249 +
1.1250 +subsection {* Examples on int *}
1.1251 +
1.1252 +inductive plus_int_test :: "int => int => int => bool"
1.1253 +where
1.1254 + "a + b = c ==> plus_int_test a b c"
1.1255 +
1.1256 +code_pred [inductify, skip_proof] plus_int_test .
1.1257 +code_pred [new_random_dseq inductify] plus_int_test .
1.1258 +
1.1259 +thm plus_int_test.equation
1.1260 +thm plus_int_test.new_random_dseq_equation
1.1261 +
1.1262 +values [expected "{1::int}"] "{a. plus_int_test a 6 7}"
1.1263 +values [expected "{1::int}"] "{b. plus_int_test 6 b 7}"
1.1264 +values [expected "{11::int}"] "{c. plus_int_test 5 6 c}"
1.1265 +
1.1266 +inductive minus_int_test :: "int => int => int => bool"
1.1267 +where
1.1268 + "a - b = c ==> minus_int_test a b c"
1.1269 +
1.1270 +code_pred [inductify, skip_proof] minus_int_test .
1.1271 +code_pred [new_random_dseq inductify] minus_int_test .
1.1272 +
1.1273 +thm minus_int_test.equation
1.1274 +thm minus_int_test.new_random_dseq_equation
1.1275 +
1.1276 +values [expected "{4::int}"] "{c. minus_int_test 9 5 c}"
1.1277 +values [expected "{9::int}"] "{a. minus_int_test a 4 5}"
1.1278 +values [expected "{- 1::int}"] "{b. minus_int_test 4 b 5}"
1.1279 +
1.1280 +subsection {* minus on bool *}
1.1281 +
1.1282 +inductive All :: "nat => bool"
1.1283 +where
1.1284 + "All x"
1.1285 +
1.1286 +inductive None :: "nat => bool"
1.1287 +
1.1288 +definition "test_minus_bool x = (None x - All x)"
1.1289 +
1.1290 +code_pred [inductify] test_minus_bool .
1.1291 +thm test_minus_bool.equation
1.1292 +
1.1293 +values "{x. test_minus_bool x}"
1.1294 +
1.1295 +subsection {* Functions *}
1.1296 +
1.1297 +fun partial_hd :: "'a list => 'a option"
1.1298 +where
1.1299 + "partial_hd [] = Option.None"
1.1300 +| "partial_hd (x # xs) = Some x"
1.1301 +
1.1302 +inductive hd_predicate
1.1303 +where
1.1304 + "partial_hd xs = Some x ==> hd_predicate xs x"
1.1305 +
1.1306 +code_pred (expected_modes: i => i => bool, i => o => bool) hd_predicate .
1.1307 +
1.1308 +thm hd_predicate.equation
1.1309 +
1.1310 +subsection {* Locales *}
1.1311 +
1.1312 +inductive hd_predicate2 :: "('a list => 'a option) => 'a list => 'a => bool"
1.1313 +where
1.1314 + "partial_hd' xs = Some x ==> hd_predicate2 partial_hd' xs x"
1.1315 +
1.1316 +
1.1317 +thm hd_predicate2.intros
1.1318 +
1.1319 +code_pred (expected_modes: i => i => i => bool, i => i => o => bool) hd_predicate2 .
1.1320 +thm hd_predicate2.equation
1.1321 +
1.1322 +locale A = fixes partial_hd :: "'a list => 'a option" begin
1.1323 +
1.1324 +inductive hd_predicate_in_locale :: "'a list => 'a => bool"
1.1325 +where
1.1326 + "partial_hd xs = Some x ==> hd_predicate_in_locale xs x"
1.1327 +
1.1328 +end
1.1329 +
1.1330 +text {* The global introduction rules must be redeclared as introduction rules and then
1.1331 + one could invoke code_pred. *}
1.1332 +
1.1333 +declare A.hd_predicate_in_locale.intros [unfolded Predicate.eq_is_eq[symmetric], code_pred_intro]
1.1334 +
1.1335 +code_pred (expected_modes: i => i => i => bool, i => i => o => bool) A.hd_predicate_in_locale
1.1336 +unfolding eq_is_eq by (auto elim: A.hd_predicate_in_locale.cases)
1.1337 +
1.1338 +interpretation A partial_hd .
1.1339 +thm hd_predicate_in_locale.intros
1.1340 +text {* A locally compliant solution with a trivial interpretation fails, because
1.1341 +the predicate compiler has very strict assumptions about the terms and their structure. *}
1.1342 +
1.1343 +(*code_pred hd_predicate_in_locale .*)
1.1344 +
1.1345 +section {* Integer example *}
1.1346 +
1.1347 +definition three :: int
1.1348 +where "three = 3"
1.1349 +
1.1350 +inductive is_three
1.1351 +where
1.1352 + "is_three three"
1.1353 +
1.1354 +code_pred is_three .
1.1355 +
1.1356 +thm is_three.equation
1.1357 +
1.1358 +section {* String.literal example *}
1.1359 +
1.1360 +definition Error_1
1.1361 +where
1.1362 + "Error_1 = STR ''Error 1''"
1.1363 +
1.1364 +definition Error_2
1.1365 +where
1.1366 + "Error_2 = STR ''Error 2''"
1.1367 +
1.1368 +inductive "is_error" :: "String.literal \<Rightarrow> bool"
1.1369 +where
1.1370 + "is_error Error_1"
1.1371 +| "is_error Error_2"
1.1372 +
1.1373 +code_pred is_error .
1.1374 +
1.1375 +thm is_error.equation
1.1376 +
1.1377 +inductive is_error' :: "String.literal \<Rightarrow> bool"
1.1378 +where
1.1379 + "is_error' (STR ''Error1'')"
1.1380 +| "is_error' (STR ''Error2'')"
1.1381 +
1.1382 +code_pred is_error' .
1.1383 +
1.1384 +thm is_error'.equation
1.1385 +
1.1386 +datatype ErrorObject = Error String.literal int
1.1387 +
1.1388 +inductive is_error'' :: "ErrorObject \<Rightarrow> bool"
1.1389 +where
1.1390 + "is_error'' (Error Error_1 3)"
1.1391 +| "is_error'' (Error Error_2 4)"
1.1392 +
1.1393 +code_pred is_error'' .
1.1394 +
1.1395 +thm is_error''.equation
1.1396 +
1.1397 +section {* Another function example *}
1.1398 +
1.1399 +consts f :: "'a \<Rightarrow> 'a"
1.1400 +
1.1401 +inductive fun_upd :: "(('a * 'b) * ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
1.1402 +where
1.1403 + "fun_upd ((x, a), s) (s(x := f a))"
1.1404 +
1.1405 +code_pred fun_upd .
1.1406 +
1.1407 +thm fun_upd.equation
1.1408 +
1.1409 +section {* Examples for detecting switches *}
1.1410 +
1.1411 +inductive detect_switches1 where
1.1412 + "detect_switches1 [] []"
1.1413 +| "detect_switches1 (x # xs) (y # ys)"
1.1414 +
1.1415 +code_pred [detect_switches, skip_proof] detect_switches1 .
1.1416 +
1.1417 +thm detect_switches1.equation
1.1418 +
1.1419 +inductive detect_switches2 :: "('a => bool) => bool"
1.1420 +where
1.1421 + "detect_switches2 P"
1.1422 +
1.1423 +code_pred [detect_switches, skip_proof] detect_switches2 .
1.1424 +thm detect_switches2.equation
1.1425 +
1.1426 +inductive detect_switches3 :: "('a => bool) => 'a list => bool"
1.1427 +where
1.1428 + "detect_switches3 P []"
1.1429 +| "detect_switches3 P (x # xs)"
1.1430 +
1.1431 +code_pred [detect_switches, skip_proof] detect_switches3 .
1.1432 +
1.1433 +thm detect_switches3.equation
1.1434 +
1.1435 +inductive detect_switches4 :: "('a => bool) => 'a list => 'a list => bool"
1.1436 +where
1.1437 + "detect_switches4 P [] []"
1.1438 +| "detect_switches4 P (x # xs) (y # ys)"
1.1439 +
1.1440 +code_pred [detect_switches, skip_proof] detect_switches4 .
1.1441 +thm detect_switches4.equation
1.1442 +
1.1443 +inductive detect_switches5 :: "('a => 'a => bool) => 'a list => 'a list => bool"
1.1444 +where
1.1445 + "detect_switches5 P [] []"
1.1446 +| "detect_switches5 P xs ys ==> P x y ==> detect_switches5 P (x # xs) (y # ys)"
1.1447 +
1.1448 +code_pred [detect_switches, skip_proof] detect_switches5 .
1.1449 +
1.1450 +thm detect_switches5.equation
1.1451 +
1.1452 +inductive detect_switches6 :: "(('a => 'b => bool) * 'a list * 'b list) => bool"
1.1453 +where
1.1454 + "detect_switches6 (P, [], [])"
1.1455 +| "detect_switches6 (P, xs, ys) ==> P x y ==> detect_switches6 (P, x # xs, y # ys)"
1.1456 +
1.1457 +code_pred [detect_switches, skip_proof] detect_switches6 .
1.1458 +
1.1459 +inductive detect_switches7 :: "('a => bool) => ('b => bool) => ('a * 'b list) => bool"
1.1460 +where
1.1461 + "detect_switches7 P Q (a, [])"
1.1462 +| "P a ==> Q x ==> detect_switches7 P Q (a, x#xs)"
1.1463 +
1.1464 +code_pred [skip_proof] detect_switches7 .
1.1465 +
1.1466 +thm detect_switches7.equation
1.1467 +
1.1468 +inductive detect_switches8 :: "nat => bool"
1.1469 +where
1.1470 + "detect_switches8 0"
1.1471 +| "x mod 2 = 0 ==> detect_switches8 (Suc x)"
1.1472 +
1.1473 +code_pred [detect_switches, skip_proof] detect_switches8 .
1.1474 +
1.1475 +thm detect_switches8.equation
1.1476 +
1.1477 +inductive detect_switches9 :: "nat => nat => bool"
1.1478 +where
1.1479 + "detect_switches9 0 0"
1.1480 +| "detect_switches9 0 (Suc x)"
1.1481 +| "detect_switches9 (Suc x) 0"
1.1482 +| "x = y ==> detect_switches9 (Suc x) (Suc y)"
1.1483 +| "c1 = c2 ==> detect_switches9 c1 c2"
1.1484 +
1.1485 +code_pred [detect_switches, skip_proof] detect_switches9 .
1.1486 +
1.1487 +thm detect_switches9.equation
1.1488 +
1.1489 +
1.1490 +
1.1491 +end