17 val _ = by (assume_tac 1) |
17 val _ = by (assume_tac 1) |
18 in val SELECT_AX = result() |
18 in val SELECT_AX = result() |
19 end; |
19 end; |
20 |
20 |
21 (*------------------------------------------------------------------------- |
21 (*------------------------------------------------------------------------- |
22 * A useful congruence rule |
22 * Congruence rule needed for TFL, but not for general simplification |
23 *-------------------------------------------------------------------------*) |
23 *-------------------------------------------------------------------------*) |
24 local val [p1,p2] = goal HOL.thy "(M = N) ==> \ |
24 local val [p1,p2] = goal HOL.thy "(M = N) ==> \ |
25 \ (!!x. ((x = N) ==> (f x = g x))) ==> \ |
25 \ (!!x. ((x = N) ==> (f x = g x))) ==> \ |
26 \ (Let M f = Let N g)"; |
26 \ (Let M f = Let N g)"; |
27 val _ = by (simp_tac (HOL_ss addsimps[Let_def,p1]) 1); |
27 val _ = by (simp_tac (HOL_ss addsimps[Let_def,p1]) 1); |
28 val _ = by (rtac p2 1); |
28 val _ = by (rtac p2 1); |
29 val _ = by (rtac refl 1); |
29 val _ = by (rtac refl 1); |
30 in val LET_CONG = result() RS eq_reflection |
30 in val LET_CONG = result() end; |
31 end; |
|
32 |
|
33 val COND_CONG = if_cong RS eq_reflection; |
|
34 |
31 |
35 fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]); |
32 fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]); |
36 |
33 |
37 val eqT = prove"(x = True) --> x" |
34 val eqT = prove"(x = True) --> x" |
38 val rev_eq_mp = prove"(x = y) --> y --> x" |
35 val rev_eq_mp = prove"(x = y) --> y --> x" |