Envir.(beta_)eta_contract;
authorwenzelm
Mon Feb 06 20:58:54 2006 +0100 (2006-02-06)
changeset 18929d81435108688
parent 18928 042608ffa2ec
child 18930 29d39c10822e
Envir.(beta_)eta_contract;
src/HOL/Import/proof_kernel.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/inductive_realizer.ML
src/Pure/Proof/reconstruct.ML
src/Pure/drule.ML
src/Pure/meta_simplifier.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Mon Feb 06 11:01:28 2006 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Mon Feb 06 20:58:54 2006 +0100
     1.3 @@ -1052,9 +1052,9 @@
     1.4  
     1.5  fun rearrange sg tm th =
     1.6      let
     1.7 -	val tm' = Pattern.beta_eta_contract tm
     1.8 +	val tm' = Envir.beta_eta_contract tm
     1.9  	fun find []      n = permute_prems 0 1 0 (implies_intr (Thm.cterm_of sg tm) th)
    1.10 -	  | find (p::ps) n = if tm' aconv (Pattern.beta_eta_contract p)
    1.11 +	  | find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p)
    1.12  			     then permute_prems n 1 0 th
    1.13  			     else find ps (n+1)
    1.14      in
     2.1 --- a/src/HOL/Tools/datatype_realizer.ML	Mon Feb 06 11:01:28 2006 +0100
     2.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Mon Feb 06 20:58:54 2006 +0100
     2.3 @@ -72,7 +72,7 @@
     2.4                    val rT = List.nth (rec_result_Ts, i);
     2.5                    val vs' = filter_out is_unit vs;
     2.6                    val f = mk_Free "f" (map fastype_of vs' ---> rT) j;
     2.7 -                  val f' = Pattern.eta_contract (list_abs_free
     2.8 +                  val f' = Envir.eta_contract (list_abs_free
     2.9                      (map dest_Free vs, if i mem is then list_comb (f, vs')
    2.10                        else HOLogic.unit));
    2.11                  in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
     3.1 --- a/src/HOL/Tools/inductive_realizer.ML	Mon Feb 06 11:01:28 2006 +0100
     3.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Mon Feb 06 20:58:54 2006 +0100
     3.3 @@ -336,7 +336,7 @@
     3.4          end
     3.5        else ((recs, dummies), replicate (length rs) Extraction.nullt))
     3.6          ((get #rec_thms dt_info, dummies), rss);
     3.7 -    val rintrs = map (fn (intr, c) => Pattern.eta_contract
     3.8 +    val rintrs = map (fn (intr, c) => Envir.eta_contract
     3.9        (Extraction.realizes_of thy2 vs
    3.10          c (prop_of (forall_intr_list (map (cterm_of (sign_of thy2) o Var)
    3.11            (rev (Term.add_vars (prop_of intr) []) \\ params')) intr))))
     4.1 --- a/src/Pure/Proof/reconstruct.ML	Mon Feb 06 11:01:28 2006 +0100
     4.2 +++ b/src/Pure/Proof/reconstruct.ML	Mon Feb 06 20:58:54 2006 +0100
     4.3 @@ -326,7 +326,7 @@
     4.4    | prop_of0 Hs (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts
     4.5    | prop_of0 _ _ = error "prop_of: partial proof object";
     4.6  
     4.7 -val prop_of' = Pattern.eta_contract oo (Envir.beta_norm oo prop_of0);
     4.8 +val prop_of' = Envir.beta_eta_contract oo prop_of0;
     4.9  val prop_of = prop_of' [];
    4.10  
    4.11  
     5.1 --- a/src/Pure/drule.ML	Mon Feb 06 11:01:28 2006 +0100
     5.2 +++ b/src/Pure/drule.ML	Mon Feb 06 20:58:54 2006 +0100
     5.3 @@ -854,7 +854,7 @@
     5.4        | is_norm (t $ u) = is_norm t andalso is_norm u
     5.5        | is_norm (Abs (_, _, t)) = is_norm t
     5.6        | is_norm _ = true;
     5.7 -  in is_norm (Pattern.beta_eta_contract tm) end;
     5.8 +  in is_norm (Envir.beta_eta_contract tm) end;
     5.9  
    5.10  fun norm_hhf thy t =
    5.11    if is_norm_hhf t then t
    5.12 @@ -1012,7 +1012,7 @@
    5.13      fun rename [] t = ([], t)
    5.14        | rename (x' :: xs) (Abs (x, T, t)) =
    5.15            let val (xs', t') = rename xs t
    5.16 -          in (xs', Abs (getOpt (x',x), T, t')) end
    5.17 +          in (xs', Abs (the_default x x', T, t')) end
    5.18        | rename xs (t $ u) =
    5.19            let
    5.20              val (xs', t') = rename xs t;
     6.1 --- a/src/Pure/meta_simplifier.ML	Mon Feb 06 11:01:28 2006 +0100
     6.2 +++ b/src/Pure/meta_simplifier.ML	Mon Feb 06 20:58:54 2006 +0100
     6.3 @@ -430,7 +430,7 @@
     6.4        raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
     6.5      val (_, elhs) = Drule.dest_equals (Thm.cprop_of (Thm.eta_conversion lhs));
     6.6      val elhs = if term_of elhs aconv term_of lhs then lhs else elhs;  (*share identical copies*)
     6.7 -    val erhs = Pattern.eta_contract (term_of rhs);
     6.8 +    val erhs = Envir.eta_contract (term_of rhs);
     6.9      val perm =
    6.10        var_perm (term_of elhs, erhs) andalso
    6.11        not (term_of elhs aconv erhs) andalso
    6.12 @@ -551,7 +551,7 @@
    6.13      let
    6.14        val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
    6.15          handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
    6.16 -    (*val lhs = Pattern.eta_contract lhs;*)
    6.17 +    (*val lhs = Envir.eta_contract lhs;*)
    6.18        val a = valOf (cong_name (head_of (term_of lhs))) handle Option =>
    6.19          raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
    6.20        val (alist, weak) = congs;
    6.21 @@ -565,7 +565,7 @@
    6.22      let
    6.23        val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
    6.24          raise SIMPLIFIER ("Congruence not a meta-equality", thm);
    6.25 -    (*val lhs = Pattern.eta_contract lhs;*)
    6.26 +    (*val lhs = Envir.eta_contract lhs;*)
    6.27        val a = valOf (cong_name (head_of lhs)) handle Option =>
    6.28          raise SIMPLIFIER ("Congruence must start with a constant", thm);
    6.29        val (alist, _) = congs;