src/HOL/Datatype_Examples/Misc_Primcorec.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 58309 a09ec6daaa19
child 61076 bdc1e2f0a86a
permissions -rw-r--r--
modernized header uniformly as section;
blanchet@58309
     1
(*  Title:      HOL/Datatype_Examples/Misc_Primcorec.thy
blanchet@54193
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@54193
     3
    Copyright   2013
blanchet@54193
     4
blanchet@54193
     5
Miscellaneous primitive corecursive function definitions.
blanchet@54193
     6
*)
blanchet@54193
     7
wenzelm@58889
     8
section {* Miscellaneous Primitive Corecursive Function Definitions *}
blanchet@54193
     9
blanchet@54193
    10
theory Misc_Primcorec
blanchet@54193
    11
imports Misc_Codatatype
blanchet@54193
    12
begin
blanchet@54193
    13
blanchet@54193
    14
primcorec simple_of_bools :: "bool \<Rightarrow> bool \<Rightarrow> simple" where
blanchet@54193
    15
  "simple_of_bools b b' = (if b then if b' then X1 else X2 else if b' then X3 else X4)"
blanchet@54193
    16
blanchet@54193
    17
primcorec simple'_of_bools :: "bool \<Rightarrow> bool \<Rightarrow> simple'" where
blanchet@54193
    18
  "simple'_of_bools b b' =
blanchet@54193
    19
     (if b then if b' then X1' () else X2' () else if b' then X3' () else X4' ())"
blanchet@54193
    20
blanchet@54193
    21
primcorec inc_simple'' :: "nat \<Rightarrow> simple'' \<Rightarrow> simple''" where
blanchet@54193
    22
  "inc_simple'' k s = (case s of X1'' n i \<Rightarrow> X1'' (n + k) (i + int k) | X2'' \<Rightarrow> X2'')"
blanchet@54193
    23
blanchet@54193
    24
primcorec sinterleave :: "'a stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
blanchet@54193
    25
  "sinterleave s s' = Stream (shd s) (sinterleave s' (stl s))"
blanchet@54193
    26
blanchet@54193
    27
primcorec myapp :: "'a mylist \<Rightarrow> 'a mylist \<Rightarrow> 'a mylist" where
blanchet@54193
    28
  "myapp xs ys =
blanchet@54193
    29
     (if xs = MyNil then ys
blanchet@54193
    30
      else if ys = MyNil then xs
blanchet@54193
    31
      else MyCons (myhd xs) (myapp (mytl xs) ys))"
blanchet@54193
    32
blanchet@58231
    33
primcorec shuffle_sp :: "('a \<Colon> ord, 'b \<Colon> ord, 'c, 'd) some_passive \<Rightarrow> ('d, 'a, 'b, 'c) some_passive" where
blanchet@54193
    34
  "shuffle_sp sp =
blanchet@54193
    35
     (case sp of
blanchet@54193
    36
       SP1 sp' \<Rightarrow> SP1 (shuffle_sp sp')
blanchet@54193
    37
     | SP2 a \<Rightarrow> SP3 a
blanchet@54193
    38
     | SP3 b \<Rightarrow> SP4 b
blanchet@54193
    39
     | SP4 c \<Rightarrow> SP5 c
blanchet@54193
    40
     | SP5 d \<Rightarrow> SP2 d)"
blanchet@54193
    41
blanchet@54193
    42
primcorec rename_lam :: "(string \<Rightarrow> string) \<Rightarrow> lambda \<Rightarrow> lambda" where
blanchet@54193
    43
  "rename_lam f l =
blanchet@54193
    44
     (case l of
blanchet@54193
    45
       Var s \<Rightarrow> Var (f s)
blanchet@54193
    46
     | App l l' \<Rightarrow> App (rename_lam f l) (rename_lam f l')
blanchet@54193
    47
     | Abs s l \<Rightarrow> Abs (f s) (rename_lam f l)
blanchet@55932
    48
     | Let SL l \<Rightarrow> Let (fimage (map_prod f (rename_lam f)) SL) (rename_lam f l))"
blanchet@54193
    49
blanchet@54193
    50
primcorec
blanchet@54193
    51
  j1_sum :: "('a\<Colon>{zero,one,plus}) \<Rightarrow> 'a J1" and
blanchet@54193
    52
  j2_sum :: "'a \<Rightarrow> 'a J2"
blanchet@54193
    53
where
blanchet@54193
    54
  "n = 0 \<Longrightarrow> is_J11 (j1_sum n)" |
blanchet@54193
    55
  "un_J111 (j1_sum _) = 0" |
blanchet@54193
    56
  "un_J112 (j1_sum _) = j1_sum 0" |
blanchet@54193
    57
  "un_J121 (j1_sum n) = n + 1" |
blanchet@54193
    58
  "un_J122 (j1_sum n) = j2_sum (n + 1)" |
blanchet@57090
    59
  "n = 0 \<Longrightarrow> j2_sum n = J21" |
blanchet@54193
    60
  "un_J221 (j2_sum n) = j1_sum (n + 1)" |
blanchet@54193
    61
  "un_J222 (j2_sum n) = j2_sum (n + 1)"
blanchet@54193
    62
blanchet@54193
    63
primcorec forest_of_mylist :: "'a tree mylist \<Rightarrow> 'a forest" where
blanchet@54193
    64
  "forest_of_mylist ts =
blanchet@54193
    65
     (case ts of
blanchet@54193
    66
       MyNil \<Rightarrow> FNil
blanchet@54193
    67
     | MyCons t ts \<Rightarrow> FCons t (forest_of_mylist ts))"
blanchet@54193
    68
blanchet@54193
    69
primcorec mylist_of_forest :: "'a forest \<Rightarrow> 'a tree mylist" where
blanchet@54193
    70
  "mylist_of_forest f =
blanchet@54193
    71
     (case f of
blanchet@54193
    72
       FNil \<Rightarrow> MyNil
blanchet@54193
    73
     | FCons t ts \<Rightarrow> MyCons t (mylist_of_forest ts))"
blanchet@54193
    74
blanchet@54193
    75
primcorec semi_stream :: "'a stream \<Rightarrow> 'a stream" where
blanchet@54193
    76
  "semi_stream s = Stream (shd s) (semi_stream (stl (stl s)))"
blanchet@54193
    77
blanchet@54193
    78
primcorec
blanchet@54193
    79
  tree'_of_stream :: "'a stream \<Rightarrow> 'a tree'" and
blanchet@54193
    80
  branch_of_stream :: "'a stream \<Rightarrow> 'a branch"
blanchet@54193
    81
where
blanchet@54193
    82
  "tree'_of_stream s =
blanchet@54193
    83
     TNode' (branch_of_stream (semi_stream s)) (branch_of_stream (semi_stream (stl s)))" |
blanchet@54193
    84
  "branch_of_stream s = (case s of Stream h t \<Rightarrow> Branch h (tree'_of_stream t))"
blanchet@54193
    85
blanchet@54193
    86
primcorec
blanchet@55484
    87
  id_tree :: "'a bin_rose_tree \<Rightarrow> 'a bin_rose_tree" and
blanchet@55484
    88
  id_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and
blanchet@55484
    89
  id_trees2 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist"
blanchet@55484
    90
where
blanchet@55852
    91
  "id_tree t = (case t of BRTree a ts ts' \<Rightarrow> BRTree a (id_trees1 ts) (id_trees2 ts'))" |
blanchet@55484
    92
  "id_trees1 ts = (case ts of
blanchet@55852
    93
       MyNil \<Rightarrow> MyNil
blanchet@55852
    94
     | MyCons t ts \<Rightarrow> MyCons (id_tree t) (id_trees1 ts))" |
blanchet@55484
    95
  "id_trees2 ts = (case ts of
blanchet@55852
    96
       MyNil \<Rightarrow> MyNil
blanchet@55852
    97
     | MyCons t ts \<Rightarrow> MyCons (id_tree t) (id_trees2 ts))"
blanchet@55484
    98
blanchet@55484
    99
primcorec
blanchet@55774
   100
  trunc_tree :: "'a bin_rose_tree \<Rightarrow> 'a bin_rose_tree" and
blanchet@55774
   101
  trunc_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and
blanchet@55774
   102
  trunc_trees2 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist"
blanchet@55774
   103
where
blanchet@55852
   104
  "trunc_tree t = (case t of BRTree a ts ts' \<Rightarrow> BRTree a (trunc_trees1 ts) (trunc_trees2 ts'))" |
blanchet@55774
   105
  "trunc_trees1 ts = (case ts of
blanchet@55852
   106
       MyNil \<Rightarrow> MyNil
blanchet@55852
   107
     | MyCons t _ \<Rightarrow> MyCons (trunc_tree t) MyNil)" |
blanchet@55774
   108
  "trunc_trees2 ts = (case ts of
blanchet@55852
   109
       MyNil \<Rightarrow> MyNil
blanchet@55852
   110
     | MyCons t ts \<Rightarrow> MyCons (trunc_tree t) MyNil)"
blanchet@55774
   111
blanchet@55774
   112
primcorec
blanchet@54193
   113
  freeze_exp :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) exp \<Rightarrow> ('a, 'b) exp" and
blanchet@54193
   114
  freeze_trm :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) trm \<Rightarrow> ('a, 'b) trm" and
blanchet@54193
   115
  freeze_factor :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) factor \<Rightarrow> ('a, 'b) factor"
blanchet@54193
   116
where
blanchet@54193
   117
  "freeze_exp g e =
blanchet@54193
   118
     (case e of
blanchet@54193
   119
       Term t \<Rightarrow> Term (freeze_trm g t)
blanchet@54193
   120
     | Sum t e \<Rightarrow> Sum (freeze_trm g t) (freeze_exp g e))" |
blanchet@54193
   121
  "freeze_trm g t =
blanchet@54193
   122
     (case t of
blanchet@54193
   123
       Factor f \<Rightarrow> Factor (freeze_factor g f)
blanchet@54193
   124
     | Prod f t \<Rightarrow> Prod (freeze_factor g f) (freeze_trm g t))" |
blanchet@54193
   125
  "freeze_factor g f =
blanchet@54193
   126
     (case f of
blanchet@54193
   127
       C a \<Rightarrow> C a
blanchet@54193
   128
     | V b \<Rightarrow> C (g b)
blanchet@54193
   129
     | Paren e \<Rightarrow> Paren (freeze_exp g e))"
blanchet@54193
   130
blanchet@54193
   131
primcorec poly_unity :: "'a poly_unit" where
blanchet@54193
   132
  "poly_unity = U (\<lambda>_. poly_unity)"
blanchet@54193
   133
blanchet@54193
   134
primcorec build_cps :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> bool stream) \<Rightarrow> 'a \<Rightarrow> bool stream \<Rightarrow> 'a cps" where
blanchet@54193
   135
  "shd b \<Longrightarrow> build_cps f g a b = CPS1 a" |
blanchet@54193
   136
  "_ \<Longrightarrow> build_cps f g a b = CPS2 (\<lambda>a. build_cps f g (f a) (g a))"
blanchet@54193
   137
blanchet@54193
   138
end