src/CCL/Fix.thy
changeset 36319 8feb2c4bef1a
parent 32153 a0e57fb1b930
child 42156 df219e736a5d
equal deleted inserted replaced
36318:3567d0571932 36319:8feb2c4bef1a
    96       apply simp_all
    96       apply simp_all
    97   done
    97   done
    98 
    98 
    99 (* All fixed points are lam-expressions *)
    99 (* All fixed points are lam-expressions *)
   100 
   100 
   101 lemma idgenfp_lam: "idgen(d) = d ==> d = lam x. ?f(x)"
   101 schematic_lemma idgenfp_lam: "idgen(d) = d ==> d = lam x. ?f(x)"
   102   apply (unfold idgen_def)
   102   apply (unfold idgen_def)
   103   apply (erule ssubst)
   103   apply (erule ssubst)
   104   apply (rule refl)
   104   apply (rule refl)
   105   done
   105   done
   106 
   106 
   128   apply (erule ssubst)
   128   apply (erule ssubst)
   129   apply (rule po_lam [THEN iffD2])
   129   apply (rule po_lam [THEN iffD2])
   130   apply simp
   130   apply simp
   131   done
   131   done
   132 
   132 
   133 lemma po_eta_lemma: "idgen(d) = d ==> d = lam x. ?f(x)"
   133 schematic_lemma po_eta_lemma: "idgen(d) = d ==> d = lam x. ?f(x)"
   134   apply (unfold idgen_def)
   134   apply (unfold idgen_def)
   135   apply (erule sym)
   135   apply (erule sym)
   136   done
   136   done
   137 
   137 
   138 lemma lemma1:
   138 lemma lemma1: