src/HOL/ex/Predicate_Compile_ex.thy

--- a/src/HOL/ex/Predicate_Compile_ex.thy	Thu Nov 12 09:10:37 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Thu Nov 12 09:10:42 2009 +0100
@@ -6,28 +6,28 @@
 
 inductive False' :: "bool"
 
-code_pred (mode: bool) False' .
+code_pred (expected_modes: bool) False' .
 code_pred [depth_limited] False' .
 code_pred [random] False' .
 
 inductive EmptySet :: "'a \<Rightarrow> bool"
 
-code_pred (mode: o => bool, i => bool) EmptySet .
+code_pred (expected_modes: o => bool, i => bool) EmptySet .
 
 definition EmptySet' :: "'a \<Rightarrow> bool"
 where "EmptySet' = {}"
 
-code_pred (mode: o => bool, i => bool) [inductify] EmptySet' .
+code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
 
 inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
 
-code_pred (mode: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel .
+code_pred (expected_modes: 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: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool,
+  (expected_modes: (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,
@@ -43,21 +43,21 @@
 where
   "False \<Longrightarrow> False''"
 
-code_pred (mode: []) False'' .
+code_pred (expected_modes: []) False'' .
 
 inductive EmptySet'' :: "'a \<Rightarrow> bool"
 where
   "False \<Longrightarrow> EmptySet'' x"
 
-code_pred (mode: [1]) EmptySet'' .
-code_pred (mode: [], [1]) [inductify] EmptySet'' .
+code_pred (expected_modes: [1]) EmptySet'' .
+code_pred (expected_modes: [], [1]) [inductify] EmptySet'' .
 *)
 
 inductive True' :: "bool"
 where
   "True \<Longrightarrow> True'"
 
-code_pred (mode: bool) True' .
+code_pred (expected_modes: bool) True' .
 
 consts a' :: 'a
 
@@ -65,13 +65,13 @@
 where
 "Fact a' a'"
 
-code_pred (mode: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact .
+code_pred (expected_modes: 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 => bool, i * o => bool, o * i => bool, o => bool) zerozero .
+code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero .
 code_pred [random] zerozero .
 
 inductive JamesBond :: "nat => int => code_numeral => bool"
@@ -96,7 +96,7 @@
 where
   "(x = C) \<or> (x = D) ==> is_C_or_D x"
 
-code_pred (mode: i => bool) is_C_or_D .
+code_pred (expected_modes: i => bool) is_C_or_D .
 thm is_C_or_D.equation
 
 inductive is_D_or_E
@@ -111,7 +111,7 @@
   "is_D_or_E E"
 by (auto intro: is_D_or_E.intros)
 
-code_pred (mode: o => bool, i => bool) is_D_or_E
+code_pred (expected_modes: o => bool, i => bool) is_D_or_E
 proof -
   case is_D_or_E
   from this(1) show thesis
@@ -149,7 +149,7 @@
 
 text {* Compilation of is_FGH requires elimination rule for is_F_or_G *}
 
-code_pred (mode: o => bool, i => bool) is_FGH
+code_pred (expected_modes: o => bool, i => bool) is_FGH
 proof -
   case is_F_or_G
   from this(1) show thesis
@@ -175,7 +175,7 @@
 inductive zerozero' :: "nat * nat => bool" where
   "equals (x, y) (0, 0) ==> zerozero' (x, y)"
 
-code_pred (mode: i => bool) zerozero' .
+code_pred (expected_modes: i => bool) zerozero' .
 
 lemma zerozero'_eq: "zerozero' x == zerozero x"
 proof -
@@ -195,7 +195,7 @@
 
 text {* if preprocessing fails, zerozero'' will not have all modes. *}
 
-code_pred (mode: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
+code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
 
 subsection {* Numerals *}
 
@@ -233,7 +233,7 @@
   | "even n \<Longrightarrow> odd (Suc n)"
   | "odd n \<Longrightarrow> even (Suc n)"
 
-code_pred (mode: i => bool, o => bool) even .
+code_pred (expected_modes: i => bool, o => bool) even .
 code_pred [depth_limited] even .
 code_pred [random] even .
 
@@ -256,7 +256,7 @@
 
 definition odd' where "odd' x == \<not> even x"
 
-code_pred (mode: i => bool) [inductify] odd' .
+code_pred (expected_modes: i => bool) [inductify] odd' .
 code_pred [inductify, depth_limited] odd' .
 code_pred [inductify, random] odd' .
 
@@ -268,7 +268,7 @@
 where
   "n mod 2 = 0 \<Longrightarrow> is_even n"
 
-code_pred (mode: i => bool) is_even .
+code_pred (expected_modes: i => bool) is_even .
 
 subsection {* append predicate *}
 
@@ -276,8 +276,8 @@
     "append [] xs xs"
   | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
 
-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 (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 .
@@ -294,7 +294,7 @@
 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}"
 
-value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])"
+value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
 value [code] "Predicate.the (slice ([]::int list))"
 
 
@@ -310,7 +310,7 @@
 
 lemmas [code_pred_intros] = append2_Nil append2.intros(2)
 
-code_pred (mode: i => i => o => bool, o => o => i => bool, o => i => i => bool,
+code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool,
   i => o => i => bool, i => i => i => bool) append2
 proof -
   case append2
@@ -331,7 +331,7 @@
   "tupled_append ([], xs, xs)"
 | "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
 
-code_pred (mode: i * i * o => bool, o * o * i => bool, o * i * i => bool,
+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 .
 thm tupled_append.equation
@@ -346,7 +346,7 @@
 | "[| 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 => bool, o * o * i => bool, o * i * i => bool,
+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' .
 thm tupled_append'.equation
 
@@ -355,7 +355,7 @@
   "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 => bool, o * o * i => bool, o * i * i => bool,
+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'' .
 thm tupled_append''.equation
 
@@ -364,7 +364,7 @@
   "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 => bool, o * o * i => bool, o * i * i => bool,
+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''' .
 thm tupled_append'''.equation
 
@@ -375,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: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP .
+code_pred (expected_modes: 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 *}
@@ -387,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: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 .
+code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 .
 code_pred [depth_limited] filter1 .
 code_pred [random] filter1 .
 
@@ -399,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: i => i => i => bool, i => i => o => bool) filter2 .
+code_pred (expected_modes: i => i => i => bool, i => i => o => bool) filter2 .
 code_pred [depth_limited] filter2 .
 code_pred [random] filter2 .
 thm filter2.equation
@@ -410,7 +410,7 @@
 where
   "List.filter P xs = ys ==> filter3 P xs ys"
 
-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 (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
 
@@ -418,7 +418,7 @@
 where
   "List.filter P xs = ys ==> filter4 P xs ys"
 
-code_pred (mode: i => i => o => bool, i => i => i => bool) filter4 .
+code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .
 code_pred [depth_limited] filter4 .
 code_pred [random] filter4 .
 
@@ -428,7 +428,7 @@
     "rev [] []"
   | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
 
-code_pred (mode: i => o => bool, o => i => bool, i => i => bool) rev .
+code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev .
 
 thm rev.equation
 
@@ -438,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 => bool, o * i => bool, i * i => bool) tupled_rev .
+code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev .
 thm tupled_rev.equation
 
 subsection {* partition predicate *}
@@ -449,7 +449,7 @@
   | "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: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool,
+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 .
@@ -465,7 +465,7 @@
   | "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 => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool,
+code_pred (expected_modes: (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
@@ -477,7 +477,7 @@
 
 subsection {* transitive predicate *}
 
-code_pred (mode: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,
+code_pred (modes: (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 -
@@ -577,9 +577,8 @@
 values 5
  "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
 
-(* FIXME:
 values 3 "{(a,q). step (par nil nil) a q}"
-*)
+
 
 inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
 where
@@ -686,7 +685,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: i => o => bool, i => i => bool) [inductify] set_of .
+code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of .
 thm set_of.equation
 
 code_pred [inductify] is_ord .
@@ -702,19 +701,15 @@
 thm rel_comp.equation
 code_pred [inductify] Image .
 thm Image.equation
-(*TODO: *)
-
-declare Id_on_def[unfolded UNION_def, code_pred_def]
-
-code_pred [inductify] Id_on .
+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 .
 thm Id_on.equation
 code_pred [inductify] Domain .
 thm Domain.equation
 code_pred [inductify] Range .
 thm Range.equation
 code_pred [inductify] Field .
-declare Sigma_def[unfolded UNION_def, code_pred_def]
-declare refl_on_def[unfolded UNION_def, code_pred_def]
+thm Field.equation
 code_pred [inductify] refl_on .
 thm refl_on.equation
 code_pred [inductify] total_on .
@@ -737,13 +732,13 @@
 
 (*values [random] 1 "{xs. size_listP (xs::nat list) (5::nat)}"*)
 
-code_pred (mode: i => o => bool, o => i => bool, i => i => bool) [inductify] concat .
+code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify] List.concat .
 thm concatP.equation
 
 values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
 values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}"
 
-code_pred [inductify, depth_limited] concat .
+code_pred [inductify, depth_limited] List.concat .
 thm concatP.depth_limited_equation
 
 values [depth_limit = 3] 3
@@ -758,12 +753,12 @@
 values [depth_limit = 5] 3
   "{xs. concatP xs [(1::int), 2]}"
 
-code_pred (mode: i => o => bool, i => i => bool) [inductify] hd .
+code_pred (expected_modes: 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: i => o => bool, i => i => bool) [inductify] tl .
+code_pred (expected_modes: 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]}"
@@ -876,7 +871,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: o => bool, i => bool) S\<^isub>4p .
+code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p .
 
 subsection {* Lambda *}
 
@@ -928,12 +923,15 @@
   | 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: i => i => o => bool, i => i => i => bool) typing .
+code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing .
 thm typing.equation
 
-code_pred (mode: i => o => bool as reduce, i => i => bool) beta .
+code_pred (modes: i => o => bool as reduce) beta .
 thm beta.equation
 
+ 
+values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \<rightarrow>\<^sub>\<beta> x}"
+
 code_pred [random] typing .
 
 values [random] 1 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"