# HG changeset patch
# User traytel
# Date 1384338205 -3600
# Node ID 914e2ab723f0d1d550ee6ea9d61fba9080e7ac72
# Parent  4ca60c4301472b72be1757f9eff3f341f3408ae0
tuned example

diff -r 4ca60c430147 -r 914e2ab723f0 src/HOL/BNF/Examples/Process.thy
--- a/src/HOL/BNF/Examples/Process.thy	Wed Nov 13 12:32:26 2013 +0100
+++ b/src/HOL/BNF/Examples/Process.thy	Wed Nov 13 11:23:25 2013 +0100
@@ -81,24 +81,17 @@
 
 datatype x_y_ax = x | y | ax
 
-definition "isA \<equiv> \<lambda> K. case K of x \<Rightarrow> False     |y \<Rightarrow> True  |ax \<Rightarrow> True"
-definition "pr  \<equiv> \<lambda> K. case K of x \<Rightarrow> undefined |y \<Rightarrow> ''b'' |ax \<Rightarrow> ''a''"
-definition "co  \<equiv> \<lambda> K. case K of x \<Rightarrow> undefined |y \<Rightarrow> x    |ax \<Rightarrow> x"
-lemmas Action_defs = isA_def pr_def co_def
+primcorec F :: "x_y_ax \<Rightarrow> char list process" where
+  "xyax = x \<Longrightarrow> isChoice (F xyax)"
+| "ch1Of (F xyax) = F ax"
+| "ch2Of (F xyax) = F y"
+| "prefOf (F xyax) = (if xyax = y then ''b'' else ''a'')"
+| "contOf (F xyax) = F x"
 
-definition "c1  \<equiv> \<lambda> K. case K of x \<Rightarrow> ax   |y \<Rightarrow> undefined |ax \<Rightarrow> undefined"
-definition "c2  \<equiv> \<lambda> K. case K of x \<Rightarrow> y    |y \<Rightarrow> undefined |ax \<Rightarrow> undefined"
-lemmas Choice_defs = c1_def c2_def
-
-definition "F \<equiv> process_unfold isA pr co c1 c2"
 definition "X = F x"  definition "Y = F y"  definition "AX = F ax"
 
 lemma X_Y_AX: "X = Choice AX Y"  "Y = Action ''b'' X"  "AX = Action ''a'' X"
-unfolding X_def Y_def AX_def F_def
-using process.unfold(2)[of isA x "pr" co c1 c2]
-      process.unfold(1)[of isA y "pr" co c1 c2]
-      process.unfold(1)[of isA ax "pr" co c1 c2]
-unfolding Action_defs Choice_defs by simp_all
+unfolding X_def Y_def AX_def by (subst F.code, simp)+
 
 (* end product: *)
 lemma X_AX: