equal
deleted
inserted
replaced
2 |
2 |
3 theory RG_Hoare imports RG_Tran begin |
3 theory RG_Hoare imports RG_Tran begin |
4 |
4 |
5 subsection {* Proof System for Component Programs *} |
5 subsection {* Proof System for Component Programs *} |
6 |
6 |
7 declare Un_subset_iff [simp del] le_sup_iff [simp del] |
7 declare Un_subset_iff [simp del] sup.bounded_iff [simp del] |
8 |
8 |
9 definition stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where |
9 definition stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where |
10 "stable \<equiv> \<lambda>f g. (\<forall>x y. x \<in> f \<longrightarrow> (x, y) \<in> g \<longrightarrow> y \<in> f)" |
10 "stable \<equiv> \<lambda>f g. (\<forall>x y. x \<in> f \<longrightarrow> (x, y) \<in> g \<longrightarrow> y \<in> f)" |
11 |
11 |
12 inductive |
12 inductive |