# 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 \ PRIMREC" - CONST: "CONST k \ PRIMREC" + CONSTANT: "CONSTANT k \ PRIMREC" PROJ: "PROJ i \ PRIMREC" COMP: "g \ PRIMREC ==> fs \ lists PRIMREC ==> COMP g fs \ PRIMREC" PREC: "f \ PRIMREC ==> g \ PRIMREC ==> PREC f g \ 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 \ PRIMREC ==> \k. \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: "(\l. case l of [] => 0 | x # l' => ack (x, x)) \ 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 == \l \ list(nat). list_case(0, \x xs. succ(x), l)" - CONST :: "i=>i" - "CONST(k) == \l \ list(nat). k" + CONSTANT :: "i=>i" + "CONSTANT(k) == \l \ list(nat). k" PROJ :: "i=>i" "PROJ(i) == \l \ list(nat). list_case(0, \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 \ nat; l \ list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)" by (simp add: SC_def) -lemma CONST: "l \ list(nat) ==> CONST(k) ` l = k" - by (simp add: CONST_def) +lemma CONSTANT: "l \ list(nat) ==> CONSTANT(k) ` l = k" + by (simp add: CONSTANT_def) lemma PROJ_0: "[| x \ nat; l \ list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x" by (simp add: PROJ_def) @@ -83,12 +83,12 @@ domains prim_rec \ "list(nat)->nat" intros "SC \ prim_rec" - "k \ nat ==> CONST(k) \ prim_rec" + "k \ nat ==> CONSTANT(k) \ prim_rec" "i \ nat ==> PROJ(i) \ prim_rec" "[| g \ prim_rec; fs\list(prim_rec) |] ==> COMP(g,fs) \ prim_rec" "[| f \ prim_rec; g \ prim_rec |] ==> PREC(f,g) \ 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\nat; j\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 \ nat; j \ 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 \ list(nat); k \ nat |] ==> CONST(k) ` l < ack(k, list_add(l))" - by (simp add: CONST_def lt_ack1) +lemma CONSTANT_case: + "[| l \ list(nat); k \ nat |] ==> CONSTANT(k) ` l < ack(k, list_add(l))" + by (simp add: CONSTANT_def lt_ack1) lemma PROJ_case [rule_format]: "l \ list(nat) ==> \i \ nat. PROJ(i) ` l < ack(0, list_add(l))" @@ -359,7 +359,7 @@ lemma ack_bounds_prim_rec: "f \ prim_rec ==> \k \ nat. \l \ 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: