src/HOL/Tools/datatype_rep_proofs.ML
changeset 5553 ae42b36a50c2
parent 5303 22029546d109
child 5661 6ecb6ea25f19
equal deleted inserted replaced
5552:dcd3e7711cac 5553:ae42b36a50c2
   315         val thy' = Theory.add_defs_i defs thy;
   315         val thy' = Theory.add_defs_i defs thy;
   316         val def_thms = map (get_axiom thy') (map fst defs);
   316         val def_thms = map (get_axiom thy') (map fst defs);
   317 
   317 
   318         (* prove characteristic equations *)
   318         (* prove characteristic equations *)
   319 
   319 
   320         val rewrites = def_thms @ (map meta_eq rec_rewrites);
   320         val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
   321         val char_thms' = map (fn eqn => prove_goalw_cterm rewrites
   321         val char_thms' = map (fn eqn => prove_goalw_cterm rewrites
   322           (cterm_of (sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns;
   322           (cterm_of (sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns;
   323 
   323 
   324       in (thy', char_thms' @ char_thms) end;
   324       in (thy', char_thms' @ char_thms) end;
   325 
   325 
   379               HOLogic.mk_mem (Rep_t $ mk_Free "x" T i, Const (rep_set_name, UnivT)))
   379               HOLogic.mk_mem (Rep_t $ mk_Free "x" T i, Const (rep_set_name, UnivT)))
   380           end;
   380           end;
   381 
   381 
   382         val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
   382         val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
   383 
   383 
   384         val rewrites = map meta_eq iso_char_thms;
   384         val rewrites = map mk_meta_eq iso_char_thms;
   385         val inj_thms' = map (fn r => r RS injD) inj_thms;
   385         val inj_thms' = map (fn r => r RS injD) inj_thms;
   386 
   386 
   387         val inj_thm = prove_goalw_cterm [] (cterm_of (sign_of thy5)
   387         val inj_thm = prove_goalw_cterm [] (cterm_of (sign_of thy5)
   388           (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
   388           (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
   389             [indtac induction 1,
   389             [indtac induction 1,
   428     (* prove theorem  Rep_i (Constr_j ...) = Inj_j ...  *)
   428     (* prove theorem  Rep_i (Constr_j ...) = Inj_j ...  *)
   429     
   429     
   430     fun prove_constr_rep_thm eqn =
   430     fun prove_constr_rep_thm eqn =
   431       let
   431       let
   432         val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
   432         val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
   433         val rewrites = constr_defs @ (map (meta_eq o #2) newT_iso_axms)
   433         val rewrites = constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
   434       in prove_goalw_cterm [] (cterm_of (sign_of thy5) eqn) (fn _ =>
   434       in prove_goalw_cterm [] (cterm_of (sign_of thy5) eqn) (fn _ =>
   435         [resolve_tac inj_thms 1,
   435         [resolve_tac inj_thms 1,
   436          rewrite_goals_tac rewrites,
   436          rewrite_goals_tac rewrites,
   437          rtac refl 1,
   437          rtac refl 1,
   438          resolve_tac rep_intrs 2,
   438          resolve_tac rep_intrs 2,
   522         [rtac indrule_lemma' 1, indtac rep_induct 1,
   522         [rtac indrule_lemma' 1, indtac rep_induct 1,
   523          EVERY (map (fn (prem, r) => (EVERY
   523          EVERY (map (fn (prem, r) => (EVERY
   524            [REPEAT (eresolve_tac Abs_inverse_thms 1),
   524            [REPEAT (eresolve_tac Abs_inverse_thms 1),
   525             simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
   525             simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
   526             DEPTH_SOLVE_1 (ares_tac [prem] 1)]))
   526             DEPTH_SOLVE_1 (ares_tac [prem] 1)]))
   527               (prems ~~ (constr_defs @ (map meta_eq iso_char_thms))))]);
   527               (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
   528 
   528 
   529     val thy7 = PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] thy6;
   529     val thy7 = PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] thy6;
   530 
   530 
   531   in (thy7, constr_inject, dist_rewrites, dt_induct)
   531   in (thy7, constr_inject, dist_rewrites, dt_induct)
   532   end;
   532   end;