796 induct_tac v 1, |
796 induct_tac v 1, |
797 ALLGOALS (fn i => tac i (i-1))]) |
797 ALLGOALS (fn i => tac i (i-1))]) |
798 end |
798 end |
799 handle _ => raise DTYPE_ERR {func="prove_nchotomy", mesg="failed"}; |
799 handle _ => raise DTYPE_ERR {func="prove_nchotomy", mesg="failed"}; |
800 |
800 |
|
801 (*--------------------------------------------------------------------------- |
|
802 * Turn nchotomy into exhaustion: |
|
803 * [| !!y1..yi. v = C1 y1..yi ==> P; ...; !!y1..yj. v = Cn y1..yj ==> P |] |
|
804 * ==> P |
|
805 *---------------------------------------------------------------------------*) |
|
806 fun mk_exhaust nchotomy = |
|
807 let val tac = rtac impI 1 THEN |
|
808 REPEAT(SOMEGOAL(eresolve_tac [disjE,exE])) |
|
809 in standard(rule_by_tactic tac (nchotomy RS spec RS rev_mp)) end; |
|
810 |
|
811 (* find name of v in exhaustion: *) |
|
812 fun exhaust_var thm = |
|
813 let val _ $ ( _ $ Var((x,_),_) $ _ ) = |
|
814 hd(Logic.strip_assums_hyp(hd(prems_of thm))) |
|
815 in x end; |
801 |
816 |
802 (*--------------------------------------------------------------------------- |
817 (*--------------------------------------------------------------------------- |
803 * Brings the preceeding functions together. |
818 * Brings the preceeding functions together. |
804 *---------------------------------------------------------------------------*) |
819 *---------------------------------------------------------------------------*) |
805 fun case_thms sign case_rewrites induct_tac = |
820 fun case_thms sign case_rewrites induct_tac = |
839 fun build_record (thy,(ty,cl),itac) = |
854 fun build_record (thy,(ty,cl),itac) = |
840 let val sign = sign_of thy |
855 let val sign = sign_of thy |
841 fun const s = Const(s, the(Sign.const_type sign s)) |
856 fun const s = Const(s, the(Sign.const_type sign s)) |
842 val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl |
857 val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl |
843 val {nchotomy,case_cong} = case_thms sign case_rewrites itac |
858 val {nchotomy,case_cong} = case_thms sign case_rewrites itac |
|
859 val exhaustion = mk_exhaust nchotomy |
|
860 val exh_var = exhaust_var exhaustion; |
|
861 fun exhaust_tac a = res_inst_tac [(exh_var,a)] exhaustion; |
844 fun induct_tac a i = |
862 fun induct_tac a i = |
845 STATE(fn st => |
863 STATE(fn st => |
846 (if Datatype.occs_in_prems a i st |
864 (if Datatype.occs_in_prems a i st |
847 then warning "Induction variable occurs also among premises!" |
865 then warning "Induction variable occurs also among premises!" |
848 else (); |
866 else (); |
851 (ty, {constructors = map(fn s => const s handle _ => const("op "^s)) cl, |
869 (ty, {constructors = map(fn s => const s handle _ => const("op "^s)) cl, |
852 case_const = const (ty^"_case"), |
870 case_const = const (ty^"_case"), |
853 case_rewrites = map mk_rw case_rewrites, |
871 case_rewrites = map mk_rw case_rewrites, |
854 induct_tac = induct_tac, |
872 induct_tac = induct_tac, |
855 nchotomy = nchotomy, |
873 nchotomy = nchotomy, |
|
874 exhaustion = exhaustion, |
|
875 exhaust_tac = exhaust_tac, |
856 case_cong = case_cong}) |
876 case_cong = case_cong}) |
857 end |
877 end |
858 end; |
878 end; |
859 |
879 |
860 |
880 |