equal
deleted
inserted
replaced
41 in |
41 in |
42 |
42 |
43 (*For simplifying both sides of an equation: |
43 (*For simplifying both sides of an equation: |
44 [| a=c; b=c |] ==> b=a |
44 [| a=c; b=c |] ==> b=a |
45 Can use resolve_tac [split_eqn] to prepare an equation for simplification. *) |
45 Can use resolve_tac [split_eqn] to prepare an equation for simplification. *) |
46 val split_eqn = Drule.standard (sym RSN (2,trans) RS sym); |
46 val split_eqn = Drule.export_without_context (sym RSN (2,trans) RS sym); |
47 |
47 |
48 |
48 |
49 (* [| a=b; b=c |] ==> reduce(a,c) *) |
49 (* [| a=b; b=c |] ==> reduce(a,c) *) |
50 val red_trans = Drule.standard (trans RS red_if_equal); |
50 val red_trans = Drule.export_without_context (trans RS red_if_equal); |
51 |
51 |
52 (*For REWRITE rule: Make a reduction rule for simplification, e.g. |
52 (*For REWRITE rule: Make a reduction rule for simplification, e.g. |
53 [| a: C(0); ... ; a=c: C(0) |] ==> rec(0,a,b) = c: C(0) *) |
53 [| a: C(0); ... ; a=c: C(0) |] ==> rec(0,a,b) = c: C(0) *) |
54 fun simp_rule rl = rl RS trans; |
54 fun simp_rule rl = rl RS trans; |
55 |
55 |