author | haftmann |
Sat, 05 Jul 2014 11:01:53 +0200 | |
changeset 57514 | bdc2c6b40bf2 |
parent 55932 | 68c5104d2204 |
child 58231 | ad45b22a0b39 |
permissions | -rw-r--r-- |
55075 | 1 |
(* Title: HOL/BNF_Examples/Misc_Primrec.thy |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
3 |
Copyright 2013 |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
4 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
5 |
Miscellaneous primitive recursive function definitions. |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
6 |
*) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
7 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
8 |
header {* Miscellaneous Primitive Recursive Function Definitions *} |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
9 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
10 |
theory Misc_Primrec |
53304 | 11 |
imports Misc_Datatype |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
12 |
begin |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
13 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55484
diff
changeset
|
14 |
primrec nat_of_simple :: "simple \<Rightarrow> nat" where |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
15 |
"nat_of_simple X1 = 1" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
16 |
"nat_of_simple X2 = 2" | |
54193 | 17 |
"nat_of_simple X3 = 3" | |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
18 |
"nat_of_simple X4 = 4" |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
19 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55484
diff
changeset
|
20 |
primrec simple_of_simple' :: "simple' \<Rightarrow> simple" where |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
21 |
"simple_of_simple' (X1' _) = X1" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
22 |
"simple_of_simple' (X2' _) = X2" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
23 |
"simple_of_simple' (X3' _) = X3" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
24 |
"simple_of_simple' (X4' _) = X4" |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
25 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55484
diff
changeset
|
26 |
primrec inc_simple'' :: "nat \<Rightarrow> simple'' \<Rightarrow> simple''" where |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
27 |
"inc_simple'' k (X1'' n i) = X1'' (n + k) (i + int k)" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
28 |
"inc_simple'' _ X2'' = X2''" |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
29 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55484
diff
changeset
|
30 |
primrec myapp :: "'a mylist \<Rightarrow> 'a mylist \<Rightarrow> 'a mylist" where |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
31 |
"myapp MyNil ys = ys" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
32 |
"myapp (MyCons x xs) ys = MyCons x (myapp xs ys)" |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
33 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55484
diff
changeset
|
34 |
primrec myrev :: "'a mylist \<Rightarrow> 'a mylist" where |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
35 |
"myrev MyNil = MyNil" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
36 |
"myrev (MyCons x xs) = myapp (myrev xs) (MyCons x MyNil)" |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
37 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55484
diff
changeset
|
38 |
primrec shuffle_sp :: "('a, 'b, 'c, 'd) some_passive \<Rightarrow> ('d, 'a, 'b, 'c) some_passive" where |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
39 |
"shuffle_sp (SP1 sp) = SP1 (shuffle_sp sp)" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
40 |
"shuffle_sp (SP2 a) = SP3 a" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
41 |
"shuffle_sp (SP3 b) = SP4 b" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
42 |
"shuffle_sp (SP4 c) = SP5 c" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
43 |
"shuffle_sp (SP5 d) = SP2 d" |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
44 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55484
diff
changeset
|
45 |
primrec |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
46 |
hf_size :: "hfset \<Rightarrow> nat" |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
47 |
where |
54019 | 48 |
"hf_size (HFset X) = 1 + setsum id (fset (fimage hf_size X))" |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
49 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55484
diff
changeset
|
50 |
primrec rename_lam :: "(string \<Rightarrow> string) \<Rightarrow> lambda \<Rightarrow> lambda" where |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
51 |
"rename_lam f (Var s) = Var (f s)" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
52 |
"rename_lam f (App l l') = App (rename_lam f l) (rename_lam f l')" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
53 |
"rename_lam f (Abs s l) = Abs (f s) (rename_lam f l)" | |
55932 | 54 |
"rename_lam f (Let SL l) = Let (fimage (map_prod f (rename_lam f)) SL) (rename_lam f l)" |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
55 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55484
diff
changeset
|
56 |
primrec |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
57 |
sum_i1 :: "('a\<Colon>{zero,plus}) I1 \<Rightarrow> 'a" and |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
58 |
sum_i2 :: "'a I2 \<Rightarrow> 'a" |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
59 |
where |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
60 |
"sum_i1 (I11 n i) = n + sum_i1 i" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
61 |
"sum_i1 (I12 n i) = n + sum_i2 i" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
62 |
"sum_i2 I21 = 0" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
63 |
"sum_i2 (I22 i j) = sum_i1 i + sum_i2 j" |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
64 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55484
diff
changeset
|
65 |
primrec forest_of_mylist :: "'a tree mylist \<Rightarrow> 'a forest" where |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
66 |
"forest_of_mylist MyNil = FNil" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
67 |
"forest_of_mylist (MyCons t ts) = FCons t (forest_of_mylist ts)" |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
68 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55484
diff
changeset
|
69 |
primrec mylist_of_forest :: "'a forest \<Rightarrow> 'a tree mylist" where |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
70 |
"mylist_of_forest FNil = MyNil" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
71 |
"mylist_of_forest (FCons t ts) = MyCons t (mylist_of_forest ts)" |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
72 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
73 |
definition frev :: "'a forest \<Rightarrow> 'a forest" where |
53622 | 74 |
"frev = forest_of_mylist \<circ> myrev \<circ> mylist_of_forest" |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
75 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55484
diff
changeset
|
76 |
primrec |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
77 |
mirror_tree :: "'a tree \<Rightarrow> 'a tree" and |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
78 |
mirror_forest :: "'a forest \<Rightarrow> 'a forest" |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
79 |
where |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
80 |
"mirror_tree TEmpty = TEmpty" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
81 |
"mirror_tree (TNode x ts) = TNode x (mirror_forest ts)" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
82 |
"mirror_forest FNil = FNil" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
83 |
"mirror_forest (FCons t ts) = frev (FCons (mirror_tree t) (mirror_forest ts))" |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
84 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55484
diff
changeset
|
85 |
primrec |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
86 |
mylist_of_tree' :: "'a tree' \<Rightarrow> 'a mylist" and |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
87 |
mylist_of_branch :: "'a branch \<Rightarrow> 'a mylist" |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
88 |
where |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
89 |
"mylist_of_tree' TEmpty' = MyNil" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
90 |
"mylist_of_tree' (TNode' b b') = myapp (mylist_of_branch b) (mylist_of_branch b')" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
91 |
"mylist_of_branch (Branch x t) = MyCons x (mylist_of_tree' t)" |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
92 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55484
diff
changeset
|
93 |
primrec |
55484 | 94 |
id_tree :: "'a bin_rose_tree \<Rightarrow> 'a bin_rose_tree" and |
95 |
id_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and |
|
96 |
id_trees2 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" |
|
97 |
where |
|
98 |
"id_tree (BRTree a ts ts') = BRTree a (id_trees1 ts) (id_trees2 ts')" | |
|
99 |
"id_trees1 MyNil = MyNil" | |
|
100 |
"id_trees1 (MyCons t ts) = MyCons (id_tree t) (id_trees1 ts)" | |
|
101 |
"id_trees2 MyNil = MyNil" | |
|
102 |
"id_trees2 (MyCons t ts) = MyCons (id_tree t) (id_trees2 ts)" |
|
103 |
||
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55484
diff
changeset
|
104 |
primrec |
55774 | 105 |
trunc_tree :: "'a bin_rose_tree \<Rightarrow> 'a bin_rose_tree" and |
106 |
trunc_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and |
|
107 |
trunc_trees2 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" |
|
108 |
where |
|
109 |
"trunc_tree (BRTree a ts ts') = BRTree a (trunc_trees1 ts) (trunc_trees2 ts')" | |
|
110 |
"trunc_trees1 MyNil = MyNil" | |
|
111 |
"trunc_trees1 (MyCons t ts) = MyCons (id_tree t) MyNil" | |
|
112 |
"trunc_trees2 MyNil = MyNil" | |
|
113 |
"trunc_trees2 (MyCons t ts) = MyCons (id_tree t) MyNil" |
|
114 |
||
115 |
primrec |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
116 |
is_ground_exp :: "('a, 'b) exp \<Rightarrow> bool" and |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
117 |
is_ground_trm :: "('a, 'b) trm \<Rightarrow> bool" and |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
118 |
is_ground_factor :: "('a, 'b) factor \<Rightarrow> bool" |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
119 |
where |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
120 |
"is_ground_exp (Term t) \<longleftrightarrow> is_ground_trm t" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
121 |
"is_ground_exp (Sum t e) \<longleftrightarrow> is_ground_trm t \<and> is_ground_exp e" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
122 |
"is_ground_trm (Factor f) \<longleftrightarrow> is_ground_factor f" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
123 |
"is_ground_trm (Prod f t) \<longleftrightarrow> is_ground_factor f \<and> is_ground_trm t" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
124 |
"is_ground_factor (C _) \<longleftrightarrow> True" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
125 |
"is_ground_factor (V _) \<longleftrightarrow> False" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
126 |
"is_ground_factor (Paren e) \<longleftrightarrow> is_ground_exp e" |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
127 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55484
diff
changeset
|
128 |
primrec map_ftreeA :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
129 |
"map_ftreeA f (FTLeaf x) = FTLeaf (f x)" | |
53622 | 130 |
"map_ftreeA f (FTNode g) = FTNode (map_ftreeA f \<circ> g)" |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
131 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55484
diff
changeset
|
132 |
primrec map_ftreeB :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ftree \<Rightarrow> 'b ftree" where |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
133 |
"map_ftreeB f (FTLeaf x) = FTLeaf (f x)" | |
53622 | 134 |
"map_ftreeB f (FTNode g) = FTNode (map_ftreeB f \<circ> g \<circ> the_inv f)" |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
135 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
136 |
end |