# HG changeset patch
# User wenzelm
# Date 1147898084 -7200
# Node ID 187234ec6050eedd0cbdc07252f63f5ec6ccc019
# Parent  a4894fb2a5f2e8601695ead25f31df4b2e5750d6
renamed CONST to CONSTANT;

diff -r a4894fb2a5f2 -r 187234ec6050 src/HOL/ex/Primrec.thy
--- a/src/HOL/ex/Primrec.thy	Wed May 17 12:28:47 2006 +0200
+++ b/src/HOL/ex/Primrec.thy	Wed May 17 22:34:44 2006 +0200
@@ -46,8 +46,8 @@
   SC :: "nat list => nat"
   "SC l == Suc (zeroHd l)"
 
-  CONST :: "nat => nat list => nat"
-  "CONST k l == k"
+  CONSTANT :: "nat => nat list => nat"
+  "CONSTANT k l == k"
 
   PROJ :: "nat => nat list => nat"
   "PROJ i l == zeroHd (drop i l)"
@@ -66,7 +66,7 @@
 inductive PRIMREC
   intros
     SC: "SC \<in> PRIMREC"
-    CONST: "CONST k \<in> PRIMREC"
+    CONSTANT: "CONSTANT k \<in> PRIMREC"
     PROJ: "PROJ i \<in> PRIMREC"
     COMP: "g \<in> PRIMREC ==> fs \<in> lists PRIMREC ==> COMP g fs \<in> PRIMREC"
     PREC: "f \<in> PRIMREC ==> g \<in> PRIMREC ==> PREC f g \<in> PRIMREC"
@@ -78,8 +78,8 @@
   apply (simp add: SC_def)
   done
 
-lemma CONST [simp]: "CONST k l = k"
-  apply (simp add: CONST_def)
+lemma CONSTANT [simp]: "CONSTANT k l = k"
+  apply (simp add: CONSTANT_def)
   done
 
 lemma PROJ_0 [simp]: "PROJ 0 (x # l) = x"
@@ -148,7 +148,7 @@
   done
 
 
-text {* PROPERTY A 4'? Extra lemma needed for @{term CONST} case, constant functions *}
+text {* PROPERTY A 4'? Extra lemma needed for @{term CONSTANT} case, constant functions *}
 
 lemma less_ack1 [iff]: "i < ack (i, j)"
   apply (induct i)
@@ -251,7 +251,7 @@
   apply (simp_all add: le_add1 le_imp_less_Suc)
   done
 
-lemma CONST_case: "CONST k l < ack (k, list_add l)"
+lemma CONSTANT_case: "CONSTANT k l < ack (k, list_add l)"
   apply simp
   done
 
@@ -336,7 +336,7 @@
 
 lemma ack_bounds_PRIMREC: "f \<in> PRIMREC ==> \<exists>k. \<forall>l. f l < ack (k, list_add l)"
   apply (erule PRIMREC.induct)
-      apply (blast intro: SC_case CONST_case PROJ_case COMP_case PREC_case)+
+      apply (blast intro: SC_case CONSTANT_case PROJ_case COMP_case PREC_case)+
   done
 
 lemma ack_not_PRIMREC: "(\<lambda>l. case l of [] => 0 | x # l' => ack (x, x)) \<notin> PRIMREC"
diff -r a4894fb2a5f2 -r 187234ec6050 src/ZF/Induct/Primrec.thy
--- a/src/ZF/Induct/Primrec.thy	Wed May 17 12:28:47 2006 +0200
+++ b/src/ZF/Induct/Primrec.thy	Wed May 17 22:34:44 2006 +0200
@@ -21,8 +21,8 @@
   SC :: "i"
   "SC == \<lambda>l \<in> list(nat). list_case(0, \<lambda>x xs. succ(x), l)"
 
-  CONST :: "i=>i"
-  "CONST(k) == \<lambda>l \<in> list(nat). k"
+  CONSTANT :: "i=>i"
+  "CONSTANT(k) == \<lambda>l \<in> list(nat). k"
 
   PROJ :: "i=>i"
   "PROJ(i) == \<lambda>l \<in> list(nat). list_case(0, \<lambda>x xs. x, drop(i,l))"
@@ -40,7 +40,7 @@
   ACK :: "i=>i"
 primrec
   "ACK(0) = SC"
-  "ACK(succ(i)) = PREC (CONST (ACK(i) ` [1]), COMP(ACK(i), [PROJ(0)]))"
+  "ACK(succ(i)) = PREC (CONSTANT (ACK(i) ` [1]), COMP(ACK(i), [PROJ(0)]))"
 
 syntax
   ack :: "[i,i]=>i"
@@ -55,8 +55,8 @@
 lemma SC: "[| x \<in> nat;  l \<in> list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)"
   by (simp add: SC_def)
 
-lemma CONST: "l \<in> list(nat) ==> CONST(k) ` l = k"
-  by (simp add: CONST_def)
+lemma CONSTANT: "l \<in> list(nat) ==> CONSTANT(k) ` l = k"
+  by (simp add: CONSTANT_def)
 
 lemma PROJ_0: "[| x \<in> nat;  l \<in> list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x"
   by (simp add: PROJ_def)
@@ -83,12 +83,12 @@
   domains prim_rec \<subseteq> "list(nat)->nat"
   intros
     "SC \<in> prim_rec"
-    "k \<in> nat ==> CONST(k) \<in> prim_rec"
+    "k \<in> nat ==> CONSTANT(k) \<in> prim_rec"
     "i \<in> nat ==> PROJ(i) \<in> prim_rec"
     "[| g \<in> prim_rec; fs\<in>list(prim_rec) |] ==> COMP(g,fs) \<in> prim_rec"
     "[| f \<in> prim_rec; g \<in> prim_rec |] ==> PREC(f,g) \<in> prim_rec"
   monos list_mono
-  con_defs SC_def CONST_def PROJ_def COMP_def PREC_def
+  con_defs SC_def CONSTANT_def PROJ_def COMP_def PREC_def
   type_intros nat_typechecks list.intros
     lam_type list_case_type drop_type List.map_type
     apply_type rec_type
@@ -118,12 +118,12 @@
 
 lemma ack_succ_0: "ack(succ(i), 0) = ack(i,1)"
   -- {* PROPERTY A 2 *}
-  by (simp add: CONST PREC_0)
+  by (simp add: CONSTANT PREC_0)
 
 lemma ack_succ_succ:
   "[| i\<in>nat;  j\<in>nat |] ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))"
   -- {* PROPERTY A 3 *}
-  by (simp add: CONST PREC_succ COMP_1 PROJ_0)
+  by (simp add: CONSTANT PREC_succ COMP_1 PROJ_0)
 
 lemmas [simp] = ack_0 ack_succ_0 ack_succ_succ ack_type
   and [simp del] = ACK.simps
@@ -245,16 +245,16 @@
   done
 
 lemma lt_ack1: "[| i \<in> nat; j \<in> nat |] ==> i < ack(i,j)"
-  -- {* PROPERTY A 4'? Extra lemma needed for @{text CONST} case, constant functions. *}
+  -- {* PROPERTY A 4'? Extra lemma needed for @{text CONSTANT} case, constant functions. *}
   apply (induct_tac i)
    apply (simp add: nat_0_le)
   apply (erule lt_trans1 [OF succ_leI ack_lt_ack_succ1])
    apply auto
   done
 
-lemma CONST_case:
-    "[| l \<in> list(nat);  k \<in> nat |] ==> CONST(k) ` l < ack(k, list_add(l))"
-  by (simp add: CONST_def lt_ack1)
+lemma CONSTANT_case:
+    "[| l \<in> list(nat);  k \<in> nat |] ==> CONSTANT(k) ` l < ack(k, list_add(l))"
+  by (simp add: CONSTANT_def lt_ack1)
 
 lemma PROJ_case [rule_format]:
     "l \<in> list(nat) ==> \<forall>i \<in> nat. PROJ(i) ` l < ack(0, list_add(l))"
@@ -359,7 +359,7 @@
 lemma ack_bounds_prim_rec:
     "f \<in> prim_rec ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). f`l < ack(k, list_add(l))"
   apply (induct set: prim_rec)
-  apply (auto intro: SC_case CONST_case PROJ_case COMP_case PREC_case)
+  apply (auto intro: SC_case CONSTANT_case PROJ_case COMP_case PREC_case)
   done
 
 theorem ack_not_prim_rec: