Re: [isabelle] Congruence rule for Let



Hi Alex,

Actually, I had expected that the first rule works. I need to dig into this 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. Can you try if it works for your function?
No, it doesn't. This produces the same effect like the congruence rule "[| M = N; f M = g N |] ==> Let M f = Let N g", it produces too many induction hypotheses.

For example, with your congruence rule declared as fundef_cong, the following equation in the definition of compE2 generates this induction case:

  "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 Reference Manual
[...]
The ind.hyp. Andreas is referring to appears nested inside the induction rule, 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





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