--- a/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200
@@ -34,6 +34,8 @@
value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])"
value [code] "Predicate.the (append_3 ([]::int list))"
+subsection {* Tricky cases with tuples *}
+
inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
where
"tupled_append ([], xs, xs)"
@@ -43,8 +45,40 @@
thm tupled_append.equation
(*
+TODO: values with tupled modes
values "{xs. tupled_append ([1,2,3], [4,5], xs)}"
*)
+
+inductive tupled_append'
+where
+"tupled_append' ([], xs, xs)"
+| "[| ys = fst (xa, y); x # zs = snd (xa, y);
+ tupled_append' (xs, ys, x # zs) |] ==> tupled_append' (x # xs, xa, y)"
+
+code_pred tupled_append' .
+thm tupled_append'.equation
+(* TODO: Missing a few modes! *)
+
+inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
+where
+ "tupled_append'' ([], xs, xs)"
+| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, x # zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
+
+code_pred tupled_append'' .
+thm tupled_append''.equation
+(* TODO: Missing a few modes *)
+
+inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
+where
+ "tupled_append''' ([], xs, xs)"
+| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
+
+code_pred tupled_append''' .
+thm tupled_append'''.equation
+(* TODO: Missing a few modes *)
+
+section {* reverse *}
+
inductive rev where
"rev [] []"
| "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
@@ -142,6 +176,8 @@
values 20 "{(n, m). tranclp succ n m}"
*)
+subsection{* *}
+
subsection{* IMP *}
types