--- 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"
--- 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: