159 Seq.single (Drule.compose_single(complete_thm, i, thm)) |
159 Seq.single (Drule.compose_single(complete_thm, i, thm)) |
160 end |
160 end |
161 handle COMPLETENESS => Seq.empty |
161 handle COMPLETENESS => Seq.empty |
162 |
162 |
163 |
163 |
164 val pat_completeness = Method.SIMPLE_METHOD (pat_complete_tac 1) |
164 val pat_completeness = Method.SIMPLE_METHOD' pat_complete_tac |
165 |
165 |
166 val by_pat_completeness_simp = |
166 val by_pat_completeness_simp = |
167 Proof.global_terminal_proof |
167 Proof.global_terminal_proof |
168 (Method.Basic (K pat_completeness), |
168 (Method.Basic (K pat_completeness), |
169 SOME (Method.Source (Args.src (("simp_all", []), Position.none)))) |
169 SOME (Method.Source_i (Args.src (("HOL.simp_all", []), Position.none)))) |
170 (* FIXME avoid dynamic scoping of method name! *) |
|
171 |
170 |
172 fun termination_by_lexicographic_order name = |
171 fun termination_by_lexicographic_order name = |
173 FundefPackage.setup_termination_proof (SOME name) |
172 FundefPackage.setup_termination_proof (SOME name) |
174 #> Proof.global_terminal_proof (Method.Basic LexicographicOrder.lexicographic_order, NONE) |
173 #> Proof.global_terminal_proof (Method.Basic LexicographicOrder.lexicographic_order, NONE) |
175 |
174 |
176 val setup = |
175 val setup = |
177 Method.add_methods [("pat_completeness", Method.no_args pat_completeness, "Completeness prover for datatype patterns")] |
176 Method.add_methods [("pat_completeness", Method.no_args pat_completeness, |
|
177 "Completeness prover for datatype patterns")] |
178 |
178 |
179 |
179 |
180 |
180 |
181 |
181 |
182 local structure P = OuterParse and K = OuterKeyword in |
182 local structure P = OuterParse and K = OuterKeyword in |