added rudimentary code generation
authorhaftmann
Mon Oct 27 16:15:48 2008 +0100 (2008-10-27)
changeset 28693a1294a197d12
parent 28692 a2bc5ce0c9fc
child 28694 4e9edaef64dc
added rudimentary code generation
src/HOL/Library/Coinductive_List.thy
     1.1 --- a/src/HOL/Library/Coinductive_List.thy	Mon Oct 27 16:15:47 2008 +0100
     1.2 +++ b/src/HOL/Library/Coinductive_List.thy	Mon Oct 27 16:15:48 2008 +0100
     1.3 @@ -150,6 +150,8 @@
     1.4  definition "LNil = Abs_llist NIL"
     1.5  definition "LCons x xs = Abs_llist (CONS (Datatype.Leaf x) (Rep_llist xs))"
     1.6  
     1.7 +code_datatype LNil LCons
     1.8 +
     1.9  lemma LCons_not_LNil [iff]: "LCons x xs \<noteq> LNil"
    1.10    apply (simp add: LNil_def LCons_def)
    1.11    apply (subst Abs_llist_inject)
    1.12 @@ -196,7 +198,7 @@
    1.13  
    1.14  
    1.15  definition
    1.16 -  "llist_case c d l =
    1.17 +  [code del]: "llist_case c d l =
    1.18      List_case c (\<lambda>x y. d (inv Datatype.Leaf x) (Abs_llist y)) (Rep_llist l)"
    1.19  
    1.20  syntax  (* FIXME? *)
    1.21 @@ -205,17 +207,26 @@
    1.22  translations
    1.23    "case p of LNil \<Rightarrow> a | LCons x l \<Rightarrow> b" \<rightleftharpoons> "CONST llist_case a (\<lambda>x l. b) p"
    1.24  
    1.25 -lemma llist_case_LNil [simp]: "llist_case c d LNil = c"
    1.26 +lemma llist_case_LNil [simp, code]: "llist_case c d LNil = c"
    1.27    by (simp add: llist_case_def LNil_def
    1.28      NIL_type Abs_llist_inverse)
    1.29  
    1.30 -lemma llist_case_LCons [simp]: "llist_case c d (LCons M N) = d M N"
    1.31 +lemma llist_case_LCons [simp, code]: "llist_case c d (LCons M N) = d M N"
    1.32    by (simp add: llist_case_def LCons_def
    1.33      CONS_type Abs_llist_inverse Rep_llist Rep_llist_inverse inj_Leaf)
    1.34  
    1.35 +lemma llist_case_cert:
    1.36 +  includes meta_conjunction_syntax
    1.37 +  assumes "CASE \<equiv> llist_case c d"
    1.38 +  shows "(CASE LNil \<equiv> c) && (CASE (LCons M N) \<equiv> d M N)"
    1.39 +  using assms by simp_all
    1.40 +
    1.41 +setup {*
    1.42 +  Code.add_case @{thm llist_case_cert}
    1.43 +*}
    1.44  
    1.45  definition
    1.46 -  "llist_corec a f =
    1.47 +  [code del]: "llist_corec a f =
    1.48      Abs_llist (LList_corec a
    1.49        (\<lambda>z.
    1.50          case f z of None \<Rightarrow> None
    1.51 @@ -251,7 +262,7 @@
    1.52    qed
    1.53  qed
    1.54  
    1.55 -lemma llist_corec:
    1.56 +lemma llist_corec [code]:
    1.57    "llist_corec a f =
    1.58      (case f a of None \<Rightarrow> LNil | Some (z, w) \<Rightarrow> LCons z (llist_corec w f))"
    1.59  proof (cases "f a")