src/HOL/HOL.thy
changeset 59628 2b15625b85fc
parent 59621 291934bac95e
child 59779 b6bda9140e39
     1.1 --- a/src/HOL/HOL.thy	Fri Mar 06 21:20:30 2015 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Mar 06 23:14:41 2015 +0100
     1.3 @@ -1194,60 +1194,65 @@
     1.4  let
     1.5    val (f_Let_unfold, x_Let_unfold) =
     1.6      let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_unfold}
     1.7 -    in (Thm.global_cterm_of @{theory} f, Thm.global_cterm_of @{theory} x) end
     1.8 +    in apply2 (Thm.cterm_of @{context}) (f, x) end
     1.9    val (f_Let_folded, x_Let_folded) =
    1.10      let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_folded}
    1.11 -    in (Thm.global_cterm_of @{theory} f, Thm.global_cterm_of @{theory} x) end;
    1.12 +    in apply2 (Thm.cterm_of @{context}) (f, x) end;
    1.13    val g_Let_folded =
    1.14      let val [(_ $ _ $ (g $ _))] = Thm.prems_of @{thm Let_folded}
    1.15 -    in Thm.global_cterm_of @{theory} g end;
    1.16 +    in Thm.cterm_of @{context} g end;
    1.17    fun count_loose (Bound i) k = if i >= k then 1 else 0
    1.18      | count_loose (s $ t) k = count_loose s k + count_loose t k
    1.19      | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
    1.20      | count_loose _ _ = 0;
    1.21    fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) =
    1.22 -   case t
    1.23 -    of Abs (_, _, t') => count_loose t' 0 <= 1
    1.24 -     | _ => true;
    1.25 -in fn _ => fn ctxt => fn ct => if is_trivial_let (Thm.term_of ct)
    1.26 -  then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
    1.27 -  else let (*Norbert Schirmer's case*)
    1.28 -    val thy = Proof_Context.theory_of ctxt;
    1.29 -    val t = Thm.term_of ct;
    1.30 -    val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
    1.31 -  in Option.map (hd o Variable.export ctxt' ctxt o single)
    1.32 -    (case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in normal form *)
    1.33 -      if is_Free x orelse is_Bound x orelse is_Const x
    1.34 -      then SOME @{thm Let_def}
    1.35 -      else
    1.36 -        let
    1.37 -          val n = case f of (Abs (x, _, _)) => x | _ => "x";
    1.38 -          val cx = Thm.global_cterm_of thy x;
    1.39 -          val xT = Thm.typ_of_cterm cx;
    1.40 -          val cf = Thm.global_cterm_of thy f;
    1.41 -          val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
    1.42 -          val (_ $ _ $ g) = Thm.prop_of fx_g;
    1.43 -          val g' = abstract_over (x,g);
    1.44 -          val abs_g'= Abs (n,xT,g');
    1.45 -        in (if (g aconv g')
    1.46 -             then
    1.47 -                let
    1.48 -                  val rl =
    1.49 -                    cterm_instantiate [(f_Let_unfold, cf), (x_Let_unfold, cx)] @{thm Let_unfold};
    1.50 -                in SOME (rl OF [fx_g]) end
    1.51 -             else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g') then NONE (*avoid identity conversion*)
    1.52 -             else let
    1.53 -                   val g'x = abs_g'$x;
    1.54 -                   val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.global_cterm_of thy g'x));
    1.55 -                   val rl = cterm_instantiate
    1.56 -                             [(f_Let_folded, Thm.global_cterm_of thy f), (x_Let_folded, cx),
    1.57 -                              (g_Let_folded, Thm.global_cterm_of thy abs_g')]
    1.58 -                             @{thm Let_folded};
    1.59 -                 in SOME (rl OF [Thm.transitive fx_g g_g'x])
    1.60 -                 end)
    1.61 -        end
    1.62 -    | _ => NONE)
    1.63 -  end
    1.64 +    (case t of
    1.65 +      Abs (_, _, t') => count_loose t' 0 <= 1
    1.66 +    | _ => true);
    1.67 +in
    1.68 +  fn _ => fn ctxt => fn ct =>
    1.69 +    if is_trivial_let (Thm.term_of ct)
    1.70 +    then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
    1.71 +    else
    1.72 +      let (*Norbert Schirmer's case*)
    1.73 +        val t = Thm.term_of ct;
    1.74 +        val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
    1.75 +      in
    1.76 +        Option.map (hd o Variable.export ctxt' ctxt o single)
    1.77 +          (case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in normal form *)
    1.78 +            if is_Free x orelse is_Bound x orelse is_Const x
    1.79 +            then SOME @{thm Let_def}
    1.80 +            else
    1.81 +              let
    1.82 +                val n = case f of (Abs (x, _, _)) => x | _ => "x";
    1.83 +                val cx = Thm.cterm_of ctxt x;
    1.84 +                val xT = Thm.typ_of_cterm cx;
    1.85 +                val cf = Thm.cterm_of ctxt f;
    1.86 +                val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
    1.87 +                val (_ $ _ $ g) = Thm.prop_of fx_g;
    1.88 +                val g' = abstract_over (x, g);
    1.89 +                val abs_g'= Abs (n, xT, g');
    1.90 +              in
    1.91 +                if g aconv g' then
    1.92 +                  let
    1.93 +                    val rl =
    1.94 +                      cterm_instantiate [(f_Let_unfold, cf), (x_Let_unfold, cx)] @{thm Let_unfold};
    1.95 +                  in SOME (rl OF [fx_g]) end
    1.96 +                else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g')
    1.97 +                then NONE (*avoid identity conversion*)
    1.98 +                else
    1.99 +                  let
   1.100 +                    val g'x = abs_g' $ x;
   1.101 +                    val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x));
   1.102 +                    val rl =
   1.103 +                      @{thm Let_folded} |> cterm_instantiate
   1.104 +                        [(f_Let_folded, Thm.cterm_of ctxt f),
   1.105 +                         (x_Let_folded, cx),
   1.106 +                         (g_Let_folded, Thm.cterm_of ctxt abs_g')];
   1.107 +                  in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
   1.108 +              end
   1.109 +          | _ => NONE)
   1.110 +      end
   1.111  end *}
   1.112  
   1.113  lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"