replaced "Eps" by "The";
authorwenzelm
Fri Jul 20 21:59:11 2001 +0200 (2001-07-20)
changeset 11435bd1a7f53c11b
parent 11434 996bd4eb0ef3
child 11436 3f74b80d979f
replaced "Eps" by "The";
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Jul 20 21:58:19 2001 +0200
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Jul 20 21:59:11 2001 +0200
     1.3 @@ -245,8 +245,7 @@
     1.4          (cert (HOLogic.mk_Trueprop (mk_conj rec_unique_ts))) (K [tac]))
     1.5        end;
     1.6  
     1.7 -    val rec_total_thms = map (fn r =>
     1.8 -      r RS ex1_implies_ex RS (some_eq_ex RS iffD2)) rec_unique_thms;
     1.9 +    val rec_total_thms = map (fn r => r RS theI') rec_unique_thms;
    1.10  
    1.11      (* define primrec combinators *)
    1.12  
    1.13 @@ -265,7 +264,7 @@
    1.14            (reccomb_names ~~ recTs ~~ rec_result_Ts)) |>
    1.15        (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
    1.16          ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
    1.17 -           Const ("Eps", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
    1.18 +           Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
    1.19               HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set))))))
    1.20                 (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) |>>
    1.21        parent_path flat_names;
    1.22 @@ -277,7 +276,7 @@
    1.23  
    1.24      val rec_thms = map (fn t => prove_goalw_cterm reccomb_defs
    1.25        (cterm_of (Theory.sign_of thy2) t) (fn _ =>
    1.26 -        [rtac some1_equality 1,
    1.27 +        [rtac the1_equality 1,
    1.28           resolve_tac rec_unique_thms 1,
    1.29           resolve_tac rec_intrs 1,
    1.30           rewrite_goals_tac [o_def, fun_rel_comp_def],
     2.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Jul 20 21:58:19 2001 +0200
     2.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Jul 20 21:59:11 2001 +0200
     2.3 @@ -29,12 +29,12 @@
     2.4  
     2.5  val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
     2.6  
     2.7 -(* figure out internal names *)
     2.8 +
     2.9 +(** theory context references **)
    2.10  
    2.11 -val image_name = Sign.intern_const (Theory.sign_of Set.thy) "image";
    2.12 -val UNIV_name = Sign.intern_const (Theory.sign_of Set.thy) "UNIV";
    2.13 -val inj_on_name = Sign.intern_const (Theory.sign_of Fun.thy) "inj_on";
    2.14 -val inv_name = Sign.intern_const (Theory.sign_of Fun.thy) "inv";
    2.15 +val f_myinv_f = thm "f_myinv_f";
    2.16 +val myinv_f_f = thm "myinv_f_f";
    2.17 +
    2.18  
    2.19  fun exh_thm_of (dt_info : datatype_info Symtab.table) tname =
    2.20    #exhaustion (the (Symtab.lookup (dt_info, tname)));
    2.21 @@ -287,7 +287,7 @@
    2.22  	    prove_goalw_cterm [] 
    2.23  	      (cterm_of sg
    2.24  	       (HOLogic.mk_Trueprop 
    2.25 -		(Const (inj_on_name, [AbsT, UnivT] ---> HOLogic.boolT) $
    2.26 +		(Const ("Fun.inj_on", [AbsT, UnivT] ---> HOLogic.boolT) $
    2.27  		 Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT))))
    2.28                (fn _ => [rtac inj_on_inverseI 1, etac thm1 1]);
    2.29  
    2.30 @@ -297,8 +297,8 @@
    2.31  	    prove_goalw_cterm []
    2.32  	      (cterm_of sg
    2.33  	       (HOLogic.mk_Trueprop
    2.34 -		(Const (inj_on_name, [RepT, setT] ---> HOLogic.boolT) $
    2.35 -		 Const (Rep_name, RepT) $ Const (UNIV_name, setT))))
    2.36 +		(Const ("Fun.inj_on", [RepT, setT] ---> HOLogic.boolT) $
    2.37 +		 Const (Rep_name, RepT) $ Const ("UNIV", setT))))
    2.38                (fn _ => [rtac inj_inverseI 1, rtac thm2 1])
    2.39  
    2.40        in (inj_Abs_thm, inj_Rep_thm) end;
    2.41 @@ -419,8 +419,8 @@
    2.42          HOLogic.mk_mem (mk_Free "x" Univ_elT i, Const (set_name, UnivT)) $
    2.43            (if i < length newTs then Const ("True", HOLogic.boolT)
    2.44             else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
    2.45 -             Const (image_name, [isoT, HOLogic.mk_setT T] ---> UnivT) $
    2.46 -               Const (iso_name, isoT) $ Const (UNIV_name, HOLogic.mk_setT T)))
    2.47 +             Const ("image", [isoT, HOLogic.mk_setT T] ---> UnivT) $
    2.48 +               Const (iso_name, isoT) $ Const ("UNIV", HOLogic.mk_setT T)))
    2.49        end;
    2.50  
    2.51      val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t
    2.52 @@ -443,11 +443,6 @@
    2.53                 rtac (sym RS range_eqI) 1,
    2.54                 resolve_tac iso_char_thms 1])])));
    2.55  
    2.56 -    val Abs_inverse_thms' = (map #1 newT_iso_axms) @ map (fn r => r RS mp RS f_inv_f) iso_thms;
    2.57 -
    2.58 -    val Abs_inverse_thms = map (fn r => r RS subst) (Abs_inverse_thms' @
    2.59 -      map mk_funs_inv Abs_inverse_thms');
    2.60 -
    2.61      (* prove  inj dt_Rep_i  and  dt_Rep_i x : dt_rep_set_i *)
    2.62  
    2.63      fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
    2.64 @@ -511,6 +506,14 @@
    2.65  
    2.66      val (iso_inj_thms, iso_elem_thms) = foldr prove_iso_thms
    2.67        (tl descr, (map snd newT_iso_inj_thms, map #3 newT_iso_axms));
    2.68 +    val iso_inj_thms_unfolded = drop (length (hd descr), iso_inj_thms);
    2.69 +
    2.70 +    val Abs_inverse_thms' =
    2.71 +      map #1 newT_iso_axms @
    2.72 +      map2 (fn (r_inj, r) => f_myinv_f OF [r_inj, r RS mp]) (iso_inj_thms_unfolded, iso_thms);
    2.73 +
    2.74 +    val Abs_inverse_thms = map (fn r => r RS subst) (Abs_inverse_thms' @
    2.75 +      map mk_funs_inv Abs_inverse_thms');
    2.76  
    2.77      (******************* freeness theorems for constructors *******************)
    2.78  
    2.79 @@ -586,8 +589,8 @@
    2.80      val _ = message "Proving induction rule for datatypes ...";
    2.81  
    2.82      val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
    2.83 -      (map (fn r => r RS inv_f_f RS subst) (drop (length newTs, iso_inj_thms)));
    2.84 -    val Rep_inverse_thms' = map (fn r => r RS inv_f_f)
    2.85 +      (map (fn r => r RS myinv_f_f RS subst) (drop (length newTs, iso_inj_thms)));
    2.86 +    val Rep_inverse_thms' = map (fn r => r RS myinv_f_f)
    2.87        (drop (length newTs, iso_inj_thms));
    2.88  
    2.89      fun mk_indrule_lemma ((prems, concls), ((i, _), T)) =
    2.90 @@ -598,7 +601,7 @@
    2.91          val Abs_t = if i < length newTs then
    2.92              Const (Sign.intern_const (Theory.sign_of thy6)
    2.93                ("Abs_" ^ (nth_elem (i, new_type_names))), Univ_elT --> T)
    2.94 -          else Const (inv_name, [T --> Univ_elT, Univ_elT] ---> T) $
    2.95 +          else Const ("Inductive.myinv", [T --> Univ_elT, Univ_elT] ---> T) $
    2.96              Const (nth_elem (i, all_rep_names), T --> Univ_elT)
    2.97  
    2.98        in (prems @ [HOLogic.imp $ HOLogic.mk_mem (Rep_t,