src/HOL/IMP/Denotational.thy
 changeset 52402 c2f30ba4bb98 parent 52401 56e83c57f953 child 58889 5b7a9633cfa8
equal inserted replaced
52401:56e83c57f953 52402:c2f30ba4bb98
`    69 "chain S = (\<forall>i. S i \<subseteq> S(Suc i))"`
`    69 "chain S = (\<forall>i. S i \<subseteq> S(Suc i))"`
`    70 `
`    70 `
`    71 lemma chain_total: "chain S \<Longrightarrow> S i \<le> S j \<or> S j \<le> S i"`
`    71 lemma chain_total: "chain S \<Longrightarrow> S i \<le> S j \<or> S j \<le> S i"`
`    72 by (metis chain_def le_cases lift_Suc_mono_le)`
`    72 by (metis chain_def le_cases lift_Suc_mono_le)`
`    73 `
`    73 `
`    74 definition cont :: "('a set \<Rightarrow> 'a set) \<Rightarrow> bool" where`
`    74 definition cont :: "('a set \<Rightarrow> 'b set) \<Rightarrow> bool" where`
`    75 "cont f = (\<forall>S. chain S \<longrightarrow> f(UN n. S n) = (UN n. f(S n)))"`
`    75 "cont f = (\<forall>S. chain S \<longrightarrow> f(UN n. S n) = (UN n. f(S n)))"`
`    76 `
`    76 `
`    77 lemma mono_if_cont: fixes f :: "'a set \<Rightarrow> 'a set"`
`    77 lemma mono_if_cont: fixes f :: "'a set \<Rightarrow> 'b set"`
`    78   assumes "cont f" shows "mono f"`
`    78   assumes "cont f" shows "mono f"`
`    79 proof`
`    79 proof`
`    80   fix a b :: "'a set" assume "a \<subseteq> b"`
`    80   fix a b :: "'a set" assume "a \<subseteq> b"`
`    81   let ?S = "\<lambda>n::nat. if n=0 then a else b"`
`    81   let ?S = "\<lambda>n::nat. if n=0 then a else b"`
`    82   have "chain ?S" using `a \<subseteq> b` by(auto simp: chain_def)`
`    82   have "chain ?S" using `a \<subseteq> b` by(auto simp: chain_def)`