equal
deleted
inserted
replaced
154 fun casesplit_free fv i th = |
154 fun casesplit_free fv i th = |
155 let |
155 let |
156 val (subgoalth, exp) = IsaND.fix_alls i th; |
156 val (subgoalth, exp) = IsaND.fix_alls i th; |
157 val subgoalth' = atomize_goals subgoalth; |
157 val subgoalth' = atomize_goals subgoalth; |
158 val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1); |
158 val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1); |
159 val sgn = Thm.sign_of_thm th; |
159 val sgn = Thm.theory_of_thm th; |
160 |
160 |
161 val splitter_thm = mk_casesplit_goal_thm sgn fv gt; |
161 val splitter_thm = mk_casesplit_goal_thm sgn fv gt; |
162 val nsplits = Thm.nprems_of splitter_thm; |
162 val nsplits = Thm.nprems_of splitter_thm; |
163 |
163 |
164 val split_goal_th = splitter_thm RS subgoalth'; |
164 val split_goal_th = splitter_thm RS subgoalth'; |
184 handle Fail _ => NONE (* dest_skolem *) |
184 handle Fail _ => NONE (* dest_skolem *) |
185 end; |
185 end; |
186 val (n,ty) = case Library.get_first getter freets |
186 val (n,ty) = case Library.get_first getter freets |
187 of SOME (n, ty) => (n, ty) |
187 of SOME (n, ty) => (n, ty) |
188 | _ => error ("no such variable " ^ vstr); |
188 | _ => error ("no such variable " ^ vstr); |
189 val sgn = Thm.sign_of_thm th; |
189 val sgn = Thm.theory_of_thm th; |
190 |
190 |
191 val splitter_thm = mk_casesplit_goal_thm sgn (n,ty) gt; |
191 val splitter_thm = mk_casesplit_goal_thm sgn (n,ty) gt; |
192 val nsplits = Thm.nprems_of splitter_thm; |
192 val nsplits = Thm.nprems_of splitter_thm; |
193 |
193 |
194 val split_goal_th = splitter_thm RS subgoalth'; |
194 val split_goal_th = splitter_thm RS subgoalth'; |
267 case split done during recdef's case analysis, this would avoid us |
267 case split done during recdef's case analysis, this would avoid us |
268 having to (re)search for variables to split. *) |
268 having to (re)search for variables to split. *) |
269 fun splitto splitths genth = |
269 fun splitto splitths genth = |
270 let |
270 let |
271 val _ = not (null splitths) orelse error "splitto: no given splitths"; |
271 val _ = not (null splitths) orelse error "splitto: no given splitths"; |
272 val sgn = Thm.sign_of_thm genth; |
272 val sgn = Thm.theory_of_thm genth; |
273 |
273 |
274 (* check if we are a member of splitths - FIXME: quicker and |
274 (* check if we are a member of splitths - FIXME: quicker and |
275 more flexible with discrim net. *) |
275 more flexible with discrim net. *) |
276 fun solve_by_splitth th split = |
276 fun solve_by_splitth th split = |
277 Thm.biresolution false [(false,split)] 1 th; |
277 Thm.biresolution false [(false,split)] 1 th; |