111 fun prep_case open_params split sg prop name i = |
111 fun prep_case open_params split sg prop name i = |
112 let |
112 let |
113 val Bi = hhf_nth_subgoal sg (i,prop); |
113 val Bi = hhf_nth_subgoal sg (i,prop); |
114 val all_xs = Logic.strip_params Bi |
114 val all_xs = Logic.strip_params Bi |
115 val n = length all_xs - (if_none open_params 0) |
115 val n = length all_xs - (if_none open_params 0) |
116 val ind_xs = take(n,all_xs) and goal_xs = drop(n,all_xs) |
116 val (ind_xs, goal_xs) = splitAt(n,all_xs) |
117 val rename = if is_none open_params then I else apfst Syntax.internal |
117 val rename = if is_none open_params then I else apfst Syntax.internal |
118 val xs = map rename ind_xs @ goal_xs |
118 val xs = map rename ind_xs @ goal_xs |
119 val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi); |
119 val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi); |
120 val named_asms = |
120 val named_asms = |
121 (case split of None => [("", asms)] |
121 (case split of None => [("", asms)] |
122 | Some t => |
122 | Some t => |
123 let val h = length (Logic.strip_assums_hyp(nth_subgoal(i,t))) |
123 let val h = length (Logic.strip_assums_hyp(nth_subgoal(i,t))) |
124 in [(hypsN, Library.take (h, asms)), (premsN, Library.drop (h, asms))] end); |
124 val (ps,qs) = splitAt(h, asms) |
|
125 in [(hypsN, ps), (premsN, qs)] end); |
125 val concl = Term.list_abs (xs, Logic.strip_assums_concl Bi); |
126 val concl = Term.list_abs (xs, Logic.strip_assums_concl Bi); |
126 val bind = ((case_conclN, 0), Some (ObjectLogic.drop_judgment sg concl)); |
127 val bind = ((case_conclN, 0), Some (ObjectLogic.drop_judgment sg concl)); |
127 in (name, {fixes = xs, assumes = named_asms, binds = [bind]}) end; |
128 in (name, {fixes = xs, assumes = named_asms, binds = [bind]}) end; |
128 |
129 |
129 fun make open_params split (sg, prop) names = |
130 fun make open_params split (sg, prop) names = |