author | wenzelm |
Mon, 24 Oct 2016 11:42:39 +0200 | |
changeset 64367 | a424f2737646 |
parent 64267 | b9a1486e79be |
permissions | -rw-r--r-- |
58309
a09ec6daaa19
renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
blanchet
parents:
58231
diff
changeset
|
1 |
(* Title: HOL/Datatype_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 |
|
63167 | 8 |
section \<open>Miscellaneous Primitive Recursive Function Definitions\<close> |
53303
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 |
|
61076 | 38 |
primrec shuffle_sp :: "('a :: ord, 'b :: ord, '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 |
64267 | 48 |
"hf_size (HFset X) = 1 + sum 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 |
|
62536
656e9653c645
made 'size' plugin compatible with locales again (and added regression test)
blanchet
parents:
61076
diff
changeset
|
56 |
primrec (in loc) |
656e9653c645
made 'size' plugin compatible with locales again (and added regression test)
blanchet
parents:
61076
diff
changeset
|
57 |
sum_i1 :: "('b::{zero,plus}) I1 \<Rightarrow> 'b" and |
656e9653c645
made 'size' plugin compatible with locales again (and added regression test)
blanchet
parents:
61076
diff
changeset
|
58 |
sum_i2 :: "'b I2 \<Rightarrow> 'b" |
53303
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 |
|
62536
656e9653c645
made 'size' plugin compatible with locales again (and added regression test)
blanchet
parents:
61076
diff
changeset
|
65 |
context loc |
656e9653c645
made 'size' plugin compatible with locales again (and added regression test)
blanchet
parents:
61076
diff
changeset
|
66 |
begin |
656e9653c645
made 'size' plugin compatible with locales again (and added regression test)
blanchet
parents:
61076
diff
changeset
|
67 |
|
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
|
68 |
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
|
69 |
"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
|
70 |
"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
|
71 |
|
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
|
72 |
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
|
73 |
"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
|
74 |
"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
|
75 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
76 |
definition frev :: "'a forest \<Rightarrow> 'a forest" where |
53622 | 77 |
"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
|
78 |
|
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
|
79 |
primrec |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
80 |
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
|
81 |
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
|
82 |
where |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
83 |
"mirror_tree TEmpty = TEmpty" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
84 |
"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
|
85 |
"mirror_forest FNil = FNil" | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
86 |
"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
|
87 |
|
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
|
88 |
primrec |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
89 |
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
|
90 |
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
|
91 |
where |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
92 |
"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
|
93 |
"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
|
94 |
"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
|
95 |
|
62536
656e9653c645
made 'size' plugin compatible with locales again (and added regression test)
blanchet
parents:
61076
diff
changeset
|
96 |
end |
656e9653c645
made 'size' plugin compatible with locales again (and added regression test)
blanchet
parents:
61076
diff
changeset
|
97 |
|
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
|
98 |
primrec |
55484 | 99 |
id_tree :: "'a bin_rose_tree \<Rightarrow> 'a bin_rose_tree" and |
100 |
id_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and |
|
101 |
id_trees2 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" |
|
102 |
where |
|
103 |
"id_tree (BRTree a ts ts') = BRTree a (id_trees1 ts) (id_trees2 ts')" | |
|
104 |
"id_trees1 MyNil = MyNil" | |
|
105 |
"id_trees1 (MyCons t ts) = MyCons (id_tree t) (id_trees1 ts)" | |
|
106 |
"id_trees2 MyNil = MyNil" | |
|
107 |
"id_trees2 (MyCons t ts) = MyCons (id_tree t) (id_trees2 ts)" |
|
108 |
||
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
|
109 |
primrec |
55774 | 110 |
trunc_tree :: "'a bin_rose_tree \<Rightarrow> 'a bin_rose_tree" and |
111 |
trunc_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and |
|
112 |
trunc_trees2 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" |
|
113 |
where |
|
114 |
"trunc_tree (BRTree a ts ts') = BRTree a (trunc_trees1 ts) (trunc_trees2 ts')" | |
|
115 |
"trunc_trees1 MyNil = MyNil" | |
|
116 |
"trunc_trees1 (MyCons t ts) = MyCons (id_tree t) MyNil" | |
|
117 |
"trunc_trees2 MyNil = MyNil" | |
|
118 |
"trunc_trees2 (MyCons t ts) = MyCons (id_tree t) MyNil" |
|
119 |
||
120 |
primrec |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
121 |
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
|
122 |
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
|
123 |
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
|
124 |
where |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
125 |
"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
|
126 |
"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
|
127 |
"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
|
128 |
"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
|
129 |
"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
|
130 |
"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
|
131 |
"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
|
132 |
|
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
|
133 |
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
|
134 |
"map_ftreeA f (FTLeaf x) = FTLeaf (f x)" | |
53622 | 135 |
"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
|
136 |
|
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
|
137 |
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
|
138 |
"map_ftreeB f (FTLeaf x) = FTLeaf (f x)" | |
53622 | 139 |
"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
|
140 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
141 |
end |