src/HOL/ex/Primrec.thy
changeset 19676 187234ec6050
parent 16731 124b4782944f
child 19736 d8d0f8f51d69
     1.1 --- a/src/HOL/ex/Primrec.thy	Wed May 17 12:28:47 2006 +0200
     1.2 +++ b/src/HOL/ex/Primrec.thy	Wed May 17 22:34:44 2006 +0200
     1.3 @@ -46,8 +46,8 @@
     1.4    SC :: "nat list => nat"
     1.5    "SC l == Suc (zeroHd l)"
     1.6  
     1.7 -  CONST :: "nat => nat list => nat"
     1.8 -  "CONST k l == k"
     1.9 +  CONSTANT :: "nat => nat list => nat"
    1.10 +  "CONSTANT k l == k"
    1.11  
    1.12    PROJ :: "nat => nat list => nat"
    1.13    "PROJ i l == zeroHd (drop i l)"
    1.14 @@ -66,7 +66,7 @@
    1.15  inductive PRIMREC
    1.16    intros
    1.17      SC: "SC \<in> PRIMREC"
    1.18 -    CONST: "CONST k \<in> PRIMREC"
    1.19 +    CONSTANT: "CONSTANT k \<in> PRIMREC"
    1.20      PROJ: "PROJ i \<in> PRIMREC"
    1.21      COMP: "g \<in> PRIMREC ==> fs \<in> lists PRIMREC ==> COMP g fs \<in> PRIMREC"
    1.22      PREC: "f \<in> PRIMREC ==> g \<in> PRIMREC ==> PREC f g \<in> PRIMREC"
    1.23 @@ -78,8 +78,8 @@
    1.24    apply (simp add: SC_def)
    1.25    done
    1.26  
    1.27 -lemma CONST [simp]: "CONST k l = k"
    1.28 -  apply (simp add: CONST_def)
    1.29 +lemma CONSTANT [simp]: "CONSTANT k l = k"
    1.30 +  apply (simp add: CONSTANT_def)
    1.31    done
    1.32  
    1.33  lemma PROJ_0 [simp]: "PROJ 0 (x # l) = x"
    1.34 @@ -148,7 +148,7 @@
    1.35    done
    1.36  
    1.37  
    1.38 -text {* PROPERTY A 4'? Extra lemma needed for @{term CONST} case, constant functions *}
    1.39 +text {* PROPERTY A 4'? Extra lemma needed for @{term CONSTANT} case, constant functions *}
    1.40  
    1.41  lemma less_ack1 [iff]: "i < ack (i, j)"
    1.42    apply (induct i)
    1.43 @@ -251,7 +251,7 @@
    1.44    apply (simp_all add: le_add1 le_imp_less_Suc)
    1.45    done
    1.46  
    1.47 -lemma CONST_case: "CONST k l < ack (k, list_add l)"
    1.48 +lemma CONSTANT_case: "CONSTANT k l < ack (k, list_add l)"
    1.49    apply simp
    1.50    done
    1.51  
    1.52 @@ -336,7 +336,7 @@
    1.53  
    1.54  lemma ack_bounds_PRIMREC: "f \<in> PRIMREC ==> \<exists>k. \<forall>l. f l < ack (k, list_add l)"
    1.55    apply (erule PRIMREC.induct)
    1.56 -      apply (blast intro: SC_case CONST_case PROJ_case COMP_case PREC_case)+
    1.57 +      apply (blast intro: SC_case CONSTANT_case PROJ_case COMP_case PREC_case)+
    1.58    done
    1.59  
    1.60  lemma ack_not_PRIMREC: "(\<lambda>l. case l of [] => 0 | x # l' => ack (x, x)) \<notin> PRIMREC"