Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue

This says excplitly that your resulting rule instance will be produced by
Drule.instantiate_normalize, and thus in beta-normal form.  So you loose
if you try to make a plain then_conv step based on something that is not
in beta-normal form.

So what normalizations does instantiate_normalize do (beta?, eta?,
beta-eta?, how deep?). Looking at the source code does not really help

fun instantiate_normalize instpair th =
   Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR

Even if looking 4 levels deep from here (COMP_INCR -> COMP -> compose ->
bicompose), one finds no comment mentioning normal forms, nor any
function whose name would suggest any particular kind of normalization.

Peter has already mentioned it but I want to do it more explicitly because this thread clearly shows how the canonical "look at the ML source"-approach fails.
ML source is not the real documentation!

How should I know that instantiate_normalize do beta-normalization?

By looking at this?

fun bicompose_aux flatten match (state, (stpairs, Bs, Bi, C), lifted)
                        (eres_flg, orule, nsubgoal) =
 let val Thm (sder, {maxidx=smax, shyps=sshyps, hyps=shyps, ...}) = state
     and Thm (rder, {maxidx=rmax, shyps=rshyps, hyps=rhyps,
             tpairs=rtpairs, prop=rprop,...}) = orule
         (*How many hyps to skip over during normalization*)
and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0)
     val thy = Theory.deref (merge_thys2 state orule);
     (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
     fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) =
       let val normt = Envir.norm_term env;
           (*perform minimal copying here by examining env*)
           val (ntpairs, normp) =
             if Envir.is_empty env then (tpairs, (Bs @ As, C))
             let val ntps = map (pairself normt) tpairs
             in if Envir.above env smax then
                  (*no assignments in state; normalize the rule only*)
                  if lifted
                  then (ntps, (Bs @ map (norm_term_skip env nlift) As, C))
                  else (ntps, (Bs @ map normt As, C))
                else if match then raise COMPOSE
                else (*normalize the new rule fully*)
                  (ntps, (map normt (Bs @ As), normt C))
           val th =
             Thm (deriv_rule2
                   ((if Envir.is_empty env then I
                     else if Envir.above env smax then
(fn f => fn der => f (Proofterm.norm_proof' env der))
                       curry op oo (Proofterm.norm_proof' env))
(Proofterm.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder,
                {tags = [],
                 maxidx = Envir.maxidx_of env,
shyps = Envir.insert_sorts env (Sorts.union rshyps sshyps),
                 hyps = union_hyps rhyps shyps,
                 tpairs = ntpairs,
                 prop = Logic.list_implies normp,
                 thy_ref = Theory.check_thy thy})
        in  Seq.cons th thq  end  handle COMPOSE => thq;
     val (rAs,B) = Logic.strip_prems(nsubgoal, [], rprop)
       handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]);
     (*Modify assumptions, deleting n-th if n>0 for e-resolution*)
     fun newAs(As0, n, dpairs, tpairs) =
       let val (As1, rder') =
         if not lifted then (As0, rder)
           let val rename = rename_bvars dpairs tpairs B As0
           in (map (rename strip_apply) As0,
             deriv_rule1 (Proofterm.map_proof_terms (rename K) I) rder)
in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n)
          handle TERM _ =>
          raise THM("bicompose: 1st premise", 0, [orule])
     val env = Envir.empty(Int.max(rmax,smax));
     val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi);
     val dpairs = BBi :: (rtpairs at stpairs);

     (*elim-resolution: try each assumption in turn*)
     fun eres [] = raise THM ("bicompose: no premises", 0, [orule, state])
       | eres (A1 :: As) =
             val A = SOME A1;
val (close, asms, concl) = Logic.assum_problems (nlift + 1, A1);
             val concl' = close concl;
             fun tryasms [] _ = Seq.empty
               | tryasms (asm :: rest) n =
                   if Term.could_unify (asm, concl) then
                     let val asm' = close asm in
(case Seq.pull (Unify.unifiers (thy, env, (asm', concl') :: dpairs)) of
                         NONE => tryasms rest (n + 1)
                       | cell as SOME ((_, tpairs), _) =>
Seq.it_right (addth A (newAs (As, n, [BBi, (concl', asm')], tpairs)))
                             (Seq.make (fn () => cell),
Seq.make (fn () => Seq.pull (tryasms rest (n + 1)))))
                   else tryasms rest (n + 1);
           in tryasms asms 1 end;

     (*ordinary resolution*)
     fun res () =
       (case Seq.pull (Unify.unifiers (thy, env, dpairs)) of
         NONE => Seq.empty
       | cell as SOME ((_, tpairs), _) =>
           Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs)))
             (Seq.make (fn () => cell), Seq.empty));
   if eres_flg then eres (rev rAs) else res ()

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.