1128 val Ts = binder_types T; |
1128 val Ts = binder_types T; |
1129 val T_cong = nth Ts pos; |
1129 val T_cong = nth Ts pos; |
1130 fun mk_prem z = Free (z, T_cong); |
1130 fun mk_prem z = Free (z, T_cong); |
1131 fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts); |
1131 fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts); |
1132 val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y)); |
1132 val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y)); |
1133 fun tac { context, prems } = Simplifier.rewrite_goals_tac prems |
1133 in |
1134 THEN ALLGOALS (Proof_Context.fact_tac [Drule.reflexive_thm]); |
1134 Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl |
1135 in Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl tac end; |
1135 (fn {context = ctxt', prems} => |
|
1136 Simplifier.rewrite_goals_tac ctxt' prems |
|
1137 THEN ALLGOALS (Proof_Context.fact_tac ctxt' [Drule.reflexive_thm])) |
|
1138 end; |
1136 |
1139 |
1137 fun add_case thm thy = |
1140 fun add_case thm thy = |
1138 let |
1141 let |
1139 val (case_const, (k, cos)) = case_cert thm; |
1142 val (case_const, (k, cos)) = case_cert thm; |
1140 val _ = case (filter_out (is_constr thy) o map_filter I) cos |
1143 val _ = case (filter_out (is_constr thy) o map_filter I) cos |