51 |
51 |
52 domain 'a tree = |
52 domain 'a tree = |
53 Node (lazy "'a tree") (lazy "'a tree") | |
53 Node (lazy "'a tree") (lazy "'a tree") | |
54 Leaf (lazy "'a") |
54 Leaf (lazy "'a") |
55 |
55 |
56 consts |
56 fixrec |
57 mirror :: "'a tree \<rightarrow> 'a tree" |
57 mirror :: "'a tree \<rightarrow> 'a tree" |
58 pick :: "'a tree \<rightarrow> 'a convex_pd" |
58 where |
59 |
|
60 fixrec |
|
61 mirror_Leaf: "mirror\<cdot>(Leaf\<cdot>a) = Leaf\<cdot>a" |
59 mirror_Leaf: "mirror\<cdot>(Leaf\<cdot>a) = Leaf\<cdot>a" |
62 mirror_Node: "mirror\<cdot>(Node\<cdot>l\<cdot>r) = Node\<cdot>(mirror\<cdot>r)\<cdot>(mirror\<cdot>l)" |
60 | mirror_Node: "mirror\<cdot>(Node\<cdot>l\<cdot>r) = Node\<cdot>(mirror\<cdot>r)\<cdot>(mirror\<cdot>l)" |
63 |
61 |
64 fixpat |
62 fixpat |
65 mirror_strict [simp]: "mirror\<cdot>\<bottom>" |
63 mirror_strict [simp]: "mirror\<cdot>\<bottom>" |
66 |
64 |
67 fixrec |
65 fixrec |
|
66 pick :: "'a tree \<rightarrow> 'a convex_pd" |
|
67 where |
68 pick_Leaf: "pick\<cdot>(Leaf\<cdot>a) = {a}\<natural>" |
68 pick_Leaf: "pick\<cdot>(Leaf\<cdot>a) = {a}\<natural>" |
69 pick_Node: "pick\<cdot>(Node\<cdot>l\<cdot>r) = pick\<cdot>l +\<natural> pick\<cdot>r" |
69 | pick_Node: "pick\<cdot>(Node\<cdot>l\<cdot>r) = pick\<cdot>l +\<natural> pick\<cdot>r" |
70 |
70 |
71 fixpat |
71 fixpat |
72 pick_strict [simp]: "pick\<cdot>\<bottom>" |
72 pick_strict [simp]: "pick\<cdot>\<bottom>" |
73 |
73 |
74 lemma pick_mirror: "pick\<cdot>(mirror\<cdot>t) = pick\<cdot>t" |
74 lemma pick_mirror: "pick\<cdot>(mirror\<cdot>t) = pick\<cdot>t" |
75 by (induct t rule: tree.ind) |
75 by (induct t rule: tree.ind) |
76 (simp_all add: convex_plus_ac) |
76 (simp_all add: convex_plus_ac) |
77 |
77 |
78 consts |
78 fixrec tree1 :: "int lift tree" |
79 tree1 :: "int lift tree" |
79 where "tree1 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>(Leaf\<cdot>(Def 2))) |
80 tree2 :: "int lift tree" |
80 \<cdot>(Node\<cdot>(Leaf\<cdot>(Def 3))\<cdot>(Leaf\<cdot>(Def 4)))" |
81 tree3 :: "int lift tree" |
|
82 |
81 |
83 fixrec |
82 fixrec tree2 :: "int lift tree" |
84 "tree1 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>(Leaf\<cdot>(Def 2))) |
83 where "tree2 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>(Leaf\<cdot>(Def 2))) |
85 \<cdot>(Node\<cdot>(Leaf\<cdot>(Def 3))\<cdot>(Leaf\<cdot>(Def 4)))" |
84 \<cdot>(Node\<cdot>\<bottom>\<cdot>(Leaf\<cdot>(Def 4)))" |
86 |
85 |
87 fixrec |
86 fixrec tree3 :: "int lift tree" |
88 "tree2 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>(Leaf\<cdot>(Def 2))) |
87 where "tree3 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>tree3) |
89 \<cdot>(Node\<cdot>\<bottom>\<cdot>(Leaf\<cdot>(Def 4)))" |
88 \<cdot>(Node\<cdot>(Leaf\<cdot>(Def 3))\<cdot>(Leaf\<cdot>(Def 4)))" |
90 |
|
91 fixrec |
|
92 "tree3 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>tree3) |
|
93 \<cdot>(Node\<cdot>(Leaf\<cdot>(Def 3))\<cdot>(Leaf\<cdot>(Def 4)))" |
|
94 |
89 |
95 declare tree1_simps tree2_simps tree3_simps [simp del] |
90 declare tree1_simps tree2_simps tree3_simps [simp del] |
96 |
91 |
97 lemma pick_tree1: |
92 lemma pick_tree1: |
98 "pick\<cdot>tree1 = {Def 1, Def 2, Def 3, Def 4}\<natural>" |
93 "pick\<cdot>tree1 = {Def 1, Def 2, Def 3, Def 4}\<natural>" |