<commit_before>(*  Title:      HOL/ex/Primrec
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1997  University of Cambridge

Primitive Recursive Functions

Proof adopted from
<NAME>, 
A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.

See also <NAME>, Introduction to Mathematical Logic.
(Van Nostrand, 1964), page 250, exercise 11.
*)


(** Useful special cases of evaluation ***)

Goalw [SC_def] "SC (x#l) = Suc x";
by (Asm_simp_tac 1);
qed "SC";

Goalw [CONST_def] "CONST k l = k";
by (Asm_simp_tac 1);
qed "CONST";

Goalw [PROJ_def] "PROJ(0) (x#l) = x";
by (Asm_simp_tac 1);
qed "PROJ_0";

Goalw [COMP_def] "COMP g [f] l = g [f l]";
by (Asm_simp_tac 1);
qed "COMP_1";

Goalw [PREC_def] "PREC f g (0#l) = f l";
by (Asm_simp_tac 1);
qed "PREC_0";

Goalw [PREC_def] "PREC f g (Suc x # l) = g (PREC f g (x#l) # x # l)";
by (Asm_simp_tac 1);
qed "PREC_Suc";

Addsimps [SC, CONST, PROJ_0, COMP_1, PREC_0, PREC_Suc];


(*PROPERTY A 4*)
Goal "j < ack(i,j)";
by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "less_ack2";

AddIffs [less_ack2];

(*PROPERTY A 5-, the single-step lemma*)
Goal "ack(i,j) < ack(i, Suc(j))";
by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "ack_less_ack_Suc2";

AddIffs [ack_less_ack_Suc2];

(*PROPERTY A 5, monotonicity for < *)
Goal "j<k --> ack(i,j) < ack(i,k)";
by (res_inst_tac [("u","i"),("v","k")] ack.induct 1);
by (ALLGOALS Asm_simp_tac);
by (blast_tac (claset() addSEs [less_SucE] addIs [less_trans]) 1);
qed_spec_mp "ack_less_mono2";

(*PROPERTY A 5', monotonicity for<=*)
Goal "j<=k ==> ack(i,j)<=ack(i,k)";
by (full_simp_tac (simpset() addsimps [order_le_less]) 1);
by (blast_tac (claset() addIs [ack_less_mono2]) 1);
qed "ack_le_mono2";

(*PROPERTY A 6*)
Goal "ack(i, Suc(j)) <= ack(Suc(i), j)";
by (induct_tac "j" 1);
by (ALLGOALS Asm_simp_tac);
by (blast_tac (claset() addIs [ack_le_mono2, less_ack2 RS Suc_leI, 
			      le_trans]) 1);
qed "ack2_le_ack1";

AddIffs [ack2_le_ack1];

(*PROPERTY A 7-, the single-step lemma*)
Goal "ack(i,j) < ack(Suc(i),j)";
by (blast_tac (claset() addIs [ack_less_mono2, less_le_trans]) 1);
qed "ack_less_ack_Suc1";

AddIffs [ack_less_ack_Suc1];

(*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*)
Goal "i < ack(i,j)";
by (induct_tac "i" 1);
by (ALLGOALS Asm_simp_tac);
by (blast_tac (claset() addIs [Suc_leI, le_less_trans]) 1);
qed "less_ack1";
AddIffs [less_ack1];

(*PROPERTY A 8*)
Goal "ack(1,j) = j + #2";
by (induct_tac "j" 1);
by (ALLGOALS Asm_simp_tac);
qed "ack_1";
Addsimps [ack_1];

(*PROPERTY A 9.  The unary 1 and 2 in ack is essential for the rewriting.*)
Goal "ack(2,j) = #2*j + #3";
by (induct_tac "j" 1);
by (ALLGOALS Asm_simp_tac);
qed "ack_2";
Addsimps [ack_2];


(*PROPERTY A 7, monotonicity for < [not clear why ack_1 is now needed first!]*)
Goal "ack(i,k) < ack(Suc(i+i'),k)";
by (res_inst_tac [("u","i"),("v","k")] ack.induct 1);
by (ALLGOALS Asm_full_simp_tac);
by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 2);
by (res_inst_tac [("u","i'"),("v","n")] ack.induct 1);
by (ALLGOALS Asm_simp_tac);
by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 1);
by (blast_tac (claset() addIs [Suc_leI RS le_less_trans, ack_less_mono2]) 1);
val lemma = result();

Goal "i<j ==> ack(i,k) < ack(j,k)";
by (dtac less_eq_Suc_add 1);
by (blast_tac (claset() addSIs [lemma]) 1);
qed "ack_less_mono1";

(*PROPERTY A 7', monotonicity for<=*)
Goal "i<=j ==> ack(i,k)<=ack(j,k)";
by (full_simp_tac (simpset() addsimps [order_le_less]) 1);
by (blast_tac (claset() addIs [ack_less_mono1]) 1);
qed "ack_le_mono1";

(*PROPERTY A 10*)
Goal "ack(i1, ack(i2,j)) < ack(#2 + (i1+i2), j)";
by (simp_tac numeral_ss 1);
by (rtac (ack2_le_ack1 RSN (2,less_le_trans)) 1);
by (Asm_simp_tac 1);
by (rtac (le_add1 RS ack_le_mono1 RS le_less_trans) 1);
by (rtac (ack_less_mono1 RS ack_less_mono2) 1);
by (simp_tac (simpset() addsimps [le_imp_less_Suc, le_add2]) 1);
qed "ack_nest_bound";

(*PROPERTY A 11*)
Goal "ack(i1,j) + ack(i2,j) < ack(#4 + (i1 + i2), j)";
by (res_inst_tac [("j", "ack(2, ack(i1 + i2, j))")] less_trans 1);
by (Asm_simp_tac 1);
by (rtac (ack_nest_bound RS less_le_trans) 2);
by (Asm_simp_tac 2);
by (cut_inst_tac [("i","i1"), ("m1","i2"), ("k","j")] 
    (le_add1 RS ack_le_mono1) 1);
by (cut_inst_tac [("i","i2"), ("m1","i1"), ("k","j")] 
    (le_add2 RS ack_le_mono1) 1);<commit_msg>changed to cope with the rewriting of #2+n to Suc(Suc n)<commit_after>(*  Title:      HOL/ex/Primrec
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1997  University of Cambridge

Primitive Recursive Functions

Proof adopted from
Nora Szasz, 
A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.

See also E. Mendelson, Introduction to Mathematical Logic.
(Van Nostrand, 1964), page 250, exercise 11.
*)


(** Useful special cases of evaluation ***)

Goalw [SC_def] "SC (x#l) = Suc x";
by (Asm_simp_tac 1);
qed "SC";

Goalw [CONST_def] "CONST k l = k";
by (Asm_simp_tac 1);
qed "CONST";

Goalw [PROJ_def] "PROJ(0) (x#l) = x";
by (Asm_simp_tac 1);
qed "PROJ_0";

Goalw [COMP_def] "COMP g [f] l = g [f l]";
by (Asm_simp_tac 1);
qed "COMP_1";

Goalw [PREC_def] "PREC f g (0#l) = f l";
by (Asm_simp_tac 1);
qed "PREC_0";

Goalw [PREC_def] "PREC f g (Suc x # l) = g (PREC f g (x#l) # x # l)";
by (Asm_simp_tac 1);
qed "PREC_Suc";

Addsimps [SC, CONST, PROJ_0, COMP_1, PREC_0, PREC_Suc];


(*PROPERTY A 4*)
Goal "j < ack(i,j)";
by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "less_ack2";

AddIffs [less_ack2];

(*PROPERTY A 5-, the single-step lemma*)
Goal "ack(i,j) < ack(i, Suc(j))";
by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "ack_less_ack_Suc2";

AddIffs [ack_less_ack_Suc2];

(*PROPERTY A 5, monotonicity for < *)
Goal "j<k --> ack(i,j) < ack(i,k)";
by (res_inst_tac [("u","i"),("v","k")] ack.induct 1);
by (ALLGOALS Asm_simp_tac);
by (blast_tac (claset() addSEs [less_SucE] addIs [less_trans]) 1);
qed_spec_mp "ack_less_mono2";

(*PROPERTY A 5', monotonicity for<=*)
Goal "j<=k ==> ack(i,j)<=ack(i,k)";
by (full_simp_tac (simpset() addsimps [order_le_less]) 1);
by (blast_tac (claset() addIs [ack_less_mono2]) 1);
qed "ack_le_mono2";

(*PROPERTY A 6*)
Goal "ack(i, Suc(j)) <= ack(Suc(i), j)";
by (induct_tac "j" 1);
by (ALLGOALS Asm_simp_tac);
by (blast_tac (claset() addIs [ack_le_mono2, less_ack2 RS Suc_leI, 
			      le_trans]) 1);
qed "ack2_le_ack1";

AddIffs [ack2_le_ack1];

(*PROPERTY A 7-, the single-step lemma*)
Goal "ack(i,j) < ack(Suc(i),j)";
by (blast_tac (claset() addIs [ack_less_mono2, less_le_trans]) 1);
qed "ack_less_ack_Suc1";

AddIffs [ack_less_ack_Suc1];

(*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*)
Goal "i < ack(i,j)";
by (induct_tac "i" 1);
by (ALLGOALS Asm_simp_tac);
by (blast_tac (claset() addIs [Suc_leI, le_less_trans]) 1);
qed "less_ack1";
AddIffs [less_ack1];

(*PROPERTY A 8*)
Goal "ack(1,j) = j + #2";
by (induct_tac "j" 1);
by (ALLGOALS Asm_simp_tac);
qed "ack_1";
Addsimps [ack_1];

(*PROPERTY A 9.  The unary 1 and 2 in ack is essential for the rewriting.*)
Goal "ack(2,j) = #2*j + #3";
by (induct_tac "j" 1);
by (ALLGOALS Asm_simp_tac);
qed "ack_2";
Addsimps [ack_2];


(*PROPERTY A 7, monotonicity for < [not clear why ack_1 is now needed first!]*)
Goal "ack(i,k) < ack(Suc(i+i'),k)";
by (res_inst_tac [("u","i"),("v","k")] ack.induct 1);
by (ALLGOALS Asm_full_simp_tac);
by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 2);
by (res_inst_tac [("u","i'"),("v","n")] ack.induct 1);
by (ALLGOALS Asm_simp_tac);
by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 1);
by (blast_tac (claset() addIs [Suc_leI RS le_less_trans, ack_less_mono2]) 1);
val lemma = result();

Goal "i<j ==> ack(i,k) < ack(j,k)";
by (dtac less_eq_Suc_add 1);
by (blast_tac (claset() addSIs [lemma]) 1);
qed "ack_less_mono1";

(*PROPERTY A 7', monotonicity for<=*)
Goal "i<=j ==> ack(i,k)<=ack(j,k)";
by (full_simp_tac (simpset() addsimps [order_le_less]) 1);
by (blast_tac (claset() addIs [ack_less_mono1]) 1);
qed "ack_le_mono1";

(*PROPERTY A 10*)
Goal "ack(i1, ack(i2,j)) < ack(#2 + (i1+i2), j)";
by (simp_tac numeral_ss 1);
by (rtac (ack2_le_ack1 RSN (2,less_le_trans)) 1);
by (Asm_simp_tac 1);
by (rtac (le_add1 RS ack_le_mono1 RS le_less_trans) 1);
by (rtac (ack_less_mono1 RS ack_less_mono2) 1);
by (simp_tac (simpset() addsimps [le_imp_less_Suc, le_add2]) 1);
qed "ack_nest_bound";

(*PROPERTY A 11*)
Goal "ack(i1,j) + ack(i2,j) < ack(#4 + (i1 + i2), j)";
by (res_inst_tac [("j", "ack(2, ack(i1 + i2, j))")] less_trans 1);
by (Asm_simp_tac 1);
by (rtac (ack_nest_bound RS less_le_trans) 2);
by (asm_simp_tac (simpset() addsimps [Suc3_eq_add_3]) 2);
by (cut_inst_tac [("i","i1"), ("m1","i2"), ("k","j")] 
    (le_add1 RS ack_le_mono1) 1);
by (cut_inst_tac [("i","i2"), ("m1","i1"), ("k","j")] 
    (le_add2 RS ack_le_mono1) 1);
{'fraction_non_alphanumeric': 0.1918960244648318, 'fraction_numerical': 0.0337483617300131, 'mean_word_length': 5.44405348346235, 'pattern_counts': {'":': 0, '<': 47, '<?xml version=': 0, '>': 15, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6848714', 'n_tokens_mistral': 4684, 'n_tokens_neox': 4435, 'n_words': 1126}