977 |
977 |
978 val nchotomy_thmss = nchotomy_taut_thmss |
978 val nchotomy_thmss = nchotomy_taut_thmss |
979 |> (if is_none tac_opt then map2 append (take actual_nn thmss'') else I); |
979 |> (if is_none tac_opt then map2 append (take actual_nn thmss'') else I); |
980 val exclude_thmss = thmss'' |> is_none tac_opt ? drop actual_nn; |
980 val exclude_thmss = thmss'' |> is_none tac_opt ? drop actual_nn; |
981 |
981 |
|
982 val ps = |
|
983 Variable.variant_frees lthy (maps (maps #fun_args) disc_eqnss) [("P", HOLogic.boolT)]; |
|
984 |
982 val exhaust_thmss = |
985 val exhaust_thmss = |
983 map2 (fn false => K [] |
986 map2 (fn false => K [] |
984 | true => fn disc_eqns as {fun_args, ...} :: _ => |
987 | true => fn disc_eqns as {fun_args, ...} :: _ => |
985 let |
988 let |
986 val p = Bound (length fun_args); |
989 val p = Bound (length fun_args); |
987 fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p); |
990 fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p); |
988 in |
991 in |
989 [mk_imp_p (map (mk_imp_p o map HOLogic.mk_Trueprop o #prems) disc_eqns)] |
992 [mk_imp_p (map (mk_imp_p o map HOLogic.mk_Trueprop o #prems) disc_eqns)] |
990 end) |
993 end) |
991 de_facto_exhaustives disc_eqnss |
994 de_facto_exhaustives disc_eqnss |
992 |> list_all_fun_args [("P", HOLogic.boolT)] |
995 |> list_all_fun_args ps |
993 |> map3 (fn disc_eqns as {fun_args, ...} :: _ => fn [] => K [] |
996 |> map3 (fn disc_eqns as {fun_args, ...} :: _ => fn [] => K [] |
994 | [nchotomy_thm] => fn [goal] => |
997 | [nchotomy_thm] => fn [goal] => |
995 [mk_primcorec_exhaust_tac lthy ("" (* for "P" *) :: map (fst o dest_Free) fun_args) |
998 [mk_primcorec_exhaust_tac lthy ("" (* for "P" *) :: map (fst o dest_Free) fun_args) |
996 (length disc_eqns) nchotomy_thm |
999 (length disc_eqns) nchotomy_thm |
997 |> K |> Goal.prove lthy [] [] goal |
1000 |> K |> Goal.prove lthy [] [] goal |