equal
deleted
inserted
replaced
1341 (*sledgehammer*); |
1341 (*sledgehammer*); |
1342 apply clarify |
1342 apply clarify |
1343 apply (rule_tac x = c in exI) |
1343 apply (rule_tac x = c in exI) |
1344 apply safe |
1344 apply safe |
1345 apply (case_tac "x = 0") |
1345 apply (case_tac "x = 0") |
1346 prefer 2 |
1346 apply (metis OrderedGroup.abs_ge_zero OrderedGroup.abs_zero order_less_le Ring_and_Field.split_mult_pos_le) |
1347 apply (subgoal_tac "x = Suc (x - 1)") |
1347 apply (subgoal_tac "x = Suc (x - 1)") |
1348 apply (erule ssubst) back |
1348 apply metis |
1349 apply (erule spec) |
|
1350 apply (rule Suc_pred') |
|
1351 apply simp |
1349 apply simp |
1352 apply (metis OrderedGroup.abs_ge_zero OrderedGroup.abs_zero order_less_le Ring_and_Field.split_mult_pos_le) |
|
1353 done |
1350 done |
1354 |
1351 |
1355 |
1352 |
1356 lemma bigo_fix2: |
1353 lemma bigo_fix2: |
1357 "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==> |
1354 "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==> |