src/HOL/Tools/datatype_rep_proofs.ML
changeset 10911 eb5721204b38
parent 9315 f793f05024f6
child 11435 bd1a7f53c11b
equal deleted inserted replaced
10910:058775a575db 10911:eb5721204b38
   624     val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
   624     val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
   625     val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
   625     val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
   626       map (Free o apfst fst o dest_Var) Ps;
   626       map (Free o apfst fst o dest_Var) Ps;
   627     val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
   627     val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
   628 
   628 
   629     val dt_induct = prove_goalw_cterm [] (cert
   629     val dt_induct = prove_goalw_cterm [InductivePackage.inductive_forall_def] (cert
   630       (DatatypeProp.make_ind descr sorts)) (fn prems =>
   630       (DatatypeProp.make_ind descr sorts)) (fn prems =>
   631         [rtac indrule_lemma' 1, indtac rep_induct 1,
   631         [rtac indrule_lemma' 1, indtac rep_induct 1,
   632          EVERY (map (fn (prem, r) => (EVERY
   632          EVERY (map (fn (prem, r) => (EVERY
   633            [REPEAT (eresolve_tac (Funs_IntE::Abs_inverse_thms) 1),
   633            [REPEAT (eresolve_tac (Funs_IntE::Abs_inverse_thms) 1),
   634             simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
   634             simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
   636               rtac allI 1, dtac FunsD 1, etac CollectD 1]))]))
   636               rtac allI 1, dtac FunsD 1, etac CollectD 1]))]))
   637                 (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
   637                 (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
   638 
   638 
   639     val (thy7, [dt_induct']) = thy6 |>
   639     val (thy7, [dt_induct']) = thy6 |>
   640       Theory.add_path big_name |>
   640       Theory.add_path big_name |>
   641       PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
   641       PureThy.add_thms [(("induct", dt_induct),
       
   642         [Drule.rule_attribute (K InductivePackage.rulify), case_names_induct])] |>>
   642       Theory.parent_path;
   643       Theory.parent_path;
   643 
   644 
   644   in (thy7, constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct')
   645   in (thy7, constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct')
   645   end;
   646   end;
   646 
   647