# HG changeset patch
# User bulwahn
# Date 1258013430 -3600
# Node ID dd564a26fd2f7213a67a23b96de37091608e357d
# Parent  b6bf2dc5aed7407f473b3bb2fce610ae92ac38a0
adopted predicate compiler examples to new syntax for modes

diff -r b6bf2dc5aed7 -r dd564a26fd2f src/HOL/ex/Predicate_Compile_ex.thy
--- 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