src/HOL/ex/Primrec.thy
changeset 11701 3d51fbf81c17
parent 11464 ddea204de5bc
child 11704 3c50a2cd6f00
     1.1 --- a/src/HOL/ex/Primrec.thy	Fri Oct 05 21:50:37 2001 +0200
     1.2 +++ b/src/HOL/ex/Primrec.thy	Fri Oct 05 21:52:39 2001 +0200
     1.3 @@ -159,16 +159,16 @@
     1.4  
     1.5  text {* PROPERTY A 8 *}
     1.6  
     1.7 -lemma ack_1 [simp]: "ack (1', j) = j + #2"
     1.8 +lemma ack_1 [simp]: "ack (Suc 0, j) = j + # 2"
     1.9    apply (induct j)
    1.10     apply simp_all
    1.11    done
    1.12  
    1.13  
    1.14 -text {* PROPERTY A 9.  The unary @{term 1} and @{term 2} in @{term
    1.15 +text {* PROPERTY A 9.  The unary @{text 1} and @{text 2} in @{term
    1.16    ack} is essential for the rewriting. *}
    1.17  
    1.18 -lemma ack_2 [simp]: "ack (2, j) = #2 * j + #3"
    1.19 +lemma ack_2 [simp]: "ack (Suc (Suc 0), j) = # 2 * j + # 3"
    1.20    apply (induct j)
    1.21     apply simp_all
    1.22    done
    1.23 @@ -203,7 +203,7 @@
    1.24  
    1.25  text {* PROPERTY A 10 *}
    1.26  
    1.27 -lemma ack_nest_bound: "ack(i1, ack (i2, j)) < ack (#2 + (i1 + i2), j)"
    1.28 +lemma ack_nest_bound: "ack(i1, ack (i2, j)) < ack (# 2 + (i1 + i2), j)"
    1.29    apply (simp add: numerals)
    1.30    apply (rule ack2_le_ack1 [THEN [2] less_le_trans])
    1.31    apply simp
    1.32 @@ -215,8 +215,8 @@
    1.33  
    1.34  text {* PROPERTY A 11 *}
    1.35  
    1.36 -lemma ack_add_bound: "ack (i1, j) + ack (i2, j) < ack (#4 + (i1 + i2), j)"
    1.37 -  apply (rule_tac j = "ack (2, ack (i1 + i2, j))" in less_trans)
    1.38 +lemma ack_add_bound: "ack (i1, j) + ack (i2, j) < ack (# 4 + (i1 + i2), j)"
    1.39 +  apply (rule_tac j = "ack (Suc (Suc 0), ack (i1 + i2, j))" in less_trans)
    1.40     prefer 2
    1.41     apply (rule ack_nest_bound [THEN less_le_trans])
    1.42     apply (simp add: Suc3_eq_add_3)
    1.43 @@ -231,7 +231,7 @@
    1.44    used @{text "k + 4"}.  Quantified version must be nested @{text
    1.45    "\<exists>k'. \<forall>i j. ..."} *}
    1.46  
    1.47 -lemma ack_add_bound2: "i < ack (k, j) ==> i + j < ack (#4 + k, j)"
    1.48 +lemma ack_add_bound2: "i < ack (k, j) ==> i + j < ack (# 4 + k, j)"
    1.49    apply (rule_tac j = "ack (k, j) + ack (0, j)" in less_trans)
    1.50     prefer 2
    1.51     apply (rule ack_add_bound [THEN less_le_trans])