--- a/src/HOL/ex/Predicate_Compile_ex.thy Sat Jan 16 21:14:15 2010 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Wed Jan 20 11:56:45 2010 +0100
@@ -1,5 +1,5 @@
theory Predicate_Compile_ex
-imports Main Predicate_Compile_Alternative_Defs
+imports Predicate_Compile_Alternative_Defs
begin
subsection {* Basic predicates *}
@@ -7,8 +7,35 @@
inductive False' :: "bool"
code_pred (expected_modes: bool) False' .
-code_pred [depth_limited] False' .
-code_pred [random] False' .
+code_pred [dseq] False' .
+code_pred [random_dseq] False' .
+
+values [expected "{}" pred] "{x. False'}"
+values [expected "{}" dseq 1] "{x. False'}"
+values [expected "{}" random_dseq 1, 1, 1] "{x. False'}"
+
+value "False'"
+
+
+inductive True' :: "bool"
+where
+ "True ==> True'"
+
+code_pred True' .
+code_pred [dseq] True' .
+code_pred [random_dseq] True' .
+
+thm True'.equation
+thm True'.dseq_equation
+thm True'.random_dseq_equation
+values [expected "{()}" ]"{x. True'}"
+values [expected "{}" dseq 0] "{x. True'}"
+values [expected "{()}" dseq 1] "{x. True'}"
+values [expected "{()}" dseq 2] "{x. True'}"
+values [expected "{}" random_dseq 1, 1, 0] "{x. True'}"
+values [expected "{}" random_dseq 1, 1, 1] "{x. True'}"
+values [expected "{()}" random_dseq 1, 1, 2] "{x. True'}"
+values [expected "{()}" random_dseq 1, 1, 3] "{x. True'}"
inductive EmptySet :: "'a \<Rightarrow> bool"
@@ -38,6 +65,7 @@
EmptyClosure .
thm EmptyClosure.equation
+
(* TODO: inductive package is broken!
inductive False'' :: "bool"
where
@@ -53,12 +81,6 @@
code_pred (expected_modes: [], [1]) [inductify] EmptySet'' .
*)
-inductive True' :: "bool"
-where
- "True \<Longrightarrow> True'"
-
-code_pred (expected_modes: bool) True' .
-
consts a' :: 'a
inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
@@ -72,7 +94,30 @@
"zerozero (0, 0)"
code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero .
-code_pred [random] zerozero .
+code_pred [dseq] zerozero .
+code_pred [random_dseq] zerozero .
+
+thm zerozero.equation
+thm zerozero.dseq_equation
+thm zerozero.random_dseq_equation
+
+text {* We expect the user to expand the tuples in the values command.
+The following values command is not supported. *}
+(*values "{x. zerozero x}" *)
+text {* Instead, the user must type *}
+values "{(x, y). zerozero (x, y)}"
+
+values [expected "{}" dseq 0] "{(x, y). zerozero (x, y)}"
+values [expected "{(0::nat, 0::nat)}" dseq 1] "{(x, y). zerozero (x, y)}"
+values [expected "{(0::nat, 0::nat)}" dseq 2] "{(x, y). zerozero (x, y)}"
+values [expected "{}" random_dseq 1, 1, 2] "{(x, y). zerozero (x, y)}"
+values [expected "{(0::nat, 0:: nat)}" random_dseq 1, 1, 3] "{(x, y). zerozero (x, y)}"
+
+inductive nested_tuples :: "((int * int) * int * int) => bool"
+where
+ "nested_tuples ((0, 1), 2, 3)"
+
+code_pred nested_tuples .
inductive JamesBond :: "nat => int => code_numeral => bool"
where
@@ -80,16 +125,17 @@
code_pred JamesBond .
-values "{(a, b, c). JamesBond a b c}"
-values "{(a, c, b). JamesBond a b c}"
-values "{(b, a, c). JamesBond a b c}"
-values "{(b, c, a). JamesBond a b c}"
-values "{(c, a, b). JamesBond a b c}"
-values "{(c, b, a). JamesBond a b c}"
+values [expected "{(0::nat, 0::int , 7::code_numeral)}"] "{(a, b, c). JamesBond a b c}"
+values [expected "{(0::nat, 7::code_numeral, 0:: int)}"] "{(a, c, b). JamesBond a b c}"
+values [expected "{(0::int, 0::nat, 7::code_numeral)}"] "{(b, a, c). JamesBond a b c}"
+values [expected "{(0::int, 7::code_numeral, 0::nat)}"] "{(b, c, a). JamesBond a b c}"
+values [expected "{(7::code_numeral, 0::nat, 0::int)}"] "{(c, a, b). JamesBond a b c}"
+values [expected "{(7::code_numeral, 0::int, 0::nat)}"] "{(c, b, a). JamesBond a b c}"
-values "{(a, b). JamesBond 0 b a}"
-values "{(c, a). JamesBond a 0 c}"
-values "{(a, c). JamesBond a 0 c}"
+values [expected "{(7::code_numeral, 0::int)}"] "{(a, b). JamesBond 0 b a}"
+values [expected "{(7::code_numeral, 0::nat)}"] "{(c, a). JamesBond a 0 c}"
+values [expected "{(0::nat, 7::code_numeral)}"] "{(a, c). JamesBond a 0 c}"
+
subsection {* Alternative Rules *}
@@ -119,14 +165,14 @@
case is_D_or_E
from this(1) show thesis
proof
- fix x
- assume x: "a1 = x"
- assume "x = D \<or> x = E"
+ fix xa
+ assume x: "x = xa"
+ assume "xa = D \<or> xa = E"
from this show thesis
proof
- assume "x = D" from this x is_D_or_E(2) show thesis by simp
+ assume "xa = D" from this x is_D_or_E(2) show thesis by simp
next
- assume "x = E" from this x is_D_or_E(3) show thesis by simp
+ assume "xa = E" from this x is_D_or_E(3) show thesis by simp
qed
qed
qed
@@ -157,15 +203,15 @@
case is_F_or_G
from this(1) show thesis
proof
- fix x
- assume x: "a1 = x"
- assume "x = F \<or> x = G"
+ fix xa
+ assume x: "x = xa"
+ assume "xa = F \<or> xa = G"
from this show thesis
proof
- assume "x = F"
+ assume "xa = F"
from this x is_F_or_G(2) show thesis by simp
next
- assume "x = G"
+ assume "xa = G"
from this x is_F_or_G(3) show thesis by simp
qed
qed
@@ -200,15 +246,16 @@
code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
-subsection {* Numerals *}
+subsection {* Sets and Numerals *}
definition
- "one_or_two == {Suc 0, (Suc (Suc 0))}"
+ "one_or_two = {Suc 0, (Suc (Suc 0))}"
-(*code_pred [inductify] one_or_two .*)
-code_pred [inductify, random] one_or_two .
-(*values "{x. one_or_two x}"*)
-values [random] "{x. one_or_two x}"
+code_pred [inductify] one_or_two .
+code_pred [dseq] one_or_two .
+(*code_pred [random_dseq] one_or_two .*)
+values [expected "{Suc 0::nat, 2::nat}"] "{x. one_or_two x}"
+(*values [random_dseq 1,1,2] "{x. one_or_two x}"*)
inductive one_or_two' :: "nat => bool"
where
@@ -222,13 +269,12 @@
definition one_or_two'':
"one_or_two'' == {1, (2::nat)}"
-
-code_pred [inductify] one_or_two'' .
+ML {* prop_of @{thm one_or_two''} *}
+(*code_pred [inductify] one_or_two'' .
thm one_or_two''.equation
values "{x. one_or_two'' x}"
-
-
+*)
subsection {* even predicate *}
inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
@@ -237,35 +283,55 @@
| "odd n \<Longrightarrow> even (Suc n)"
code_pred (expected_modes: i => bool, o => bool) even .
-code_pred [depth_limited] even .
-code_pred [random] even .
+code_pred [dseq] even .
+code_pred [random_dseq] even .
thm odd.equation
thm even.equation
-thm odd.depth_limited_equation
-thm even.depth_limited_equation
-thm even.random_equation
-thm odd.random_equation
+thm odd.dseq_equation
+thm even.dseq_equation
+thm odd.random_dseq_equation
+thm even.random_dseq_equation
values "{x. even 2}"
values "{x. odd 2}"
values 10 "{n. even n}"
values 10 "{n. odd n}"
-values [depth_limit = 2] "{x. even 6}"
-values [depth_limit = 7] "{x. even 6}"
-values [depth_limit = 2] "{x. odd 7}"
-values [depth_limit = 8] "{x. odd 7}"
-values [depth_limit = 7] 10 "{n. even n}"
+values [expected "{}" dseq 2] "{x. even 6}"
+values [expected "{}" dseq 6] "{x. even 6}"
+values [expected "{()}" dseq 7] "{x. even 6}"
+values [dseq 2] "{x. odd 7}"
+values [dseq 6] "{x. odd 7}"
+values [dseq 7] "{x. odd 7}"
+values [expected "{()}" dseq 8] "{x. odd 7}"
+
+values [expected "{}" dseq 0] 8 "{x. even x}"
+values [expected "{0::nat}" dseq 1] 8 "{x. even x}"
+values [expected "{0::nat, 2}" dseq 3] 8 "{x. even x}"
+values [expected "{0::nat, 2}" dseq 4] 8 "{x. even x}"
+values [expected "{0::nat, 2, 4}" dseq 6] 8 "{x. even x}"
+
+values [random_dseq 1, 1, 0] 8 "{x. even x}"
+values [random_dseq 1, 1, 1] 8 "{x. even x}"
+values [random_dseq 1, 1, 2] 8 "{x. even x}"
+values [random_dseq 1, 1, 3] 8 "{x. even x}"
+values [random_dseq 1, 1, 6] 8 "{x. even x}"
+
+values [expected "{}" random_dseq 1, 1, 7] "{x. odd 7}"
+values [random_dseq 1, 1, 8] "{x. odd 7}"
+values [random_dseq 1, 1, 9] "{x. odd 7}"
definition odd' where "odd' x == \<not> even x"
code_pred (expected_modes: i => bool) [inductify] odd' .
-code_pred [inductify, depth_limited] odd' .
-code_pred [inductify, random] odd' .
+code_pred [dseq inductify] odd' .
+code_pred [random_dseq inductify] odd' .
-thm odd'.depth_limited_equation
-values [depth_limit = 2] "{x. odd' 7}"
-values [depth_limit = 9] "{x. odd' 7}"
+values [expected "{}" dseq 2] "{x. odd' 7}"
+values [expected "{()}" dseq 9] "{x. odd' 7}"
+values [expected "{}" dseq 2] "{x. odd' 8}"
+values [expected "{}" dseq 10] "{x. odd' 8}"
+
inductive is_even :: "nat \<Rightarrow> bool"
where
@@ -280,22 +346,28 @@
| "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix,
- i => o => i => bool as suffix) append .
-code_pred [depth_limited] append .
-code_pred [random] append .
-code_pred [annotated] append .
+ i => o => i => bool as suffix, i => i => i => bool) append .
+code_pred [dseq] append .
+code_pred [random_dseq] append .
thm append.equation
-thm append.depth_limited_equation
-thm append.random_equation
-thm append.annotated_equation
+thm append.dseq_equation
+thm append.random_dseq_equation
values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
-values [depth_limit = 3] "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
-values [random] 1 "{(ys, zs). append [1::nat, 2] ys zs}"
+values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
+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)]}"
+values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
+values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
+values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
+values [random_dseq 1, 1, 1] 10 "{(xs, ys, zs::int list). append xs ys zs}"
+values [random_dseq 1, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
+values [random_dseq 3, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
+values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
+values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}"
value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
value [code] "Predicate.the (slice ([]::int list))"
@@ -320,11 +392,11 @@
from append2(1) show thesis
proof
fix xs
- assume "a1 = []" "a2 = xs" "a3 = xs"
+ assume "xa = []" "xb = xs" "xc = xs"
from this append2(2) show thesis by simp
next
fix xs ys zs x
- assume "a1 = x # xs" "a2 = ys" "a3 = x # zs" "append2 xs ys zs"
+ assume "xa = x # xs" "xb = ys" "xc = x # zs" "append2 xs ys zs"
from this append2(3) show thesis by fastsimp
qed
qed
@@ -336,11 +408,10 @@
code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
i * o * i => bool, i * i * i => bool) tupled_append .
-code_pred [random] tupled_append .
+code_pred [random_dseq] tupled_append .
thm tupled_append.equation
-(*TODO: values with tupled modes*)
-(*values "{xs. tupled_append ([1,2,3], [4,5], xs)}"*)
+values "{xs. tupled_append ([(1::nat), 2, 3], [4, 5], xs)}"
inductive tupled_append'
where
@@ -358,7 +429,7 @@
| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
- i * o * i => bool, i * i * i => bool) [inductify] tupled_append'' .
+ i * o * i => bool, i * i * i => bool) tupled_append'' .
thm tupled_append''.equation
inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
@@ -367,7 +438,7 @@
| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
- i * o * i => bool, i * i * i => bool) [inductify] tupled_append''' .
+ i * o * i => bool, i * i * i => bool) tupled_append''' .
thm tupled_append'''.equation
subsection {* map_ofP predicate *}
@@ -390,39 +461,46 @@
| "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys"
code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 .
-code_pred [depth_limited] filter1 .
-code_pred [random] filter1 .
+code_pred [dseq] filter1 .
+code_pred [random_dseq] filter1 .
thm filter1.equation
+values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
+values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
+values [expected "{[0::nat, 2, 4]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
+
inductive filter2
where
"filter2 P [] []"
| "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)"
| "\<not> P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys"
-code_pred (expected_modes: i => i => i => bool, i => i => o => bool) filter2 .
-code_pred [depth_limited] filter2 .
-code_pred [random] filter2 .
+code_pred (expected_modes: (i => bool) => i => i => bool, (i => bool) => i => o => bool) filter2 .
+code_pred [dseq] filter2 .
+code_pred [random_dseq] filter2 .
+
thm filter2.equation
-thm filter2.random_equation
+thm filter2.random_dseq_equation
+(*
inductive filter3
for P
where
"List.filter P xs = ys ==> filter3 P xs ys"
-code_pred (expected_modes: (o => bool) => i => o => bool, (o => bool) => i => i => bool , (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter3 .
-code_pred [depth_limited] filter3 .
-thm filter3.depth_limited_equation
+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 .
+code_pred [dseq] filter3 .
+thm filter3.dseq_equation
+*)
inductive filter4
where
"List.filter P xs = ys ==> filter4 P xs ys"
-code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .
-code_pred [depth_limited] filter4 .
-code_pred [random] filter4 .
+(*code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .*)
+(*code_pred [depth_limited] filter4 .*)
+(*code_pred [random] filter4 .*)
subsection {* reverse predicate *}
@@ -452,9 +530,10 @@
| "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool,
- (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool) partition .
-code_pred [depth_limited] partition .
-code_pred [random] partition .
+ (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool)
+ partition .
+code_pred [dseq] partition .
+code_pred [random_dseq] partition .
values 10 "{(ys, zs). partition is_even
[0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
@@ -489,19 +568,44 @@
from this converse_tranclpE[OF this(1)] show thesis by metis
qed
-code_pred [depth_limited] tranclp .
-code_pred [random] tranclp .
+
+code_pred [dseq] tranclp .
+code_pred [random_dseq] tranclp .
thm tranclp.equation
-thm tranclp.random_equation
+thm tranclp.random_dseq_equation
+
+inductive rtrancl' :: "'a => 'a => ('a => 'a => bool) => bool"
+where
+ "rtrancl' x x r"
+| "r x y ==> rtrancl' y z r ==> rtrancl' x z r"
+
+code_pred [random_dseq] rtrancl' .
+
+thm rtrancl'.random_dseq_equation
+
+inductive rtrancl'' :: "('a * 'a * ('a \<Rightarrow> 'a \<Rightarrow> bool)) \<Rightarrow> bool"
+where
+ "rtrancl'' (x, x, r)"
+| "r x y \<Longrightarrow> rtrancl'' (y, z, r) \<Longrightarrow> rtrancl'' (x, z, r)"
+
+code_pred rtrancl'' .
+
+inductive rtrancl''' :: "('a * ('a * 'a) * ('a * 'a => bool)) => bool"
+where
+ "rtrancl''' (x, (x, x), r)"
+| "r (x, y) ==> rtrancl''' (y, (z, z), r) ==> rtrancl''' (x, (z, z), r)"
+
+code_pred rtrancl''' .
+
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
"succ 0 1"
| "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
-code_pred succ .
-code_pred [random] succ .
+code_pred (modes: i => i => bool, i => o => bool, o => i => bool, o => o => bool) succ .
+code_pred [random_dseq] succ .
thm succ.equation
-thm succ.random_equation
+thm succ.random_dseq_equation
values 10 "{(m, n). succ n m}"
values "{m. succ 0 m}"
@@ -531,10 +635,55 @@
code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph .
thm not_reachable_in_example_graph.equation
-
+thm tranclp.equation
value "not_reachable_in_example_graph 0 3"
value "not_reachable_in_example_graph 4 8"
value "not_reachable_in_example_graph 5 6"
+text {* rtrancl compilation is strange! *}
+(*
+value "not_reachable_in_example_graph 0 4"
+value "not_reachable_in_example_graph 1 6"
+value "not_reachable_in_example_graph 8 4"*)
+
+code_pred [dseq] not_reachable_in_example_graph .
+
+values [dseq 6] "{x. tranclp example_graph 0 3}"
+
+values [dseq 0] "{x. not_reachable_in_example_graph 0 3}"
+values [dseq 0] "{x. not_reachable_in_example_graph 0 4}"
+values [dseq 20] "{x. not_reachable_in_example_graph 0 4}"
+values [dseq 6] "{x. not_reachable_in_example_graph 0 3}"
+values [dseq 3] "{x. not_reachable_in_example_graph 4 2}"
+values [dseq 6] "{x. not_reachable_in_example_graph 4 2}"
+
+
+inductive not_reachable_in_example_graph' :: "int => int => bool"
+where "\<not> (rtranclp example_graph x y) ==> not_reachable_in_example_graph' x y"
+
+code_pred not_reachable_in_example_graph' .
+
+value "not_reachable_in_example_graph' 0 3"
+(* value "not_reachable_in_example_graph' 0 5" would not terminate *)
+
+
+(*values [depth_limited 0] "{x. not_reachable_in_example_graph' 0 3}"*)
+(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
+(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"*)
+(*values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
+(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
+(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
+
+code_pred [dseq] not_reachable_in_example_graph' .
+
+(*thm not_reachable_in_example_graph'.dseq_equation*)
+
+(*values [dseq 0] "{x. not_reachable_in_example_graph' 0 3}"*)
+(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
+(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"
+values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
+(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
+(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
+
subsection {* IMP *}
@@ -564,6 +713,7 @@
(While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))))
[3,5] t}"
+
inductive tupled_exec :: "(com \<times> state \<times> state) \<Rightarrow> bool" where
"tupled_exec (Skip, s, s)" |
"tupled_exec (Ass x e, s, s[x := e(s)])" |
@@ -575,6 +725,8 @@
code_pred tupled_exec .
+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)}"
+
subsection {* CCS *}
text{* This example formalizes finite CCS processes without communication or
@@ -633,13 +785,16 @@
where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
code_pred [inductify] Min .
+thm Min.equation
subsection {* Lexicographic order *}
+declare lexord_def[code_pred_def]
code_pred [inductify] lexord .
-code_pred [inductify, random] lexord .
+code_pred [random_dseq inductify] lexord .
+
thm lexord.equation
-thm lexord.random_equation
+thm lexord.random_dseq_equation
inductive less_than_nat :: "nat * nat => bool"
where
@@ -648,38 +803,100 @@
code_pred less_than_nat .
-code_pred [depth_limited] less_than_nat .
-code_pred [random] less_than_nat .
+code_pred [dseq] less_than_nat .
+code_pred [random_dseq] less_than_nat .
inductive test_lexord :: "nat list * nat list => bool"
where
"lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)"
-code_pred [random] test_lexord .
-code_pred [depth_limited] test_lexord .
-thm test_lexord.depth_limited_equation
-thm test_lexord.random_equation
+code_pred test_lexord .
+code_pred [dseq] test_lexord .
+code_pred [random_dseq] test_lexord .
+thm test_lexord.dseq_equation
+thm test_lexord.random_dseq_equation
values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
-values [depth_limit = 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
+(*values [depth_limited 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"*)
+declare list.size(3,4)[code_pred_def]
lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
-
+(*
code_pred [inductify] lexn .
thm lexn.equation
+*)
+(*
+code_pred [random_dseq inductify] lexn .
+thm lexn.random_dseq_equation
-code_pred [random] lexn .
+values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
+*)
+inductive has_length
+where
+ "has_length [] 0"
+| "has_length xs i ==> has_length (x # xs) (Suc i)"
+
+lemma has_length:
+ "has_length xs n = (length xs = n)"
+proof (rule iffI)
+ assume "has_length xs n"
+ from this show "length xs = n"
+ by (rule has_length.induct) auto
+next
+ assume "length xs = n"
+ from this show "has_length xs n"
+ by (induct xs arbitrary: n) (auto intro: has_length.intros)
+qed
-thm lexn.random_equation
+lemma lexn_intros [code_pred_intro]:
+ "has_length xs i ==> has_length ys i ==> r (x, y) ==> lexn r (Suc i) (x # xs, y # ys)"
+ "lexn r i (xs, ys) ==> lexn r (Suc i) (x # xs, x # ys)"
+proof -
+ assume "has_length xs i" "has_length ys i" "r (x, y)"
+ from this has_length show "lexn r (Suc i) (x # xs, y # ys)"
+ unfolding lexn_conv Collect_def mem_def
+ by fastsimp
+next
+ assume "lexn r i (xs, ys)"
+ thm lexn_conv
+ from this show "lexn r (Suc i) (x#xs, x#ys)"
+ unfolding Collect_def mem_def lexn_conv
+ apply auto
+ apply (rule_tac x="x # xys" in exI)
+ by auto
+qed
+
+code_pred [random_dseq inductify] lexn
+proof -
+ fix n xs ys
+ assume 1: "lexn r n (xs, ys)"
+ assume 2: "\<And>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"
+ assume 3: "\<And>i x xs' ys'. r = r ==> n = Suc i ==> (xs, ys) = (x # xs', x # ys') ==> lexn r i (xs', ys') ==> thesis"
+ from 1 2 3 show thesis
+ unfolding lexn_conv Collect_def mem_def
+ apply (auto simp add: has_length)
+ apply (case_tac xys)
+ apply auto
+ apply fastsimp
+ apply fastsimp done
+qed
+
+
+values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
+
code_pred [inductify] lenlex .
thm lenlex.equation
-code_pred [inductify, random] lenlex .
-thm lenlex.random_equation
+code_pred [random_dseq inductify] lenlex .
+thm lenlex.random_dseq_equation
+values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}"
+thm lists.intros
+(*
code_pred [inductify] lists .
-thm lists.equation
+*)
+(*thm lists.equation*)
subsection {* AVL Tree *}
@@ -693,12 +910,14 @@
"avl ET = True"
"avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and>
h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
-
+(*
code_pred [inductify] avl .
-thm avl.equation
+thm avl.equation*)
-code_pred [random] avl .
-thm avl.random_equation
+code_pred [random_dseq inductify] avl .
+thm avl.random_dseq_equation
+
+values [random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
fun set_of
where
@@ -714,30 +933,57 @@
code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of .
thm set_of.equation
-code_pred [inductify] is_ord .
+code_pred (expected_modes: i => bool) [inductify] is_ord .
thm is_ord_aux.equation
thm is_ord.equation
subsection {* Definitions about Relations *}
+term "converse"
+code_pred (modes:
+ (i * i => bool) => i * i => bool,
+ (i * o => bool) => o * i => bool,
+ (i * o => bool) => i * i => bool,
+ (o * i => bool) => i * o => bool,
+ (o * i => bool) => i * i => bool,
+ (o * o => bool) => o * o => bool,
+ (o * o => bool) => i * o => bool,
+ (o * o => bool) => o * i => bool,
+ (o * o => bool) => i * i => bool) [inductify] converse .
-code_pred [inductify] converse .
thm converse.equation
code_pred [inductify] rel_comp .
thm rel_comp.equation
code_pred [inductify] Image .
thm Image.equation
-code_pred (expected_modes: (o => bool) => o => bool, (o => bool) => i * o => bool,
- (o => bool) => o * i => bool, (o => bool) => i => bool) [inductify] Id_on .
+declare singleton_iff[code_pred_inline]
+declare Id_on_def[unfolded Bex_def UNION_def singleton_iff, code_pred_def]
+
+code_pred (expected_modes:
+ (o => bool) => o => bool,
+ (o => bool) => i * o => bool,
+ (o => bool) => o * i => bool,
+ (o => bool) => i => bool,
+ (i => bool) => i * o => bool,
+ (i => bool) => o * i => bool,
+ (i => bool) => i => bool) [inductify] Id_on .
thm Id_on.equation
-code_pred [inductify] Domain .
+thm Domain_def
+code_pred (modes:
+ (o * o => bool) => o => bool,
+ (o * o => bool) => i => bool,
+ (i * o => bool) => i => bool) [inductify] Domain .
thm Domain.equation
-code_pred [inductify] Range .
+code_pred (modes:
+ (o * o => bool) => o => bool,
+ (o * o => bool) => i => bool,
+ (o * i => bool) => i => bool) [inductify] Range .
thm Range.equation
code_pred [inductify] Field .
thm Field.equation
+(*thm refl_on_def
code_pred [inductify] refl_on .
-thm refl_on.equation
+thm refl_on.equation*)
code_pred [inductify] total_on .
thm total_on.equation
code_pred [inductify] antisym .
@@ -751,11 +997,11 @@
subsection {* Inverting list functions *}
-code_pred [inductify] length .
-code_pred [inductify, random] length .
+(*code_pred [inductify] length .
+code_pred [random inductify] length .
thm size_listP.equation
thm size_listP.random_equation
-
+*)
(*values [random] 1 "{xs. size_listP (xs::nat list) (5::nat)}"*)
code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify] List.concat .
@@ -764,19 +1010,19 @@
values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}"
-code_pred [inductify, depth_limited] List.concat .
-thm concatP.depth_limited_equation
+code_pred [dseq inductify] List.concat .
+thm concatP.dseq_equation
-values [depth_limit = 3] 3
+values [dseq 3] 3
"{xs. concatP xs ([0] :: nat list)}"
-values [depth_limit = 5] 3
+values [dseq 5] 3
"{xs. concatP xs ([1] :: int list)}"
-values [depth_limit = 5] 3
+values [dseq 5] 3
"{xs. concatP xs ([1] :: nat list)}"
-values [depth_limit = 5] 3
+values [dseq 5] 3
"{xs. concatP xs [(1::int), 2]}"
code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd .
@@ -803,11 +1049,11 @@
code_pred [inductify] zip .
thm zipP.equation
-(*code_pred [inductify] upt .*)
+code_pred [inductify] upt .
code_pred [inductify] remdups .
thm remdupsP.equation
-code_pred [inductify, depth_limited] remdups .
-values [depth_limit = 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
+code_pred [dseq inductify] remdups .
+values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
code_pred [inductify] remove1 .
thm remove1P.equation
@@ -815,13 +1061,12 @@
code_pred [inductify] removeAll .
thm removeAllP.equation
-code_pred [inductify, depth_limited] removeAll .
+code_pred [dseq inductify] removeAll .
-values [depth_limit = 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}"
+values [dseq 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}"
code_pred [inductify] distinct .
thm distinct.equation
-
code_pred [inductify] replicate .
thm replicateP.equation
values 5 "{(n, xs). replicateP n (0::int) xs}"
@@ -837,7 +1082,7 @@
code_pred [inductify] foldr .
code_pred [inductify] foldl .
code_pred [inductify] filter .
-code_pred [inductify, random] filter .
+code_pred [random_dseq inductify] filter .
subsection {* Context Free Grammar *}
@@ -852,11 +1097,11 @@
| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
code_pred [inductify] S\<^isub>1p .
-code_pred [inductify, random] S\<^isub>1p .
+code_pred [random_dseq inductify] S\<^isub>1p .
thm S\<^isub>1p.equation
-thm S\<^isub>1p.random_equation
+thm S\<^isub>1p.random_dseq_equation
-values [random] 5 "{x. S\<^isub>1p x}"
+values [random_dseq 5, 5, 5] 5 "{x. S\<^isub>1p x}"
inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
"[] \<in> S\<^isub>2"
@@ -866,12 +1111,12 @@
| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
-code_pred [inductify, random] S\<^isub>2 .
-thm S\<^isub>2.random_equation
-thm A\<^isub>2.random_equation
-thm B\<^isub>2.random_equation
+code_pred [random_dseq inductify] S\<^isub>2p .
+thm S\<^isub>2p.random_dseq_equation
+thm A\<^isub>2p.random_dseq_equation
+thm B\<^isub>2p.random_dseq_equation
-values [random] 10 "{x. S\<^isub>2 x}"
+values [random_dseq 5, 5, 5] 10 "{x. S\<^isub>2p x}"
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
"[] \<in> S\<^isub>3"
@@ -881,10 +1126,10 @@
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
-code_pred [inductify] S\<^isub>3 .
-thm S\<^isub>3.equation
+code_pred [inductify] S\<^isub>3p .
+thm S\<^isub>3p.equation
-values 10 "{x. S\<^isub>3 x}"
+values 10 "{x. S\<^isub>3p x}"
inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
"[] \<in> S\<^isub>4"
@@ -950,7 +1195,7 @@
code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing .
thm typing.equation
-code_pred (modes: i => o => bool as reduce') beta .
+code_pred (modes: i => i => bool, i => o => bool as reduce') beta .
thm beta.equation
values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \<rightarrow>\<^sub>\<beta> x}"
@@ -959,18 +1204,19 @@
value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))"
-code_pred [random] typing .
+code_pred [dseq] typing .
+code_pred [random_dseq] typing .
-values [random] 1 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"
+values [random_dseq 1,1,5] 10 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"
subsection {* A minimal example of yet another semantics *}
text {* thanks to Elke Salecker *}
types
-vname = nat
-vvalue = int
-var_assign = "vname \<Rightarrow> vvalue" --"variable assignment"
+ vname = nat
+ vvalue = int
+ var_assign = "vname \<Rightarrow> vvalue" --"variable assignment"
datatype ir_expr =
IrConst vvalue
@@ -981,10 +1227,10 @@
IntVal vvalue
record configuration =
-Env :: var_assign
+ Env :: var_assign
inductive eval_var ::
-"ir_expr \<Rightarrow> configuration \<Rightarrow> val \<Rightarrow> bool"
+ "ir_expr \<Rightarrow> configuration \<Rightarrow> val \<Rightarrow> bool"
where
irconst: "eval_var (IrConst i) conf (IntVal i)"
| objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)"