src/HOL/Library/Tree.thy
changeset 57569 e20a999f7161
parent 57530 439f881c8744
child 57687 cca7e8788481
equal deleted inserted replaced
57568:2c65870c706f 57569:e20a999f7161
     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)"