--- a/src/HOL/ex/Predicate_Compile_ex.thy Thu Nov 12 09:10:22 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Thu Nov 12 09:10:30 2009 +0100
@@ -6,31 +6,35 @@
inductive False' :: "bool"
-code_pred (mode : []) False' .
+code_pred (mode: bool) False' .
code_pred [depth_limited] False' .
code_pred [random] False' .
inductive EmptySet :: "'a \<Rightarrow> bool"
-code_pred (mode: [], [1]) EmptySet .
+code_pred (mode: o => bool, i => bool) EmptySet .
definition EmptySet' :: "'a \<Rightarrow> bool"
where "EmptySet' = {}"
-code_pred (mode: [], [1]) [inductify] EmptySet' .
+code_pred (mode: o => bool, i => bool) [inductify] EmptySet' .
inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
-code_pred (mode: [], [1], [2], [1, 2]) EmptyRel .
+code_pred (mode: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel .
inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
code_pred
- (mode: [] ==> [], [] ==> [1], [] ==> [2], [] ==> [1, 2],
- [1] ==> [], [1] ==> [1], [1] ==> [2], [1] ==> [1, 2],
- [2] ==> [], [2] ==> [1], [2] ==> [2], [2] ==> [1, 2],
- [1, 2] ==> [], [1, 2] ==> [1], [1, 2] ==> [2], [1, 2] ==> [1, 2])
+ (mode: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool,
+ (o => o => bool) => o => i => bool, (o => o => bool) => i => i => bool,
+ (i => o => bool) => o => o => bool, (i => o => bool) => i => o => bool,
+ (i => o => bool) => o => i => bool, (i => o => bool) => i => i => bool,
+ (o => i => bool) => o => o => bool, (o => i => bool) => i => o => bool,
+ (o => i => bool) => o => i => bool, (o => i => bool) => i => i => bool,
+ (i => i => bool) => o => o => bool, (i => i => bool) => i => o => bool,
+ (i => i => bool) => o => i => bool, (i => i => bool) => i => i => bool)
EmptyClosure .
thm EmptyClosure.equation
@@ -48,11 +52,12 @@
code_pred (mode: [1]) EmptySet'' .
code_pred (mode: [], [1]) [inductify] EmptySet'' .
*)
+
inductive True' :: "bool"
where
"True \<Longrightarrow> True'"
-code_pred (mode: []) True' .
+code_pred (mode: bool) True' .
consts a' :: 'a
@@ -60,13 +65,13 @@
where
"Fact a' a'"
-code_pred (mode: [], [1], [2], [1, 2]) Fact .
+code_pred (mode: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact .
inductive zerozero :: "nat * nat => bool"
where
"zerozero (0, 0)"
-code_pred (mode: [i], [(i, o)], [(o, i)], [o]) zerozero .
+code_pred (mode: i => bool, i * o => bool, o * i => bool, o => bool) zerozero .
code_pred [random] zerozero .
inductive JamesBond :: "nat => int => code_numeral => bool"
@@ -91,7 +96,7 @@
where
"(x = C) \<or> (x = D) ==> is_C_or_D x"
-code_pred (mode: [1]) is_C_or_D .
+code_pred (mode: i => bool) is_C_or_D .
thm is_C_or_D.equation
inductive is_D_or_E
@@ -106,7 +111,7 @@
"is_D_or_E E"
by (auto intro: is_D_or_E.intros)
-code_pred (mode: [], [1]) is_D_or_E
+code_pred (mode: o => bool, i => bool) is_D_or_E
proof -
case is_D_or_E
from this(1) show thesis
@@ -144,7 +149,7 @@
text {* Compilation of is_FGH requires elimination rule for is_F_or_G *}
-code_pred (mode: [], [1]) is_FGH
+code_pred (mode: o => bool, i => bool) is_FGH
proof -
case is_F_or_G
from this(1) show thesis
@@ -170,7 +175,7 @@
inductive zerozero' :: "nat * nat => bool" where
"equals (x, y) (0, 0) ==> zerozero' (x, y)"
-code_pred (mode: [1]) zerozero' .
+code_pred (mode: i => bool) zerozero' .
lemma zerozero'_eq: "zerozero' x == zerozero x"
proof -
@@ -190,7 +195,7 @@
text {* if preprocessing fails, zerozero'' will not have all modes. *}
-code_pred (mode: [o], [(i, o)], [(o,i)], [i]) [inductify] zerozero'' .
+code_pred (mode: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
subsection {* Numerals *}
@@ -228,7 +233,7 @@
| "even n \<Longrightarrow> odd (Suc n)"
| "odd n \<Longrightarrow> even (Suc n)"
-code_pred (mode: [], [1]) even .
+code_pred (mode: i => bool, o => bool) even .
code_pred [depth_limited] even .
code_pred [random] even .
@@ -251,7 +256,7 @@
definition odd' where "odd' x == \<not> even x"
-code_pred (mode: [1]) [inductify] odd' .
+code_pred (mode: i => bool) [inductify] odd' .
code_pred [inductify, depth_limited] odd' .
code_pred [inductify, random] odd' .
@@ -263,7 +268,7 @@
where
"n mod 2 = 0 \<Longrightarrow> is_even n"
-code_pred (mode: [1]) is_even .
+code_pred (mode: i => bool) is_even .
subsection {* append predicate *}
@@ -271,7 +276,8 @@
"append [] xs xs"
| "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
-code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append .
+code_pred (mode: i => i => o => bool, o => o => i => bool as "slice", o => i => i => bool as prefix,
+ i => o => i => bool as suffix, i => i => i => bool) append .
code_pred [depth_limited] append .
code_pred [random] append .
code_pred [annotated] append .
@@ -289,7 +295,7 @@
values [random] 1 "{(ys, zs). append [1::nat, 2] ys zs}"
value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])"
-value [code] "Predicate.the (append_3 ([]::int list))"
+value [code] "Predicate.the (slice ([]::int list))"
text {* tricky case with alternative rules *}
@@ -304,7 +310,8 @@
lemmas [code_pred_intros] = append2_Nil append2.intros(2)
-code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append2
+code_pred (mode: i => i => o => bool, o => o => i => bool, o => i => i => bool,
+ i => o => i => bool, i => i => i => bool) append2
proof -
case append2
from append2(1) show thesis
@@ -324,13 +331,14 @@
"tupled_append ([], xs, xs)"
| "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
-code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) tupled_append .
+code_pred (mode: 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 .
thm tupled_append.equation
-(*
-TODO: values with tupled modes
-values "{xs. tupled_append ([1,2,3], [4,5], xs)}"
-*)
+
+(*TODO: values with tupled modes*)
+(*values "{xs. tupled_append ([1,2,3], [4,5], xs)}"*)
+
inductive tupled_append'
where
@@ -338,7 +346,8 @@
| "[| ys = fst (xa, y); x # zs = snd (xa, y);
tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)"
-code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) tupled_append' .
+code_pred (mode: i * i * o => bool, o * o * i => bool, o * i * i => bool,
+ 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"
@@ -346,7 +355,8 @@
"tupled_append'' ([], xs, xs)"
| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
-code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) [inductify] tupled_append'' .
+code_pred (mode: i * i * o => bool, o * o * i => bool, o * i * i => bool,
+ i * o * i => bool, i * i * i => bool) [inductify] tupled_append'' .
thm tupled_append''.equation
inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
@@ -354,7 +364,8 @@
"tupled_append''' ([], xs, xs)"
| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
-code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) [inductify] tupled_append''' .
+code_pred (mode: i * i * o => bool, o * o * i => bool, o * i * i => bool,
+ i * o * i => bool, i * i * i => bool) [inductify] tupled_append''' .
thm tupled_append'''.equation
subsection {* map_ofP predicate *}
@@ -364,7 +375,7 @@
"map_ofP ((a, b)#xs) a b"
| "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
-code_pred (mode: [1], [1, 2], [1, 2, 3], [1, 3]) map_ofP .
+code_pred (mode: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP .
thm map_ofP.equation
subsection {* filter predicate *}
@@ -376,7 +387,7 @@
| "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)"
| "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys"
-code_pred (mode: [1] ==> [1], [1] ==> [1, 2]) filter1 .
+code_pred (mode: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 .
code_pred [depth_limited] filter1 .
code_pred [random] filter1 .
@@ -388,7 +399,7 @@
| "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 (mode: [1, 2, 3], [1, 2]) filter2 .
+code_pred (mode: i => i => i => bool, i => i => o => bool) filter2 .
code_pred [depth_limited] filter2 .
code_pred [random] filter2 .
thm filter2.equation
@@ -399,7 +410,7 @@
where
"List.filter P xs = ys ==> filter3 P xs ys"
-code_pred (mode: [] ==> [1], [] ==> [1, 2], [1] ==> [1], [1] ==> [1, 2]) filter3 .
+code_pred (mode: (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
@@ -407,7 +418,7 @@
where
"List.filter P xs = ys ==> filter4 P xs ys"
-code_pred (mode: [1, 2], [1, 2, 3]) filter4 .
+code_pred (mode: i => i => o => bool, i => i => i => bool) filter4 .
code_pred [depth_limited] filter4 .
code_pred [random] filter4 .
@@ -417,7 +428,7 @@
"rev [] []"
| "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
-code_pred (mode: [1], [2], [1, 2]) rev .
+code_pred (mode: i => o => bool, o => i => bool, i => i => bool) rev .
thm rev.equation
@@ -427,7 +438,7 @@
"tupled_rev ([], [])"
| "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)"
-code_pred (mode: [(i, o)], [(o, i)], [i]) tupled_rev .
+code_pred (mode: i * o => bool, o * i => bool, i * i => bool) tupled_rev .
thm tupled_rev.equation
subsection {* partition predicate *}
@@ -438,7 +449,8 @@
| "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
| "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
-code_pred (mode: [1] ==> [1], [1] ==> [2, 3], [1] ==> [1, 2], [1] ==> [1, 3], [1] ==> [1, 2, 3]) partition .
+code_pred (mode: (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 .
@@ -453,7 +465,8 @@
| "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)"
| "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)"
-code_pred (mode: [i] ==> [i], [i] ==> [(i, i, o)], [i] ==> [(i, o, i)], [i] ==> [(o, i, i)], [i] ==> [(i, o, o)]) tupled_partition .
+code_pred (mode: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool,
+ (i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition .
thm tupled_partition.equation
@@ -464,7 +477,9 @@
subsection {* transitive predicate *}
-code_pred (mode: [1] ==> [1, 2], [1] ==> [1], [2] ==> [1, 2], [2] ==> [2], [] ==> [1, 2], [] ==> [1], [] ==> [2], [] ==> []) tranclp
+code_pred (mode: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,
+ (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,
+ (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp
proof -
case tranclp
from this converse_tranclpE[OF this(1)] show thesis by metis
@@ -490,7 +505,7 @@
text {* values command needs mode annotation of the parameter succ
to disambiguate which mode is to be chosen. *}
-
+(* TODO: adopt to new mode syntax *)
values [mode: [1]] 20 "{n. tranclp succ 10 n}"
values [mode: [2]] 10 "{n. tranclp succ n 10}"
values 20 "{(n, m). tranclp succ n m}"
@@ -671,7 +686,7 @@
| "is_ord (MKT n l r h) =
((\<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)"
-code_pred (mode: [1], [1, 2]) [inductify] set_of .
+code_pred (mode: i => o => bool, i => i => bool) [inductify] set_of .
thm set_of.equation
code_pred [inductify] is_ord .
@@ -722,7 +737,7 @@
(*values [random] 1 "{xs. size_listP (xs::nat list) (5::nat)}"*)
-code_pred (mode: [1], [2], [1, 2]) [inductify] concat .
+code_pred (mode: i => o => bool, o => i => bool, i => i => bool) [inductify] concat .
thm concatP.equation
values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
@@ -731,7 +746,7 @@
code_pred [inductify, depth_limited] concat .
thm concatP.depth_limited_equation
-values [depth_limit = 3] 3
+values [depth_limit = 3] 3
"{xs. concatP xs ([0] :: nat list)}"
values [depth_limit = 5] 3
@@ -743,12 +758,12 @@
values [depth_limit = 5] 3
"{xs. concatP xs [(1::int), 2]}"
-code_pred (mode: [1], [1, 2]) [inductify] hd .
+code_pred (mode: i => o => bool, i => i => bool) [inductify] hd .
thm hdP.equation
values "{x. hdP [1, 2, (3::int)] x}"
values "{(xs, x). hdP [1, 2, (3::int)] 1}"
-code_pred (mode: [1], [1, 2]) [inductify] tl .
+code_pred (mode: i => o => bool, i => i => bool) [inductify] tl .
thm tlP.equation
values "{x. tlP [1, 2, (3::nat)] x}"
values "{x. tlP [1, 2, (3::int)] [3]}"
@@ -861,7 +876,7 @@
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
-code_pred (mode: [], [1]) S\<^isub>4p .
+code_pred (mode: o => bool, i => bool) S\<^isub>4p .
subsection {* Lambda *}
@@ -913,14 +928,14 @@
| appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
| abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
-code_pred (mode: [1, 2], [1, 2, 3]) typing .
+code_pred (mode: i => i => o => bool, i => i => i => bool) typing .
thm typing.equation
-code_pred (mode: [1], [1, 2]) beta .
+code_pred (mode: i => o => bool as reduce, i => i => bool) beta .
thm beta.equation
code_pred [random] typing .
-values [random] "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"
+values [random] 1 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"
end
\ No newline at end of file