1111 fun mk_prem z = Free (z, T_cong); |
1111 fun mk_prem z = Free (z, T_cong); |
1112 fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts); |
1112 fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts); |
1113 val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y)); |
1113 val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y)); |
1114 fun tac { context, prems } = Simplifier.rewrite_goals_tac prems |
1114 fun tac { context, prems } = Simplifier.rewrite_goals_tac prems |
1115 THEN ALLGOALS (Proof_Context.fact_tac [Drule.reflexive_thm]); |
1115 THEN ALLGOALS (Proof_Context.fact_tac [Drule.reflexive_thm]); |
1116 in Skip_Proof.prove_global thy (x :: y :: zs) [prem] concl tac end; |
1116 in Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl tac end; |
1117 |
1117 |
1118 fun add_case thm thy = |
1118 fun add_case thm thy = |
1119 let |
1119 let |
1120 val (case_const, (k, cos)) = case_cert thm; |
1120 val (case_const, (k, cos)) = case_cert thm; |
1121 val _ = case (filter_out (is_constr thy) o map_filter I) cos |
1121 val _ = case (filter_out (is_constr thy) o map_filter I) cos |