equal
deleted
inserted
replaced
98 from Semi.hyps obtain ac1 where ih1: "?G P c1 Q ac1" by blast |
98 from Semi.hyps obtain ac1 where ih1: "?G P c1 Q ac1" by blast |
99 from Semi.hyps obtain ac2 where ih2: "?G Q c2 R ac2" by blast |
99 from Semi.hyps obtain ac2 where ih2: "?G Q c2 R ac2" by blast |
100 show ?case (is "\<exists>ac. ?C ac") |
100 show ?case (is "\<exists>ac. ?C ac") |
101 proof |
101 proof |
102 show "?C(Asemi ac1 ac2)" |
102 show "?C(Asemi ac1 ac2)" |
103 using ih1 ih2 by (fastsimp elim!: pre_mono vc_mono) |
103 using ih1 ih2 by (fastforce elim!: pre_mono vc_mono) |
104 qed |
104 qed |
105 next |
105 next |
106 case (If P b c1 Q c2) |
106 case (If P b c1 Q c2) |
107 from If.hyps obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1" |
107 from If.hyps obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1" |
108 by blast |
108 by blast |