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 (* Blast cannot prove these (yet?). |
|
104 Move somewhere else? |
|
105 Goal "(ALL x:A. x=a) = (A = {a})"; |
|
106 by(Blast_tac 1); |
|
107 qed "ball_triv_one_point1"; |
|
108 |
|
109 Goal "(ALL x:A. a=x) = (A = {a})"; |
|
110 by(Blast_tac 1); |
|
111 qed "ball_triv_one_point2"; |
|
112 *) |
|
113 |
103 Goal "(EX x:A. x=a) = (a:A)"; |
114 Goal "(EX x:A. x=a) = (a:A)"; |
104 by(Blast_tac 1); |
115 by(Blast_tac 1); |
105 qed "bex_triv_one_point1"; |
116 qed "bex_triv_one_point1"; |
106 |
117 |
107 Goal "(EX x:A. a=x) = (a:A)"; |
118 Goal "(EX x:A. a=x) = (a:A)"; |
110 |
121 |
111 Goal "(EX x:A. x=a & P x) = (a:A & P a)"; |
122 Goal "(EX x:A. x=a & P x) = (a:A & P a)"; |
112 by(Blast_tac 1); |
123 by(Blast_tac 1); |
113 qed "bex_one_point1"; |
124 qed "bex_one_point1"; |
114 |
125 |
|
126 Goal "(EX x:A. a=x & P x) = (a:A & P a)"; |
|
127 by(Blast_tac 1); |
|
128 qed "bex_one_point2"; |
|
129 |
115 Goal "(ALL x:A. x=a --> P x) = (a:A --> P a)"; |
130 Goal "(ALL x:A. x=a --> P x) = (a:A --> P a)"; |
116 by(Blast_tac 1); |
131 by(Blast_tac 1); |
117 qed "ball_one_point1"; |
132 qed "ball_one_point1"; |
118 |
133 |
119 Goal "(ALL x:A. a=x --> P x) = (a:A --> P a)"; |
134 Goal "(ALL x:A. a=x --> P x) = (a:A --> P a)"; |
120 by(Blast_tac 1); |
135 by(Blast_tac 1); |
121 qed "ball_one_point2"; |
136 qed "ball_one_point2"; |
122 |
137 |
123 Addsimps [bex_triv_one_point1,bex_triv_one_point2,bex_one_point1, |
138 Addsimps [bex_triv_one_point1,bex_triv_one_point2, |
|
139 bex_one_point1,bex_one_point2, |
124 ball_one_point1,ball_one_point2]; |
140 ball_one_point1,ball_one_point2]; |
125 |
141 |
126 let |
142 let |
127 val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) |
143 val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) |
128 ("EX x:A. P(x) & Q(x)",HOLogic.boolT) |
144 ("EX x:A. P(x) & Q(x)",HOLogic.boolT) |
131 Quantifier1.prove_one_point_ex_tac; |
147 Quantifier1.prove_one_point_ex_tac; |
132 |
148 |
133 val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; |
149 val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; |
134 |
150 |
135 val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) |
151 val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) |
136 ("ALL x:A. P(x) & P'(x) --> Q(x)",HOLogic.boolT) |
152 ("ALL x:A. P(x) --> Q(x)",HOLogic.boolT) |
137 |
153 |
138 val swap = prove_goal thy |
154 val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN |
139 "((!x. A x & EP x --> Q x) = (!x. E x --> A x & P x --> Q x)) ==> \ |
|
140 \ ((!x. A x --> EP x --> Q x) = (!x. A x --> E x --> P x --> Q x))" |
|
141 (fn ths => [cut_facts_tac ths 1, Blast_tac 1]); |
|
142 |
|
143 val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN rtac swap 1 THEN |
|
144 Quantifier1.prove_one_point_all_tac; |
155 Quantifier1.prove_one_point_all_tac; |
145 |
156 |
146 val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; |
157 val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; |
147 |
158 |
148 val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex; |
159 val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex; |