equal
deleted
inserted
replaced
|
1 theory Isar = Sets: |
|
2 |
|
3 section{*A Taste of Structured Proofs in Isar*} |
|
4 |
|
5 lemma [intro?]: "mono f \<Longrightarrow> x \<in> f (lfp f) \<Longrightarrow> x \<in> lfp f" |
|
6 by(simp only: lfp_unfold [symmetric]) |
|
7 |
|
8 lemma "lfp(\<lambda>T. A \<union> M\<inverse> `` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}" |
|
9 (is "lfp ?F = ?toA") |
|
10 proof |
|
11 show "lfp ?F \<subseteq> ?toA" |
|
12 by (blast intro!: lfp_lowerbound intro:rtrancl_trans) |
|
13 |
|
14 show "?toA \<subseteq> lfp ?F" |
|
15 proof |
|
16 fix s assume "s \<in> ?toA" |
|
17 then obtain t where stM: "(s,t) \<in> M\<^sup>*" and tA: "t \<in> A" by blast |
|
18 from stM show "s \<in> lfp ?F" |
|
19 proof (rule converse_rtrancl_induct) |
|
20 from tA have "t \<in> ?F (lfp ?F)" by blast |
|
21 with mono_ef show "t \<in> lfp ?F" .. |
|
22 fix s s' assume "(s,s') \<in> M" and "(s',t) \<in> M\<^sup>*" and "s' \<in> lfp ?F" |
|
23 then have "s \<in> ?F (lfp ?F)" by blast |
|
24 with mono_ef show "s \<in> lfp ?F" .. |
|
25 qed |
|
26 qed |
|
27 qed |
|
28 |
|
29 end |
|
30 |