equal
deleted
inserted
replaced
8 |
8 |
9 datatype_new 'a tree = Leaf | Node (left: "'a tree") (val: 'a) (right: "'a tree") |
9 datatype_new 'a tree = Leaf | Node (left: "'a tree") (val: 'a) (right: "'a tree") |
10 where |
10 where |
11 "left Leaf = Leaf" |
11 "left Leaf = Leaf" |
12 | "right Leaf = Leaf" |
12 | "right Leaf = Leaf" |
|
13 datatype_compat tree |
13 |
14 |
14 lemma neq_Leaf_iff: "(t \<noteq> Leaf) = (\<exists>l a r. t = Node l a r)" |
15 lemma neq_Leaf_iff: "(t \<noteq> Leaf) = (\<exists>l a r. t = Node l a r)" |
15 by (cases t) auto |
16 by (cases t) auto |
16 |
17 |
17 lemma set_tree_Node2: "set_tree(Node l x r) = insert x (set_tree l \<union> set_tree r)" |
18 lemma set_tree_Node2: "set_tree(Node l x r) = insert x (set_tree l \<union> set_tree r)" |