*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue*From*: Ondřej Kunčar <kuncar at in.tum.de>*Date*: Tue, 23 Oct 2012 11:43:03 +0200*In-reply-to*: <1350977142.3906.79.camel@lapbroy33>*References*: <1350924337.3906.54.camel@lapbroy33> <alpine.LNX.2.00.1210222057450.14640@macbroy20.informatik.tu-muenchen.de> <1350977142.3906.79.camel@lapbroy33>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:16.0) Gecko/20121007 Thunderbird/16.0

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 here: fun instantiate_normalize instpair th = Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl); 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.

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*)

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)) else 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)) end val th = Thm (deriv_rule2 ((if Envir.is_empty env then I else if Envir.above env smax then

else curry op oo (Proofterm.norm_proof' env))

{tags = [], maxidx = Envir.maxidx_of env,

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) else 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) end;

handle TERM _ => raise THM("bicompose: 1st premise", 0, [orule]) end; 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) = let val A = SOME 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

NONE => tryasms rest (n + 1) | cell as SOME ((_, tpairs), _) =>

(Seq.make (fn () => cell),

end 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)); in if eres_flg then eres (rev rAs) else res () end;

**Follow-Ups**:

**References**:**[isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue***From:*Peter Lammich

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

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

- Previous by Date: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
- Next by Date: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
- Previous by Thread: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
- Next by Thread: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
- Cl-isabelle-users October 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list