# HG changeset patch # User blanchet # Date 1382532816 -7200 # Node ID bc07627c5dcdfc4a72ddb7c48262b04430210bee # Parent a5eec4263b3ab2e62213c4e4cda1c61462818733 added 'primcorec' examples diff -r a5eec4263b3a -r bc07627c5dcd src/HOL/BNF/Examples/Misc_Codatatype.thy --- a/src/HOL/BNF/Examples/Misc_Codatatype.thy Wed Oct 23 09:58:30 2013 +0200 +++ b/src/HOL/BNF/Examples/Misc_Codatatype.thy Wed Oct 23 14:53:36 2013 +0200 @@ -19,9 +19,9 @@ codatatype simple'' = X1'' nat int | X2'' -codatatype 'a stream = Stream 'a "'a stream" +codatatype 'a stream = Stream (shd: 'a) (stl: "'a stream") -codatatype 'a mylist = MyNil | MyCons 'a "'a mylist" +codatatype 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist") codatatype ('b, 'c, 'd, 'e) some_passive = SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e diff -r a5eec4263b3a -r bc07627c5dcd src/HOL/BNF/Examples/Misc_Datatype.thy --- a/src/HOL/BNF/Examples/Misc_Datatype.thy Wed Oct 23 09:58:30 2013 +0200 +++ b/src/HOL/BNF/Examples/Misc_Datatype.thy Wed Oct 23 14:53:36 2013 +0200 @@ -19,7 +19,7 @@ datatype_new simple'' = X1'' nat int | X2'' -datatype_new 'a mylist = MyNil | MyCons 'a "'a mylist" +datatype_new 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist") datatype_new ('b, 'c, 'd, 'e) some_passive = SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e diff -r a5eec4263b3a -r bc07627c5dcd src/HOL/BNF/Examples/Misc_Primcorec.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BNF/Examples/Misc_Primcorec.thy Wed Oct 23 14:53:36 2013 +0200 @@ -0,0 +1,112 @@ +(* Title: HOL/BNF/Examples/Misc_Primcorec.thy + Author: Jasmin Blanchette, TU Muenchen + Copyright 2013 + +Miscellaneous primitive corecursive function definitions. +*) + +header {* Miscellaneous Primitive Corecursive Function Definitions *} + +theory Misc_Primcorec +imports Misc_Codatatype +begin + +primcorec simple_of_bools :: "bool \ bool \ simple" where + "simple_of_bools b b' = (if b then if b' then X1 else X2 else if b' then X3 else X4)" + +primcorec simple'_of_bools :: "bool \ bool \ simple'" where + "simple'_of_bools b b' = + (if b then if b' then X1' () else X2' () else if b' then X3' () else X4' ())" + +primcorec inc_simple'' :: "nat \ simple'' \ simple''" where + "inc_simple'' k s = (case s of X1'' n i \ X1'' (n + k) (i + int k) | X2'' \ X2'')" + +primcorec sinterleave :: "'a stream \ 'a stream \ 'a stream" where + "sinterleave s s' = Stream (shd s) (sinterleave s' (stl s))" + +primcorec myapp :: "'a mylist \ 'a mylist \ 'a mylist" where + "myapp xs ys = + (if xs = MyNil then ys + else if ys = MyNil then xs + else MyCons (myhd xs) (myapp (mytl xs) ys))" + +primcorec shuffle_sp :: "('a, 'b, 'c, 'd) some_passive \ ('d, 'a, 'b, 'c) some_passive" where + "shuffle_sp sp = + (case sp of + SP1 sp' \ SP1 (shuffle_sp sp') + | SP2 a \ SP3 a + | SP3 b \ SP4 b + | SP4 c \ SP5 c + | SP5 d \ SP2 d)" + +primcorec rename_lam :: "(string \ string) \ lambda \ lambda" where + "rename_lam f l = + (case l of + Var s \ Var (f s) + | App l l' \ App (rename_lam f l) (rename_lam f l') + | Abs s l \ Abs (f s) (rename_lam f l) + | Let SL l \ Let (fimage (map_pair f (rename_lam f)) SL) (rename_lam f l))" + +primcorec + j1_sum :: "('a\{zero,one,plus}) \ 'a J1" and + j2_sum :: "'a \ 'a J2" +where + "n = 0 \ is_J11 (j1_sum n)" | + "un_J111 (j1_sum _) = 0" | + "un_J112 (j1_sum _) = j1_sum 0" | + "un_J121 (j1_sum n) = n + 1" | + "un_J122 (j1_sum n) = j2_sum (n + 1)" | + "n = 0 \ is_J21 (j2_sum n)" | + "un_J221 (j2_sum n) = j1_sum (n + 1)" | + "un_J222 (j2_sum n) = j2_sum (n + 1)" + +primcorec forest_of_mylist :: "'a tree mylist \ 'a forest" where + "forest_of_mylist ts = + (case ts of + MyNil \ FNil + | MyCons t ts \ FCons t (forest_of_mylist ts))" + +primcorec mylist_of_forest :: "'a forest \ 'a tree mylist" where + "mylist_of_forest f = + (case f of + FNil \ MyNil + | FCons t ts \ MyCons t (mylist_of_forest ts))" + +primcorec semi_stream :: "'a stream \ 'a stream" where + "semi_stream s = Stream (shd s) (semi_stream (stl (stl s)))" + +primcorec + tree'_of_stream :: "'a stream \ 'a tree'" and + branch_of_stream :: "'a stream \ 'a branch" +where + "tree'_of_stream s = + TNode' (branch_of_stream (semi_stream s)) (branch_of_stream (semi_stream (stl s)))" | + "branch_of_stream s = (case s of Stream h t \ Branch h (tree'_of_stream t))" + +primcorec + freeze_exp :: "('b \ 'a) \ ('a, 'b) exp \ ('a, 'b) exp" and + freeze_trm :: "('b \ 'a) \ ('a, 'b) trm \ ('a, 'b) trm" and + freeze_factor :: "('b \ 'a) \ ('a, 'b) factor \ ('a, 'b) factor" +where + "freeze_exp g e = + (case e of + Term t \ Term (freeze_trm g t) + | Sum t e \ Sum (freeze_trm g t) (freeze_exp g e))" | + "freeze_trm g t = + (case t of + Factor f \ Factor (freeze_factor g f) + | Prod f t \ Prod (freeze_factor g f) (freeze_trm g t))" | + "freeze_factor g f = + (case f of + C a \ C a + | V b \ C (g b) + | Paren e \ Paren (freeze_exp g e))" + +primcorec poly_unity :: "'a poly_unit" where + "poly_unity = U (\_. poly_unity)" + +primcorec build_cps :: "('a \ 'a) \ ('a \ bool stream) \ 'a \ bool stream \ 'a cps" where + "shd b \ build_cps f g a b = CPS1 a" | + "_ \ build_cps f g a b = CPS2 (\a. build_cps f g (f a) (g a))" + +end diff -r a5eec4263b3a -r bc07627c5dcd src/HOL/BNF/Examples/Misc_Primrec.thy --- a/src/HOL/BNF/Examples/Misc_Primrec.thy Wed Oct 23 09:58:30 2013 +0200 +++ b/src/HOL/BNF/Examples/Misc_Primrec.thy Wed Oct 23 14:53:36 2013 +0200 @@ -14,7 +14,7 @@ primrec_new nat_of_simple :: "simple \ nat" where "nat_of_simple X1 = 1" | "nat_of_simple X2 = 2" | - "nat_of_simple X3 = 2" | + "nat_of_simple X3 = 3" | "nat_of_simple X4 = 4" primrec_new simple_of_simple' :: "simple' \ simple" where diff -r a5eec4263b3a -r bc07627c5dcd src/HOL/ROOT --- a/src/HOL/ROOT Wed Oct 23 09:58:30 2013 +0200 +++ b/src/HOL/ROOT Wed Oct 23 14:53:36 2013 +0200 @@ -733,6 +733,7 @@ theories [condition = ISABELLE_FULL_TEST] Misc_Codatatype Misc_Datatype + Misc_Primcorec Misc_Primrec session "HOL-Word" (main) in Word = HOL +