1875 |
1875 |
1876 In contrast, the next example is arguably more naturally expressed in the |
1876 In contrast, the next example is arguably more naturally expressed in the |
1877 constructor view: |
1877 constructor view: |
1878 *} |
1878 *} |
1879 |
1879 |
1880 primcorec_notyet |
1880 primcorec |
1881 random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process" |
1881 random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process" |
1882 where |
1882 where |
1883 "n mod 4 = 0 \<Longrightarrow> random_process s f n = Fail" | |
1883 "n mod 4 = 0 \<Longrightarrow> random_process s f n = Fail" | |
1884 "n mod 4 = 1 \<Longrightarrow> |
1884 "n mod 4 = 1 \<Longrightarrow> |
1885 random_process s f n = Skip (random_process s f (f n))" | |
1885 random_process s f n = Skip (random_process s f (f n))" | |
1985 |
1985 |
1986 The next example illustrates how to cope with selectors defined for several |
1986 The next example illustrates how to cope with selectors defined for several |
1987 constructors: |
1987 constructors: |
1988 *} |
1988 *} |
1989 |
1989 |
1990 primcorec_notyet |
1990 primcorec |
1991 random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process" |
1991 random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process" |
1992 where |
1992 where |
1993 "n mod 4 = 0 \<Longrightarrow> is_Fail (random_process s f n)" | |
1993 "n mod 4 = 0 \<Longrightarrow> is_Fail (random_process s f n)" | |
1994 "n mod 4 = 1 \<Longrightarrow> is_Skip (random_process s f n)" | |
1994 "n mod 4 = 1 \<Longrightarrow> is_Skip (random_process s f n)" | |
1995 "n mod 4 = 2 \<Longrightarrow> is_Action (random_process s f n)" | |
1995 "n mod 4 = 2 \<Longrightarrow> is_Action (random_process s f n)" | |
1996 "n mod 4 = 3 \<Longrightarrow> is_Choice (random_process s f n)" | |
1996 "n mod 4 = 3 \<Longrightarrow> is_Choice (random_process s f n)" | |
1997 "cont (random_process s f n) = random_process s f (f n)" (* of Skip FIXME *) | |
1997 "cont (random_process s f n) = random_process s f (f n)" of Skip | |
1998 "prefix (random_process s f n) = shd s" | |
1998 "prefix (random_process s f n) = shd s" | |
1999 "cont (random_process s f n) = random_process (stl s) f (f n)" (* of Action FIXME *) | |
1999 "cont (random_process s f n) = random_process (stl s) f (f n)" of Action | |
2000 "left (random_process s f n) = random_process (every_snd s) f (f n)" | |
2000 "left (random_process s f n) = random_process (every_snd s) f (f n)" | |
2001 "right (random_process s f n) = random_process (every_snd (stl s)) f (f n)" (*<*) |
2001 "right (random_process s f n) = random_process (every_snd (stl s)) f (f n)" |
2002 (*>*) |
|
2003 |
2002 |
2004 text {* |
2003 text {* |
2005 \noindent |
2004 \noindent |
2006 Using the @{text "of"} keyword, different equations are specified for @{const |
2005 Using the @{text "of"} keyword, different equations are specified for @{const |
2007 cont} depending on which constructor is selected. |
2006 cont} depending on which constructor is selected. |