1.1 --- a/src/HOL/BNF/Examples/Process.thy	Wed Nov 13 12:32:26 2013 +0100
     1.2 +++ b/src/HOL/BNF/Examples/Process.thy	Wed Nov 13 11:23:25 2013 +0100
     1.3 @@ -81,24 +81,17 @@
     1.4  
     1.5  datatype x_y_ax = x | y | ax
     1.6  
     1.7 -definition "isA \<equiv> \<lambda> K. case K of x \<Rightarrow> False     |y \<Rightarrow> True  |ax \<Rightarrow> True"
     1.8 -definition "pr  \<equiv> \<lambda> K. case K of x \<Rightarrow> undefined |y \<Rightarrow> ''b'' |ax \<Rightarrow> ''a''"
     1.9 -definition "co  \<equiv> \<lambda> K. case K of x \<Rightarrow> undefined |y \<Rightarrow> x    |ax \<Rightarrow> x"
    1.10 -lemmas Action_defs = isA_def pr_def co_def
    1.11 +primcorec F :: "x_y_ax \<Rightarrow> char list process" where
    1.12 +  "xyax = x \<Longrightarrow> isChoice (F xyax)"
    1.13 +| "ch1Of (F xyax) = F ax"
    1.14 +| "ch2Of (F xyax) = F y"
    1.15 +| "prefOf (F xyax) = (if xyax = y then ''b'' else ''a'')"
    1.16 +| "contOf (F xyax) = F x"
    1.17  
    1.18 -definition "c1  \<equiv> \<lambda> K. case K of x \<Rightarrow> ax   |y \<Rightarrow> undefined |ax \<Rightarrow> undefined"
    1.19 -definition "c2  \<equiv> \<lambda> K. case K of x \<Rightarrow> y    |y \<Rightarrow> undefined |ax \<Rightarrow> undefined"
    1.20 -lemmas Choice_defs = c1_def c2_def
    1.21 -
    1.22 -definition "F \<equiv> process_unfold isA pr co c1 c2"
    1.23  definition "X = F x"  definition "Y = F y"  definition "AX = F ax"
    1.24  
    1.25  lemma X_Y_AX: "X = Choice AX Y"  "Y = Action ''b'' X"  "AX = Action ''a'' X"
    1.26 -unfolding X_def Y_def AX_def F_def
    1.27 -using process.unfold(2)[of isA x "pr" co c1 c2]
    1.28 -      process.unfold(1)[of isA y "pr" co c1 c2]
    1.29 -      process.unfold(1)[of isA ax "pr" co c1 c2]
    1.30 -unfolding Action_defs Choice_defs by simp_all
    1.31 +unfolding X_def Y_def AX_def by (subst F.code, simp)+
    1.32  
    1.33  (* end product: *)
    1.34  lemma X_AX: