126 ALLGOALS ObjectLogic.atomize_tac, |
126 ALLGOALS ObjectLogic.atomize_tac, |
127 rewrite_goals_tac (o_def :: map mk_meta_eq rec_rewrites), |
127 rewrite_goals_tac (o_def :: map mk_meta_eq rec_rewrites), |
128 REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i => |
128 REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i => |
129 REPEAT (etac allE i) THEN atac i)) 1)]); |
129 REPEAT (etac allE i) THEN atac i)) 1)]); |
130 |
130 |
131 val {path, ...} = Sign.rep_sg sg; |
|
132 val ind_name = Thm.name_of_thm induction; |
131 val ind_name = Thm.name_of_thm induction; |
133 val vs = map (fn i => List.nth (pnames, i)) is; |
132 val vs = map (fn i => List.nth (pnames, i)) is; |
134 val (thy', thm') = thy |
133 val (thy', thm') = thy |
135 |> Theory.absolute_path |
134 |> Theory.absolute_path |
136 |> PureThy.store_thm |
135 |> PureThy.store_thm |
137 ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), []) |
136 ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), []) |
138 |>> Theory.add_path (NameSpace.pack (getOpt (path,[]))); |
137 |>> Theory.restore_naming thy; |
139 |
138 |
140 val ivs = Drule.vars_of_terms |
139 val ivs = Drule.vars_of_terms |
141 [Logic.varify (DatatypeProp.make_ind [descr] sorts)]; |
140 [Logic.varify (DatatypeProp.make_ind [descr] sorts)]; |
142 val rvs = Drule.vars_of_terms [prop_of thm']; |
141 val rvs = Drule.vars_of_terms [prop_of thm']; |
143 val ivs1 = map Var (filter_out (fn (_, T) => |
142 val ivs1 = map Var (filter_out (fn (_, T) => |
198 [rtac (cterm_instantiate [(cert y, cert y')] exhaustion) 1, |
197 [rtac (cterm_instantiate [(cert y, cert y')] exhaustion) 1, |
199 ALLGOALS (EVERY' |
198 ALLGOALS (EVERY' |
200 [asm_simp_tac (HOL_basic_ss addsimps case_rewrites), |
199 [asm_simp_tac (HOL_basic_ss addsimps case_rewrites), |
201 resolve_tac prems, asm_simp_tac HOL_basic_ss])]); |
200 resolve_tac prems, asm_simp_tac HOL_basic_ss])]); |
202 |
201 |
203 val {path, ...} = Sign.rep_sg sg; |
|
204 val exh_name = Thm.name_of_thm exhaustion; |
202 val exh_name = Thm.name_of_thm exhaustion; |
205 val (thy', thm') = thy |
203 val (thy', thm') = thy |
206 |> Theory.absolute_path |
204 |> Theory.absolute_path |
207 |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), []) |
205 |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), []) |
208 |>> Theory.add_path (NameSpace.pack (getOpt (path,[]))); |
206 |>> Theory.restore_naming thy; |
209 |
207 |
210 val P = Var (("P", 0), rT' --> HOLogic.boolT); |
208 val P = Var (("P", 0), rT' --> HOLogic.boolT); |
211 val prf = forall_intr_prf (y, forall_intr_prf (P, |
209 val prf = forall_intr_prf (y, forall_intr_prf (P, |
212 foldr (fn ((p, r), prf) => |
210 foldr (fn ((p, r), prf) => |
213 forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p), |
211 forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p), |