equal
deleted
inserted
replaced
169 |
169 |
170 (** primrec **) |
170 (** primrec **) |
171 |
171 |
172 fun mk_primrec_decl ((fname, tname), axms) = |
172 fun mk_primrec_decl ((fname, tname), axms) = |
173 let |
173 let |
|
174 (*Isolate type name from the structure's identifier it may be stored in*) |
|
175 val tname' = implode (snd (take_suffix (not_equal ".") (explode tname))); |
|
176 |
174 fun mk_prove (name, eqn) = |
177 fun mk_prove (name, eqn) = |
175 "val " ^ name ^ " = store_thm (" ^ quote name |
178 "val " ^ name ^ " = store_thm (" ^ quote name |
176 ^ ", prove_goalw thy [get_def thy " ^ fname ^ "] " ^ eqn ^ "\n\ |
179 ^ ", prove_goalw thy [get_def thy " |
|
180 ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ "\n\ |
177 \ (fn _ => [Simp_tac 1]));"; |
181 \ (fn _ => [Simp_tac 1]));"; |
178 |
182 |
179 val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms); |
183 val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms); |
180 in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms) |
184 in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms) |
181 ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";") |
185 ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";") |