1.1 --- a/src/HOL/BNF/Examples/Misc_Codatatype.thy	Wed Oct 23 09:58:30 2013 +0200
     1.2 +++ b/src/HOL/BNF/Examples/Misc_Codatatype.thy	Wed Oct 23 14:53:36 2013 +0200
     1.3 @@ -19,9 +19,9 @@
     1.4  
     1.5  codatatype simple'' = X1'' nat int | X2''
     1.6  
     1.7 -codatatype 'a stream = Stream 'a "'a stream"
     1.8 +codatatype 'a stream = Stream (shd: 'a) (stl: "'a stream")
     1.9  
    1.10 -codatatype 'a mylist = MyNil | MyCons 'a "'a mylist"
    1.11 +codatatype 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist")
    1.12  
    1.13  codatatype ('b, 'c, 'd, 'e) some_passive =
    1.14    SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e

     2.1 --- a/src/HOL/BNF/Examples/Misc_Datatype.thy	Wed Oct 23 09:58:30 2013 +0200
     2.2 +++ b/src/HOL/BNF/Examples/Misc_Datatype.thy	Wed Oct 23 14:53:36 2013 +0200
     2.3 @@ -19,7 +19,7 @@
     2.4  
     2.5  datatype_new simple'' = X1'' nat int | X2''
     2.6  
     2.7 -datatype_new 'a mylist = MyNil | MyCons 'a "'a mylist"
     2.8 +datatype_new 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist")
     2.9  
    2.10  datatype_new ('b, 'c, 'd, 'e) some_passive =
    2.11    SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/BNF/Examples/Misc_Primcorec.thy	Wed Oct 23 14:53:36 2013 +0200
     3.3 @@ -0,0 +1,112 @@
     3.4 +(*  Title:      HOL/BNF/Examples/Misc_Primcorec.thy
     3.5 +    Author:     Jasmin Blanchette, TU Muenchen
     3.6 +    Copyright   2013
     3.7 +
     3.8 +Miscellaneous primitive corecursive function definitions.
     3.9 +*)
    3.10 +
    3.11 +header {* Miscellaneous Primitive Corecursive Function Definitions *}
    3.12 +
    3.13 +theory Misc_Primcorec
    3.14 +imports Misc_Codatatype
    3.15 +begin
    3.16 +
    3.17 +primcorec simple_of_bools :: "bool \<Rightarrow> bool \<Rightarrow> simple" where
    3.18 +  "simple_of_bools b b' = (if b then if b' then X1 else X2 else if b' then X3 else X4)"
    3.19 +
    3.20 +primcorec simple'_of_bools :: "bool \<Rightarrow> bool \<Rightarrow> simple'" where
    3.21 +  "simple'_of_bools b b' =
    3.22 +     (if b then if b' then X1' () else X2' () else if b' then X3' () else X4' ())"
    3.23 +
    3.24 +primcorec inc_simple'' :: "nat \<Rightarrow> simple'' \<Rightarrow> simple''" where
    3.25 +  "inc_simple'' k s = (case s of X1'' n i \<Rightarrow> X1'' (n + k) (i + int k) | X2'' \<Rightarrow> X2'')"
    3.26 +
    3.27 +primcorec sinterleave :: "'a stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
    3.28 +  "sinterleave s s' = Stream (shd s) (sinterleave s' (stl s))"
    3.29 +
    3.30 +primcorec myapp :: "'a mylist \<Rightarrow> 'a mylist \<Rightarrow> 'a mylist" where
    3.31 +  "myapp xs ys =
    3.32 +     (if xs = MyNil then ys
    3.33 +      else if ys = MyNil then xs
    3.34 +      else MyCons (myhd xs) (myapp (mytl xs) ys))"
    3.35 +
    3.36 +primcorec shuffle_sp :: "('a, 'b, 'c, 'd) some_passive \<Rightarrow> ('d, 'a, 'b, 'c) some_passive" where
    3.37 +  "shuffle_sp sp =
    3.38 +     (case sp of
    3.39 +       SP1 sp' \<Rightarrow> SP1 (shuffle_sp sp')
    3.40 +     | SP2 a \<Rightarrow> SP3 a
    3.41 +     | SP3 b \<Rightarrow> SP4 b
    3.42 +     | SP4 c \<Rightarrow> SP5 c
    3.43 +     | SP5 d \<Rightarrow> SP2 d)"
    3.44 +
    3.45 +primcorec rename_lam :: "(string \<Rightarrow> string) \<Rightarrow> lambda \<Rightarrow> lambda" where
    3.46 +  "rename_lam f l =
    3.47 +     (case l of
    3.48 +       Var s \<Rightarrow> Var (f s)
    3.49 +     | App l l' \<Rightarrow> App (rename_lam f l) (rename_lam f l')
    3.50 +     | Abs s l \<Rightarrow> Abs (f s) (rename_lam f l)
    3.51 +     | Let SL l \<Rightarrow> Let (fimage (map_pair f (rename_lam f)) SL) (rename_lam f l))"
    3.52 +
    3.53 +primcorec
    3.54 +  j1_sum :: "('a\<Colon>{zero,one,plus}) \<Rightarrow> 'a J1" and
    3.55 +  j2_sum :: "'a \<Rightarrow> 'a J2"
    3.56 +where
    3.57 +  "n = 0 \<Longrightarrow> is_J11 (j1_sum n)" |
    3.58 +  "un_J111 (j1_sum _) = 0" |
    3.59 +  "un_J112 (j1_sum _) = j1_sum 0" |
    3.60 +  "un_J121 (j1_sum n) = n + 1" |
    3.61 +  "un_J122 (j1_sum n) = j2_sum (n + 1)" |
    3.62 +  "n = 0 \<Longrightarrow> is_J21 (j2_sum n)" |
    3.63 +  "un_J221 (j2_sum n) = j1_sum (n + 1)" |
    3.64 +  "un_J222 (j2_sum n) = j2_sum (n + 1)"
    3.65 +
    3.66 +primcorec forest_of_mylist :: "'a tree mylist \<Rightarrow> 'a forest" where
    3.67 +  "forest_of_mylist ts =
    3.68 +     (case ts of
    3.69 +       MyNil \<Rightarrow> FNil
    3.70 +     | MyCons t ts \<Rightarrow> FCons t (forest_of_mylist ts))"
    3.71 +
    3.72 +primcorec mylist_of_forest :: "'a forest \<Rightarrow> 'a tree mylist" where
    3.73 +  "mylist_of_forest f =
    3.74 +     (case f of
    3.75 +       FNil \<Rightarrow> MyNil
    3.76 +     | FCons t ts \<Rightarrow> MyCons t (mylist_of_forest ts))"
    3.77 +
    3.78 +primcorec semi_stream :: "'a stream \<Rightarrow> 'a stream" where
    3.79 +  "semi_stream s = Stream (shd s) (semi_stream (stl (stl s)))"
    3.80 +
    3.81 +primcorec
    3.82 +  tree'_of_stream :: "'a stream \<Rightarrow> 'a tree'" and
    3.83 +  branch_of_stream :: "'a stream \<Rightarrow> 'a branch"
    3.84 +where
    3.85 +  "tree'_of_stream s =
    3.86 +     TNode' (branch_of_stream (semi_stream s)) (branch_of_stream (semi_stream (stl s)))" |
    3.87 +  "branch_of_stream s = (case s of Stream h t \<Rightarrow> Branch h (tree'_of_stream t))"
    3.88 +
    3.89 +primcorec
    3.90 +  freeze_exp :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) exp \<Rightarrow> ('a, 'b) exp" and
    3.91 +  freeze_trm :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) trm \<Rightarrow> ('a, 'b) trm" and
    3.92 +  freeze_factor :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) factor \<Rightarrow> ('a, 'b) factor"
    3.93 +where
    3.94 +  "freeze_exp g e =
    3.95 +     (case e of
    3.96 +       Term t \<Rightarrow> Term (freeze_trm g t)
    3.97 +     | Sum t e \<Rightarrow> Sum (freeze_trm g t) (freeze_exp g e))" |
    3.98 +  "freeze_trm g t =
    3.99 +     (case t of
   3.100 +       Factor f \<Rightarrow> Factor (freeze_factor g f)
   3.101 +     | Prod f t \<Rightarrow> Prod (freeze_factor g f) (freeze_trm g t))" |
   3.102 +  "freeze_factor g f =
   3.103 +     (case f of
   3.104 +       C a \<Rightarrow> C a
   3.105 +     | V b \<Rightarrow> C (g b)
   3.106 +     | Paren e \<Rightarrow> Paren (freeze_exp g e))"
   3.107 +
   3.108 +primcorec poly_unity :: "'a poly_unit" where
   3.109 +  "poly_unity = U (\<lambda>_. poly_unity)"
   3.110 +
   3.111 +primcorec build_cps :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> bool stream) \<Rightarrow> 'a \<Rightarrow> bool stream \<Rightarrow> 'a cps" where
   3.112 +  "shd b \<Longrightarrow> build_cps f g a b = CPS1 a" |
   3.113 +  "_ \<Longrightarrow> build_cps f g a b = CPS2 (\<lambda>a. build_cps f g (f a) (g a))"
   3.114 +
   3.115 +end

     4.1 --- a/src/HOL/BNF/Examples/Misc_Primrec.thy	Wed Oct 23 09:58:30 2013 +0200
     4.2 +++ b/src/HOL/BNF/Examples/Misc_Primrec.thy	Wed Oct 23 14:53:36 2013 +0200
     4.3 @@ -14,7 +14,7 @@
     4.4  primrec_new nat_of_simple :: "simple \<Rightarrow> nat" where
     4.5    "nat_of_simple X1 = 1" |
     4.6    "nat_of_simple X2 = 2" |
     4.7 -  "nat_of_simple X3 = 2" |
     4.8 +  "nat_of_simple X3 = 3" |
     4.9    "nat_of_simple X4 = 4"
    4.10  
    4.11  primrec_new simple_of_simple' :: "simple' \<Rightarrow> simple" where

     5.1 --- a/src/HOL/ROOT	Wed Oct 23 09:58:30 2013 +0200
     5.2 +++ b/src/HOL/ROOT	Wed Oct 23 14:53:36 2013 +0200
     5.3 @@ -733,6 +733,7 @@
     5.4    theories [condition = ISABELLE_FULL_TEST]
     5.5      Misc_Codatatype
     5.6      Misc_Datatype
     5.7 +    Misc_Primcorec
     5.8      Misc_Primrec
     5.9  
    5.10  session "HOL-Word" (main) in Word = HOL +