src/ZF/Induct/Primrec.thy
changeset 19676 187234ec6050
parent 18415 eb68dc98bda2
child 20503 503ac4c5ef91
     1.1 --- a/src/ZF/Induct/Primrec.thy	Wed May 17 12:28:47 2006 +0200
     1.2 +++ b/src/ZF/Induct/Primrec.thy	Wed May 17 22:34:44 2006 +0200
     1.3 @@ -21,8 +21,8 @@
     1.4    SC :: "i"
     1.5    "SC == \<lambda>l \<in> list(nat). list_case(0, \<lambda>x xs. succ(x), l)"
     1.6  
     1.7 -  CONST :: "i=>i"
     1.8 -  "CONST(k) == \<lambda>l \<in> list(nat). k"
     1.9 +  CONSTANT :: "i=>i"
    1.10 +  "CONSTANT(k) == \<lambda>l \<in> list(nat). k"
    1.11  
    1.12    PROJ :: "i=>i"
    1.13    "PROJ(i) == \<lambda>l \<in> list(nat). list_case(0, \<lambda>x xs. x, drop(i,l))"
    1.14 @@ -40,7 +40,7 @@
    1.15    ACK :: "i=>i"
    1.16  primrec
    1.17    "ACK(0) = SC"
    1.18 -  "ACK(succ(i)) = PREC (CONST (ACK(i) ` [1]), COMP(ACK(i), [PROJ(0)]))"
    1.19 +  "ACK(succ(i)) = PREC (CONSTANT (ACK(i) ` [1]), COMP(ACK(i), [PROJ(0)]))"
    1.20  
    1.21  syntax
    1.22    ack :: "[i,i]=>i"
    1.23 @@ -55,8 +55,8 @@
    1.24  lemma SC: "[| x \<in> nat;  l \<in> list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)"
    1.25    by (simp add: SC_def)
    1.26  
    1.27 -lemma CONST: "l \<in> list(nat) ==> CONST(k) ` l = k"
    1.28 -  by (simp add: CONST_def)
    1.29 +lemma CONSTANT: "l \<in> list(nat) ==> CONSTANT(k) ` l = k"
    1.30 +  by (simp add: CONSTANT_def)
    1.31  
    1.32  lemma PROJ_0: "[| x \<in> nat;  l \<in> list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x"
    1.33    by (simp add: PROJ_def)
    1.34 @@ -83,12 +83,12 @@
    1.35    domains prim_rec \<subseteq> "list(nat)->nat"
    1.36    intros
    1.37      "SC \<in> prim_rec"
    1.38 -    "k \<in> nat ==> CONST(k) \<in> prim_rec"
    1.39 +    "k \<in> nat ==> CONSTANT(k) \<in> prim_rec"
    1.40      "i \<in> nat ==> PROJ(i) \<in> prim_rec"
    1.41      "[| g \<in> prim_rec; fs\<in>list(prim_rec) |] ==> COMP(g,fs) \<in> prim_rec"
    1.42      "[| f \<in> prim_rec; g \<in> prim_rec |] ==> PREC(f,g) \<in> prim_rec"
    1.43    monos list_mono
    1.44 -  con_defs SC_def CONST_def PROJ_def COMP_def PREC_def
    1.45 +  con_defs SC_def CONSTANT_def PROJ_def COMP_def PREC_def
    1.46    type_intros nat_typechecks list.intros
    1.47      lam_type list_case_type drop_type List.map_type
    1.48      apply_type rec_type
    1.49 @@ -118,12 +118,12 @@
    1.50  
    1.51  lemma ack_succ_0: "ack(succ(i), 0) = ack(i,1)"
    1.52    -- {* PROPERTY A 2 *}
    1.53 -  by (simp add: CONST PREC_0)
    1.54 +  by (simp add: CONSTANT PREC_0)
    1.55  
    1.56  lemma ack_succ_succ:
    1.57    "[| i\<in>nat;  j\<in>nat |] ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))"
    1.58    -- {* PROPERTY A 3 *}
    1.59 -  by (simp add: CONST PREC_succ COMP_1 PROJ_0)
    1.60 +  by (simp add: CONSTANT PREC_succ COMP_1 PROJ_0)
    1.61  
    1.62  lemmas [simp] = ack_0 ack_succ_0 ack_succ_succ ack_type
    1.63    and [simp del] = ACK.simps
    1.64 @@ -245,16 +245,16 @@
    1.65    done
    1.66  
    1.67  lemma lt_ack1: "[| i \<in> nat; j \<in> nat |] ==> i < ack(i,j)"
    1.68 -  -- {* PROPERTY A 4'? Extra lemma needed for @{text CONST} case, constant functions. *}
    1.69 +  -- {* PROPERTY A 4'? Extra lemma needed for @{text CONSTANT} case, constant functions. *}
    1.70    apply (induct_tac i)
    1.71     apply (simp add: nat_0_le)
    1.72    apply (erule lt_trans1 [OF succ_leI ack_lt_ack_succ1])
    1.73     apply auto
    1.74    done
    1.75  
    1.76 -lemma CONST_case:
    1.77 -    "[| l \<in> list(nat);  k \<in> nat |] ==> CONST(k) ` l < ack(k, list_add(l))"
    1.78 -  by (simp add: CONST_def lt_ack1)
    1.79 +lemma CONSTANT_case:
    1.80 +    "[| l \<in> list(nat);  k \<in> nat |] ==> CONSTANT(k) ` l < ack(k, list_add(l))"
    1.81 +  by (simp add: CONSTANT_def lt_ack1)
    1.82  
    1.83  lemma PROJ_case [rule_format]:
    1.84      "l \<in> list(nat) ==> \<forall>i \<in> nat. PROJ(i) ` l < ack(0, list_add(l))"
    1.85 @@ -359,7 +359,7 @@
    1.86  lemma ack_bounds_prim_rec:
    1.87      "f \<in> prim_rec ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). f`l < ack(k, list_add(l))"
    1.88    apply (induct set: prim_rec)
    1.89 -  apply (auto intro: SC_case CONST_case PROJ_case COMP_case PREC_case)
    1.90 +  apply (auto intro: SC_case CONSTANT_case PROJ_case COMP_case PREC_case)
    1.91    done
    1.92  
    1.93  theorem ack_not_prim_rec: