src/HOL/Tools/datatype_rep_proofs.ML
changeset 11471 ba2c252b55ad
parent 11435 bd1a7f53c11b
child 11539 0f17da240450
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Aug 07 19:26:42 2001 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Aug 07 19:29:08 2001 +0200
     1.3 @@ -411,38 +411,6 @@
     1.4          rule_by_tactic (atac 2) (thm RSN (2, inv'))
     1.5        end;
     1.6  
     1.7 -    (* prove  x : dt_rep_set_i --> x : range dt_Rep_i *)
     1.8 -
     1.9 -    fun mk_iso_t (((set_name, iso_name), i), T) =
    1.10 -      let val isoT = T --> Univ_elT
    1.11 -      in HOLogic.imp $ 
    1.12 -        HOLogic.mk_mem (mk_Free "x" Univ_elT i, Const (set_name, UnivT)) $
    1.13 -          (if i < length newTs then Const ("True", HOLogic.boolT)
    1.14 -           else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
    1.15 -             Const ("image", [isoT, HOLogic.mk_setT T] ---> UnivT) $
    1.16 -               Const (iso_name, isoT) $ Const ("UNIV", HOLogic.mk_setT T)))
    1.17 -      end;
    1.18 -
    1.19 -    val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t
    1.20 -      (rep_set_names ~~ all_rep_names ~~ (0 upto (length descr' - 1)) ~~ recTs)));
    1.21 -
    1.22 -    (* all the theorems are proved by one single simultaneous induction *)
    1.23 -
    1.24 -    val iso_thms = if length descr = 1 then [] else
    1.25 -      drop (length newTs, split_conj_thm
    1.26 -        (prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ =>
    1.27 -           [indtac rep_induct 1,
    1.28 -            REPEAT (rtac TrueI 1),
    1.29 -            REPEAT (EVERY
    1.30 -              [rewrite_goals_tac [mk_meta_eq Collect_mem_eq],
    1.31 -               REPEAT (etac Funs_IntE 1),
    1.32 -               REPEAT (eresolve_tac [rangeE, Funs_rangeE] 1),
    1.33 -               REPEAT (eresolve_tac (map (fn (iso, _, _) => iso RS subst) newT_iso_axms @
    1.34 -                 map (fn (iso, _, _) => mk_funs_inv iso RS subst) newT_iso_axms) 1),
    1.35 -               TRY (hyp_subst_tac 1),
    1.36 -               rtac (sym RS range_eqI) 1,
    1.37 -               resolve_tac iso_char_thms 1])])));
    1.38 -
    1.39      (* prove  inj dt_Rep_i  and  dt_Rep_i x : dt_rep_set_i *)
    1.40  
    1.41      fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
    1.42 @@ -464,7 +432,8 @@
    1.43          val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
    1.44  
    1.45          val rewrites = map mk_meta_eq iso_char_thms;
    1.46 -        val inj_thms' = flat (map (fn r => [r RS injD, r RS inj_o]) inj_thms);
    1.47 +        val inj_thms' = flat (map (fn r => [r RS injD, r RS inj_o])
    1.48 +          (map snd newT_iso_inj_thms @ inj_thms));
    1.49  
    1.50          val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
    1.51            (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
    1.52 @@ -501,16 +470,50 @@
    1.53  			 REPEAT (FIRST [atac 1, etac spec 1,
    1.54  				 resolve_tac (FunsI :: elem_thms) 1])])]);
    1.55  
    1.56 -      in (inj_thms @ inj_thms'', elem_thms @ (split_conj_thm elem_thm))
    1.57 +      in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
    1.58 +      end;
    1.59 +
    1.60 +    val (iso_inj_thms_unfolded, iso_elem_thms) = foldr prove_iso_thms
    1.61 +      (tl descr, ([], map #3 newT_iso_axms));
    1.62 +    val iso_inj_thms = map snd newT_iso_inj_thms @ iso_inj_thms_unfolded;
    1.63 +
    1.64 +    (* prove  x : dt_rep_set_i --> x : range dt_Rep_i *)
    1.65 +
    1.66 +    fun mk_iso_t (((set_name, iso_name), i), T) =
    1.67 +      let val isoT = T --> Univ_elT
    1.68 +      in HOLogic.imp $ 
    1.69 +        HOLogic.mk_mem (mk_Free "x" Univ_elT i, Const (set_name, UnivT)) $
    1.70 +          (if i < length newTs then Const ("True", HOLogic.boolT)
    1.71 +           else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
    1.72 +             Const ("image", [isoT, HOLogic.mk_setT T] ---> UnivT) $
    1.73 +               Const (iso_name, isoT) $ Const ("UNIV", HOLogic.mk_setT T)))
    1.74        end;
    1.75  
    1.76 -    val (iso_inj_thms, iso_elem_thms) = foldr prove_iso_thms
    1.77 -      (tl descr, (map snd newT_iso_inj_thms, map #3 newT_iso_axms));
    1.78 -    val iso_inj_thms_unfolded = drop (length (hd descr), iso_inj_thms);
    1.79 +    val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t
    1.80 +      (rep_set_names ~~ all_rep_names ~~ (0 upto (length descr' - 1)) ~~ recTs)));
    1.81 +
    1.82 +    (* all the theorems are proved by one single simultaneous induction *)
    1.83 +
    1.84 +    val iso_thms = if length descr = 1 then [] else
    1.85 +      drop (length newTs, split_conj_thm
    1.86 +        (prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ =>
    1.87 +           [indtac rep_induct 1,
    1.88 +            REPEAT (rtac TrueI 1),
    1.89 +            REPEAT (EVERY
    1.90 +              [rewrite_goals_tac [mk_meta_eq Collect_mem_eq],
    1.91 +               REPEAT (etac Funs_IntE 1),
    1.92 +               REPEAT (eresolve_tac (rangeE ::
    1.93 +                 map (fn r => r RS Funs_rangeE) iso_inj_thms_unfolded) 1),
    1.94 +               REPEAT (eresolve_tac (map (fn (iso, _, _) => iso RS subst) newT_iso_axms @
    1.95 +                 map (fn (iso, _, _) => mk_funs_inv iso RS subst) newT_iso_axms) 1),
    1.96 +               TRY (hyp_subst_tac 1),
    1.97 +               rtac (sym RS range_eqI) 1,
    1.98 +               resolve_tac iso_char_thms 1])])));
    1.99  
   1.100      val Abs_inverse_thms' =
   1.101        map #1 newT_iso_axms @
   1.102 -      map2 (fn (r_inj, r) => f_myinv_f OF [r_inj, r RS mp]) (iso_inj_thms_unfolded, iso_thms);
   1.103 +      map2 (fn (r_inj, r) => f_myinv_f OF [r_inj, r RS mp])
   1.104 +        (iso_inj_thms_unfolded, iso_thms);
   1.105  
   1.106      val Abs_inverse_thms = map (fn r => r RS subst) (Abs_inverse_thms' @
   1.107        map mk_funs_inv Abs_inverse_thms');
   1.108 @@ -589,9 +592,8 @@
   1.109      val _ = message "Proving induction rule for datatypes ...";
   1.110  
   1.111      val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
   1.112 -      (map (fn r => r RS myinv_f_f RS subst) (drop (length newTs, iso_inj_thms)));
   1.113 -    val Rep_inverse_thms' = map (fn r => r RS myinv_f_f)
   1.114 -      (drop (length newTs, iso_inj_thms));
   1.115 +      (map (fn r => r RS myinv_f_f RS subst) iso_inj_thms_unfolded);
   1.116 +    val Rep_inverse_thms' = map (fn r => r RS myinv_f_f) iso_inj_thms_unfolded;
   1.117  
   1.118      fun mk_indrule_lemma ((prems, concls), ((i, _), T)) =
   1.119        let