68 "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x", |
68 "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x", |
69 (*two needed for the one-point-rule quantifier simplification procs*) |
69 (*two needed for the one-point-rule quantifier simplification procs*) |
70 "(? x. x=t & P(x)) = P(t)", (*essential for termination!!*) |
70 "(? x. x=t & P(x)) = P(t)", (*essential for termination!!*) |
71 "(! x. t=x --> P(x)) = P(t)" ]; (*covers a stray case*) |
71 "(! x. t=x --> P(x)) = P(t)" ]; (*covers a stray case*) |
72 |
72 |
73 val imp_cong = impI RSN |
73 val imp_cong = standard(impI RSN |
74 (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))" |
74 (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))" |
75 (fn _=> [(Blast_tac 1)]) RS mp RS mp); |
75 (fn _=> [(Blast_tac 1)]) RS mp RS mp)); |
76 |
76 |
77 (*Miniscoping: pushing in existential quantifiers*) |
77 (*Miniscoping: pushing in existential quantifiers*) |
78 val ex_simps = map prover |
78 val ex_simps = map prover |
79 ["(EX x. P x & Q) = ((EX x. P x) & Q)", |
79 ["(EX x. P x & Q) = ((EX x. P x) & Q)", |
80 "(EX x. P & Q x) = (P & (EX x. Q x))", |
80 "(EX x. P & Q x) = (P & (EX x. Q x))", |
107 end; |
107 end; |
108 |
108 |
109 bind_thms ("ex_simps", ex_simps); |
109 bind_thms ("ex_simps", ex_simps); |
110 bind_thms ("all_simps", all_simps); |
110 bind_thms ("all_simps", all_simps); |
111 bind_thm ("not_not", not_not); |
111 bind_thm ("not_not", not_not); |
|
112 bind_thm ("imp_cong", imp_cong); |
112 |
113 |
113 (* Elimination of True from asumptions: *) |
114 (* Elimination of True from asumptions: *) |
114 |
115 |
115 val True_implies_equals = prove_goal (the_context ()) |
116 val True_implies_equals = prove_goal (the_context ()) |
116 "(True ==> PROP P) == PROP P" |
117 "(True ==> PROP P) == PROP P" |