TFL/thms.sml
 changeset 3458 5ff4bfab859c parent 3302 404fe31fd8d2 child 6498 1ebbe18fe236
equal inserted replaced
3457:a8ab7c64817c 3458:5ff4bfab859c
`    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"`