98 by (simp_tac (simpset() addsimps [Bex_def]) 1); |
98 by (simp_tac (simpset() addsimps [Bex_def]) 1); |
99 qed "bex_triv"; |
99 qed "bex_triv"; |
100 |
100 |
101 Addsimps [ball_triv, bex_triv]; |
101 Addsimps [ball_triv, bex_triv]; |
102 |
102 |
103 Goalw [Bex_def] "(ALL x:A. x=a --> P x) = (a:A --> P a)"; |
103 Goal "(EX x:A. x=a) = (a:A)"; |
104 by(Blast_tac 1); |
104 by(Blast_tac 1); |
105 qed "ball_one_point"; |
105 qed "bex_triv_one_point1"; |
|
106 |
|
107 Goal "(EX x:A. a=x) = (a:A)"; |
|
108 by(Blast_tac 1); |
|
109 qed "bex_triv_one_point2"; |
106 |
110 |
107 Goal "(EX x:A. x=a & P x) = (a:A & P a)"; |
111 Goal "(EX x:A. x=a & P x) = (a:A & P a)"; |
108 by(Blast_tac 1); |
112 by(Blast_tac 1); |
109 qed "bex_one_point"; |
113 qed "bex_one_point1"; |
110 |
114 |
111 Addsimps [ball_one_point,bex_one_point]; |
115 Goal "(ALL x:A. x=a --> P x) = (a:A --> P a)"; |
|
116 by(Blast_tac 1); |
|
117 qed "ball_one_point1"; |
|
118 |
|
119 Goal "(ALL x:A. a=x --> P x) = (a:A --> P a)"; |
|
120 by(Blast_tac 1); |
|
121 qed "ball_one_point2"; |
|
122 |
|
123 Addsimps [bex_triv_one_point1,bex_triv_one_point2,bex_one_point1, |
|
124 ball_one_point1,ball_one_point2]; |
112 |
125 |
113 let |
126 let |
114 val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) |
127 val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) |
115 ("EX x:A. P(x) & Q(x)",HOLogic.boolT) |
128 ("EX x:A. P(x) & Q(x)",HOLogic.boolT) |
116 |
129 |