src/HOL/Tools/datatype_rep_proofs.ML
changeset 11951 381135c295ef
parent 11827 16ef206e6648
child 11957 f1657e0291ca
equal deleted inserted replaced
11950:9bd6e8e62a06 11951:381135c295ef
   436         val inj_thms' = flat (map (fn r => [r RS injD, r RS inj_o])
   436         val inj_thms' = flat (map (fn r => [r RS injD, r RS inj_o])
   437           (map snd newT_iso_inj_thms @ inj_thms));
   437           (map snd newT_iso_inj_thms @ inj_thms));
   438 
   438 
   439         val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
   439         val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
   440           (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
   440           (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
   441             [indtac induction 1,
   441             [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
   442              REPEAT (EVERY
   442              REPEAT (EVERY
   443                [rtac allI 1, rtac impI 1,
   443                [rtac allI 1, rtac impI 1,
   444                 exh_tac (exh_thm_of dt_info) 1,
   444                 exh_tac (exh_thm_of dt_info) 1,
   445                 REPEAT (EVERY
   445                 REPEAT (EVERY
   446                   [hyp_subst_tac 1,
   446                   [hyp_subst_tac 1,
   447                    rewrite_goals_tac rewrites,
   447                    rewrite_goals_tac rewrites,
   448                    REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
   448                    REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
   449                    (eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
   449                    (eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
   450                    ORELSE (EVERY
   450                    ORELSE (EVERY
   451                      [REPEAT (etac Scons_inject 1),
   451                      [REPEAT (eresolve_tac (Scons_inject :: sum_case_inject ::
   452                       REPEAT (dresolve_tac
   452                         map make_elim (inj_thms' @
   453                         (inj_thms' @ [Leaf_inject, Lim_inject, Inl_inject, Inr_inject]) 1),
   453                           [Leaf_inject, Lim_inject, Inl_inject, Inr_inject])) 1),
   454                       REPEAT ((EVERY [etac allE 1, dtac mp 1, atac 1]) ORELSE
   454                       REPEAT ((EVERY [etac allE 1, dtac mp 1, atac 1]) ORELSE
   455                               (dtac inj_fun_lemma 1 THEN atac 1)),
   455                               (dtac inj_fun_lemma 1 THEN atac 1)),
   456                       TRY (hyp_subst_tac 1),
   456                       REPEAT (hyp_subst_tac 1),
   457                       rtac refl 1])])])]);
   457                       rtac refl 1])])])]);
   458 
   458 
   459         val inj_thms'' = map (fn r => r RS datatype_injI)
   459         val inj_thms'' = map (fn r => r RS datatype_injI)
   460                              (split_conj_thm inj_thm);
   460                              (split_conj_thm inj_thm);
   461 
   461 
   462         val elem_thm = 
   462         val elem_thm = 
   463 	    prove_goalw_cterm []
   463 	    prove_goalw_cterm []
   464 	      (cterm_of (Theory.sign_of thy5)
   464 	      (cterm_of (Theory.sign_of thy5)
   465 	       (HOLogic.mk_Trueprop (mk_conj ind_concl2)))
   465 	       (HOLogic.mk_Trueprop (mk_conj ind_concl2)))
   466 	      (fn _ =>
   466 	      (fn _ =>
   467 	       [indtac induction 1,
   467 	       [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
   468 		rewrite_goals_tac (o_def :: rewrites),
   468 		rewrite_goals_tac (o_def :: rewrites),
   469 		REPEAT (EVERY
   469 		REPEAT (EVERY
   470 			[resolve_tac rep_intrs 1,
   470 			[resolve_tac rep_intrs 1,
   471 			 REPEAT (FIRST [atac 1, etac spec 1,
   471 			 REPEAT (FIRST [atac 1, etac spec 1,
   472 				 resolve_tac (FunsI :: elem_thms) 1])])]);
   472 				 resolve_tac (FunsI :: elem_thms) 1])])]);