equal
deleted
inserted
replaced
154 end |
154 end |
155 |
155 |
156 val mk_number = HOLogic.mk_nat |
156 val mk_number = HOLogic.mk_nat |
157 val dest_number = HOLogic.dest_nat |
157 val dest_number = HOLogic.dest_nat |
158 |
158 |
159 fun nums_to i = map mk_number (0 upto (i - 1)) |
159 fun nums_to i = map_range mk_number i |
160 |
160 |
161 val nth_simps = [thm "List.nth_Cons_0", thm "List.nth_Cons_Suc"] |
161 val nth_simps = [@{thm List.nth_Cons_0}, @{thm List.nth_Cons_Suc}] |
162 val nth_ss = (HOL_basic_ss addsimps nth_simps) |
162 val nth_ss = (HOL_basic_ss addsimps nth_simps) |
163 val simp_nth_tac = simp_tac nth_ss |
163 val simp_nth_tac = simp_tac nth_ss |
164 |
164 |
165 |
165 |
166 fun tabulate_tlist thy l = |
166 fun tabulate_tlist thy l = |
167 let |
167 let |
168 val n = length (HOLogic.dest_list l) |
168 val n = length (HOLogic.dest_list l) |
169 val table = Inttab.make (map (fn i => (i, Simplifier.rewrite nth_ss (cterm_of thy (mk_nth l $ mk_number i)))) (0 upto n - 1)) |
169 val table = Inttab.make (map_range (fn i => (i, Simplifier.rewrite nth_ss (cterm_of thy (mk_nth l $ mk_number i)))) n) |
170 in |
170 in |
171 the o Inttab.lookup table |
171 the o Inttab.lookup table |
172 end |
172 end |
173 |
173 |
174 val get_elem = snd o Logic.dest_equals o prop_of |
174 val get_elem = snd o Logic.dest_equals o prop_of |
248 end |
248 end |
249 in set_m2 end |
249 in set_m2 end |
250 |
250 |
251 val goal = HOLogic.mk_Trueprop (mk_approx (Var (("G", 0), scgT)) RD1 RD2 Ms1 Ms2) |
251 val goal = HOLogic.mk_Trueprop (mk_approx (Var (("G", 0), scgT)) RD1 RD2 Ms1 Ms2) |
252 |
252 |
253 val tac = (EVERY (map (fn n => EVERY (map (set_m1 n) (0 upto M - 1))) (0 upto N - 1))) |
253 val tac = (EVERY (map_range (fn n => EVERY (map_range (set_m1 n) M)) N)) |
254 THEN (rtac approx_empty 1) |
254 THEN (rtac approx_empty 1) |
255 |
255 |
256 val approx_thm = goal |
256 val approx_thm = goal |
257 |> cterm_of thy |
257 |> cterm_of thy |
258 |> Goal.init |
258 |> Goal.init |