# HG changeset patch
# User bulwahn
# Date 1256630636 -3600
# Node ID 75b01355e5d4142a8ca4234e9e479c44911eddff
# Parent  d0c00b81db1da8e8d0cda0be1fffea7d87c1f861
adding test case for inlining of predicate compiler

diff -r d0c00b81db1d -r 75b01355e5d4 src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Tue Oct 27 09:03:56 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Tue Oct 27 09:03:56 2009 +0100
@@ -8,7 +8,7 @@
 
 code_pred (mode: []) False' .
 code_pred [depth_limited] False' .
-code_pred [rpred, show_compilation] False' .
+code_pred [rpred] False' .
 
 inductive EmptySet :: "'a \<Rightarrow> bool"
 
@@ -35,12 +35,12 @@
 
 code_pred (mode: []) False'' .
 
-inductive EmptySet' :: "'a \<Rightarrow> bool"
+inductive EmptySet'' :: "'a \<Rightarrow> bool"
 where
-  "False \<Longrightarrow> EmptySet' x"
+  "False \<Longrightarrow> EmptySet'' x"
 
-code_pred (mode: [1]) EmptySet' .
-code_pred (mode: [], [1]) [inductify] EmptySet' .
+code_pred (mode: [1]) EmptySet'' .
+code_pred (mode: [], [1]) [inductify] EmptySet'' .
 
 inductive True' :: "bool"
 where
@@ -63,6 +63,36 @@
 code_pred zerozero .
 code_pred [rpred, show_compilation] zerozero .
 
+subsection {* Preprocessor Inlining  *}
+
+definition "equals == (op =)"
+ 
+inductive zerozero' where
+  "equals (x, y) (0, 0) ==> zerozero' (x, y)"
+
+code_pred (mode: [1]) zerozero' .
+
+lemma zerozero'_eq: "zerozero' == zerozero"
+proof -
+  have "zerozero' = zerozero"
+    apply (auto simp add: mem_def)
+    apply (cases rule: zerozero'.cases)
+    apply (auto simp add: equals_def intro: zerozero.intros)
+    apply (cases rule: zerozero.cases)
+    apply (auto simp add: equals_def intro: zerozero'.intros)
+    done
+  from this show "zerozero' == zerozero" by auto
+qed
+
+declare zerozero'_eq [code_pred_inline]
+
+definition "zerozero'' x == zerozero' x"
+
+text {* if preprocessing fails, zerozero'' will not have all modes. *}
+ML {* Predicate_Compile_Inline_Defs.get @{context} *}
+(* TODO: *)
+code_pred (mode: [1]) [inductify, show_intermediate_results] zerozero'' .
+
 subsection {* even predicate *}
 
 inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
@@ -516,10 +546,11 @@
 code_pred [inductify] Image .
 thm Image.equation
 (*TODO: *)
+
 declare Id_on_def[unfolded UNION_def, code_pred_def]
 
-(*code_pred [inductify] Id_on .
-thm Id_on.equation*)
+code_pred [inductify] Id_on .
+thm Id_on.equation
 code_pred [inductify] Domain .
 thm Domain.equation
 code_pred [inductify] Range .
@@ -527,8 +558,8 @@
 code_pred [inductify] Field .
 declare Sigma_def[unfolded UNION_def, code_pred_def]
 declare refl_on_def[unfolded UNION_def, code_pred_def]
-(*code_pred [inductify] refl_on .
-thm refl_on.equation*)
+code_pred [inductify] refl_on .
+thm refl_on.equation
 code_pred [inductify] total_on .
 thm total_on.equation
 code_pred [inductify] antisym .