moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
1.1 --- a/src/HOL/IsaMakefile Tue Mar 23 19:03:05 2010 -0700
1.2 +++ b/src/HOL/IsaMakefile Wed Mar 24 17:40:43 2010 +0100
1.3 @@ -55,6 +55,7 @@
1.4 HOL-Number_Theory \
1.5 HOL-Old_Number_Theory \
1.6 HOL-Quotient_Examples \
1.7 + HOL-Predicate_Compile_Examples \
1.8 HOL-Prolog \
1.9 HOL-Proofs-Extraction \
1.10 HOL-Proofs-Lambda \
1.11 @@ -964,7 +965,7 @@
1.12 ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \
1.13 ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \
1.14 ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy \
1.15 - ex/Predicate_Compile_ex.thy ex/Predicate_Compile_Quickcheck.thy \
1.16 + ex/Predicate_Compile_Quickcheck.thy \
1.17 ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy \
1.18 ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \
1.19 ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
1.20 @@ -1282,6 +1283,13 @@
1.21 Quotient_Examples/LarryInt.thy Quotient_Examples/LarryDatatype.thy
1.22 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
1.23
1.24 +## HOL-Predicate_Compile_Examples
1.25 +
1.26 +HOL-Predicate_Compile_Examples: HOL $(LOG)/HOL-Predicate_Compile_Examples.gz
1.27 +
1.28 +$(LOG)/HOL-Predicate_Compile_Examples.gz: $(OUT)/HOL \
1.29 + Predicate_Compile_Examples/ROOT.ML Predicate_Compile_Examples/Predicate_Compile_Examples.thy
1.30 + @$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples
1.31
1.32 ## clean
1.33
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Wed Mar 24 17:40:43 2010 +0100
2.3 @@ -0,0 +1,1278 @@
2.4 +theory Predicate_Compile_Examples
2.5 +imports "../ex/Predicate_Compile_Alternative_Defs"
2.6 +begin
2.7 +
2.8 +subsection {* Basic predicates *}
2.9 +
2.10 +inductive False' :: "bool"
2.11 +
2.12 +code_pred (expected_modes: bool) False' .
2.13 +code_pred [dseq] False' .
2.14 +code_pred [random_dseq] False' .
2.15 +
2.16 +values [expected "{}" pred] "{x. False'}"
2.17 +values [expected "{}" dseq 1] "{x. False'}"
2.18 +values [expected "{}" random_dseq 1, 1, 1] "{x. False'}"
2.19 +
2.20 +value "False'"
2.21 +
2.22 +
2.23 +inductive True' :: "bool"
2.24 +where
2.25 + "True ==> True'"
2.26 +
2.27 +code_pred True' .
2.28 +code_pred [dseq] True' .
2.29 +code_pred [random_dseq] True' .
2.30 +
2.31 +thm True'.equation
2.32 +thm True'.dseq_equation
2.33 +thm True'.random_dseq_equation
2.34 +values [expected "{()}" ]"{x. True'}"
2.35 +values [expected "{}" dseq 0] "{x. True'}"
2.36 +values [expected "{()}" dseq 1] "{x. True'}"
2.37 +values [expected "{()}" dseq 2] "{x. True'}"
2.38 +values [expected "{}" random_dseq 1, 1, 0] "{x. True'}"
2.39 +values [expected "{}" random_dseq 1, 1, 1] "{x. True'}"
2.40 +values [expected "{()}" random_dseq 1, 1, 2] "{x. True'}"
2.41 +values [expected "{()}" random_dseq 1, 1, 3] "{x. True'}"
2.42 +
2.43 +inductive EmptySet :: "'a \<Rightarrow> bool"
2.44 +
2.45 +code_pred (expected_modes: o => bool, i => bool) EmptySet .
2.46 +
2.47 +definition EmptySet' :: "'a \<Rightarrow> bool"
2.48 +where "EmptySet' = {}"
2.49 +
2.50 +code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
2.51 +
2.52 +inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
2.53 +
2.54 +code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel .
2.55 +
2.56 +inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
2.57 +for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
2.58 +
2.59 +code_pred
2.60 + (expected_modes: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool,
2.61 + (o => o => bool) => o => i => bool, (o => o => bool) => i => i => bool,
2.62 + (i => o => bool) => o => o => bool, (i => o => bool) => i => o => bool,
2.63 + (i => o => bool) => o => i => bool, (i => o => bool) => i => i => bool,
2.64 + (o => i => bool) => o => o => bool, (o => i => bool) => i => o => bool,
2.65 + (o => i => bool) => o => i => bool, (o => i => bool) => i => i => bool,
2.66 + (i => i => bool) => o => o => bool, (i => i => bool) => i => o => bool,
2.67 + (i => i => bool) => o => i => bool, (i => i => bool) => i => i => bool)
2.68 + EmptyClosure .
2.69 +
2.70 +thm EmptyClosure.equation
2.71 +
2.72 +(* TODO: inductive package is broken!
2.73 +inductive False'' :: "bool"
2.74 +where
2.75 + "False \<Longrightarrow> False''"
2.76 +
2.77 +code_pred (expected_modes: []) False'' .
2.78 +
2.79 +inductive EmptySet'' :: "'a \<Rightarrow> bool"
2.80 +where
2.81 + "False \<Longrightarrow> EmptySet'' x"
2.82 +
2.83 +code_pred (expected_modes: [1]) EmptySet'' .
2.84 +code_pred (expected_modes: [], [1]) [inductify] EmptySet'' .
2.85 +*)
2.86 +
2.87 +consts a' :: 'a
2.88 +
2.89 +inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
2.90 +where
2.91 +"Fact a' a'"
2.92 +
2.93 +code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact .
2.94 +
2.95 +inductive zerozero :: "nat * nat => bool"
2.96 +where
2.97 + "zerozero (0, 0)"
2.98 +
2.99 +code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero .
2.100 +code_pred [dseq] zerozero .
2.101 +code_pred [random_dseq] zerozero .
2.102 +
2.103 +thm zerozero.equation
2.104 +thm zerozero.dseq_equation
2.105 +thm zerozero.random_dseq_equation
2.106 +
2.107 +text {* We expect the user to expand the tuples in the values command.
2.108 +The following values command is not supported. *}
2.109 +(*values "{x. zerozero x}" *)
2.110 +text {* Instead, the user must type *}
2.111 +values "{(x, y). zerozero (x, y)}"
2.112 +
2.113 +values [expected "{}" dseq 0] "{(x, y). zerozero (x, y)}"
2.114 +values [expected "{(0::nat, 0::nat)}" dseq 1] "{(x, y). zerozero (x, y)}"
2.115 +values [expected "{(0::nat, 0::nat)}" dseq 2] "{(x, y). zerozero (x, y)}"
2.116 +values [expected "{}" random_dseq 1, 1, 2] "{(x, y). zerozero (x, y)}"
2.117 +values [expected "{(0::nat, 0:: nat)}" random_dseq 1, 1, 3] "{(x, y). zerozero (x, y)}"
2.118 +
2.119 +inductive nested_tuples :: "((int * int) * int * int) => bool"
2.120 +where
2.121 + "nested_tuples ((0, 1), 2, 3)"
2.122 +
2.123 +code_pred nested_tuples .
2.124 +
2.125 +inductive JamesBond :: "nat => int => code_numeral => bool"
2.126 +where
2.127 + "JamesBond 0 0 7"
2.128 +
2.129 +code_pred JamesBond .
2.130 +
2.131 +values [expected "{(0::nat, 0::int , 7::code_numeral)}"] "{(a, b, c). JamesBond a b c}"
2.132 +values [expected "{(0::nat, 7::code_numeral, 0:: int)}"] "{(a, c, b). JamesBond a b c}"
2.133 +values [expected "{(0::int, 0::nat, 7::code_numeral)}"] "{(b, a, c). JamesBond a b c}"
2.134 +values [expected "{(0::int, 7::code_numeral, 0::nat)}"] "{(b, c, a). JamesBond a b c}"
2.135 +values [expected "{(7::code_numeral, 0::nat, 0::int)}"] "{(c, a, b). JamesBond a b c}"
2.136 +values [expected "{(7::code_numeral, 0::int, 0::nat)}"] "{(c, b, a). JamesBond a b c}"
2.137 +
2.138 +values [expected "{(7::code_numeral, 0::int)}"] "{(a, b). JamesBond 0 b a}"
2.139 +values [expected "{(7::code_numeral, 0::nat)}"] "{(c, a). JamesBond a 0 c}"
2.140 +values [expected "{(0::nat, 7::code_numeral)}"] "{(a, c). JamesBond a 0 c}"
2.141 +
2.142 +
2.143 +subsection {* Alternative Rules *}
2.144 +
2.145 +datatype char = C | D | E | F | G | H
2.146 +
2.147 +inductive is_C_or_D
2.148 +where
2.149 + "(x = C) \<or> (x = D) ==> is_C_or_D x"
2.150 +
2.151 +code_pred (expected_modes: i => bool) is_C_or_D .
2.152 +thm is_C_or_D.equation
2.153 +
2.154 +inductive is_D_or_E
2.155 +where
2.156 + "(x = D) \<or> (x = E) ==> is_D_or_E x"
2.157 +
2.158 +lemma [code_pred_intro]:
2.159 + "is_D_or_E D"
2.160 +by (auto intro: is_D_or_E.intros)
2.161 +
2.162 +lemma [code_pred_intro]:
2.163 + "is_D_or_E E"
2.164 +by (auto intro: is_D_or_E.intros)
2.165 +
2.166 +code_pred (expected_modes: o => bool, i => bool) is_D_or_E
2.167 +proof -
2.168 + case is_D_or_E
2.169 + from this(1) show thesis
2.170 + proof
2.171 + fix xa
2.172 + assume x: "x = xa"
2.173 + assume "xa = D \<or> xa = E"
2.174 + from this show thesis
2.175 + proof
2.176 + assume "xa = D" from this x is_D_or_E(2) show thesis by simp
2.177 + next
2.178 + assume "xa = E" from this x is_D_or_E(3) show thesis by simp
2.179 + qed
2.180 + qed
2.181 +qed
2.182 +
2.183 +thm is_D_or_E.equation
2.184 +
2.185 +inductive is_F_or_G
2.186 +where
2.187 + "x = F \<or> x = G ==> is_F_or_G x"
2.188 +
2.189 +lemma [code_pred_intro]:
2.190 + "is_F_or_G F"
2.191 +by (auto intro: is_F_or_G.intros)
2.192 +
2.193 +lemma [code_pred_intro]:
2.194 + "is_F_or_G G"
2.195 +by (auto intro: is_F_or_G.intros)
2.196 +
2.197 +inductive is_FGH
2.198 +where
2.199 + "is_F_or_G x ==> is_FGH x"
2.200 +| "is_FGH H"
2.201 +
2.202 +text {* Compilation of is_FGH requires elimination rule for is_F_or_G *}
2.203 +
2.204 +code_pred (expected_modes: o => bool, i => bool) is_FGH
2.205 +proof -
2.206 + case is_F_or_G
2.207 + from this(1) show thesis
2.208 + proof
2.209 + fix xa
2.210 + assume x: "x = xa"
2.211 + assume "xa = F \<or> xa = G"
2.212 + from this show thesis
2.213 + proof
2.214 + assume "xa = F"
2.215 + from this x is_F_or_G(2) show thesis by simp
2.216 + next
2.217 + assume "xa = G"
2.218 + from this x is_F_or_G(3) show thesis by simp
2.219 + qed
2.220 + qed
2.221 +qed
2.222 +
2.223 +subsection {* Preprocessor Inlining *}
2.224 +
2.225 +definition "equals == (op =)"
2.226 +
2.227 +inductive zerozero' :: "nat * nat => bool" where
2.228 + "equals (x, y) (0, 0) ==> zerozero' (x, y)"
2.229 +
2.230 +code_pred (expected_modes: i => bool) zerozero' .
2.231 +
2.232 +lemma zerozero'_eq: "zerozero' x == zerozero x"
2.233 +proof -
2.234 + have "zerozero' = zerozero"
2.235 + apply (auto simp add: mem_def)
2.236 + apply (cases rule: zerozero'.cases)
2.237 + apply (auto simp add: equals_def intro: zerozero.intros)
2.238 + apply (cases rule: zerozero.cases)
2.239 + apply (auto simp add: equals_def intro: zerozero'.intros)
2.240 + done
2.241 + from this show "zerozero' x == zerozero x" by auto
2.242 +qed
2.243 +
2.244 +declare zerozero'_eq [code_pred_inline]
2.245 +
2.246 +definition "zerozero'' x == zerozero' x"
2.247 +
2.248 +text {* if preprocessing fails, zerozero'' will not have all modes. *}
2.249 +
2.250 +code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
2.251 +
2.252 +subsection {* Sets and Numerals *}
2.253 +
2.254 +definition
2.255 + "one_or_two = {Suc 0, (Suc (Suc 0))}"
2.256 +
2.257 +code_pred [inductify] one_or_two .
2.258 +
2.259 +code_pred [dseq] one_or_two .
2.260 +code_pred [random_dseq] one_or_two .
2.261 +thm one_or_two.dseq_equation
2.262 +values [expected "{Suc 0::nat, 2::nat}"] "{x. one_or_two x}"
2.263 +values [random_dseq 0,0,10] 3 "{x. one_or_two x}"
2.264 +
2.265 +inductive one_or_two' :: "nat => bool"
2.266 +where
2.267 + "one_or_two' 1"
2.268 +| "one_or_two' 2"
2.269 +
2.270 +code_pred one_or_two' .
2.271 +thm one_or_two'.equation
2.272 +
2.273 +values "{x. one_or_two' x}"
2.274 +
2.275 +definition one_or_two'':
2.276 + "one_or_two'' == {1, (2::nat)}"
2.277 +
2.278 +code_pred [inductify] one_or_two'' .
2.279 +thm one_or_two''.equation
2.280 +
2.281 +values "{x. one_or_two'' x}"
2.282 +
2.283 +subsection {* even predicate *}
2.284 +
2.285 +inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
2.286 + "even 0"
2.287 + | "even n \<Longrightarrow> odd (Suc n)"
2.288 + | "odd n \<Longrightarrow> even (Suc n)"
2.289 +
2.290 +code_pred (expected_modes: i => bool, o => bool) even .
2.291 +code_pred [dseq] even .
2.292 +code_pred [random_dseq] even .
2.293 +
2.294 +thm odd.equation
2.295 +thm even.equation
2.296 +thm odd.dseq_equation
2.297 +thm even.dseq_equation
2.298 +thm odd.random_dseq_equation
2.299 +thm even.random_dseq_equation
2.300 +
2.301 +values "{x. even 2}"
2.302 +values "{x. odd 2}"
2.303 +values 10 "{n. even n}"
2.304 +values 10 "{n. odd n}"
2.305 +values [expected "{}" dseq 2] "{x. even 6}"
2.306 +values [expected "{}" dseq 6] "{x. even 6}"
2.307 +values [expected "{()}" dseq 7] "{x. even 6}"
2.308 +values [dseq 2] "{x. odd 7}"
2.309 +values [dseq 6] "{x. odd 7}"
2.310 +values [dseq 7] "{x. odd 7}"
2.311 +values [expected "{()}" dseq 8] "{x. odd 7}"
2.312 +
2.313 +values [expected "{}" dseq 0] 8 "{x. even x}"
2.314 +values [expected "{0::nat}" dseq 1] 8 "{x. even x}"
2.315 +values [expected "{0::nat, 2}" dseq 3] 8 "{x. even x}"
2.316 +values [expected "{0::nat, 2}" dseq 4] 8 "{x. even x}"
2.317 +values [expected "{0::nat, 2, 4}" dseq 6] 8 "{x. even x}"
2.318 +
2.319 +values [random_dseq 1, 1, 0] 8 "{x. even x}"
2.320 +values [random_dseq 1, 1, 1] 8 "{x. even x}"
2.321 +values [random_dseq 1, 1, 2] 8 "{x. even x}"
2.322 +values [random_dseq 1, 1, 3] 8 "{x. even x}"
2.323 +values [random_dseq 1, 1, 6] 8 "{x. even x}"
2.324 +
2.325 +values [expected "{}" random_dseq 1, 1, 7] "{x. odd 7}"
2.326 +values [random_dseq 1, 1, 8] "{x. odd 7}"
2.327 +values [random_dseq 1, 1, 9] "{x. odd 7}"
2.328 +
2.329 +definition odd' where "odd' x == \<not> even x"
2.330 +
2.331 +code_pred (expected_modes: i => bool) [inductify] odd' .
2.332 +code_pred [dseq inductify] odd' .
2.333 +code_pred [random_dseq inductify] odd' .
2.334 +
2.335 +values [expected "{}" dseq 2] "{x. odd' 7}"
2.336 +values [expected "{()}" dseq 9] "{x. odd' 7}"
2.337 +values [expected "{}" dseq 2] "{x. odd' 8}"
2.338 +values [expected "{}" dseq 10] "{x. odd' 8}"
2.339 +
2.340 +
2.341 +inductive is_even :: "nat \<Rightarrow> bool"
2.342 +where
2.343 + "n mod 2 = 0 \<Longrightarrow> is_even n"
2.344 +
2.345 +code_pred (expected_modes: i => bool) is_even .
2.346 +
2.347 +subsection {* append predicate *}
2.348 +
2.349 +inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
2.350 + "append [] xs xs"
2.351 + | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
2.352 +
2.353 +code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix,
2.354 + i => o => i => bool as suffix, i => i => i => bool) append .
2.355 +code_pred [dseq] append .
2.356 +code_pred [random_dseq] append .
2.357 +
2.358 +thm append.equation
2.359 +thm append.dseq_equation
2.360 +thm append.random_dseq_equation
2.361 +
2.362 +values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
2.363 +values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
2.364 +values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
2.365 +
2.366 +values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
2.367 +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)]}"
2.368 +values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
2.369 +values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
2.370 +values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
2.371 +values [random_dseq 1, 1, 1] 10 "{(xs, ys, zs::int list). append xs ys zs}"
2.372 +values [random_dseq 1, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
2.373 +values [random_dseq 3, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
2.374 +values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
2.375 +values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}"
2.376 +
2.377 +value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
2.378 +value [code] "Predicate.the (slice ([]::int list))"
2.379 +
2.380 +
2.381 +text {* tricky case with alternative rules *}
2.382 +
2.383 +inductive append2
2.384 +where
2.385 + "append2 [] xs xs"
2.386 +| "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)"
2.387 +
2.388 +lemma append2_Nil: "append2 [] (xs::'b list) xs"
2.389 + by (simp add: append2.intros(1))
2.390 +
2.391 +lemmas [code_pred_intro] = append2_Nil append2.intros(2)
2.392 +
2.393 +code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool,
2.394 + i => o => i => bool, i => i => i => bool) append2
2.395 +proof -
2.396 + case append2
2.397 + from append2(1) show thesis
2.398 + proof
2.399 + fix xs
2.400 + assume "xa = []" "xb = xs" "xc = xs"
2.401 + from this append2(2) show thesis by simp
2.402 + next
2.403 + fix xs ys zs x
2.404 + assume "xa = x # xs" "xb = ys" "xc = x # zs" "append2 xs ys zs"
2.405 + from this append2(3) show thesis by fastsimp
2.406 + qed
2.407 +qed
2.408 +
2.409 +inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
2.410 +where
2.411 + "tupled_append ([], xs, xs)"
2.412 +| "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
2.413 +
2.414 +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
2.415 + i * o * i => bool, i * i * i => bool) tupled_append .
2.416 +code_pred [random_dseq] tupled_append .
2.417 +thm tupled_append.equation
2.418 +
2.419 +values "{xs. tupled_append ([(1::nat), 2, 3], [4, 5], xs)}"
2.420 +
2.421 +inductive tupled_append'
2.422 +where
2.423 +"tupled_append' ([], xs, xs)"
2.424 +| "[| ys = fst (xa, y); x # zs = snd (xa, y);
2.425 + tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)"
2.426 +
2.427 +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
2.428 + i * o * i => bool, i * i * i => bool) tupled_append' .
2.429 +thm tupled_append'.equation
2.430 +
2.431 +inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
2.432 +where
2.433 + "tupled_append'' ([], xs, xs)"
2.434 +| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
2.435 +
2.436 +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
2.437 + i * o * i => bool, i * i * i => bool) tupled_append'' .
2.438 +thm tupled_append''.equation
2.439 +
2.440 +inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
2.441 +where
2.442 + "tupled_append''' ([], xs, xs)"
2.443 +| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
2.444 +
2.445 +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
2.446 + i * o * i => bool, i * i * i => bool) tupled_append''' .
2.447 +thm tupled_append'''.equation
2.448 +
2.449 +subsection {* map_ofP predicate *}
2.450 +
2.451 +inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
2.452 +where
2.453 + "map_ofP ((a, b)#xs) a b"
2.454 +| "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
2.455 +
2.456 +code_pred (expected_modes: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP .
2.457 +thm map_ofP.equation
2.458 +
2.459 +subsection {* filter predicate *}
2.460 +
2.461 +inductive filter1
2.462 +for P
2.463 +where
2.464 + "filter1 P [] []"
2.465 +| "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)"
2.466 +| "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys"
2.467 +
2.468 +code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 .
2.469 +code_pred [dseq] filter1 .
2.470 +code_pred [random_dseq] filter1 .
2.471 +
2.472 +thm filter1.equation
2.473 +
2.474 +values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
2.475 +values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
2.476 +values [expected "{[0::nat, 2, 4]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
2.477 +
2.478 +inductive filter2
2.479 +where
2.480 + "filter2 P [] []"
2.481 +| "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)"
2.482 +| "\<not> P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys"
2.483 +
2.484 +code_pred (expected_modes: (i => bool) => i => i => bool, (i => bool) => i => o => bool) filter2 .
2.485 +code_pred [dseq] filter2 .
2.486 +code_pred [random_dseq] filter2 .
2.487 +
2.488 +thm filter2.equation
2.489 +thm filter2.random_dseq_equation
2.490 +
2.491 +(*
2.492 +inductive filter3
2.493 +for P
2.494 +where
2.495 + "List.filter P xs = ys ==> filter3 P xs ys"
2.496 +
2.497 +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 .
2.498 +
2.499 +code_pred [dseq] filter3 .
2.500 +thm filter3.dseq_equation
2.501 +*)
2.502 +(*
2.503 +inductive filter4
2.504 +where
2.505 + "List.filter P xs = ys ==> filter4 P xs ys"
2.506 +
2.507 +code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .
2.508 +(*code_pred [depth_limited] filter4 .*)
2.509 +(*code_pred [random] filter4 .*)
2.510 +*)
2.511 +subsection {* reverse predicate *}
2.512 +
2.513 +inductive rev where
2.514 + "rev [] []"
2.515 + | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
2.516 +
2.517 +code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev .
2.518 +
2.519 +thm rev.equation
2.520 +
2.521 +values "{xs. rev [0, 1, 2, 3::nat] xs}"
2.522 +
2.523 +inductive tupled_rev where
2.524 + "tupled_rev ([], [])"
2.525 +| "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)"
2.526 +
2.527 +code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev .
2.528 +thm tupled_rev.equation
2.529 +
2.530 +subsection {* partition predicate *}
2.531 +
2.532 +inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
2.533 + for f where
2.534 + "partition f [] [] []"
2.535 + | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
2.536 + | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
2.537 +
2.538 +code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool,
2.539 + (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool)
2.540 + partition .
2.541 +code_pred [dseq] partition .
2.542 +code_pred [random_dseq] partition .
2.543 +
2.544 +values 10 "{(ys, zs). partition is_even
2.545 + [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
2.546 +values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
2.547 +values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
2.548 +
2.549 +inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool"
2.550 + for f where
2.551 + "tupled_partition f ([], [], [])"
2.552 + | "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)"
2.553 + | "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)"
2.554 +
2.555 +code_pred (expected_modes: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool,
2.556 + (i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition .
2.557 +
2.558 +thm tupled_partition.equation
2.559 +
2.560 +lemma [code_pred_intro]:
2.561 + "r a b \<Longrightarrow> tranclp r a b"
2.562 + "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
2.563 + by auto
2.564 +
2.565 +subsection {* transitive predicate *}
2.566 +
2.567 +text {* Also look at the tabled transitive closure in the Library *}
2.568 +
2.569 +code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,
2.570 + (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,
2.571 + (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp
2.572 +proof -
2.573 + case tranclp
2.574 + from this converse_tranclpE[OF this(1)] show thesis by metis
2.575 +qed
2.576 +
2.577 +
2.578 +code_pred [dseq] tranclp .
2.579 +code_pred [random_dseq] tranclp .
2.580 +thm tranclp.equation
2.581 +thm tranclp.random_dseq_equation
2.582 +
2.583 +inductive rtrancl' :: "'a => 'a => ('a => 'a => bool) => bool"
2.584 +where
2.585 + "rtrancl' x x r"
2.586 +| "r x y ==> rtrancl' y z r ==> rtrancl' x z r"
2.587 +
2.588 +code_pred [random_dseq] rtrancl' .
2.589 +
2.590 +thm rtrancl'.random_dseq_equation
2.591 +
2.592 +inductive rtrancl'' :: "('a * 'a * ('a \<Rightarrow> 'a \<Rightarrow> bool)) \<Rightarrow> bool"
2.593 +where
2.594 + "rtrancl'' (x, x, r)"
2.595 +| "r x y \<Longrightarrow> rtrancl'' (y, z, r) \<Longrightarrow> rtrancl'' (x, z, r)"
2.596 +
2.597 +code_pred rtrancl'' .
2.598 +
2.599 +inductive rtrancl''' :: "('a * ('a * 'a) * ('a * 'a => bool)) => bool"
2.600 +where
2.601 + "rtrancl''' (x, (x, x), r)"
2.602 +| "r (x, y) ==> rtrancl''' (y, (z, z), r) ==> rtrancl''' (x, (z, z), r)"
2.603 +
2.604 +code_pred rtrancl''' .
2.605 +
2.606 +
2.607 +inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
2.608 + "succ 0 1"
2.609 + | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
2.610 +
2.611 +code_pred (modes: i => i => bool, i => o => bool, o => i => bool, o => o => bool) succ .
2.612 +code_pred [random_dseq] succ .
2.613 +thm succ.equation
2.614 +thm succ.random_dseq_equation
2.615 +
2.616 +values 10 "{(m, n). succ n m}"
2.617 +values "{m. succ 0 m}"
2.618 +values "{m. succ m 0}"
2.619 +
2.620 +text {* values command needs mode annotation of the parameter succ
2.621 +to disambiguate which mode is to be chosen. *}
2.622 +
2.623 +values [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
2.624 +values [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
2.625 +values 20 "{(n, m). tranclp succ n m}"
2.626 +
2.627 +inductive example_graph :: "int => int => bool"
2.628 +where
2.629 + "example_graph 0 1"
2.630 +| "example_graph 1 2"
2.631 +| "example_graph 1 3"
2.632 +| "example_graph 4 7"
2.633 +| "example_graph 4 5"
2.634 +| "example_graph 5 6"
2.635 +| "example_graph 7 6"
2.636 +| "example_graph 7 8"
2.637 +
2.638 +inductive not_reachable_in_example_graph :: "int => int => bool"
2.639 +where "\<not> (tranclp example_graph x y) ==> not_reachable_in_example_graph x y"
2.640 +
2.641 +code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph .
2.642 +
2.643 +thm not_reachable_in_example_graph.equation
2.644 +thm tranclp.equation
2.645 +value "not_reachable_in_example_graph 0 3"
2.646 +value "not_reachable_in_example_graph 4 8"
2.647 +value "not_reachable_in_example_graph 5 6"
2.648 +text {* rtrancl compilation is strange! *}
2.649 +(*
2.650 +value "not_reachable_in_example_graph 0 4"
2.651 +value "not_reachable_in_example_graph 1 6"
2.652 +value "not_reachable_in_example_graph 8 4"*)
2.653 +
2.654 +code_pred [dseq] not_reachable_in_example_graph .
2.655 +
2.656 +values [dseq 6] "{x. tranclp example_graph 0 3}"
2.657 +
2.658 +values [dseq 0] "{x. not_reachable_in_example_graph 0 3}"
2.659 +values [dseq 0] "{x. not_reachable_in_example_graph 0 4}"
2.660 +values [dseq 20] "{x. not_reachable_in_example_graph 0 4}"
2.661 +values [dseq 6] "{x. not_reachable_in_example_graph 0 3}"
2.662 +values [dseq 3] "{x. not_reachable_in_example_graph 4 2}"
2.663 +values [dseq 6] "{x. not_reachable_in_example_graph 4 2}"
2.664 +
2.665 +
2.666 +inductive not_reachable_in_example_graph' :: "int => int => bool"
2.667 +where "\<not> (rtranclp example_graph x y) ==> not_reachable_in_example_graph' x y"
2.668 +
2.669 +code_pred not_reachable_in_example_graph' .
2.670 +
2.671 +value "not_reachable_in_example_graph' 0 3"
2.672 +(* value "not_reachable_in_example_graph' 0 5" would not terminate *)
2.673 +
2.674 +
2.675 +(*values [depth_limited 0] "{x. not_reachable_in_example_graph' 0 3}"*)
2.676 +(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
2.677 +(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"*)
2.678 +(*values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
2.679 +(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
2.680 +(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
2.681 +
2.682 +code_pred [dseq] not_reachable_in_example_graph' .
2.683 +
2.684 +(*thm not_reachable_in_example_graph'.dseq_equation*)
2.685 +
2.686 +(*values [dseq 0] "{x. not_reachable_in_example_graph' 0 3}"*)
2.687 +(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
2.688 +(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"
2.689 +values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
2.690 +(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
2.691 +(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
2.692 +
2.693 +
2.694 +subsection {* IMP *}
2.695 +
2.696 +types
2.697 + var = nat
2.698 + state = "int list"
2.699 +
2.700 +datatype com =
2.701 + Skip |
2.702 + Ass var "state => int" |
2.703 + Seq com com |
2.704 + IF "state => bool" com com |
2.705 + While "state => bool" com
2.706 +
2.707 +inductive exec :: "com => state => state => bool" where
2.708 +"exec Skip s s" |
2.709 +"exec (Ass x e) s (s[x := e(s)])" |
2.710 +"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
2.711 +"b s ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
2.712 +"~b s ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
2.713 +"~b s ==> exec (While b c) s s" |
2.714 +"b s1 ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
2.715 +
2.716 +code_pred exec .
2.717 +
2.718 +values "{t. exec
2.719 + (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))))
2.720 + [3,5] t}"
2.721 +
2.722 +
2.723 +inductive tupled_exec :: "(com \<times> state \<times> state) \<Rightarrow> bool" where
2.724 +"tupled_exec (Skip, s, s)" |
2.725 +"tupled_exec (Ass x e, s, s[x := e(s)])" |
2.726 +"tupled_exec (c1, s1, s2) ==> tupled_exec (c2, s2, s3) ==> tupled_exec (Seq c1 c2, s1, s3)" |
2.727 +"b s ==> tupled_exec (c1, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
2.728 +"~b s ==> tupled_exec (c2, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
2.729 +"~b s ==> tupled_exec (While b c, s, s)" |
2.730 +"b s1 ==> tupled_exec (c, s1, s2) ==> tupled_exec (While b c, s2, s3) ==> tupled_exec (While b c, s1, s3)"
2.731 +
2.732 +code_pred tupled_exec .
2.733 +
2.734 +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)}"
2.735 +
2.736 +subsection {* CCS *}
2.737 +
2.738 +text{* This example formalizes finite CCS processes without communication or
2.739 +recursion. For simplicity, labels are natural numbers. *}
2.740 +
2.741 +datatype proc = nil | pre nat proc | or proc proc | par proc proc
2.742 +
2.743 +inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where
2.744 +"step (pre n p) n p" |
2.745 +"step p1 a q \<Longrightarrow> step (or p1 p2) a q" |
2.746 +"step p2 a q \<Longrightarrow> step (or p1 p2) a q" |
2.747 +"step p1 a q \<Longrightarrow> step (par p1 p2) a (par q p2)" |
2.748 +"step p2 a q \<Longrightarrow> step (par p1 p2) a (par p1 q)"
2.749 +
2.750 +code_pred step .
2.751 +
2.752 +inductive steps where
2.753 +"steps p [] p" |
2.754 +"step p a q \<Longrightarrow> steps q as r \<Longrightarrow> steps p (a#as) r"
2.755 +
2.756 +code_pred steps .
2.757 +
2.758 +values 3
2.759 + "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
2.760 +
2.761 +values 5
2.762 + "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
2.763 +
2.764 +values 3 "{(a,q). step (par nil nil) a q}"
2.765 +
2.766 +
2.767 +inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
2.768 +where
2.769 +"tupled_step (pre n p, n, p)" |
2.770 +"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
2.771 +"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
2.772 +"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par q p2)" |
2.773 +"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par p1 q)"
2.774 +
2.775 +code_pred tupled_step .
2.776 +thm tupled_step.equation
2.777 +
2.778 +subsection {* divmod *}
2.779 +
2.780 +inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
2.781 + "k < l \<Longrightarrow> divmod_rel k l 0 k"
2.782 + | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
2.783 +
2.784 +code_pred divmod_rel ..
2.785 +thm divmod_rel.equation
2.786 +value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
2.787 +
2.788 +subsection {* Transforming predicate logic into logic programs *}
2.789 +
2.790 +subsection {* Transforming functions into logic programs *}
2.791 +definition
2.792 + "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)"
2.793 +
2.794 +code_pred [inductify] case_f .
2.795 +thm case_fP.equation
2.796 +thm case_fP.intros
2.797 +
2.798 +fun fold_map_idx where
2.799 + "fold_map_idx f i y [] = (y, [])"
2.800 +| "fold_map_idx f i y (x # xs) =
2.801 + (let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs
2.802 + in (y'', x' # xs'))"
2.803 +
2.804 +text {* mode analysis explores thousand modes - this is infeasible at the moment... *}
2.805 +(*code_pred [inductify, show_steps] fold_map_idx .*)
2.806 +
2.807 +subsection {* Minimum *}
2.808 +
2.809 +definition Min
2.810 +where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
2.811 +
2.812 +code_pred [inductify] Min .
2.813 +thm Min.equation
2.814 +
2.815 +subsection {* Lexicographic order *}
2.816 +
2.817 +declare lexord_def[code_pred_def]
2.818 +code_pred [inductify] lexord .
2.819 +code_pred [random_dseq inductify] lexord .
2.820 +
2.821 +thm lexord.equation
2.822 +thm lexord.random_dseq_equation
2.823 +
2.824 +inductive less_than_nat :: "nat * nat => bool"
2.825 +where
2.826 + "less_than_nat (0, x)"
2.827 +| "less_than_nat (x, y) ==> less_than_nat (Suc x, Suc y)"
2.828 +
2.829 +code_pred less_than_nat .
2.830 +
2.831 +code_pred [dseq] less_than_nat .
2.832 +code_pred [random_dseq] less_than_nat .
2.833 +
2.834 +inductive test_lexord :: "nat list * nat list => bool"
2.835 +where
2.836 + "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)"
2.837 +
2.838 +code_pred test_lexord .
2.839 +code_pred [dseq] test_lexord .
2.840 +code_pred [random_dseq] test_lexord .
2.841 +thm test_lexord.dseq_equation
2.842 +thm test_lexord.random_dseq_equation
2.843 +
2.844 +values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
2.845 +(*values [depth_limited 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"*)
2.846 +
2.847 +declare list.size(3,4)[code_pred_def]
2.848 +lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
2.849 +(*
2.850 +code_pred [inductify] lexn .
2.851 +thm lexn.equation
2.852 +*)
2.853 +(*
2.854 +code_pred [random_dseq inductify] lexn .
2.855 +thm lexn.random_dseq_equation
2.856 +
2.857 +values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
2.858 +*)
2.859 +inductive has_length
2.860 +where
2.861 + "has_length [] 0"
2.862 +| "has_length xs i ==> has_length (x # xs) (Suc i)"
2.863 +
2.864 +lemma has_length:
2.865 + "has_length xs n = (length xs = n)"
2.866 +proof (rule iffI)
2.867 + assume "has_length xs n"
2.868 + from this show "length xs = n"
2.869 + by (rule has_length.induct) auto
2.870 +next
2.871 + assume "length xs = n"
2.872 + from this show "has_length xs n"
2.873 + by (induct xs arbitrary: n) (auto intro: has_length.intros)
2.874 +qed
2.875 +
2.876 +lemma lexn_intros [code_pred_intro]:
2.877 + "has_length xs i ==> has_length ys i ==> r (x, y) ==> lexn r (Suc i) (x # xs, y # ys)"
2.878 + "lexn r i (xs, ys) ==> lexn r (Suc i) (x # xs, x # ys)"
2.879 +proof -
2.880 + assume "has_length xs i" "has_length ys i" "r (x, y)"
2.881 + from this has_length show "lexn r (Suc i) (x # xs, y # ys)"
2.882 + unfolding lexn_conv Collect_def mem_def
2.883 + by fastsimp
2.884 +next
2.885 + assume "lexn r i (xs, ys)"
2.886 + thm lexn_conv
2.887 + from this show "lexn r (Suc i) (x#xs, x#ys)"
2.888 + unfolding Collect_def mem_def lexn_conv
2.889 + apply auto
2.890 + apply (rule_tac x="x # xys" in exI)
2.891 + by auto
2.892 +qed
2.893 +
2.894 +code_pred [random_dseq inductify] lexn
2.895 +proof -
2.896 + fix r n xs ys
2.897 + assume 1: "lexn r n (xs, ys)"
2.898 + 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"
2.899 + 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"
2.900 + from 1 2 3 show thesis
2.901 + unfolding lexn_conv Collect_def mem_def
2.902 + apply (auto simp add: has_length)
2.903 + apply (case_tac xys)
2.904 + apply auto
2.905 + apply fastsimp
2.906 + apply fastsimp done
2.907 +qed
2.908 +
2.909 +
2.910 +values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
2.911 +thm lenlex_conv
2.912 +thm lex_conv
2.913 +declare list.size(3,4)[code_pred_def]
2.914 +(*code_pred [inductify, show_steps, show_intermediate_results] length .*)
2.915 +setup {* Predicate_Compile_Data.ignore_consts [@{const_name Orderings.top_class.top}] *}
2.916 +code_pred [inductify] lex .
2.917 +thm lex.equation
2.918 +thm lex_def
2.919 +declare lenlex_conv[code_pred_def]
2.920 +code_pred [inductify] lenlex .
2.921 +thm lenlex.equation
2.922 +
2.923 +code_pred [random_dseq inductify] lenlex .
2.924 +thm lenlex.random_dseq_equation
2.925 +
2.926 +values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}"
2.927 +thm lists.intros
2.928 +
2.929 +code_pred [inductify] lists .
2.930 +thm lists.equation
2.931 +
2.932 +subsection {* AVL Tree *}
2.933 +
2.934 +datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
2.935 +fun height :: "'a tree => nat" where
2.936 +"height ET = 0"
2.937 +| "height (MKT x l r h) = max (height l) (height r) + 1"
2.938 +
2.939 +consts avl :: "'a tree => bool"
2.940 +primrec
2.941 + "avl ET = True"
2.942 + "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and>
2.943 + h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
2.944 +(*
2.945 +code_pred [inductify] avl .
2.946 +thm avl.equation*)
2.947 +
2.948 +code_pred [random_dseq inductify] avl .
2.949 +thm avl.random_dseq_equation
2.950 +
2.951 +values [random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
2.952 +
2.953 +fun set_of
2.954 +where
2.955 +"set_of ET = {}"
2.956 +| "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"
2.957 +
2.958 +fun is_ord :: "nat tree => bool"
2.959 +where
2.960 +"is_ord ET = True"
2.961 +| "is_ord (MKT n l r h) =
2.962 + ((\<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)"
2.963 +
2.964 +code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of .
2.965 +thm set_of.equation
2.966 +
2.967 +code_pred (expected_modes: i => bool) [inductify] is_ord .
2.968 +thm is_ord_aux.equation
2.969 +thm is_ord.equation
2.970 +
2.971 +
2.972 +subsection {* Definitions about Relations *}
2.973 +term "converse"
2.974 +code_pred (modes:
2.975 + (i * i => bool) => i * i => bool,
2.976 + (i * o => bool) => o * i => bool,
2.977 + (i * o => bool) => i * i => bool,
2.978 + (o * i => bool) => i * o => bool,
2.979 + (o * i => bool) => i * i => bool,
2.980 + (o * o => bool) => o * o => bool,
2.981 + (o * o => bool) => i * o => bool,
2.982 + (o * o => bool) => o * i => bool,
2.983 + (o * o => bool) => i * i => bool) [inductify] converse .
2.984 +
2.985 +thm converse.equation
2.986 +code_pred [inductify] rel_comp .
2.987 +thm rel_comp.equation
2.988 +code_pred [inductify] Image .
2.989 +thm Image.equation
2.990 +declare singleton_iff[code_pred_inline]
2.991 +declare Id_on_def[unfolded Bex_def UNION_def singleton_iff, code_pred_def]
2.992 +
2.993 +code_pred (expected_modes:
2.994 + (o => bool) => o => bool,
2.995 + (o => bool) => i * o => bool,
2.996 + (o => bool) => o * i => bool,
2.997 + (o => bool) => i => bool,
2.998 + (i => bool) => i * o => bool,
2.999 + (i => bool) => o * i => bool,
2.1000 + (i => bool) => i => bool) [inductify] Id_on .
2.1001 +thm Id_on.equation
2.1002 +thm Domain_def
2.1003 +code_pred (modes:
2.1004 + (o * o => bool) => o => bool,
2.1005 + (o * o => bool) => i => bool,
2.1006 + (i * o => bool) => i => bool) [inductify] Domain .
2.1007 +thm Domain.equation
2.1008 +
2.1009 +thm Range_def
2.1010 +code_pred (modes:
2.1011 + (o * o => bool) => o => bool,
2.1012 + (o * o => bool) => i => bool,
2.1013 + (o * i => bool) => i => bool) [inductify] Range .
2.1014 +thm Range.equation
2.1015 +
2.1016 +code_pred [inductify] Field .
2.1017 +thm Field.equation
2.1018 +
2.1019 +thm refl_on_def
2.1020 +code_pred [inductify] refl_on .
2.1021 +thm refl_on.equation
2.1022 +code_pred [inductify] total_on .
2.1023 +thm total_on.equation
2.1024 +code_pred [inductify] antisym .
2.1025 +thm antisym.equation
2.1026 +code_pred [inductify] trans .
2.1027 +thm trans.equation
2.1028 +code_pred [inductify] single_valued .
2.1029 +thm single_valued.equation
2.1030 +thm inv_image_def
2.1031 +code_pred [inductify] inv_image .
2.1032 +thm inv_image.equation
2.1033 +
2.1034 +subsection {* Inverting list functions *}
2.1035 +
2.1036 +(*code_pred [inductify] length .
2.1037 +code_pred [random inductify] length .
2.1038 +thm size_listP.equation
2.1039 +thm size_listP.random_equation
2.1040 +*)
2.1041 +(*values [random] 1 "{xs. size_listP (xs::nat list) (5::nat)}"*)
2.1042 +
2.1043 +code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify] List.concat .
2.1044 +thm concatP.equation
2.1045 +
2.1046 +values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
2.1047 +values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}"
2.1048 +
2.1049 +code_pred [dseq inductify] List.concat .
2.1050 +thm concatP.dseq_equation
2.1051 +
2.1052 +values [dseq 3] 3
2.1053 + "{xs. concatP xs ([0] :: nat list)}"
2.1054 +
2.1055 +values [dseq 5] 3
2.1056 + "{xs. concatP xs ([1] :: int list)}"
2.1057 +
2.1058 +values [dseq 5] 3
2.1059 + "{xs. concatP xs ([1] :: nat list)}"
2.1060 +
2.1061 +values [dseq 5] 3
2.1062 + "{xs. concatP xs [(1::int), 2]}"
2.1063 +
2.1064 +code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd .
2.1065 +thm hdP.equation
2.1066 +values "{x. hdP [1, 2, (3::int)] x}"
2.1067 +values "{(xs, x). hdP [1, 2, (3::int)] 1}"
2.1068 +
2.1069 +code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] tl .
2.1070 +thm tlP.equation
2.1071 +values "{x. tlP [1, 2, (3::nat)] x}"
2.1072 +values "{x. tlP [1, 2, (3::int)] [3]}"
2.1073 +
2.1074 +code_pred [inductify] last .
2.1075 +thm lastP.equation
2.1076 +
2.1077 +code_pred [inductify] butlast .
2.1078 +thm butlastP.equation
2.1079 +
2.1080 +code_pred [inductify] take .
2.1081 +thm takeP.equation
2.1082 +
2.1083 +code_pred [inductify] drop .
2.1084 +thm dropP.equation
2.1085 +code_pred [inductify] zip .
2.1086 +thm zipP.equation
2.1087 +
2.1088 +code_pred [inductify] upt .
2.1089 +code_pred [inductify] remdups .
2.1090 +thm remdupsP.equation
2.1091 +code_pred [dseq inductify] remdups .
2.1092 +values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
2.1093 +
2.1094 +code_pred [inductify] remove1 .
2.1095 +thm remove1P.equation
2.1096 +values "{xs. remove1P 1 xs [2, (3::int)]}"
2.1097 +
2.1098 +code_pred [inductify] removeAll .
2.1099 +thm removeAllP.equation
2.1100 +code_pred [dseq inductify] removeAll .
2.1101 +
2.1102 +values [dseq 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}"
2.1103 +
2.1104 +code_pred [inductify] distinct .
2.1105 +thm distinct.equation
2.1106 +code_pred [inductify] replicate .
2.1107 +thm replicateP.equation
2.1108 +values 5 "{(n, xs). replicateP n (0::int) xs}"
2.1109 +
2.1110 +code_pred [inductify] splice .
2.1111 +thm splice.simps
2.1112 +thm spliceP.equation
2.1113 +
2.1114 +values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
2.1115 +
2.1116 +code_pred [inductify] List.rev .
2.1117 +code_pred [inductify] map .
2.1118 +code_pred [inductify] foldr .
2.1119 +code_pred [inductify] foldl .
2.1120 +code_pred [inductify] filter .
2.1121 +code_pred [random_dseq inductify] filter .
2.1122 +
2.1123 +subsection {* Context Free Grammar *}
2.1124 +
2.1125 +datatype alphabet = a | b
2.1126 +
2.1127 +inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
2.1128 + "[] \<in> S\<^isub>1"
2.1129 +| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
2.1130 +| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
2.1131 +| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
2.1132 +| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
2.1133 +| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
2.1134 +
2.1135 +code_pred [inductify] S\<^isub>1p .
2.1136 +code_pred [random_dseq inductify] S\<^isub>1p .
2.1137 +thm S\<^isub>1p.equation
2.1138 +thm S\<^isub>1p.random_dseq_equation
2.1139 +
2.1140 +values [random_dseq 5, 5, 5] 5 "{x. S\<^isub>1p x}"
2.1141 +
2.1142 +inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
2.1143 + "[] \<in> S\<^isub>2"
2.1144 +| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
2.1145 +| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
2.1146 +| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
2.1147 +| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
2.1148 +| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
2.1149 +
2.1150 +code_pred [random_dseq inductify] S\<^isub>2p .
2.1151 +thm S\<^isub>2p.random_dseq_equation
2.1152 +thm A\<^isub>2p.random_dseq_equation
2.1153 +thm B\<^isub>2p.random_dseq_equation
2.1154 +
2.1155 +values [random_dseq 5, 5, 5] 10 "{x. S\<^isub>2p x}"
2.1156 +
2.1157 +inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
2.1158 + "[] \<in> S\<^isub>3"
2.1159 +| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
2.1160 +| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
2.1161 +| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
2.1162 +| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
2.1163 +| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
2.1164 +
2.1165 +code_pred [inductify] S\<^isub>3p .
2.1166 +thm S\<^isub>3p.equation
2.1167 +
2.1168 +values 10 "{x. S\<^isub>3p x}"
2.1169 +
2.1170 +inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
2.1171 + "[] \<in> S\<^isub>4"
2.1172 +| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
2.1173 +| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
2.1174 +| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
2.1175 +| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
2.1176 +| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
2.1177 +| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
2.1178 +
2.1179 +code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p .
2.1180 +
2.1181 +subsection {* Lambda *}
2.1182 +
2.1183 +datatype type =
2.1184 + Atom nat
2.1185 + | Fun type type (infixr "\<Rightarrow>" 200)
2.1186 +
2.1187 +datatype dB =
2.1188 + Var nat
2.1189 + | App dB dB (infixl "\<degree>" 200)
2.1190 + | Abs type dB
2.1191 +
2.1192 +primrec
2.1193 + nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91)
2.1194 +where
2.1195 + "[]\<langle>i\<rangle> = None"
2.1196 +| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
2.1197 +
2.1198 +inductive nth_el' :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool"
2.1199 +where
2.1200 + "nth_el' (x # xs) 0 x"
2.1201 +| "nth_el' xs i y \<Longrightarrow> nth_el' (x # xs) (Suc i) y"
2.1202 +
2.1203 +inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50)
2.1204 + where
2.1205 + Var [intro!]: "nth_el' env x T \<Longrightarrow> env \<turnstile> Var x : T"
2.1206 + | Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)"
2.1207 + | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
2.1208 +
2.1209 +primrec
2.1210 + lift :: "[dB, nat] => dB"
2.1211 +where
2.1212 + "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
2.1213 + | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
2.1214 + | "lift (Abs T s) k = Abs T (lift s (k + 1))"
2.1215 +
2.1216 +primrec
2.1217 + subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300)
2.1218 +where
2.1219 + subst_Var: "(Var i)[s/k] =
2.1220 + (if k < i then Var (i - 1) else if i = k then s else Var i)"
2.1221 + | subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
2.1222 + | subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])"
2.1223 +
2.1224 +inductive beta :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50)
2.1225 + where
2.1226 + beta [simp, intro!]: "Abs T s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
2.1227 + | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
2.1228 + | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
2.1229 + | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
2.1230 +
2.1231 +code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing .
2.1232 +thm typing.equation
2.1233 +
2.1234 +code_pred (modes: i => i => bool, i => o => bool as reduce') beta .
2.1235 +thm beta.equation
2.1236 +
2.1237 +values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \<rightarrow>\<^sub>\<beta> x}"
2.1238 +
2.1239 +definition "reduce t = Predicate.the (reduce' t)"
2.1240 +
2.1241 +value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))"
2.1242 +
2.1243 +code_pred [dseq] typing .
2.1244 +code_pred [random_dseq] typing .
2.1245 +
2.1246 +values [random_dseq 1,1,5] 10 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"
2.1247 +
2.1248 +subsection {* A minimal example of yet another semantics *}
2.1249 +
2.1250 +text {* thanks to Elke Salecker *}
2.1251 +
2.1252 +types
2.1253 + vname = nat
2.1254 + vvalue = int
2.1255 + var_assign = "vname \<Rightarrow> vvalue" --"variable assignment"
2.1256 +
2.1257 +datatype ir_expr =
2.1258 + IrConst vvalue
2.1259 +| ObjAddr vname
2.1260 +| Add ir_expr ir_expr
2.1261 +
2.1262 +datatype val =
2.1263 + IntVal vvalue
2.1264 +
2.1265 +record configuration =
2.1266 + Env :: var_assign
2.1267 +
2.1268 +inductive eval_var ::
2.1269 + "ir_expr \<Rightarrow> configuration \<Rightarrow> val \<Rightarrow> bool"
2.1270 +where
2.1271 + irconst: "eval_var (IrConst i) conf (IntVal i)"
2.1272 +| objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)"
2.1273 +| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> eval_var (Add l r) conf (IntVal (vl+vr))"
2.1274 +
2.1275 +
2.1276 +code_pred eval_var .
2.1277 +thm eval_var.equation
2.1278 +
2.1279 +values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\<lambda>x. 0)|) val}"
2.1280 +
2.1281 +end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Wed Mar 24 17:40:43 2010 +0100
3.3 @@ -0,0 +1,1 @@
3.4 +use_thys ["Predicate_Compile_Examples"];
4.1 --- a/src/HOL/ex/Predicate_Compile_ex.thy Tue Mar 23 19:03:05 2010 -0700
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,1278 +0,0 @@
4.4 -theory Predicate_Compile_ex
4.5 -imports Predicate_Compile_Alternative_Defs
4.6 -begin
4.7 -
4.8 -subsection {* Basic predicates *}
4.9 -
4.10 -inductive False' :: "bool"
4.11 -
4.12 -code_pred (expected_modes: bool) False' .
4.13 -code_pred [dseq] False' .
4.14 -code_pred [random_dseq] False' .
4.15 -
4.16 -values [expected "{}" pred] "{x. False'}"
4.17 -values [expected "{}" dseq 1] "{x. False'}"
4.18 -values [expected "{}" random_dseq 1, 1, 1] "{x. False'}"
4.19 -
4.20 -value "False'"
4.21 -
4.22 -
4.23 -inductive True' :: "bool"
4.24 -where
4.25 - "True ==> True'"
4.26 -
4.27 -code_pred True' .
4.28 -code_pred [dseq] True' .
4.29 -code_pred [random_dseq] True' .
4.30 -
4.31 -thm True'.equation
4.32 -thm True'.dseq_equation
4.33 -thm True'.random_dseq_equation
4.34 -values [expected "{()}" ]"{x. True'}"
4.35 -values [expected "{}" dseq 0] "{x. True'}"
4.36 -values [expected "{()}" dseq 1] "{x. True'}"
4.37 -values [expected "{()}" dseq 2] "{x. True'}"
4.38 -values [expected "{}" random_dseq 1, 1, 0] "{x. True'}"
4.39 -values [expected "{}" random_dseq 1, 1, 1] "{x. True'}"
4.40 -values [expected "{()}" random_dseq 1, 1, 2] "{x. True'}"
4.41 -values [expected "{()}" random_dseq 1, 1, 3] "{x. True'}"
4.42 -
4.43 -inductive EmptySet :: "'a \<Rightarrow> bool"
4.44 -
4.45 -code_pred (expected_modes: o => bool, i => bool) EmptySet .
4.46 -
4.47 -definition EmptySet' :: "'a \<Rightarrow> bool"
4.48 -where "EmptySet' = {}"
4.49 -
4.50 -code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
4.51 -
4.52 -inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
4.53 -
4.54 -code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel .
4.55 -
4.56 -inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
4.57 -for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
4.58 -
4.59 -code_pred
4.60 - (expected_modes: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool,
4.61 - (o => o => bool) => o => i => bool, (o => o => bool) => i => i => bool,
4.62 - (i => o => bool) => o => o => bool, (i => o => bool) => i => o => bool,
4.63 - (i => o => bool) => o => i => bool, (i => o => bool) => i => i => bool,
4.64 - (o => i => bool) => o => o => bool, (o => i => bool) => i => o => bool,
4.65 - (o => i => bool) => o => i => bool, (o => i => bool) => i => i => bool,
4.66 - (i => i => bool) => o => o => bool, (i => i => bool) => i => o => bool,
4.67 - (i => i => bool) => o => i => bool, (i => i => bool) => i => i => bool)
4.68 - EmptyClosure .
4.69 -
4.70 -thm EmptyClosure.equation
4.71 -
4.72 -(* TODO: inductive package is broken!
4.73 -inductive False'' :: "bool"
4.74 -where
4.75 - "False \<Longrightarrow> False''"
4.76 -
4.77 -code_pred (expected_modes: []) False'' .
4.78 -
4.79 -inductive EmptySet'' :: "'a \<Rightarrow> bool"
4.80 -where
4.81 - "False \<Longrightarrow> EmptySet'' x"
4.82 -
4.83 -code_pred (expected_modes: [1]) EmptySet'' .
4.84 -code_pred (expected_modes: [], [1]) [inductify] EmptySet'' .
4.85 -*)
4.86 -
4.87 -consts a' :: 'a
4.88 -
4.89 -inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
4.90 -where
4.91 -"Fact a' a'"
4.92 -
4.93 -code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact .
4.94 -
4.95 -inductive zerozero :: "nat * nat => bool"
4.96 -where
4.97 - "zerozero (0, 0)"
4.98 -
4.99 -code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero .
4.100 -code_pred [dseq] zerozero .
4.101 -code_pred [random_dseq] zerozero .
4.102 -
4.103 -thm zerozero.equation
4.104 -thm zerozero.dseq_equation
4.105 -thm zerozero.random_dseq_equation
4.106 -
4.107 -text {* We expect the user to expand the tuples in the values command.
4.108 -The following values command is not supported. *}
4.109 -(*values "{x. zerozero x}" *)
4.110 -text {* Instead, the user must type *}
4.111 -values "{(x, y). zerozero (x, y)}"
4.112 -
4.113 -values [expected "{}" dseq 0] "{(x, y). zerozero (x, y)}"
4.114 -values [expected "{(0::nat, 0::nat)}" dseq 1] "{(x, y). zerozero (x, y)}"
4.115 -values [expected "{(0::nat, 0::nat)}" dseq 2] "{(x, y). zerozero (x, y)}"
4.116 -values [expected "{}" random_dseq 1, 1, 2] "{(x, y). zerozero (x, y)}"
4.117 -values [expected "{(0::nat, 0:: nat)}" random_dseq 1, 1, 3] "{(x, y). zerozero (x, y)}"
4.118 -
4.119 -inductive nested_tuples :: "((int * int) * int * int) => bool"
4.120 -where
4.121 - "nested_tuples ((0, 1), 2, 3)"
4.122 -
4.123 -code_pred nested_tuples .
4.124 -
4.125 -inductive JamesBond :: "nat => int => code_numeral => bool"
4.126 -where
4.127 - "JamesBond 0 0 7"
4.128 -
4.129 -code_pred JamesBond .
4.130 -
4.131 -values [expected "{(0::nat, 0::int , 7::code_numeral)}"] "{(a, b, c). JamesBond a b c}"
4.132 -values [expected "{(0::nat, 7::code_numeral, 0:: int)}"] "{(a, c, b). JamesBond a b c}"
4.133 -values [expected "{(0::int, 0::nat, 7::code_numeral)}"] "{(b, a, c). JamesBond a b c}"
4.134 -values [expected "{(0::int, 7::code_numeral, 0::nat)}"] "{(b, c, a). JamesBond a b c}"
4.135 -values [expected "{(7::code_numeral, 0::nat, 0::int)}"] "{(c, a, b). JamesBond a b c}"
4.136 -values [expected "{(7::code_numeral, 0::int, 0::nat)}"] "{(c, b, a). JamesBond a b c}"
4.137 -
4.138 -values [expected "{(7::code_numeral, 0::int)}"] "{(a, b). JamesBond 0 b a}"
4.139 -values [expected "{(7::code_numeral, 0::nat)}"] "{(c, a). JamesBond a 0 c}"
4.140 -values [expected "{(0::nat, 7::code_numeral)}"] "{(a, c). JamesBond a 0 c}"
4.141 -
4.142 -
4.143 -subsection {* Alternative Rules *}
4.144 -
4.145 -datatype char = C | D | E | F | G | H
4.146 -
4.147 -inductive is_C_or_D
4.148 -where
4.149 - "(x = C) \<or> (x = D) ==> is_C_or_D x"
4.150 -
4.151 -code_pred (expected_modes: i => bool) is_C_or_D .
4.152 -thm is_C_or_D.equation
4.153 -
4.154 -inductive is_D_or_E
4.155 -where
4.156 - "(x = D) \<or> (x = E) ==> is_D_or_E x"
4.157 -
4.158 -lemma [code_pred_intro]:
4.159 - "is_D_or_E D"
4.160 -by (auto intro: is_D_or_E.intros)
4.161 -
4.162 -lemma [code_pred_intro]:
4.163 - "is_D_or_E E"
4.164 -by (auto intro: is_D_or_E.intros)
4.165 -
4.166 -code_pred (expected_modes: o => bool, i => bool) is_D_or_E
4.167 -proof -
4.168 - case is_D_or_E
4.169 - from this(1) show thesis
4.170 - proof
4.171 - fix xa
4.172 - assume x: "x = xa"
4.173 - assume "xa = D \<or> xa = E"
4.174 - from this show thesis
4.175 - proof
4.176 - assume "xa = D" from this x is_D_or_E(2) show thesis by simp
4.177 - next
4.178 - assume "xa = E" from this x is_D_or_E(3) show thesis by simp
4.179 - qed
4.180 - qed
4.181 -qed
4.182 -
4.183 -thm is_D_or_E.equation
4.184 -
4.185 -inductive is_F_or_G
4.186 -where
4.187 - "x = F \<or> x = G ==> is_F_or_G x"
4.188 -
4.189 -lemma [code_pred_intro]:
4.190 - "is_F_or_G F"
4.191 -by (auto intro: is_F_or_G.intros)
4.192 -
4.193 -lemma [code_pred_intro]:
4.194 - "is_F_or_G G"
4.195 -by (auto intro: is_F_or_G.intros)
4.196 -
4.197 -inductive is_FGH
4.198 -where
4.199 - "is_F_or_G x ==> is_FGH x"
4.200 -| "is_FGH H"
4.201 -
4.202 -text {* Compilation of is_FGH requires elimination rule for is_F_or_G *}
4.203 -
4.204 -code_pred (expected_modes: o => bool, i => bool) is_FGH
4.205 -proof -
4.206 - case is_F_or_G
4.207 - from this(1) show thesis
4.208 - proof
4.209 - fix xa
4.210 - assume x: "x = xa"
4.211 - assume "xa = F \<or> xa = G"
4.212 - from this show thesis
4.213 - proof
4.214 - assume "xa = F"
4.215 - from this x is_F_or_G(2) show thesis by simp
4.216 - next
4.217 - assume "xa = G"
4.218 - from this x is_F_or_G(3) show thesis by simp
4.219 - qed
4.220 - qed
4.221 -qed
4.222 -
4.223 -subsection {* Preprocessor Inlining *}
4.224 -
4.225 -definition "equals == (op =)"
4.226 -
4.227 -inductive zerozero' :: "nat * nat => bool" where
4.228 - "equals (x, y) (0, 0) ==> zerozero' (x, y)"
4.229 -
4.230 -code_pred (expected_modes: i => bool) zerozero' .
4.231 -
4.232 -lemma zerozero'_eq: "zerozero' x == zerozero x"
4.233 -proof -
4.234 - have "zerozero' = zerozero"
4.235 - apply (auto simp add: mem_def)
4.236 - apply (cases rule: zerozero'.cases)
4.237 - apply (auto simp add: equals_def intro: zerozero.intros)
4.238 - apply (cases rule: zerozero.cases)
4.239 - apply (auto simp add: equals_def intro: zerozero'.intros)
4.240 - done
4.241 - from this show "zerozero' x == zerozero x" by auto
4.242 -qed
4.243 -
4.244 -declare zerozero'_eq [code_pred_inline]
4.245 -
4.246 -definition "zerozero'' x == zerozero' x"
4.247 -
4.248 -text {* if preprocessing fails, zerozero'' will not have all modes. *}
4.249 -
4.250 -code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
4.251 -
4.252 -subsection {* Sets and Numerals *}
4.253 -
4.254 -definition
4.255 - "one_or_two = {Suc 0, (Suc (Suc 0))}"
4.256 -
4.257 -code_pred [inductify] one_or_two .
4.258 -
4.259 -code_pred [dseq] one_or_two .
4.260 -code_pred [random_dseq] one_or_two .
4.261 -thm one_or_two.dseq_equation
4.262 -values [expected "{Suc 0::nat, 2::nat}"] "{x. one_or_two x}"
4.263 -values [random_dseq 0,0,10] 3 "{x. one_or_two x}"
4.264 -
4.265 -inductive one_or_two' :: "nat => bool"
4.266 -where
4.267 - "one_or_two' 1"
4.268 -| "one_or_two' 2"
4.269 -
4.270 -code_pred one_or_two' .
4.271 -thm one_or_two'.equation
4.272 -
4.273 -values "{x. one_or_two' x}"
4.274 -
4.275 -definition one_or_two'':
4.276 - "one_or_two'' == {1, (2::nat)}"
4.277 -
4.278 -code_pred [inductify] one_or_two'' .
4.279 -thm one_or_two''.equation
4.280 -
4.281 -values "{x. one_or_two'' x}"
4.282 -
4.283 -subsection {* even predicate *}
4.284 -
4.285 -inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
4.286 - "even 0"
4.287 - | "even n \<Longrightarrow> odd (Suc n)"
4.288 - | "odd n \<Longrightarrow> even (Suc n)"
4.289 -
4.290 -code_pred (expected_modes: i => bool, o => bool) even .
4.291 -code_pred [dseq] even .
4.292 -code_pred [random_dseq] even .
4.293 -
4.294 -thm odd.equation
4.295 -thm even.equation
4.296 -thm odd.dseq_equation
4.297 -thm even.dseq_equation
4.298 -thm odd.random_dseq_equation
4.299 -thm even.random_dseq_equation
4.300 -
4.301 -values "{x. even 2}"
4.302 -values "{x. odd 2}"
4.303 -values 10 "{n. even n}"
4.304 -values 10 "{n. odd n}"
4.305 -values [expected "{}" dseq 2] "{x. even 6}"
4.306 -values [expected "{}" dseq 6] "{x. even 6}"
4.307 -values [expected "{()}" dseq 7] "{x. even 6}"
4.308 -values [dseq 2] "{x. odd 7}"
4.309 -values [dseq 6] "{x. odd 7}"
4.310 -values [dseq 7] "{x. odd 7}"
4.311 -values [expected "{()}" dseq 8] "{x. odd 7}"
4.312 -
4.313 -values [expected "{}" dseq 0] 8 "{x. even x}"
4.314 -values [expected "{0::nat}" dseq 1] 8 "{x. even x}"
4.315 -values [expected "{0::nat, 2}" dseq 3] 8 "{x. even x}"
4.316 -values [expected "{0::nat, 2}" dseq 4] 8 "{x. even x}"
4.317 -values [expected "{0::nat, 2, 4}" dseq 6] 8 "{x. even x}"
4.318 -
4.319 -values [random_dseq 1, 1, 0] 8 "{x. even x}"
4.320 -values [random_dseq 1, 1, 1] 8 "{x. even x}"
4.321 -values [random_dseq 1, 1, 2] 8 "{x. even x}"
4.322 -values [random_dseq 1, 1, 3] 8 "{x. even x}"
4.323 -values [random_dseq 1, 1, 6] 8 "{x. even x}"
4.324 -
4.325 -values [expected "{}" random_dseq 1, 1, 7] "{x. odd 7}"
4.326 -values [random_dseq 1, 1, 8] "{x. odd 7}"
4.327 -values [random_dseq 1, 1, 9] "{x. odd 7}"
4.328 -
4.329 -definition odd' where "odd' x == \<not> even x"
4.330 -
4.331 -code_pred (expected_modes: i => bool) [inductify] odd' .
4.332 -code_pred [dseq inductify] odd' .
4.333 -code_pred [random_dseq inductify] odd' .
4.334 -
4.335 -values [expected "{}" dseq 2] "{x. odd' 7}"
4.336 -values [expected "{()}" dseq 9] "{x. odd' 7}"
4.337 -values [expected "{}" dseq 2] "{x. odd' 8}"
4.338 -values [expected "{}" dseq 10] "{x. odd' 8}"
4.339 -
4.340 -
4.341 -inductive is_even :: "nat \<Rightarrow> bool"
4.342 -where
4.343 - "n mod 2 = 0 \<Longrightarrow> is_even n"
4.344 -
4.345 -code_pred (expected_modes: i => bool) is_even .
4.346 -
4.347 -subsection {* append predicate *}
4.348 -
4.349 -inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
4.350 - "append [] xs xs"
4.351 - | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
4.352 -
4.353 -code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix,
4.354 - i => o => i => bool as suffix, i => i => i => bool) append .
4.355 -code_pred [dseq] append .
4.356 -code_pred [random_dseq] append .
4.357 -
4.358 -thm append.equation
4.359 -thm append.dseq_equation
4.360 -thm append.random_dseq_equation
4.361 -
4.362 -values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
4.363 -values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
4.364 -values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
4.365 -
4.366 -values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
4.367 -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)]}"
4.368 -values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
4.369 -values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
4.370 -values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
4.371 -values [random_dseq 1, 1, 1] 10 "{(xs, ys, zs::int list). append xs ys zs}"
4.372 -values [random_dseq 1, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
4.373 -values [random_dseq 3, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
4.374 -values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
4.375 -values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}"
4.376 -
4.377 -value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
4.378 -value [code] "Predicate.the (slice ([]::int list))"
4.379 -
4.380 -
4.381 -text {* tricky case with alternative rules *}
4.382 -
4.383 -inductive append2
4.384 -where
4.385 - "append2 [] xs xs"
4.386 -| "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)"
4.387 -
4.388 -lemma append2_Nil: "append2 [] (xs::'b list) xs"
4.389 - by (simp add: append2.intros(1))
4.390 -
4.391 -lemmas [code_pred_intro] = append2_Nil append2.intros(2)
4.392 -
4.393 -code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool,
4.394 - i => o => i => bool, i => i => i => bool) append2
4.395 -proof -
4.396 - case append2
4.397 - from append2(1) show thesis
4.398 - proof
4.399 - fix xs
4.400 - assume "xa = []" "xb = xs" "xc = xs"
4.401 - from this append2(2) show thesis by simp
4.402 - next
4.403 - fix xs ys zs x
4.404 - assume "xa = x # xs" "xb = ys" "xc = x # zs" "append2 xs ys zs"
4.405 - from this append2(3) show thesis by fastsimp
4.406 - qed
4.407 -qed
4.408 -
4.409 -inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
4.410 -where
4.411 - "tupled_append ([], xs, xs)"
4.412 -| "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
4.413 -
4.414 -code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
4.415 - i * o * i => bool, i * i * i => bool) tupled_append .
4.416 -code_pred [random_dseq] tupled_append .
4.417 -thm tupled_append.equation
4.418 -
4.419 -values "{xs. tupled_append ([(1::nat), 2, 3], [4, 5], xs)}"
4.420 -
4.421 -inductive tupled_append'
4.422 -where
4.423 -"tupled_append' ([], xs, xs)"
4.424 -| "[| ys = fst (xa, y); x # zs = snd (xa, y);
4.425 - tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)"
4.426 -
4.427 -code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
4.428 - i * o * i => bool, i * i * i => bool) tupled_append' .
4.429 -thm tupled_append'.equation
4.430 -
4.431 -inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
4.432 -where
4.433 - "tupled_append'' ([], xs, xs)"
4.434 -| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
4.435 -
4.436 -code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
4.437 - i * o * i => bool, i * i * i => bool) tupled_append'' .
4.438 -thm tupled_append''.equation
4.439 -
4.440 -inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
4.441 -where
4.442 - "tupled_append''' ([], xs, xs)"
4.443 -| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
4.444 -
4.445 -code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
4.446 - i * o * i => bool, i * i * i => bool) tupled_append''' .
4.447 -thm tupled_append'''.equation
4.448 -
4.449 -subsection {* map_ofP predicate *}
4.450 -
4.451 -inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
4.452 -where
4.453 - "map_ofP ((a, b)#xs) a b"
4.454 -| "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
4.455 -
4.456 -code_pred (expected_modes: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP .
4.457 -thm map_ofP.equation
4.458 -
4.459 -subsection {* filter predicate *}
4.460 -
4.461 -inductive filter1
4.462 -for P
4.463 -where
4.464 - "filter1 P [] []"
4.465 -| "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)"
4.466 -| "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys"
4.467 -
4.468 -code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 .
4.469 -code_pred [dseq] filter1 .
4.470 -code_pred [random_dseq] filter1 .
4.471 -
4.472 -thm filter1.equation
4.473 -
4.474 -values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
4.475 -values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
4.476 -values [expected "{[0::nat, 2, 4]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
4.477 -
4.478 -inductive filter2
4.479 -where
4.480 - "filter2 P [] []"
4.481 -| "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)"
4.482 -| "\<not> P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys"
4.483 -
4.484 -code_pred (expected_modes: (i => bool) => i => i => bool, (i => bool) => i => o => bool) filter2 .
4.485 -code_pred [dseq] filter2 .
4.486 -code_pred [random_dseq] filter2 .
4.487 -
4.488 -thm filter2.equation
4.489 -thm filter2.random_dseq_equation
4.490 -
4.491 -(*
4.492 -inductive filter3
4.493 -for P
4.494 -where
4.495 - "List.filter P xs = ys ==> filter3 P xs ys"
4.496 -
4.497 -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 .
4.498 -
4.499 -code_pred [dseq] filter3 .
4.500 -thm filter3.dseq_equation
4.501 -*)
4.502 -(*
4.503 -inductive filter4
4.504 -where
4.505 - "List.filter P xs = ys ==> filter4 P xs ys"
4.506 -
4.507 -code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .
4.508 -(*code_pred [depth_limited] filter4 .*)
4.509 -(*code_pred [random] filter4 .*)
4.510 -*)
4.511 -subsection {* reverse predicate *}
4.512 -
4.513 -inductive rev where
4.514 - "rev [] []"
4.515 - | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
4.516 -
4.517 -code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev .
4.518 -
4.519 -thm rev.equation
4.520 -
4.521 -values "{xs. rev [0, 1, 2, 3::nat] xs}"
4.522 -
4.523 -inductive tupled_rev where
4.524 - "tupled_rev ([], [])"
4.525 -| "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)"
4.526 -
4.527 -code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev .
4.528 -thm tupled_rev.equation
4.529 -
4.530 -subsection {* partition predicate *}
4.531 -
4.532 -inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
4.533 - for f where
4.534 - "partition f [] [] []"
4.535 - | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
4.536 - | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
4.537 -
4.538 -code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool,
4.539 - (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool)
4.540 - partition .
4.541 -code_pred [dseq] partition .
4.542 -code_pred [random_dseq] partition .
4.543 -
4.544 -values 10 "{(ys, zs). partition is_even
4.545 - [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
4.546 -values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
4.547 -values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
4.548 -
4.549 -inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool"
4.550 - for f where
4.551 - "tupled_partition f ([], [], [])"
4.552 - | "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)"
4.553 - | "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)"
4.554 -
4.555 -code_pred (expected_modes: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool,
4.556 - (i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition .
4.557 -
4.558 -thm tupled_partition.equation
4.559 -
4.560 -lemma [code_pred_intro]:
4.561 - "r a b \<Longrightarrow> tranclp r a b"
4.562 - "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
4.563 - by auto
4.564 -
4.565 -subsection {* transitive predicate *}
4.566 -
4.567 -text {* Also look at the tabled transitive closure in the Library *}
4.568 -
4.569 -code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,
4.570 - (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,
4.571 - (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp
4.572 -proof -
4.573 - case tranclp
4.574 - from this converse_tranclpE[OF this(1)] show thesis by metis
4.575 -qed
4.576 -
4.577 -
4.578 -code_pred [dseq] tranclp .
4.579 -code_pred [random_dseq] tranclp .
4.580 -thm tranclp.equation
4.581 -thm tranclp.random_dseq_equation
4.582 -
4.583 -inductive rtrancl' :: "'a => 'a => ('a => 'a => bool) => bool"
4.584 -where
4.585 - "rtrancl' x x r"
4.586 -| "r x y ==> rtrancl' y z r ==> rtrancl' x z r"
4.587 -
4.588 -code_pred [random_dseq] rtrancl' .
4.589 -
4.590 -thm rtrancl'.random_dseq_equation
4.591 -
4.592 -inductive rtrancl'' :: "('a * 'a * ('a \<Rightarrow> 'a \<Rightarrow> bool)) \<Rightarrow> bool"
4.593 -where
4.594 - "rtrancl'' (x, x, r)"
4.595 -| "r x y \<Longrightarrow> rtrancl'' (y, z, r) \<Longrightarrow> rtrancl'' (x, z, r)"
4.596 -
4.597 -code_pred rtrancl'' .
4.598 -
4.599 -inductive rtrancl''' :: "('a * ('a * 'a) * ('a * 'a => bool)) => bool"
4.600 -where
4.601 - "rtrancl''' (x, (x, x), r)"
4.602 -| "r (x, y) ==> rtrancl''' (y, (z, z), r) ==> rtrancl''' (x, (z, z), r)"
4.603 -
4.604 -code_pred rtrancl''' .
4.605 -
4.606 -
4.607 -inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
4.608 - "succ 0 1"
4.609 - | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
4.610 -
4.611 -code_pred (modes: i => i => bool, i => o => bool, o => i => bool, o => o => bool) succ .
4.612 -code_pred [random_dseq] succ .
4.613 -thm succ.equation
4.614 -thm succ.random_dseq_equation
4.615 -
4.616 -values 10 "{(m, n). succ n m}"
4.617 -values "{m. succ 0 m}"
4.618 -values "{m. succ m 0}"
4.619 -
4.620 -text {* values command needs mode annotation of the parameter succ
4.621 -to disambiguate which mode is to be chosen. *}
4.622 -
4.623 -values [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
4.624 -values [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
4.625 -values 20 "{(n, m). tranclp succ n m}"
4.626 -
4.627 -inductive example_graph :: "int => int => bool"
4.628 -where
4.629 - "example_graph 0 1"
4.630 -| "example_graph 1 2"
4.631 -| "example_graph 1 3"
4.632 -| "example_graph 4 7"
4.633 -| "example_graph 4 5"
4.634 -| "example_graph 5 6"
4.635 -| "example_graph 7 6"
4.636 -| "example_graph 7 8"
4.637 -
4.638 -inductive not_reachable_in_example_graph :: "int => int => bool"
4.639 -where "\<not> (tranclp example_graph x y) ==> not_reachable_in_example_graph x y"
4.640 -
4.641 -code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph .
4.642 -
4.643 -thm not_reachable_in_example_graph.equation
4.644 -thm tranclp.equation
4.645 -value "not_reachable_in_example_graph 0 3"
4.646 -value "not_reachable_in_example_graph 4 8"
4.647 -value "not_reachable_in_example_graph 5 6"
4.648 -text {* rtrancl compilation is strange! *}
4.649 -(*
4.650 -value "not_reachable_in_example_graph 0 4"
4.651 -value "not_reachable_in_example_graph 1 6"
4.652 -value "not_reachable_in_example_graph 8 4"*)
4.653 -
4.654 -code_pred [dseq] not_reachable_in_example_graph .
4.655 -
4.656 -values [dseq 6] "{x. tranclp example_graph 0 3}"
4.657 -
4.658 -values [dseq 0] "{x. not_reachable_in_example_graph 0 3}"
4.659 -values [dseq 0] "{x. not_reachable_in_example_graph 0 4}"
4.660 -values [dseq 20] "{x. not_reachable_in_example_graph 0 4}"
4.661 -values [dseq 6] "{x. not_reachable_in_example_graph 0 3}"
4.662 -values [dseq 3] "{x. not_reachable_in_example_graph 4 2}"
4.663 -values [dseq 6] "{x. not_reachable_in_example_graph 4 2}"
4.664 -
4.665 -
4.666 -inductive not_reachable_in_example_graph' :: "int => int => bool"
4.667 -where "\<not> (rtranclp example_graph x y) ==> not_reachable_in_example_graph' x y"
4.668 -
4.669 -code_pred not_reachable_in_example_graph' .
4.670 -
4.671 -value "not_reachable_in_example_graph' 0 3"
4.672 -(* value "not_reachable_in_example_graph' 0 5" would not terminate *)
4.673 -
4.674 -
4.675 -(*values [depth_limited 0] "{x. not_reachable_in_example_graph' 0 3}"*)
4.676 -(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
4.677 -(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"*)
4.678 -(*values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
4.679 -(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
4.680 -(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
4.681 -
4.682 -code_pred [dseq] not_reachable_in_example_graph' .
4.683 -
4.684 -(*thm not_reachable_in_example_graph'.dseq_equation*)
4.685 -
4.686 -(*values [dseq 0] "{x. not_reachable_in_example_graph' 0 3}"*)
4.687 -(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
4.688 -(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"
4.689 -values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
4.690 -(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
4.691 -(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
4.692 -
4.693 -
4.694 -subsection {* IMP *}
4.695 -
4.696 -types
4.697 - var = nat
4.698 - state = "int list"
4.699 -
4.700 -datatype com =
4.701 - Skip |
4.702 - Ass var "state => int" |
4.703 - Seq com com |
4.704 - IF "state => bool" com com |
4.705 - While "state => bool" com
4.706 -
4.707 -inductive exec :: "com => state => state => bool" where
4.708 -"exec Skip s s" |
4.709 -"exec (Ass x e) s (s[x := e(s)])" |
4.710 -"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
4.711 -"b s ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
4.712 -"~b s ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
4.713 -"~b s ==> exec (While b c) s s" |
4.714 -"b s1 ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
4.715 -
4.716 -code_pred exec .
4.717 -
4.718 -values "{t. exec
4.719 - (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))))
4.720 - [3,5] t}"
4.721 -
4.722 -
4.723 -inductive tupled_exec :: "(com \<times> state \<times> state) \<Rightarrow> bool" where
4.724 -"tupled_exec (Skip, s, s)" |
4.725 -"tupled_exec (Ass x e, s, s[x := e(s)])" |
4.726 -"tupled_exec (c1, s1, s2) ==> tupled_exec (c2, s2, s3) ==> tupled_exec (Seq c1 c2, s1, s3)" |
4.727 -"b s ==> tupled_exec (c1, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
4.728 -"~b s ==> tupled_exec (c2, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
4.729 -"~b s ==> tupled_exec (While b c, s, s)" |
4.730 -"b s1 ==> tupled_exec (c, s1, s2) ==> tupled_exec (While b c, s2, s3) ==> tupled_exec (While b c, s1, s3)"
4.731 -
4.732 -code_pred tupled_exec .
4.733 -
4.734 -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)}"
4.735 -
4.736 -subsection {* CCS *}
4.737 -
4.738 -text{* This example formalizes finite CCS processes without communication or
4.739 -recursion. For simplicity, labels are natural numbers. *}
4.740 -
4.741 -datatype proc = nil | pre nat proc | or proc proc | par proc proc
4.742 -
4.743 -inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where
4.744 -"step (pre n p) n p" |
4.745 -"step p1 a q \<Longrightarrow> step (or p1 p2) a q" |
4.746 -"step p2 a q \<Longrightarrow> step (or p1 p2) a q" |
4.747 -"step p1 a q \<Longrightarrow> step (par p1 p2) a (par q p2)" |
4.748 -"step p2 a q \<Longrightarrow> step (par p1 p2) a (par p1 q)"
4.749 -
4.750 -code_pred step .
4.751 -
4.752 -inductive steps where
4.753 -"steps p [] p" |
4.754 -"step p a q \<Longrightarrow> steps q as r \<Longrightarrow> steps p (a#as) r"
4.755 -
4.756 -code_pred steps .
4.757 -
4.758 -values 3
4.759 - "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
4.760 -
4.761 -values 5
4.762 - "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
4.763 -
4.764 -values 3 "{(a,q). step (par nil nil) a q}"
4.765 -
4.766 -
4.767 -inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
4.768 -where
4.769 -"tupled_step (pre n p, n, p)" |
4.770 -"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
4.771 -"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
4.772 -"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par q p2)" |
4.773 -"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par p1 q)"
4.774 -
4.775 -code_pred tupled_step .
4.776 -thm tupled_step.equation
4.777 -
4.778 -subsection {* divmod *}
4.779 -
4.780 -inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
4.781 - "k < l \<Longrightarrow> divmod_rel k l 0 k"
4.782 - | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
4.783 -
4.784 -code_pred divmod_rel ..
4.785 -thm divmod_rel.equation
4.786 -value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
4.787 -
4.788 -subsection {* Transforming predicate logic into logic programs *}
4.789 -
4.790 -subsection {* Transforming functions into logic programs *}
4.791 -definition
4.792 - "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)"
4.793 -
4.794 -code_pred [inductify] case_f .
4.795 -thm case_fP.equation
4.796 -thm case_fP.intros
4.797 -
4.798 -fun fold_map_idx where
4.799 - "fold_map_idx f i y [] = (y, [])"
4.800 -| "fold_map_idx f i y (x # xs) =
4.801 - (let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs
4.802 - in (y'', x' # xs'))"
4.803 -
4.804 -text {* mode analysis explores thousand modes - this is infeasible at the moment... *}
4.805 -(*code_pred [inductify, show_steps] fold_map_idx .*)
4.806 -
4.807 -subsection {* Minimum *}
4.808 -
4.809 -definition Min
4.810 -where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
4.811 -
4.812 -code_pred [inductify] Min .
4.813 -thm Min.equation
4.814 -
4.815 -subsection {* Lexicographic order *}
4.816 -
4.817 -declare lexord_def[code_pred_def]
4.818 -code_pred [inductify] lexord .
4.819 -code_pred [random_dseq inductify] lexord .
4.820 -
4.821 -thm lexord.equation
4.822 -thm lexord.random_dseq_equation
4.823 -
4.824 -inductive less_than_nat :: "nat * nat => bool"
4.825 -where
4.826 - "less_than_nat (0, x)"
4.827 -| "less_than_nat (x, y) ==> less_than_nat (Suc x, Suc y)"
4.828 -
4.829 -code_pred less_than_nat .
4.830 -
4.831 -code_pred [dseq] less_than_nat .
4.832 -code_pred [random_dseq] less_than_nat .
4.833 -
4.834 -inductive test_lexord :: "nat list * nat list => bool"
4.835 -where
4.836 - "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)"
4.837 -
4.838 -code_pred test_lexord .
4.839 -code_pred [dseq] test_lexord .
4.840 -code_pred [random_dseq] test_lexord .
4.841 -thm test_lexord.dseq_equation
4.842 -thm test_lexord.random_dseq_equation
4.843 -
4.844 -values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
4.845 -(*values [depth_limited 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"*)
4.846 -
4.847 -declare list.size(3,4)[code_pred_def]
4.848 -lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
4.849 -(*
4.850 -code_pred [inductify] lexn .
4.851 -thm lexn.equation
4.852 -*)
4.853 -(*
4.854 -code_pred [random_dseq inductify] lexn .
4.855 -thm lexn.random_dseq_equation
4.856 -
4.857 -values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
4.858 -*)
4.859 -inductive has_length
4.860 -where
4.861 - "has_length [] 0"
4.862 -| "has_length xs i ==> has_length (x # xs) (Suc i)"
4.863 -
4.864 -lemma has_length:
4.865 - "has_length xs n = (length xs = n)"
4.866 -proof (rule iffI)
4.867 - assume "has_length xs n"
4.868 - from this show "length xs = n"
4.869 - by (rule has_length.induct) auto
4.870 -next
4.871 - assume "length xs = n"
4.872 - from this show "has_length xs n"
4.873 - by (induct xs arbitrary: n) (auto intro: has_length.intros)
4.874 -qed
4.875 -
4.876 -lemma lexn_intros [code_pred_intro]:
4.877 - "has_length xs i ==> has_length ys i ==> r (x, y) ==> lexn r (Suc i) (x # xs, y # ys)"
4.878 - "lexn r i (xs, ys) ==> lexn r (Suc i) (x # xs, x # ys)"
4.879 -proof -
4.880 - assume "has_length xs i" "has_length ys i" "r (x, y)"
4.881 - from this has_length show "lexn r (Suc i) (x # xs, y # ys)"
4.882 - unfolding lexn_conv Collect_def mem_def
4.883 - by fastsimp
4.884 -next
4.885 - assume "lexn r i (xs, ys)"
4.886 - thm lexn_conv
4.887 - from this show "lexn r (Suc i) (x#xs, x#ys)"
4.888 - unfolding Collect_def mem_def lexn_conv
4.889 - apply auto
4.890 - apply (rule_tac x="x # xys" in exI)
4.891 - by auto
4.892 -qed
4.893 -
4.894 -code_pred [random_dseq inductify] lexn
4.895 -proof -
4.896 - fix r n xs ys
4.897 - assume 1: "lexn r n (xs, ys)"
4.898 - 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"
4.899 - 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"
4.900 - from 1 2 3 show thesis
4.901 - unfolding lexn_conv Collect_def mem_def
4.902 - apply (auto simp add: has_length)
4.903 - apply (case_tac xys)
4.904 - apply auto
4.905 - apply fastsimp
4.906 - apply fastsimp done
4.907 -qed
4.908 -
4.909 -
4.910 -values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
4.911 -thm lenlex_conv
4.912 -thm lex_conv
4.913 -declare list.size(3,4)[code_pred_def]
4.914 -(*code_pred [inductify, show_steps, show_intermediate_results] length .*)
4.915 -setup {* Predicate_Compile_Data.ignore_consts [@{const_name Orderings.top_class.top}] *}
4.916 -code_pred [inductify] lex .
4.917 -thm lex.equation
4.918 -thm lex_def
4.919 -declare lenlex_conv[code_pred_def]
4.920 -code_pred [inductify] lenlex .
4.921 -thm lenlex.equation
4.922 -
4.923 -code_pred [random_dseq inductify] lenlex .
4.924 -thm lenlex.random_dseq_equation
4.925 -
4.926 -values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}"
4.927 -thm lists.intros
4.928 -
4.929 -code_pred [inductify] lists .
4.930 -thm lists.equation
4.931 -
4.932 -subsection {* AVL Tree *}
4.933 -
4.934 -datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
4.935 -fun height :: "'a tree => nat" where
4.936 -"height ET = 0"
4.937 -| "height (MKT x l r h) = max (height l) (height r) + 1"
4.938 -
4.939 -consts avl :: "'a tree => bool"
4.940 -primrec
4.941 - "avl ET = True"
4.942 - "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and>
4.943 - h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
4.944 -(*
4.945 -code_pred [inductify] avl .
4.946 -thm avl.equation*)
4.947 -
4.948 -code_pred [random_dseq inductify] avl .
4.949 -thm avl.random_dseq_equation
4.950 -
4.951 -values [random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
4.952 -
4.953 -fun set_of
4.954 -where
4.955 -"set_of ET = {}"
4.956 -| "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"
4.957 -
4.958 -fun is_ord :: "nat tree => bool"
4.959 -where
4.960 -"is_ord ET = True"
4.961 -| "is_ord (MKT n l r h) =
4.962 - ((\<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)"
4.963 -
4.964 -code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of .
4.965 -thm set_of.equation
4.966 -
4.967 -code_pred (expected_modes: i => bool) [inductify] is_ord .
4.968 -thm is_ord_aux.equation
4.969 -thm is_ord.equation
4.970 -
4.971 -
4.972 -subsection {* Definitions about Relations *}
4.973 -term "converse"
4.974 -code_pred (modes:
4.975 - (i * i => bool) => i * i => bool,
4.976 - (i * o => bool) => o * i => bool,
4.977 - (i * o => bool) => i * i => bool,
4.978 - (o * i => bool) => i * o => bool,
4.979 - (o * i => bool) => i * i => bool,
4.980 - (o * o => bool) => o * o => bool,
4.981 - (o * o => bool) => i * o => bool,
4.982 - (o * o => bool) => o * i => bool,
4.983 - (o * o => bool) => i * i => bool) [inductify] converse .
4.984 -
4.985 -thm converse.equation
4.986 -code_pred [inductify] rel_comp .
4.987 -thm rel_comp.equation
4.988 -code_pred [inductify] Image .
4.989 -thm Image.equation
4.990 -declare singleton_iff[code_pred_inline]
4.991 -declare Id_on_def[unfolded Bex_def UNION_def singleton_iff, code_pred_def]
4.992 -
4.993 -code_pred (expected_modes:
4.994 - (o => bool) => o => bool,
4.995 - (o => bool) => i * o => bool,
4.996 - (o => bool) => o * i => bool,
4.997 - (o => bool) => i => bool,
4.998 - (i => bool) => i * o => bool,
4.999 - (i => bool) => o * i => bool,
4.1000 - (i => bool) => i => bool) [inductify] Id_on .
4.1001 -thm Id_on.equation
4.1002 -thm Domain_def
4.1003 -code_pred (modes:
4.1004 - (o * o => bool) => o => bool,
4.1005 - (o * o => bool) => i => bool,
4.1006 - (i * o => bool) => i => bool) [inductify] Domain .
4.1007 -thm Domain.equation
4.1008 -
4.1009 -thm Range_def
4.1010 -code_pred (modes:
4.1011 - (o * o => bool) => o => bool,
4.1012 - (o * o => bool) => i => bool,
4.1013 - (o * i => bool) => i => bool) [inductify] Range .
4.1014 -thm Range.equation
4.1015 -
4.1016 -code_pred [inductify] Field .
4.1017 -thm Field.equation
4.1018 -
4.1019 -thm refl_on_def
4.1020 -code_pred [inductify] refl_on .
4.1021 -thm refl_on.equation
4.1022 -code_pred [inductify] total_on .
4.1023 -thm total_on.equation
4.1024 -code_pred [inductify] antisym .
4.1025 -thm antisym.equation
4.1026 -code_pred [inductify] trans .
4.1027 -thm trans.equation
4.1028 -code_pred [inductify] single_valued .
4.1029 -thm single_valued.equation
4.1030 -thm inv_image_def
4.1031 -code_pred [inductify] inv_image .
4.1032 -thm inv_image.equation
4.1033 -
4.1034 -subsection {* Inverting list functions *}
4.1035 -
4.1036 -(*code_pred [inductify] length .
4.1037 -code_pred [random inductify] length .
4.1038 -thm size_listP.equation
4.1039 -thm size_listP.random_equation
4.1040 -*)
4.1041 -(*values [random] 1 "{xs. size_listP (xs::nat list) (5::nat)}"*)
4.1042 -
4.1043 -code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify] List.concat .
4.1044 -thm concatP.equation
4.1045 -
4.1046 -values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
4.1047 -values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}"
4.1048 -
4.1049 -code_pred [dseq inductify] List.concat .
4.1050 -thm concatP.dseq_equation
4.1051 -
4.1052 -values [dseq 3] 3
4.1053 - "{xs. concatP xs ([0] :: nat list)}"
4.1054 -
4.1055 -values [dseq 5] 3
4.1056 - "{xs. concatP xs ([1] :: int list)}"
4.1057 -
4.1058 -values [dseq 5] 3
4.1059 - "{xs. concatP xs ([1] :: nat list)}"
4.1060 -
4.1061 -values [dseq 5] 3
4.1062 - "{xs. concatP xs [(1::int), 2]}"
4.1063 -
4.1064 -code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd .
4.1065 -thm hdP.equation
4.1066 -values "{x. hdP [1, 2, (3::int)] x}"
4.1067 -values "{(xs, x). hdP [1, 2, (3::int)] 1}"
4.1068 -
4.1069 -code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] tl .
4.1070 -thm tlP.equation
4.1071 -values "{x. tlP [1, 2, (3::nat)] x}"
4.1072 -values "{x. tlP [1, 2, (3::int)] [3]}"
4.1073 -
4.1074 -code_pred [inductify] last .
4.1075 -thm lastP.equation
4.1076 -
4.1077 -code_pred [inductify] butlast .
4.1078 -thm butlastP.equation
4.1079 -
4.1080 -code_pred [inductify] take .
4.1081 -thm takeP.equation
4.1082 -
4.1083 -code_pred [inductify] drop .
4.1084 -thm dropP.equation
4.1085 -code_pred [inductify] zip .
4.1086 -thm zipP.equation
4.1087 -
4.1088 -code_pred [inductify] upt .
4.1089 -code_pred [inductify] remdups .
4.1090 -thm remdupsP.equation
4.1091 -code_pred [dseq inductify] remdups .
4.1092 -values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
4.1093 -
4.1094 -code_pred [inductify] remove1 .
4.1095 -thm remove1P.equation
4.1096 -values "{xs. remove1P 1 xs [2, (3::int)]}"
4.1097 -
4.1098 -code_pred [inductify] removeAll .
4.1099 -thm removeAllP.equation
4.1100 -code_pred [dseq inductify] removeAll .
4.1101 -
4.1102 -values [dseq 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}"
4.1103 -
4.1104 -code_pred [inductify] distinct .
4.1105 -thm distinct.equation
4.1106 -code_pred [inductify] replicate .
4.1107 -thm replicateP.equation
4.1108 -values 5 "{(n, xs). replicateP n (0::int) xs}"
4.1109 -
4.1110 -code_pred [inductify] splice .
4.1111 -thm splice.simps
4.1112 -thm spliceP.equation
4.1113 -
4.1114 -values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
4.1115 -
4.1116 -code_pred [inductify] List.rev .
4.1117 -code_pred [inductify] map .
4.1118 -code_pred [inductify] foldr .
4.1119 -code_pred [inductify] foldl .
4.1120 -code_pred [inductify] filter .
4.1121 -code_pred [random_dseq inductify] filter .
4.1122 -
4.1123 -subsection {* Context Free Grammar *}
4.1124 -
4.1125 -datatype alphabet = a | b
4.1126 -
4.1127 -inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
4.1128 - "[] \<in> S\<^isub>1"
4.1129 -| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
4.1130 -| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
4.1131 -| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
4.1132 -| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
4.1133 -| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
4.1134 -
4.1135 -code_pred [inductify] S\<^isub>1p .
4.1136 -code_pred [random_dseq inductify] S\<^isub>1p .
4.1137 -thm S\<^isub>1p.equation
4.1138 -thm S\<^isub>1p.random_dseq_equation
4.1139 -
4.1140 -values [random_dseq 5, 5, 5] 5 "{x. S\<^isub>1p x}"
4.1141 -
4.1142 -inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
4.1143 - "[] \<in> S\<^isub>2"
4.1144 -| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
4.1145 -| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
4.1146 -| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
4.1147 -| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
4.1148 -| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
4.1149 -
4.1150 -code_pred [random_dseq inductify] S\<^isub>2p .
4.1151 -thm S\<^isub>2p.random_dseq_equation
4.1152 -thm A\<^isub>2p.random_dseq_equation
4.1153 -thm B\<^isub>2p.random_dseq_equation
4.1154 -
4.1155 -values [random_dseq 5, 5, 5] 10 "{x. S\<^isub>2p x}"
4.1156 -
4.1157 -inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
4.1158 - "[] \<in> S\<^isub>3"
4.1159 -| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
4.1160 -| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
4.1161 -| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
4.1162 -| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
4.1163 -| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
4.1164 -
4.1165 -code_pred [inductify] S\<^isub>3p .
4.1166 -thm S\<^isub>3p.equation
4.1167 -
4.1168 -values 10 "{x. S\<^isub>3p x}"
4.1169 -
4.1170 -inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
4.1171 - "[] \<in> S\<^isub>4"
4.1172 -| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
4.1173 -| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
4.1174 -| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
4.1175 -| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
4.1176 -| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
4.1177 -| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
4.1178 -
4.1179 -code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p .
4.1180 -
4.1181 -subsection {* Lambda *}
4.1182 -
4.1183 -datatype type =
4.1184 - Atom nat
4.1185 - | Fun type type (infixr "\<Rightarrow>" 200)
4.1186 -
4.1187 -datatype dB =
4.1188 - Var nat
4.1189 - | App dB dB (infixl "\<degree>" 200)
4.1190 - | Abs type dB
4.1191 -
4.1192 -primrec
4.1193 - nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91)
4.1194 -where
4.1195 - "[]\<langle>i\<rangle> = None"
4.1196 -| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
4.1197 -
4.1198 -inductive nth_el' :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool"
4.1199 -where
4.1200 - "nth_el' (x # xs) 0 x"
4.1201 -| "nth_el' xs i y \<Longrightarrow> nth_el' (x # xs) (Suc i) y"
4.1202 -
4.1203 -inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50)
4.1204 - where
4.1205 - Var [intro!]: "nth_el' env x T \<Longrightarrow> env \<turnstile> Var x : T"
4.1206 - | Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)"
4.1207 - | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
4.1208 -
4.1209 -primrec
4.1210 - lift :: "[dB, nat] => dB"
4.1211 -where
4.1212 - "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
4.1213 - | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
4.1214 - | "lift (Abs T s) k = Abs T (lift s (k + 1))"
4.1215 -
4.1216 -primrec
4.1217 - subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300)
4.1218 -where
4.1219 - subst_Var: "(Var i)[s/k] =
4.1220 - (if k < i then Var (i - 1) else if i = k then s else Var i)"
4.1221 - | subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
4.1222 - | subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])"
4.1223 -
4.1224 -inductive beta :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50)
4.1225 - where
4.1226 - beta [simp, intro!]: "Abs T s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
4.1227 - | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
4.1228 - | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
4.1229 - | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
4.1230 -
4.1231 -code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing .
4.1232 -thm typing.equation
4.1233 -
4.1234 -code_pred (modes: i => i => bool, i => o => bool as reduce') beta .
4.1235 -thm beta.equation
4.1236 -
4.1237 -values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \<rightarrow>\<^sub>\<beta> x}"
4.1238 -
4.1239 -definition "reduce t = Predicate.the (reduce' t)"
4.1240 -
4.1241 -value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))"
4.1242 -
4.1243 -code_pred [dseq] typing .
4.1244 -code_pred [random_dseq] typing .
4.1245 -
4.1246 -values [random_dseq 1,1,5] 10 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"
4.1247 -
4.1248 -subsection {* A minimal example of yet another semantics *}
4.1249 -
4.1250 -text {* thanks to Elke Salecker *}
4.1251 -
4.1252 -types
4.1253 - vname = nat
4.1254 - vvalue = int
4.1255 - var_assign = "vname \<Rightarrow> vvalue" --"variable assignment"
4.1256 -
4.1257 -datatype ir_expr =
4.1258 - IrConst vvalue
4.1259 -| ObjAddr vname
4.1260 -| Add ir_expr ir_expr
4.1261 -
4.1262 -datatype val =
4.1263 - IntVal vvalue
4.1264 -
4.1265 -record configuration =
4.1266 - Env :: var_assign
4.1267 -
4.1268 -inductive eval_var ::
4.1269 - "ir_expr \<Rightarrow> configuration \<Rightarrow> val \<Rightarrow> bool"
4.1270 -where
4.1271 - irconst: "eval_var (IrConst i) conf (IntVal i)"
4.1272 -| objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)"
4.1273 -| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> eval_var (Add l r) conf (IntVal (vl+vr))"
4.1274 -
4.1275 -
4.1276 -code_pred eval_var .
4.1277 -thm eval_var.equation
4.1278 -
4.1279 -values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\<lambda>x. 0)|) val}"
4.1280 -
4.1281 -end
5.1 --- a/src/HOL/ex/ROOT.ML Tue Mar 23 19:03:05 2010 -0700
5.2 +++ b/src/HOL/ex/ROOT.ML Wed Mar 24 17:40:43 2010 +0100
5.3 @@ -12,8 +12,6 @@
5.4 "Codegenerator_Test",
5.5 "Codegenerator_Pretty_Test",
5.6 "NormalForm",
5.7 - "Predicate_Compile",
5.8 - "Predicate_Compile_ex",
5.9 "Predicate_Compile_Quickcheck"
5.10 ];
5.11