27 val neq_to_eq_False = @{thm neq_to_eq_False}; |
27 val neq_to_eq_False = @{thm neq_to_eq_False}; |
28 |
28 |
29 datatype direction = Left | Right; |
29 datatype direction = Left | Right; |
30 |
30 |
31 fun treeT T = Type (@{type_name tree}, [T]); |
31 fun treeT T = Type (@{type_name tree}, [T]); |
|
32 |
32 fun mk_tree' e T n [] = Const (@{const_name Tip}, treeT T) |
33 fun mk_tree' e T n [] = Const (@{const_name Tip}, treeT T) |
33 | mk_tree' e T n xs = |
34 | mk_tree' e T n xs = |
34 let |
35 let |
35 val m = (n - 1) div 2; |
36 val m = (n - 1) div 2; |
36 val (xsl,x::xsr) = chop m xs; |
37 val (xsl,x::xsr) = chop m xs; |
37 val l = mk_tree' e T m xsl; |
38 val l = mk_tree' e T m xsl; |
38 val r = mk_tree' e T (n-(m+1)) xsr; |
39 val r = mk_tree' e T (n-(m+1)) xsr; |
39 in |
40 in |
40 Const (@{const_name Node}, treeT T --> T --> HOLogic.boolT--> treeT T --> treeT T) $ |
41 Const (@{const_name Node}, treeT T --> T --> HOLogic.boolT--> treeT T --> treeT T) $ |
41 l $ e x $ HOLogic.false_const $ r |
42 l $ e x $ @{term False} $ r |
42 end |
43 end |
43 |
44 |
44 fun mk_tree e T xs = mk_tree' e T (length xs) xs; |
45 fun mk_tree e T xs = mk_tree' e T (length xs) xs; |
45 |
46 |
46 fun dest_tree (Const (@{const_name Tip}, _)) = [] |
47 fun dest_tree (Const (@{const_name Tip}, _)) = [] |