equal
deleted
inserted
replaced
63 |
63 |
64 subsection {* Admissibility of special formulae and propagation *} |
64 subsection {* Admissibility of special formulae and propagation *} |
65 |
65 |
66 lemma adm_less: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)" |
66 lemma adm_less: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)" |
67 apply (rule admI) |
67 apply (rule admI) |
68 apply (simp add: cont2contlub [THEN contlubE]) |
68 apply (simp add: cont2contlubE) |
69 apply (rule lub_mono) |
69 apply (rule lub_mono) |
70 apply (erule (1) cont2mono [THEN ch2ch_monofun]) |
70 apply (erule (1) ch2ch_cont) |
71 apply (erule (1) cont2mono [THEN ch2ch_monofun]) |
71 apply (erule (1) ch2ch_cont) |
72 apply assumption |
72 apply assumption |
73 done |
73 done |
74 |
74 |
75 lemma adm_conj: "\<lbrakk>adm P; adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)" |
75 lemma adm_conj: "\<lbrakk>adm P; adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)" |
76 by (fast elim: admD intro: admI) |
76 by (fast elim: admD intro: admI) |
93 |
93 |
94 lemmas adm_all2 = adm_all [rule_format] |
94 lemmas adm_all2 = adm_all [rule_format] |
95 |
95 |
96 lemma adm_subst: "\<lbrakk>cont t; adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))" |
96 lemma adm_subst: "\<lbrakk>cont t; adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))" |
97 apply (rule admI) |
97 apply (rule admI) |
98 apply (simp add: cont2contlub [THEN contlubE]) |
98 apply (simp add: cont2contlubE) |
99 apply (erule admD) |
99 apply (erule admD) |
100 apply (erule (1) cont2mono [THEN ch2ch_monofun]) |
100 apply (erule (1) ch2ch_cont) |
101 apply assumption |
101 apply assumption |
102 done |
102 done |
103 |
103 |
104 lemma adm_UU_not_less: "adm (\<lambda>x. \<not> \<bottom> \<sqsubseteq> t x)" |
104 lemma adm_UU_not_less: "adm (\<lambda>x. \<not> \<bottom> \<sqsubseteq> t x)" |
105 by (simp add: adm_not_free) |
105 by (simp add: adm_not_free) |
241 val adm_not_conj = thm "adm_not_conj"; |
241 val adm_not_conj = thm "adm_not_conj"; |
242 val adm_lemmas = thms "adm_lemmas"; |
242 val adm_lemmas = thms "adm_lemmas"; |
243 *} |
243 *} |
244 |
244 |
245 end |
245 end |
246 |
|