src/LCF/LCF.thy
changeset 19758 093690d4ba60
parent 19757 4a2a71c31968
child 22810 a8455ca995d6
equal deleted inserted replaced
19757:4a2a71c31968 19758:093690d4ba60
   368     and 2: "P(UU::'a,UU::'b)"
   368     and 2: "P(UU::'a,UU::'b)"
   369     and 3: "ALL x y. P(x,y) --> P(f(x),g(y))"
   369     and 3: "ALL x y. P(x,y) --> P(f(x),g(y))"
   370   shows "P(FIX(f),FIX(g))"
   370   shows "P(FIX(f),FIX(g))"
   371   apply (rule FIX1 [THEN ssubst, of _ f g])
   371   apply (rule FIX1 [THEN ssubst, of _ f g])
   372   apply (rule FIX2 [THEN ssubst, of _ f g])
   372   apply (rule FIX2 [THEN ssubst, of _ f g])
   373   apply (rule induct [OF 1, where ?f = "%x. <f(FST(x)),g(SND(x))>"])
   373   apply (rule induct [where ?f = "%x. <f(FST(x)),g(SND(x))>"])
       
   374   apply (rule 1)
   374   apply simp
   375   apply simp
   375   apply (rule 2)
   376   apply (rule 2)
   376   apply (simp add: expand_all_PROD)
   377   apply (simp add: expand_all_PROD)
   377   apply (rule 3)
   378   apply (rule 3)
   378   done
   379   done