1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Fri Aug 30 14:17:19 2013 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Fri Aug 30 15:05:04 2013 +0200
     1.3 @@ -7,19 +7,19 @@
     1.4  theory Datatypes
     1.5  imports Setup
     1.6  keywords
     1.7 -  "primrec_new" :: thy_decl and
     1.8 -  "primcorec" :: thy_decl
     1.9 +  "primrec_new_notyet" :: thy_decl and
    1.10 +  "primcorec_notyet" :: thy_decl
    1.11  begin
    1.12  
    1.13  (*<*)
    1.14 -(* FIXME: Evil setup until "primrec_new" and "primcorec" are in place. *)
    1.15 +(* FIXME: Evil setup until "primrec_new" and "primcorec" are bug-free. *)
    1.16  ML_command {*
    1.17  fun add_dummy_cmd _ _ lthy = lthy;
    1.18  
    1.19 -val _ = Outer_Syntax.local_theory @{command_spec "primrec_new"} ""
    1.20 +val _ = Outer_Syntax.local_theory @{command_spec "primrec_new_notyet"} ""
    1.21    (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_dummy_cmd);
    1.22  
    1.23 -val _ = Outer_Syntax.local_theory @{command_spec "primcorec"} ""
    1.24 +val _ = Outer_Syntax.local_theory @{command_spec "primcorec_notyet"} ""
    1.25    (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_dummy_cmd);
    1.26  *}
    1.27  (*>*)
    1.28 @@ -630,20 +630,24 @@
    1.29  to call a function recursively on an argument to a constructor:
    1.30  *}
    1.31  
    1.32 -    primrec_new replicate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.33 -      "rep Zero _ = []" |
    1.34 -      "rep (Suc n) a = a # rep n a"
    1.35 +    primrec_new replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
    1.36 +      "replicate Zero _ = []" |
    1.37 +      "replicate (Suc n) a = a # replicate n a"
    1.38  
    1.39  text {*
    1.40  we don't like the confusing name @{const nth}:
    1.41  *}
    1.42  
    1.43 -    primrec_new at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
    1.44 +    (* FIXME *)
    1.45 +    primrec_new_notyet at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
    1.46        "at (a # as) j =
    1.47           (case j of
    1.48              Zero \<Rightarrow> a
    1.49            | Suc j' \<Rightarrow> at as j')"
    1.50  
    1.51 +    primrec_new at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
    1.52 +      "at (a # as) j = nat_case a (at as) j"
    1.53 +
    1.54      primrec_new tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
    1.55        "tfold _ (TNil b) = b" |
    1.56        "tfold f (TCons a as) = f a (tfold f as)"
    1.57 @@ -689,13 +693,13 @@
    1.58  *}
    1.59  
    1.60      primrec_new
    1.61 -      eval\<^sub>e :: "('a, 'b) exp \<Rightarrow> real" and
    1.62 -      eval\<^sub>t :: "('a, 'b) trm \<Rightarrow> real" and
    1.63 -      eval\<^sub>f :: "('a, 'b) fct \<Rightarrow> real"
    1.64 +      eval\<^sub>e :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) exp \<Rightarrow> int" and
    1.65 +      eval\<^sub>t :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) trm \<Rightarrow> int" and
    1.66 +      eval\<^sub>f :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) fct \<Rightarrow> int"
    1.67      where
    1.68        "eval\<^sub>e \<gamma> \<xi> (Term t) = eval\<^sub>t \<gamma> \<xi> t" |
    1.69        "eval\<^sub>e \<gamma> \<xi> (Sum t e) = eval\<^sub>t \<gamma> \<xi> t + eval\<^sub>e \<gamma> \<xi> e" |
    1.70 -      "eval\<^sub>t \<gamma> \<xi> (Factor f) = eval\<^sub>f \<gamma> \<xi> f)" |
    1.71 +      "eval\<^sub>t \<gamma> \<xi> (Factor f) = eval\<^sub>f \<gamma> \<xi> f" |
    1.72        "eval\<^sub>t \<gamma> \<xi> (Prod f t) = eval\<^sub>f \<gamma> \<xi> f + eval\<^sub>t \<gamma> \<xi> t" |
    1.73        "eval\<^sub>f \<gamma> _ (Const a) = \<gamma> a" |
    1.74        "eval\<^sub>f _ \<xi> (Var b) = \<xi> b" |
    1.75 @@ -714,20 +718,14 @@
    1.76              [] \<Rightarrow> a
    1.77            | j # js' \<Rightarrow> at (map (\<lambda>t. at\<^sub>f\<^sub>f t js') ts) j)"
    1.78  
    1.79 -    primrec_new at\<^sub>f\<^sub>i :: "'a tree\<^sub>f\<^sub>i \<Rightarrow> nat list \<Rightarrow> 'a" where
    1.80 -      "at\<^sub>f\<^sub>i (Node\<^sub>f\<^sub>i a ts) js =
    1.81 -         (case js of
    1.82 -            [] \<Rightarrow> a
    1.83 -          | j # js' \<Rightarrow> at (lmap (\<lambda>t. at\<^sub>f\<^sub>i t js') ts) j)"
    1.84 -
    1.85  text {*
    1.86  Explain @{const lmap}.
    1.87  *}
    1.88  
    1.89 -    primrec_new sum_btree :: "('a\<Colon>plus) btree \<Rightarrow> 'a" where
    1.90 +    primrec_new_notyet sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
    1.91        "sum_btree (BNode a lt rt) =
    1.92 -         a + the_default Zero (option_map sum_btree lt) +
    1.93 -           the_default Zero (option_map sum_btree rt)"
    1.94 +         a + the_default 0 (option_map sum_btree lt) +
    1.95 +           the_default 0 (option_map sum_btree rt)"
    1.96  
    1.97  text {*
    1.98  Show example with function composition (ftree).
    1.99 @@ -741,7 +739,7 @@
   1.100    * e.g.
   1.101  *}
   1.102  
   1.103 -    primrec_new
   1.104 +    primrec_new_notyet
   1.105        at_tree\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" and
   1.106        at_trees\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f list \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> 'a"
   1.107      where
   1.108 @@ -754,13 +752,13 @@
   1.109              Zero \<Rightarrow> at_tree\<^sub>f\<^sub>f t
   1.110            | Suc j' \<Rightarrow> at_trees\<^sub>f\<^sub>f ts j')"
   1.111  
   1.112 -    primrec_new
   1.113 -      sum_btree :: "('a\<Colon>plus) btree \<Rightarrow> 'a" and
   1.114 -      sum_btree_option :: "('a\<Colon>plus) btree option \<Rightarrow> 'a"
   1.115 +    primrec_new_notyet
   1.116 +      sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" and
   1.117 +      sum_btree_option :: "'a btree option \<Rightarrow> 'a"
   1.118      where
   1.119        "sum_btree (BNode a lt rt) =
   1.120           a + sum_btree_option lt + sum_btree_option rt" |
   1.121 -      "sum_btree_option None = Zero" |
   1.122 +      "sum_btree_option None = 0" |
   1.123        "sum_btree_option (Some t) = sum_btree t"
   1.124  
   1.125  text {*
   1.126 @@ -858,24 +856,13 @@
   1.127  
   1.128      consts termi\<^sub>0 :: 'a
   1.129  
   1.130 -    datatype_new (*<*)(rep_compat) (*>*)('a, 'b) tlist_ =
   1.131 +    datatype_new ('a, 'b) tlist_ =
   1.132        TNil (termi: 'b) (defaults ttl: TNil)
   1.133      | TCons (thd: 'a) (ttl : "('a, 'b) tlist_") (defaults termi: "\<lambda>_ xs. termi\<^sub>0 xs")
   1.134  
   1.135 -(*<*)
   1.136 -    (* FIXME: remove hack once "primrec_new" is in place *)
   1.137 -    rep_datatype TNil TCons
   1.138 -    by (erule tlist_.induct, assumption) auto
   1.139 -(*>*)
   1.140      overloading
   1.141        termi\<^sub>0 \<equiv> "termi\<^sub>0 \<Colon> ('a, 'b) tlist_ \<Rightarrow> 'b"
   1.142      begin
   1.143 -(*<*)
   1.144 -    (* FIXME: remove hack once "primrec_new" is in place *)
   1.145 -    fun termi\<^sub>0 :: "('a, 'b) tlist_ \<Rightarrow> 'b" where
   1.146 -    "termi\<^sub>0 (TNil y) = y" |
   1.147 -    "termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs"
   1.148 -(*>*)
   1.149      primrec_new termi\<^sub>0 :: "('a, 'b) tlist_ \<Rightarrow> 'b" where
   1.150      "termi\<^sub>0 (TNil y) = y" |
   1.151      "termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs"