*To*: Alexander Krauss <krauss at in.tum.de>*Subject*: Re: [isabelle] Congruence rule for Let*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Wed, 08 Sep 2010 10:17:28 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4C87430E.5020801@in.tum.de>*References*: <4C865771.6010505@kit.edu> <4C87430E.5020801@in.tum.de>*User-agent*: Thunderbird 2.0.0.17 (X11/20080925)

Hi Alex,

Actually, I had expected that the first rule works. I need to dig intothis again. The rule that should definitely work is the following"f M = g N ==> Let M f = Let N g"It has the same effect on the induction rule as unfolding all lets. Canyou try if it works for your function?

"compE2 L ins pcs (if (e) e\<^isub>1 else e\<^isub>2) = (let els = compE2 L ins pcs e\<^isub>2; thn = compE2 L ins ((length els + 1) # pcs) e\<^isub>1; cnd = compE2 L ins ((length thn + length els + 2) # pcs) e; test = IfFalse (int (length thn) + 2); thnex = Goto (int (length els) + 1) in cnd @ [test] @ thn @ [thnex] @ els)" !!L ins pcs e e\<^isub>1 e\<^isub>2. [| ?P L ins pcs e\<^isub>2; ?P L ins ((length (compE2 L ins pcs e\<^isub>2) + 1) # pcs) e\<^isub>1; ?P L ins pcs e\<^isub>2; ?P L ins ((length (compE2 L ins ((length (compE2 L ins pcs e\<^isub>2) + 1) # pcs) e\<^isub>1) + length (compE2 L ins pcs e\<^isub>2) + 2) # pcs) e; ?P L ins pcs e\<^isub>2; ?P L ins ((length (compE2 L ins pcs e\<^isub>2) + 1) # pcs) e\<^isub>1; ?P L ins pcs e\<^isub>2; ?P L ins ((length (compE2 L ins pcs e\<^isub>2) + 1) # pcs) e\<^isub>1; ?P L ins pcs e\<^isub>2; ?P L ins pcs e\<^isub>2 |] ==> ?P L ins pcs (if (e) e\<^isub>1 else e\<^isub>2);

This seems easy enough using the functions in ch 5 of the ReferenceManual[...]The ind.hyp. Andreas is referring to appears nested inside the inductionrule, where it cannot be easily manipulated by hand...

Well, I managed to transform it, but it is not a satisfactory solution: lemma meta_all_eq_conv: "!!P b. (!!a. a = b ==> PROP P a) == PROP P b" "!!P c. (!!a b. a = c ==> PROP P a b) == PROP P c b" "!!P d. (!!a b c. a = d ==> PROP P a b c) == PROP P d b c" "!!P e. (!!a b c d. a = e ==> PROP P a b c d) == PROP P e b c d" thm compE2_compEs2.induct[unfolded meta_all_eq_conv] I need one rewrite rule for every nesting level of let expressions. Andreas

**Follow-Ups**:**Re: [isabelle] Congruence rule for Let***From:*Alexander Krauss

**References**:**[isabelle] Congruence rule for Let***From:*Andreas Lochbihler

**Re: [isabelle] Congruence rule for Let***From:*Alexander Krauss

- Previous by Date: Re: [isabelle] Congruence rule for Let
- Next by Date: Re: [isabelle] problem with class and sulocale declarations
- Previous by Thread: Re: [isabelle] Congruence rule for Let
- Next by Thread: Re: [isabelle] Congruence rule for Let
- Cl-isabelle-users September 2010 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