src/LCF/LCF.thy
 changeset 19758 093690d4ba60 parent 19757 4a2a71c31968 child 22810 a8455ca995d6
equal 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`