wneuper/isa: src/ZF/Induct/Primrec.thy@9bc16273c2d4

     1 (*  Title:      ZF/Induct/Primrec.thy

     2     ID:         $Id$

     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     4     Copyright   1994  University of Cambridge

     5 *)

     7 header {* Primitive Recursive Functions: the inductive definition *}

     9 theory Primrec imports Main begin

    11 text {*

    12   Proof adopted from \cite{szasz}.

    14   See also \cite[page 250, exercise 11]{mendelson}.

    15 *}

    18 subsection {* Basic definitions *}

    20 constdefs

    21   SC :: "i"

    22   "SC == \<lambda>l \<in> list(nat). list_case(0, \<lambda>x xs. succ(x), l)"

    24   CONST :: "i=>i"

    25   "CONST(k) == \<lambda>l \<in> list(nat). k"

    27   PROJ :: "i=>i"

    28   "PROJ(i) == \<lambda>l \<in> list(nat). list_case(0, \<lambda>x xs. x, drop(i,l))"

    30   COMP :: "[i,i]=>i"

    31   "COMP(g,fs) == \<lambda>l \<in> list(nat). g ` List.map(\<lambda>f. f`l, fs)"

    33   PREC :: "[i,i]=>i"

    34   "PREC(f,g) ==

    35      \<lambda>l \<in> list(nat). list_case(0,

    36                       \<lambda>x xs. rec(x, f`xs, \<lambda>y r. g ` Cons(r, Cons(y, xs))), l)"

    37   -- {* Note that @{text g} is applied first to @{term "PREC(f,g)`y"} and then to @{text y}! *}

    39 consts

    40   ACK :: "i=>i"

    41 primrec

    42   "ACK(0) = SC"

    43   "ACK(succ(i)) = PREC (CONST (ACK(i) ` [1]), COMP(ACK(i), [PROJ(0)]))"

    45 syntax

    46   ack :: "[i,i]=>i"

    47 translations

    48   "ack(x,y)" == "ACK(x) ` [y]"

    51 text {*

    52   \medskip Useful special cases of evaluation.

    53 *}

    55 lemma SC: "[| x \<in> nat;  l \<in> list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)"

    56   by (simp add: SC_def)

    58 lemma CONST: "l \<in> list(nat) ==> CONST(k) ` l = k"

    59   by (simp add: CONST_def)

    61 lemma PROJ_0: "[| x \<in> nat;  l \<in> list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x"

    62   by (simp add: PROJ_def)

    64 lemma COMP_1: "l \<in> list(nat) ==> COMP(g,[f]) ` l = g` [f`l]"

    65   by (simp add: COMP_def)

    67 lemma PREC_0: "l \<in> list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l"

    68   by (simp add: PREC_def)

    70 lemma PREC_succ:

    71   "[| x \<in> nat;  l \<in> list(nat) |]

    72     ==> PREC(f,g) ` (Cons(succ(x),l)) =

    73       g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))"

    74   by (simp add: PREC_def)

    77 subsection {* Inductive definition of the PR functions *}

    79 consts

    80   prim_rec :: i

    82 inductive

    83   domains prim_rec \<subseteq> "list(nat)->nat"

    84   intros

    85     "SC \<in> prim_rec"

    86     "k \<in> nat ==> CONST(k) \<in> prim_rec"

    87     "i \<in> nat ==> PROJ(i) \<in> prim_rec"

    88     "[| g \<in> prim_rec; fs\<in>list(prim_rec) |] ==> COMP(g,fs) \<in> prim_rec"

    89     "[| f \<in> prim_rec; g \<in> prim_rec |] ==> PREC(f,g) \<in> prim_rec"

    90   monos list_mono

    91   con_defs SC_def CONST_def PROJ_def COMP_def PREC_def

    92   type_intros nat_typechecks list.intros

    93     lam_type list_case_type drop_type List.map_type

    94     apply_type rec_type

    97 lemma prim_rec_into_fun [TC]: "c \<in> prim_rec ==> c \<in> list(nat) -> nat"

    98   by (erule subsetD [OF prim_rec.dom_subset])

   100 lemmas [TC] = apply_type [OF prim_rec_into_fun]

   102 declare prim_rec.intros [TC]

   103 declare nat_into_Ord [TC]

   104 declare rec_type [TC]

   106 lemma ACK_in_prim_rec [TC]: "i \<in> nat ==> ACK(i) \<in> prim_rec"

   107   by (induct_tac i) simp_all

   109 lemma ack_type [TC]: "[| i \<in> nat;  j \<in> nat |] ==>  ack(i,j) \<in> nat"

   110   by auto

   113 subsection {* Ackermann's function cases *}

   115 lemma ack_0: "j \<in> nat ==> ack(0,j) = succ(j)"

   116   -- {* PROPERTY A 1 *}

   117   by (simp add: SC)

   119 lemma ack_succ_0: "ack(succ(i), 0) = ack(i,1)"

   120   -- {* PROPERTY A 2 *}

   121   by (simp add: CONST PREC_0)

   123 lemma ack_succ_succ:

   124   "[| i\<in>nat;  j\<in>nat |] ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))"

   125   -- {* PROPERTY A 3 *}

   126   by (simp add: CONST PREC_succ COMP_1 PROJ_0)

   128 lemmas [simp] = ack_0 ack_succ_0 ack_succ_succ ack_type

   129   and [simp del] = ACK.simps

   132 lemma lt_ack2 [rule_format]: "i \<in> nat ==> \<forall>j \<in> nat. j < ack(i,j)"

   133   -- {* PROPERTY A 4 *}

   134   apply (induct_tac i)

   135    apply simp

   136   apply (rule ballI)

   137   apply (induct_tac j)

   138    apply (erule_tac [2] succ_leI [THEN lt_trans1])

   139    apply (rule nat_0I [THEN nat_0_le, THEN lt_trans])

   140    apply auto

   141   done

   143 lemma ack_lt_ack_succ2: "[|i\<in>nat; j\<in>nat|] ==> ack(i,j) < ack(i, succ(j))"

   144   -- {* PROPERTY A 5-, the single-step lemma *}

   145   by (induct_tac i) (simp_all add: lt_ack2)

   147 lemma ack_lt_mono2: "[| j<k; i \<in> nat; k \<in> nat |] ==> ack(i,j) < ack(i,k)"

   148   -- {* PROPERTY A 5, monotonicity for @{text "<"} *}

   149   apply (frule lt_nat_in_nat, assumption)

   150   apply (erule succ_lt_induct)

   151     apply assumption

   152    apply (rule_tac [2] lt_trans)

   153     apply (auto intro: ack_lt_ack_succ2)

   154   done

   156 lemma ack_le_mono2: "[|j\<le>k;  i\<in>nat;  k\<in>nat|] ==> ack(i,j) \<le> ack(i,k)"

   157   -- {* PROPERTY A 5', monotonicity for @{text \<le>} *}

   158   apply (rule_tac f = "\<lambda>j. ack (i,j) " in Ord_lt_mono_imp_le_mono)

   159      apply (assumption | rule ack_lt_mono2 ack_type [THEN nat_into_Ord])+

   160   done

   162 lemma ack2_le_ack1:

   163   "[| i\<in>nat;  j\<in>nat |] ==> ack(i, succ(j)) \<le> ack(succ(i), j)"

   164   -- {* PROPERTY A 6 *}

   165   apply (induct_tac j)

   166    apply simp_all

   167   apply (rule ack_le_mono2)

   168     apply (rule lt_ack2 [THEN succ_leI, THEN le_trans])

   169       apply auto

   170   done

   172 lemma ack_lt_ack_succ1: "[| i \<in> nat; j \<in> nat |] ==> ack(i,j) < ack(succ(i),j)"

   173   -- {* PROPERTY A 7-, the single-step lemma *}

   174   apply (rule ack_lt_mono2 [THEN lt_trans2])

   175      apply (rule_tac [4] ack2_le_ack1)

   176       apply auto

   177   done

   179 lemma ack_lt_mono1: "[| i<j; j \<in> nat; k \<in> nat |] ==> ack(i,k) < ack(j,k)"

   180   -- {* PROPERTY A 7, monotonicity for @{text "<"} *}

   181   apply (frule lt_nat_in_nat, assumption)

   182   apply (erule succ_lt_induct)

   183     apply assumption

   184    apply (rule_tac [2] lt_trans)

   185     apply (auto intro: ack_lt_ack_succ1)

   186   done

   188 lemma ack_le_mono1: "[| i\<le>j; j \<in> nat; k \<in> nat |] ==> ack(i,k) \<le> ack(j,k)"

   189   -- {* PROPERTY A 7', monotonicity for @{text \<le>} *}

   190   apply (rule_tac f = "\<lambda>j. ack (j,k) " in Ord_lt_mono_imp_le_mono)

   191      apply (assumption | rule ack_lt_mono1 ack_type [THEN nat_into_Ord])+

   192   done

   194 lemma ack_1: "j \<in> nat ==> ack(1,j) = succ(succ(j))"

   195   -- {* PROPERTY A 8 *}

   196   by (induct_tac j) simp_all

   198 lemma ack_2: "j \<in> nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))"

   199   -- {* PROPERTY A 9 *}

   200   by (induct_tac j) (simp_all add: ack_1)

   202 lemma ack_nest_bound:

   203   "[| i1 \<in> nat; i2 \<in> nat; j \<in> nat |]

   204     ==> ack(i1, ack(i2,j)) < ack(succ(succ(i1#+i2)), j)"

   205   -- {* PROPERTY A 10 *}

   206   apply (rule lt_trans2 [OF _ ack2_le_ack1])

   207     apply simp

   208     apply (rule add_le_self [THEN ack_le_mono1, THEN lt_trans1])

   209        apply auto

   210   apply (force intro: add_le_self2 [THEN ack_lt_mono1, THEN ack_lt_mono2])

   211   done

   213 lemma ack_add_bound:

   214   "[| i1 \<in> nat; i2 \<in> nat; j \<in> nat |]

   215     ==> ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)"

   216   -- {* PROPERTY A 11 *}

   217   apply (rule_tac j = "ack (succ (1), ack (i1 #+ i2, j))" in lt_trans)

   218    apply (simp add: ack_2)

   219    apply (rule_tac [2] ack_nest_bound [THEN lt_trans2])

   220       apply (rule add_le_mono [THEN leI, THEN leI])

   221          apply (auto intro: add_le_self add_le_self2 ack_le_mono1)

   222   done

   224 lemma ack_add_bound2:

   225      "[| i < ack(k,j);  j \<in> nat;  k \<in> nat |]

   226       ==> i#+j < ack(succ(succ(succ(succ(k)))), j)"

   227   -- {* PROPERTY A 12. *}

   228   -- {* Article uses existential quantifier but the ALF proof used @{term "k#+#4"}. *}

   229   -- {* Quantified version must be nested @{text "\<exists>k'. \<forall>i,j \<dots>"}. *}

   230   apply (rule_tac j = "ack (k,j) #+ ack (0,j) " in lt_trans)

   231    apply (rule_tac [2] ack_add_bound [THEN lt_trans2])

   232       apply (rule add_lt_mono)

   233          apply auto

   234   done

   237 subsection {* Main result *}

   239 declare list_add_type [simp]

   241 lemma SC_case: "l \<in> list(nat) ==> SC ` l < ack(1, list_add(l))"

   242   apply (unfold SC_def)

   243   apply (erule list.cases)

   244    apply (simp add: succ_iff)

   245   apply (simp add: ack_1 add_le_self)

   246   done

   248 lemma lt_ack1: "[| i \<in> nat; j \<in> nat |] ==> i < ack(i,j)"

   249   -- {* PROPERTY A 4'? Extra lemma needed for @{text CONST} case, constant functions. *}

   250   apply (induct_tac i)

   251    apply (simp add: nat_0_le)

   252   apply (erule lt_trans1 [OF succ_leI ack_lt_ack_succ1])

   253    apply auto

   254   done

   256 lemma CONST_case:

   257     "[| l \<in> list(nat);  k \<in> nat |] ==> CONST(k) ` l < ack(k, list_add(l))"

   258   by (simp add: CONST_def lt_ack1)

   260 lemma PROJ_case [rule_format]:

   261     "l \<in> list(nat) ==> \<forall>i \<in> nat. PROJ(i) ` l < ack(0, list_add(l))"

   262   apply (unfold PROJ_def)

   263   apply simp

   264   apply (erule list.induct)

   265    apply (simp add: nat_0_le)

   266   apply simp

   267   apply (rule ballI)

   268   apply (erule_tac n = i in natE)

   269    apply (simp add: add_le_self)

   270   apply simp

   271   apply (erule bspec [THEN lt_trans2])

   272    apply (rule_tac [2] add_le_self2 [THEN succ_leI])

   273    apply auto

   274   done

   276 text {*

   277   \medskip @{text COMP} case.

   278 *}

   280 lemma COMP_map_lemma:

   281   "fs \<in> list({f \<in> prim_rec. \<exists>kf \<in> nat. \<forall>l \<in> list(nat). f`l < ack(kf, list_add(l))})

   282     ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat).

   283       list_add(map(\<lambda>f. f ` l, fs)) < ack(k, list_add(l))"

   284   apply (erule list.induct)

   285    apply (rule_tac x = 0 in bexI)

   286     apply (simp_all add: lt_ack1 nat_0_le)

   287   apply clarify

   288   apply (rule ballI [THEN bexI])

   289   apply (rule add_lt_mono [THEN lt_trans])

   290        apply (rule_tac [5] ack_add_bound)

   291          apply blast

   292         apply auto

   293   done

   295 lemma COMP_case:

   296  "[| kg\<in>nat;

   297      \<forall>l \<in> list(nat). g`l < ack(kg, list_add(l));

   298      fs \<in> list({f \<in> prim_rec .

   299                  \<exists>kf \<in> nat. \<forall>l \<in> list(nat).

   300                         f`l < ack(kf, list_add(l))}) |]

   301    ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). COMP(g,fs)`l < ack(k, list_add(l))"

   302   apply (simp add: COMP_def)

   303   apply (frule list_CollectD)

   304   apply (erule COMP_map_lemma [THEN bexE])

   305   apply (rule ballI [THEN bexI])

   306    apply (erule bspec [THEN lt_trans])

   307     apply (rule_tac [2] lt_trans)

   308      apply (rule_tac [3] ack_nest_bound)

   309        apply (erule_tac [2] bspec [THEN ack_lt_mono2])

   310          apply auto

   311   done

   313 text {*

   314   \medskip @{text PREC} case.

   315 *}

   317 lemma PREC_case_lemma:

   318  "[| \<forall>l \<in> list(nat). f`l #+ list_add(l) < ack(kf, list_add(l));

   319      \<forall>l \<in> list(nat). g`l #+ list_add(l) < ack(kg, list_add(l));

   320      f \<in> prim_rec;  kf\<in>nat;

   321      g \<in> prim_rec;  kg\<in>nat;

   322      l \<in> list(nat) |]

   323   ==> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))"

   324   apply (unfold PREC_def)

   325   apply (erule list.cases)

   326    apply (simp add: lt_trans [OF nat_le_refl lt_ack2])

   327   apply simp

   328   apply (erule ssubst)  -- {* get rid of the needless assumption *}

   329   apply (induct_tac a)

   330    apply simp_all

   331    txt {* base case *}

   332    apply (rule lt_trans, erule bspec, assumption)

   333    apply (simp add: add_le_self [THEN ack_lt_mono1])

   334   txt {* ind step *}

   335   apply (rule succ_leI [THEN lt_trans1])

   336    apply (rule_tac j = "g ` ?ll #+ ?mm" in lt_trans1)

   337     apply (erule_tac [2] bspec)

   338     apply (rule nat_le_refl [THEN add_le_mono])

   339        apply typecheck

   340    apply (simp add: add_le_self2)

   341    txt {* final part of the simplification *}

   342   apply simp

   343   apply (rule add_le_self2 [THEN ack_le_mono1, THEN lt_trans1])

   344      apply (erule_tac [4] ack_lt_mono2)

   345       apply auto

   346   done

   348 lemma PREC_case:

   349    "[| f \<in> prim_rec;  kf\<in>nat;

   350        g \<in> prim_rec;  kg\<in>nat;

   351        \<forall>l \<in> list(nat). f`l < ack(kf, list_add(l));

   352        \<forall>l \<in> list(nat). g`l < ack(kg, list_add(l)) |]

   353     ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). PREC(f,g)`l< ack(k, list_add(l))"

   354   apply (rule ballI [THEN bexI])

   355    apply (rule lt_trans1 [OF add_le_self PREC_case_lemma])

   356           apply typecheck

   357      apply (blast intro: ack_add_bound2 list_add_type)+

   358   done

   360 lemma ack_bounds_prim_rec:

   361     "f \<in> prim_rec ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). f`l < ack(k, list_add(l))"

   362   apply (erule prim_rec.induct)

   363   apply (auto intro: SC_case CONST_case PROJ_case COMP_case PREC_case)

   364   done

   366 theorem ack_not_prim_rec:

   367     "(\<lambda>l \<in> list(nat). list_case(0, \<lambda>x xs. ack(x,x), l)) \<notin> prim_rec"

   368   apply (rule notI)

   369   apply (drule ack_bounds_prim_rec)

   370   apply force

   371   done

   373 end

author	haftmann
	Fri, 17 Jun 2005 16:12:49 +0200
changeset 16417	9bc16273c2d4
parent 13339	0f89104dd377
child 18415	eb68dc98bda2
permissions	-rw-r--r--