src/Pure/meta_simplifier.ML
changeset 12155 13c5469b4bb3
parent 11886 36d0585f87de
child 12262 11ff5f47df6e
     1.1 --- a/src/Pure/meta_simplifier.ML	Mon Nov 12 10:43:25 2001 +0100
     1.2 +++ b/src/Pure/meta_simplifier.ML	Mon Nov 12 10:44:55 2001 +0100
     1.3 @@ -653,7 +653,7 @@
     1.4            else proc_rews ps;
     1.5    in case eta_t of
     1.6         Abs _ $ _ => Some (transitive eta_thm
     1.7 -         (beta_conversion false (rhs_of eta_thm)), skel0)
     1.8 +         (beta_conversion false eta_t'), skel0)
     1.9       | _ => (case rews (sort_rrules (Net.match_term rules eta_t)) of
    1.10                 None => proc_rews (Net.match_term procs eta_t)
    1.11               | some => some)
    1.12 @@ -678,7 +678,9 @@
    1.13         None => err ("Could not prove", thm')
    1.14       | Some thm2 => (case check_conv true (beta_eta_conversion t) thm2 of
    1.15            None => err ("Should not have proved", thm2)
    1.16 -        | Some thm2' => thm2')
    1.17 +        | Some thm2' =>
    1.18 +            if op aconv (pairself term_of (dest_equals (cprop_of thm2')))
    1.19 +            then None else Some thm2')
    1.20    end;
    1.21  
    1.22  val (cA, (cB, cC)) =
    1.23 @@ -687,6 +689,9 @@
    1.24  fun transitive' thm1 None = Some thm1
    1.25    | transitive' thm1 (Some thm2) = Some (transitive thm1 thm2);
    1.26  
    1.27 +fun transitive'' None thm2 = Some thm2
    1.28 +  | transitive'' (Some thm1) thm2 = Some (transitive thm1 thm2);
    1.29 +
    1.30  fun bottomc ((simprem,useprem,mutsimp), prover, sign, maxidx) =
    1.31    let
    1.32      fun botc skel mss t =
    1.33 @@ -759,15 +764,15 @@
    1.34     may be a redex. Example: map (%x.x) = (%xs.xs) wrt map_cong *)
    1.35                            (let
    1.36                               val thm = congc (prover mss, sign, maxidx) cong t0;
    1.37 -                             val t = rhs_of thm;
    1.38 +                             val t = if_none (apsome rhs_of thm) t0;
    1.39                               val (cl, cr) = Thm.dest_comb t
    1.40                               val dVar = Var(("", 0), dummyT)
    1.41                               val skel =
    1.42                                 list_comb (h, replicate (length ts) dVar)
    1.43                             in case botc skel mss cl of
    1.44 -                                None => Some thm
    1.45 -                              | Some thm' => Some (transitive thm
    1.46 -                                  (combination thm' (reflexive cr)))
    1.47 +                                None => thm
    1.48 +                              | Some thm' => transitive'' thm
    1.49 +                                  (combination thm' (reflexive cr))
    1.50                             end handle TERM _ => error "congc result"
    1.51                                      | Pattern.MATCH => appc ()))
    1.52                    | _ => appc ()