equal
deleted
inserted
replaced
179 |> Theory.add_path (Sign.base_name fname) |
179 |> Theory.add_path (Sign.base_name fname) |
180 |> (PureThy.add_defs_i false o map Thm.no_attributes) [def]; |
180 |> (PureThy.add_defs_i false o map Thm.no_attributes) [def]; |
181 |
181 |
182 val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info) |
182 val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info) |
183 val eqn_thms = |
183 val eqn_thms = |
184 (message ("Proving equations for primrec function " ^ fname); |
184 (message ("Proving equations for primrec function " ^ fname); |
185 map (fn t => OldGoals.prove_goalw_cterm rewrites |
185 eqn_terms |> map (fn t => |
186 (Ind_Syntax.traceIt "next primrec equation = " (cterm_of (sign_of thy1) t)) |
186 standard (Goal.prove thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t) |
187 (fn _ => [rtac refl 1])) eqn_terms); |
187 (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])))); |
188 |
188 |
189 val (thy2, eqn_thms') = thy1 |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts); |
189 val (thy2, eqn_thms') = thy1 |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts); |
190 val thy3 = thy2 |
190 val thy3 = thy2 |
191 |> (#1 o PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add_global])]) |
191 |> (#1 o PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add_global])]) |
192 |> Theory.parent_path; |
192 |> Theory.parent_path; |