1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 6 * See "LICENSE_BSD2.txt" for details. 7 * 8 * @TAG(NICTA_BSD) 9 *) 10 11theory StaticFun 12imports 13 Main 14begin 15 16datatype ('a, 'b) Tree = Node 'a 'b "('a, 'b) Tree" "('a, 'b) Tree" | Leaf 17 18primrec 19 lookup_tree :: "('a, 'b) Tree \<Rightarrow> ('a \<Rightarrow> 'c :: linorder) \<Rightarrow> 'a \<Rightarrow> 'b option" 20where 21 "lookup_tree Leaf fn x = None" 22| "lookup_tree (Node y v l r) fn x = (if fn x = fn y then Some v 23 else if fn x < fn y then lookup_tree l fn x 24 else lookup_tree r fn x)" 25 26definition optional_strict_range :: "('a :: linorder) option \<Rightarrow> 'a option \<Rightarrow> 'a set" 27where 28 "optional_strict_range x y = {z. (x = None \<or> the x < z) \<and> (y = None \<or> z < the y)}" 29 30lemma optional_strict_range_split: 31 "z \<in> optional_strict_range x y 32 \<Longrightarrow> optional_strict_range x (Some z) = ({..< z} \<inter> optional_strict_range x y) 33 \<and> optional_strict_range (Some z) y = ({z <..} \<inter> optional_strict_range x y)" 34 by (auto simp add: optional_strict_range_def) 35 36lemma optional_strict_rangeI: 37 "z \<in> optional_strict_range None None" 38 "z < y \<Longrightarrow> z \<in> optional_strict_range None (Some y)" 39 "x < z \<Longrightarrow> z \<in> optional_strict_range (Some x) None" 40 "x < z \<Longrightarrow> z < y \<Longrightarrow> z \<in> optional_strict_range (Some x) (Some y)" 41 by (simp_all add: optional_strict_range_def) 42 43definition 44 tree_eq_fun_in_range :: "('a, 'b) Tree \<Rightarrow> ('a \<Rightarrow> 'c :: linorder) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'c set \<Rightarrow> bool" 45where 46 "tree_eq_fun_in_range T ord f S \<equiv> \<forall>x. (ord x \<in> S) \<longrightarrow> f x = lookup_tree T ord x" 47 48lemma tree_eq_fun_in_range_from_def: 49 "\<lbrakk> f \<equiv> lookup_tree T ord \<rbrakk> 50 \<Longrightarrow> tree_eq_fun_in_range T ord f (optional_strict_range None None)" 51 by (simp add: tree_eq_fun_in_range_def) 52 53lemma tree_eq_fun_in_range_split: 54 "tree_eq_fun_in_range (Node z v l r) ord f (optional_strict_range x y) 55 \<Longrightarrow> ord z \<in> optional_strict_range x y 56 \<Longrightarrow> tree_eq_fun_in_range l ord f (optional_strict_range x (Some (ord z))) 57 \<and> f z = Some v 58 \<and> tree_eq_fun_in_range r ord f (optional_strict_range (Some (ord z)) y)" 59 apply (simp add: tree_eq_fun_in_range_def optional_strict_range_split) 60 apply fastforce 61 done 62 63ML {* 64 65structure StaticFun = struct 66 67(* Actually build the tree -- theta (n lg(n)) *) 68fun build_tree' _ mk_leaf [] = mk_leaf 69 | build_tree' mk_node mk_leaf xs = let 70 val len = length xs 71 val (ys, zs) = chop (len div 2) xs 72 in case zs of [] => error "build_tree': impossible" 73 | ((a, b) :: zs) => mk_node a b (build_tree' mk_node mk_leaf ys) 74 (build_tree' mk_node mk_leaf zs) 75 end 76 77fun build_tree ord xs = case xs of [] => error "build_tree : empty" 78 | (idx, v) :: _ => let 79 val idxT = fastype_of idx 80 val vT = fastype_of v 81 val treeT = Type (@{type_name StaticFun.Tree}, [idxT, vT]) 82 val mk_leaf = Const (@{const_name StaticFun.Leaf}, treeT) 83 val node = Const (@{const_name StaticFun.Node}, 84 idxT --> vT --> treeT --> treeT --> treeT) 85 fun mk_node a b l r = node $ a $ b $ l $ r 86 val lookup = Const (@{const_name StaticFun.lookup_tree}, 87 treeT --> fastype_of ord --> idxT 88 --> Type (@{type_name option}, [vT])) 89 in 90 lookup $ (build_tree' mk_node mk_leaf xs) $ ord 91 end 92 93fun define_partial_map_tree name mappings ord ctxt = let 94 val tree = build_tree ord mappings 95 in Local_Theory.define 96 ((name, NoSyn), ((Thm.def_binding name, []), tree)) ctxt 97 |> apfst (apsnd snd) 98 end 99 100fun prove_partial_map_thms thm ctxt = let 101 val init = thm RS @{thm tree_eq_fun_in_range_from_def} 102 fun rec_tree thm = case Thm.concl_of thm of 103 @{term Trueprop} $ (Const (@{const_name tree_eq_fun_in_range}, _) 104 $ (Const (@{const_name Node}, _) $ z $ v $ _ $ _) $ _ $ _ $ _) => let 105 val t' = thm RS @{thm tree_eq_fun_in_range_split} 106 val solve_simp_tac = SUBGOAL (fn (t, i) => 107 (simp_tac ctxt THEN_ALL_NEW SUBGOAL (fn (t', _) => 108 raise TERM ("prove_partial_map_thms: unsolved", [t, t']))) i) 109 val r = t' |> (resolve_tac ctxt @{thms optional_strict_rangeI} 110 THEN_ALL_NEW solve_simp_tac) 1 |> Seq.hd 111 val l = r RS @{thm conjunct1} 112 val kr = r RS @{thm conjunct2} 113 val k = kr RS @{thm conjunct1} 114 val r = kr RS @{thm conjunct2} 115 in rec_tree l @ [((z, v), k)] @ rec_tree r end 116 | _ => [] 117 in rec_tree init end 118 119fun define_tree_and_save_thms name names mappings ord exsimps ctxt = let 120 val ((tree, def_thm), ctxt) = define_partial_map_tree name mappings ord ctxt 121 val thms = prove_partial_map_thms def_thm (ctxt addsimps exsimps) 122 val (idents, thms) = map_split I thms 123 val _ = map (fn ((x, y), (x', y')) => (x aconv x' andalso y aconv y') 124 orelse raise TERM ("define_tree_and_thms: different", [x, y, x', y'])) 125 (mappings ~~ idents) 126 val (_, ctxt) = Local_Theory.notes 127 (map (fn (s, t) => ((Binding.name s, []), [([t], [])])) 128 (names ~~ thms)) ctxt 129 in (tree, ctxt) end 130 131fun define_tree_and_thms_with_defs name names key_defs opt_values ord ctxt = let 132 val data = names ~~ (key_defs ~~ opt_values) 133 |> map_filter (fn (_, (_, NONE)) => NONE | (nm, (thm, SOME v)) 134 => SOME (nm, (fst (Logic.dest_equals (Thm.concl_of thm)), v))) 135 val (names, mappings) = map_split I data 136 in define_tree_and_save_thms name names mappings ord key_defs ctxt end 137 138end 139 140*} 141 142(* testing 143 144local_setup {* StaticFun.define_tree_and_save_thms @{binding tree} 145 ["one", "two", "three"] 146 [(@{term "Suc 0"}, @{term "Suc 0"}), 147 (@{term "2 :: nat"}, @{term "15 :: nat"}), 148 (@{term "3 :: nat"}, @{term "1 :: nat"})] 149 @{term "id :: nat \<Rightarrow> nat"} 150 #> snd 151*} 152print_theorems 153 154*) 155 156end 157