88 apply fast |
88 apply fast |
89 apply fast |
89 apply fast |
90 apply fast |
90 apply fast |
91 done |
91 done |
92 |
92 |
93 lemma awp_mono [rule_format (no_asm)]: "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)" |
93 lemma awp_mono [rule_format (no_asm)]: |
|
94 "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)" |
94 apply (induct_tac "c") |
95 apply (induct_tac "c") |
95 apply (simp_all (no_asm_simp)) |
96 apply (simp_all (no_asm_simp)) |
96 apply (rule allI, rule allI, rule impI) |
97 apply (rule allI, rule allI, rule impI) |
97 apply (erule allE, erule allE, erule mp) |
98 apply (erule allE, erule allE, erule mp) |
98 apply (erule allE, erule allE, erule mp, assumption) |
99 apply (erule allE, erule allE, erule mp, assumption) |
99 done |
100 done |
100 |
101 |
101 |
102 |
102 lemma vc_mono [rule_format (no_asm)]: "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)" |
103 lemma vc_mono [rule_format (no_asm)]: |
|
104 "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)" |
103 apply (induct_tac "c") |
105 apply (induct_tac "c") |
104 apply (simp_all (no_asm_simp)) |
106 apply (simp_all (no_asm_simp)) |
105 apply safe |
107 apply safe |
106 apply (erule allE,erule allE,erule impE,erule_tac [2] allE,erule_tac [2] mp) |
108 apply (erule allE,erule allE,erule impE,erule_tac [2] allE,erule_tac [2] mp) |
107 prefer 2 apply assumption |
109 prefer 2 apply assumption |