119 "(P & True) = P", "(True & P) = P", |
119 "(P & True) = P", "(True & P) = P", |
120 "(P & False) = False", "(False & P) = False", "(P & P) = P", |
120 "(P & False) = False", "(False & P) = False", "(P & P) = P", |
121 "(P | True) = True", "(True | P) = True", |
121 "(P | True) = True", "(True | P) = True", |
122 "(P | False) = P", "(False | P) = P", "(P | P) = P", |
122 "(P | False) = P", "(False | P) = P", "(P | P) = P", |
123 "((~P) = (~Q)) = (P=Q)", |
123 "((~P) = (~Q)) = (P=Q)", |
124 "(!x.P) = P", "(? x.P) = P", "? x. x=t", |
124 "(!x.P) = P", "(? x.P) = P", "? x. x=t", "? x. t=x", |
125 "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)", |
125 "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)", |
126 "(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ]; |
126 "(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ]; |
127 |
127 |
128 val meta_eq_to_obj_eq = prove_goal HOL.thy "x==y ==> x=y" |
128 val meta_eq_to_obj_eq = prove_goal HOL.thy "x==y ==> x=y" |
129 (fn [prem] => [rewtac prem, rtac refl 1]); |
129 (fn [prem] => [rewtac prem, rtac refl 1]); |