moved Inductive.myinv to Fun.inv; tuned
authorhaftmann
Mon Jul 06 14:19:13 2009 +0200 (2009-07-06)
changeset 319493f933687fae9
parent 31942 63466160ff27
child 31950 7300186d745a
moved Inductive.myinv to Fun.inv; tuned
src/HOL/Fun.thy
src/HOL/Inductive.thy
src/HOL/Tools/Datatype/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Fun.thy	Sat Jul 04 23:25:28 2009 +0200
     1.2 +++ b/src/HOL/Fun.thy	Mon Jul 06 14:19:13 2009 +0200
     1.3 @@ -496,6 +496,40 @@
     1.4  
     1.5  hide (open) const swap
     1.6  
     1.7 +
     1.8 +subsection {* Inversion of injective functions *}
     1.9 +
    1.10 +definition inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
    1.11 +  "inv f y = (THE x. f x = y)"
    1.12 +
    1.13 +lemma inv_f_f:
    1.14 +  assumes "inj f"
    1.15 +  shows "inv f (f x) = x"
    1.16 +proof -
    1.17 +  from assms have "(THE x'. f x' = f x) = (THE x'. x' = x)"
    1.18 +    by (simp only: inj_eq)
    1.19 +  also have "... = x" by (rule the_eq_trivial)
    1.20 +  finally show ?thesis by (unfold inv_def)
    1.21 +qed
    1.22 +
    1.23 +lemma f_inv_f:
    1.24 +  assumes "inj f"
    1.25 +  and "y \<in> range f"
    1.26 +  shows "f (inv f y) = y"
    1.27 +proof (unfold inv_def)
    1.28 +  from `y \<in> range f` obtain x where "y = f x" ..
    1.29 +  then have "f x = y" ..
    1.30 +  then show "f (THE x. f x = y) = y"
    1.31 +  proof (rule theI)
    1.32 +    fix x' assume "f x' = y"
    1.33 +    with `f x = y` have "f x' = f x" by simp
    1.34 +    with `inj f` show "x' = x" by (rule injD)
    1.35 +  qed
    1.36 +qed
    1.37 +
    1.38 +hide (open) const inv
    1.39 +
    1.40 +
    1.41  subsection {* Proof tool setup *} 
    1.42  
    1.43  text {* simplifies terms of the form
     2.1 --- a/src/HOL/Inductive.thy	Sat Jul 04 23:25:28 2009 +0200
     2.2 +++ b/src/HOL/Inductive.thy	Mon Jul 06 14:19:13 2009 +0200
     2.3 @@ -258,38 +258,6 @@
     2.4  
     2.5  subsection {* Inductive predicates and sets *}
     2.6  
     2.7 -text {* Inversion of injective functions. *}
     2.8 -
     2.9 -constdefs
    2.10 -  myinv :: "('a => 'b) => ('b => 'a)"
    2.11 -  "myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y"
    2.12 -
    2.13 -lemma myinv_f_f: "inj f ==> myinv f (f x) = x"
    2.14 -proof -
    2.15 -  assume "inj f"
    2.16 -  hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
    2.17 -    by (simp only: inj_eq)
    2.18 -  also have "... = x" by (rule the_eq_trivial)
    2.19 -  finally show ?thesis by (unfold myinv_def)
    2.20 -qed
    2.21 -
    2.22 -lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y"
    2.23 -proof (unfold myinv_def)
    2.24 -  assume inj: "inj f"
    2.25 -  assume "y \<in> range f"
    2.26 -  then obtain x where "y = f x" ..
    2.27 -  hence x: "f x = y" ..
    2.28 -  thus "f (THE x. f x = y) = y"
    2.29 -  proof (rule theI)
    2.30 -    fix x' assume "f x' = y"
    2.31 -    with x have "f x' = f x" by simp
    2.32 -    with inj show "x' = x" by (rule injD)
    2.33 -  qed
    2.34 -qed
    2.35 -
    2.36 -hide const myinv
    2.37 -
    2.38 -
    2.39  text {* Package setup. *}
    2.40  
    2.41  theorems basic_monos =
     3.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Sat Jul 04 23:25:28 2009 +0200
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Mon Jul 06 14:19:13 2009 +0200
     3.3 @@ -37,10 +37,6 @@
     3.4  
     3.5  (** theory context references **)
     3.6  
     3.7 -val f_myinv_f = thm "f_myinv_f";
     3.8 -val myinv_f_f = thm "myinv_f_f";
     3.9 -
    3.10 -
    3.11  fun exh_thm_of (dt_info : info Symtab.table) tname =
    3.12    #exhaustion (the (Symtab.lookup dt_info tname));
    3.13  
    3.14 @@ -162,7 +158,7 @@
    3.15                    app_bnds (mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
    3.16                in (j + 1, list_all (map (pair "x") Ts,
    3.17                    HOLogic.mk_Trueprop
    3.18 -                    (Free (List.nth (rep_set_names', k), UnivT') $ free_t)) :: prems,
    3.19 +                    (Free (nth rep_set_names' k, UnivT') $ free_t)) :: prems,
    3.20                  mk_lim free_t Ts :: ts)
    3.21                end
    3.22            | _ =>
    3.23 @@ -225,7 +221,7 @@
    3.24                val free_t = mk_Free "x" T j
    3.25            in (case (strip_dtyp dt, strip_type T) of
    3.26                ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim
    3.27 -                (Const (List.nth (all_rep_names, m), U --> Univ_elT) $
    3.28 +                (Const (nth all_rep_names m, U --> Univ_elT) $
    3.29                     app_bnds free_t (length Us)) Us :: r_args)
    3.30              | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
    3.31            end;
    3.32 @@ -295,8 +291,8 @@
    3.33      fun make_iso_def k ks n ((fs, eqns, i), (cname, cargs)) =
    3.34        let
    3.35          val argTs = map (typ_of_dtyp descr' sorts) cargs;
    3.36 -        val T = List.nth (recTs, k);
    3.37 -        val rep_name = List.nth (all_rep_names, k);
    3.38 +        val T = nth recTs k;
    3.39 +        val rep_name = nth all_rep_names k;
    3.40          val rep_const = Const (rep_name, T --> Univ_elT);
    3.41          val constr = Const (cname, argTs ---> T);
    3.42  
    3.43 @@ -311,7 +307,7 @@
    3.44                     Ts @ [Us ---> Univ_elT])
    3.45                  else
    3.46                    (i2 + 1, i2', ts @ [mk_lim
    3.47 -                     (Const (List.nth (all_rep_names, j), U --> Univ_elT) $
    3.48 +                     (Const (nth all_rep_names j, U --> Univ_elT) $
    3.49                          app_bnds (mk_Free "x" T' i2) (length Us)) Us], Ts)
    3.50              | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts))
    3.51            end;
    3.52 @@ -339,7 +335,7 @@
    3.53            let
    3.54              val (fs', eqns', _) = Library.foldl (make_iso_def k ks (length constrs))
    3.55                ((fs, eqns, 1), constrs);
    3.56 -            val iso = (List.nth (recTs, k), List.nth (all_rep_names, k))
    3.57 +            val iso = (nth recTs k, nth all_rep_names k)
    3.58            in (fs', eqns', isos @ [iso]) end;
    3.59          
    3.60          val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds);
    3.61 @@ -397,9 +393,9 @@
    3.62  
    3.63          fun mk_ind_concl (i, _) =
    3.64            let
    3.65 -            val T = List.nth (recTs, i);
    3.66 -            val Rep_t = Const (List.nth (all_rep_names, i), T --> Univ_elT);
    3.67 -            val rep_set_name = List.nth (rep_set_names, i)
    3.68 +            val T = nth recTs i;
    3.69 +            val Rep_t = Const (nth all_rep_names i, T --> Univ_elT);
    3.70 +            val rep_set_name = nth rep_set_names i
    3.71            in (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $
    3.72                  HOLogic.mk_eq (Rep_t $ mk_Free "x" T i, Rep_t $ Bound 0) $
    3.73                    HOLogic.mk_eq (mk_Free "x" T i, Bound 0)),
    3.74 @@ -490,7 +486,7 @@
    3.75  
    3.76      val Abs_inverse_thms' =
    3.77        map #1 newT_iso_axms @
    3.78 -      map2 (fn r_inj => fn r => f_myinv_f OF [r_inj, r RS mp])
    3.79 +      map2 (fn r_inj => fn r => @{thm f_inv_f} OF [r_inj, r RS mp])
    3.80          iso_inj_thms_unfolded iso_thms;
    3.81  
    3.82      val Abs_inverse_thms = maps (mk_funs_inv thy5) Abs_inverse_thms';
    3.83 @@ -578,22 +574,22 @@
    3.84      val _ = message config "Proving induction rule for datatypes ...";
    3.85  
    3.86      val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
    3.87 -      (map (fn r => r RS myinv_f_f RS subst) iso_inj_thms_unfolded);
    3.88 -    val Rep_inverse_thms' = map (fn r => r RS myinv_f_f) iso_inj_thms_unfolded;
    3.89 +      (map (fn r => r RS @{thm inv_f_f} RS subst) iso_inj_thms_unfolded);
    3.90 +    val Rep_inverse_thms' = map (fn r => r RS @{thm inv_f_f}) iso_inj_thms_unfolded;
    3.91  
    3.92      fun mk_indrule_lemma ((prems, concls), ((i, _), T)) =
    3.93        let
    3.94 -        val Rep_t = Const (List.nth (all_rep_names, i), T --> Univ_elT) $
    3.95 +        val Rep_t = Const (nth all_rep_names i, T --> Univ_elT) $
    3.96            mk_Free "x" T i;
    3.97  
    3.98          val Abs_t = if i < length newTs then
    3.99              Const (Sign.intern_const thy6
   3.100 -              ("Abs_" ^ (List.nth (new_type_names, i))), Univ_elT --> T)
   3.101 -          else Const ("Inductive.myinv", [T --> Univ_elT, Univ_elT] ---> T) $
   3.102 -            Const (List.nth (all_rep_names, i), T --> Univ_elT)
   3.103 +              ("Abs_" ^ (nth new_type_names i)), Univ_elT --> T)
   3.104 +          else Const (@{const_name Fun.inv}, [T --> Univ_elT, Univ_elT] ---> T) $
   3.105 +            Const (nth all_rep_names i, T --> Univ_elT)
   3.106  
   3.107        in (prems @ [HOLogic.imp $
   3.108 -            (Const (List.nth (rep_set_names, i), UnivT') $ Rep_t) $
   3.109 +            (Const (nth rep_set_names i, UnivT') $ Rep_t) $
   3.110                (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
   3.111            concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i])
   3.112        end;