src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
changeset 39655 8ad7fe9d6f0b
child 39657 5e57675b7e40
     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