compile
authorblanchet
Fri Sep 14 12:09:27 2012 +0200 (2012-09-14)
changeset 49369d9800bc28427
parent 49368 df359ce891ac
child 49370 be6e749fd003
compile
src/HOL/Codatatype/Examples/Stream.thy
src/HOL/Codatatype/Examples/TreeFsetI.thy
     1.1 --- a/src/HOL/Codatatype/Examples/Stream.thy	Fri Sep 14 12:09:27 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Examples/Stream.thy	Fri Sep 14 12:09:27 2012 +0200
     1.3 @@ -133,27 +133,27 @@
     1.4  definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
     1.5  
     1.6  lemma "ones \<oplus> ones = twos"
     1.7 -by (intro stream_coind[where phi="%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"])
     1.8 +by (intro stream_coind[where P="%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"])
     1.9     auto
    1.10  
    1.11  lemma "n \<cdot> twos = ns (2 * n)"
    1.12 -by (intro stream_coind[where phi="%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"])
    1.13 +by (intro stream_coind[where P="%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"])
    1.14     force+
    1.15  
    1.16  lemma prod_scalar: "(n * m) \<cdot> xs = n \<cdot> m \<cdot> xs"
    1.17 -by (intro stream_coind[where phi="%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"])
    1.18 +by (intro stream_coind[where P="%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"])
    1.19     force+
    1.20  
    1.21  lemma scalar_plus: "n \<cdot> (xs \<oplus> ys) = n \<cdot> xs \<oplus> n \<cdot> ys"
    1.22 -by (intro stream_coind[where phi="%x1 x2. \<exists>n xs ys. x1 = n \<cdot> (xs \<oplus> ys) \<and> x2 = n \<cdot> xs \<oplus> n \<cdot> ys"])
    1.23 +by (intro stream_coind[where P="%x1 x2. \<exists>n xs ys. x1 = n \<cdot> (xs \<oplus> ys) \<and> x2 = n \<cdot> xs \<oplus> n \<cdot> ys"])
    1.24     (force simp: add_mult_distrib2)+
    1.25  
    1.26  lemma plus_comm: "xs \<oplus> ys = ys \<oplus> xs"
    1.27 -by (intro stream_coind[where phi="%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"])
    1.28 +by (intro stream_coind[where P="%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"])
    1.29     force+
    1.30  
    1.31  lemma plus_assoc: "(xs \<oplus> ys) \<oplus> zs = xs \<oplus> ys \<oplus> zs"
    1.32 -by (intro stream_coind[where phi="%x1 x2. \<exists>xs ys zs. x1 = (xs \<oplus> ys) \<oplus> zs \<and> x2 = xs \<oplus> ys \<oplus> zs"])
    1.33 +by (intro stream_coind[where P="%x1 x2. \<exists>xs ys zs. x1 = (xs \<oplus> ys) \<oplus> zs \<and> x2 = xs \<oplus> ys \<oplus> zs"])
    1.34     force+
    1.35  
    1.36  end
     2.1 --- a/src/HOL/Codatatype/Examples/TreeFsetI.thy	Fri Sep 14 12:09:27 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy	Fri Sep 14 12:09:27 2012 +0200
     2.3 @@ -52,7 +52,7 @@
     2.4  lemmas treeFsetI_coind = mp[OF treeFsetI.pred_coinduct]
     2.5  
     2.6  lemma "tmap (f o g) x = tmap f (tmap g x)"
     2.7 -by (intro treeFsetI_coind[where phi="%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])
     2.8 +by (intro treeFsetI_coind[where P="%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])
     2.9     force+
    2.10  
    2.11  end