# HG changeset patch
# User bulwahn
# Date 1269243013 -3600
# Node ID f8f882329a98bc5c2c50f0aeeae8e4a312f61edc
# Parent  9bb2c5b0c2975e6c8b6318025c73d1fb317a8e5b
enabling a previously broken example of the predicate compiler again

diff -r 9bb2c5b0c297 -r f8f882329a98 src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Mon Mar 22 08:30:13 2010 +0100
@@ -496,14 +496,15 @@
 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 (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .
 (*code_pred [depth_limited] filter4 .*)
 (*code_pred [random] filter4 .*)
-
+*)
 subsection {* reverse predicate *}
 
 inductive rev where
@@ -889,11 +890,11 @@
 
 code_pred [random_dseq inductify] lexn
 proof -
-  fix n xs ys
+  fix r 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   
+  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"
+  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"
+  from 1 2 3 show thesis
     unfolding lexn_conv Collect_def mem_def
     apply (auto simp add: has_length)
     apply (case_tac xys)
@@ -913,7 +914,7 @@
 thm lex.equation
 thm lex_def
 declare lenlex_conv[code_pred_def]
-code_pred [inductify, show_steps, show_intermediate_results] lenlex .
+code_pred [inductify] lenlex .
 thm lenlex.equation
 
 code_pred [random_dseq inductify] lenlex .
@@ -923,7 +924,6 @@
 thm lists.intros
 
 code_pred [inductify] lists .
-
 thm lists.equation
 
 subsection {* AVL Tree *}
@@ -1002,8 +1002,8 @@
   (o * o => bool) => i => bool,
   (i * o => bool) => i => bool) [inductify] Domain .
 thm Domain.equation
+
 thm Range_def
-
 code_pred (modes:
   (o * o => bool) => o => bool,
   (o * o => bool) => i => bool,
@@ -1013,9 +1013,9 @@
 code_pred [inductify] Field .
 thm Field.equation
 
-(*thm refl_on_def
+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 .
@@ -1025,9 +1025,9 @@
 code_pred [inductify] single_valued .
 thm single_valued.equation
 thm inv_image_def
-(*code_pred [inductify] inv_image .
+code_pred [inductify] inv_image .
 thm inv_image.equation
-*)
+
 subsection {* Inverting list functions *}
 
 (*code_pred [inductify] length .
@@ -1275,4 +1275,4 @@
 
 values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\<lambda>x. 0)|) val}"
 
-end
\ No newline at end of file
+end