equal
deleted
inserted
replaced
123 by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 1); |
123 by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 1); |
124 by (blast_tac (claset() addIs [Suc_leI RS le_less_trans, ack_less_mono2]) 1); |
124 by (blast_tac (claset() addIs [Suc_leI RS le_less_trans, ack_less_mono2]) 1); |
125 val lemma = result(); |
125 val lemma = result(); |
126 |
126 |
127 Goal "i<j ==> ack(i,k) < ack(j,k)"; |
127 Goal "i<j ==> ack(i,k) < ack(j,k)"; |
128 by (dtac less_eq_Suc_add 1); |
128 by (dtac less_imp_Suc_add 1); |
129 by (blast_tac (claset() addSIs [lemma]) 1); |
129 by (blast_tac (claset() addSIs [lemma]) 1); |
130 qed "ack_less_mono1"; |
130 qed "ack_less_mono1"; |
131 |
131 |
132 (*PROPERTY A 7', monotonicity for<=*) |
132 (*PROPERTY A 7', monotonicity for<=*) |
133 Goal "i<=j ==> ack(i,k)<=ack(j,k)"; |
133 Goal "i<=j ==> ack(i,k)<=ack(j,k)"; |