# HG changeset patch # User paulson # Date 914860371 -3600 # Node ID e0f9d930e9562d91bd8ffa331a4eee612bebc67e # Parent 3eecc7fbfad869a4b54082e0cbc80f0c5e7476fc Needs separate theory Primrec_defs due to new inductive defs package diff -r 3eecc7fbfad8 -r e0f9d930e956 src/ZF/ex/Primrec.ML --- a/src/ZF/ex/Primrec.ML Mon Dec 28 16:50:37 1998 +0100 +++ b/src/ZF/ex/Primrec.ML Mon Dec 28 16:52:51 1998 +0100 @@ -14,65 +14,23 @@ (Van Nostrand, 1964), page 250, exercise 11. *) -open Primrec; - -val pr_typechecks = - nat_typechecks @ list.intrs @ - [lam_type, list_case_type, drop_type, map_type, apply_type, rec_type]; - -(** Useful special cases of evaluation ***) - -simpset_ref() := simpset() setSolver (type_auto_tac pr_typechecks); - -Goalw [SC_def] - "[| x:nat; l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)"; -by (Asm_simp_tac 1); -qed "SC"; - -Goalw [CONST_def] - "[| l: list(nat) |] ==> CONST(k) ` l = k"; -by (Asm_simp_tac 1); -qed "CONST"; - -Goalw [PROJ_def] - "[| x: nat; l: list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x"; -by (Asm_simp_tac 1); -qed "PROJ_0"; - -Goalw [COMP_def] - "[| l: list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]"; -by (Asm_simp_tac 1); -qed "COMP_1"; - -Goalw [PREC_def] - "l: list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l"; -by (Asm_simp_tac 1); -qed "PREC_0"; - -Goalw [PREC_def] - "[| x:nat; l: list(nat) |] ==> \ -\ PREC(f,g) ` (Cons(succ(x),l)) = \ -\ g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))"; -by (Asm_simp_tac 1); -qed "PREC_succ"; - (*** Inductive definition of the PR functions ***) -(* c: primrec ==> c: list(nat) -> nat *) -val primrec_into_fun = primrec.dom_subset RS subsetD; +(* c: prim_rec ==> c: list(nat) -> nat *) +val prim_rec_into_fun = prim_rec.dom_subset RS subsetD; -simpset_ref() := simpset() setSolver (type_auto_tac ([primrec_into_fun] @ - pr_typechecks @ primrec.intrs)); +simpset_ref() := simpset() setSolver (type_auto_tac ([prim_rec_into_fun] @ + pr_typechecks @ prim_rec.intrs)); -Goalw [ACK_def] "i:nat ==> ACK(i): primrec"; +Goalw [ACK_def] "i:nat ==> ACK(i): prim_rec"; by (etac nat_induct 1); by (ALLGOALS Asm_simp_tac); -qed "ACK_in_primrec"; +qed "ACK_in_prim_rec"; val ack_typechecks = - [ACK_in_primrec, primrec_into_fun RS apply_type, + [ACK_in_prim_rec, prim_rec_into_fun RS apply_type, add_type, list_add_type, nat_into_Ord] @ - nat_typechecks @ list.intrs @ primrec.intrs; + nat_typechecks @ list.intrs @ prim_rec.intrs; (*strict typechecking for the Ackermann proof; instantiates no vars*) fun tc_tac rls = @@ -96,8 +54,6 @@ qed "ack_succ_0"; (*PROPERTY A 3*) -(*Could be proved in Primrec0, like the previous two cases, but using - primrec_into_fun makes type-checking easier!*) Goalw [ACK_def] "[| i:nat; j:nat |] ==> \ \ ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))"; @@ -257,7 +213,7 @@ (** COMP case **) -Goal "fs : list({f: primrec . \ +Goal "fs : list({f: prim_rec . \ \ EX kf:nat. ALL l:list(nat). \ \ f`l < ack(kf, list_add(l))}) \ \ ==> EX k:nat. ALL l: list(nat). \ @@ -278,7 +234,7 @@ Goalw [COMP_def] "[| kg: nat; \ \ ALL l:list(nat). g`l < ack(kg, list_add(l)); \ -\ fs : list({f: primrec . \ +\ fs : list({f: prim_rec . \ \ EX kf:nat. ALL l:list(nat). \ \ f`l < ack(kf, list_add(l))}) \ \ |] ==> EX k:nat. ALL l: list(nat). COMP(g,fs)`l < ack(k, list_add(l))"; @@ -298,8 +254,8 @@ Goalw [PREC_def] "[| ALL l:list(nat). f`l #+ list_add(l) < ack(kf, list_add(l)); \ \ ALL l:list(nat). g`l #+ list_add(l) < ack(kg, list_add(l)); \ -\ f: primrec; kf: nat; \ -\ g: primrec; kg: nat; \ +\ f: prim_rec; kf: nat; \ +\ g: prim_rec; kg: nat; \ \ l: list(nat) \ \ |] ==> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))"; by (etac list.elim 1); @@ -326,8 +282,8 @@ by (tc_tac []); qed "PREC_case_lemma"; -Goal "[| f: primrec; kf: nat; \ -\ g: primrec; kg: nat; \ +Goal "[| f: prim_rec; kf: nat; \ +\ g: prim_rec; kg: nat; \ \ ALL l:list(nat). f`l < ack(kf, list_add(l)); \ \ ALL l:list(nat). g`l < ack(kg, list_add(l)) \ \ |] ==> EX k:nat. ALL l: list(nat). PREC(f,g)`l< ack(k, list_add(l))"; @@ -340,20 +296,20 @@ rtac (ack_add_bound2 RS ballI) THEN' etac bspec]))); qed "PREC_case"; -Goal "f:primrec ==> EX k:nat. ALL l:list(nat). f`l < ack(k, list_add(l))"; -by (etac primrec.induct 1); +Goal "f:prim_rec ==> EX k:nat. ALL l:list(nat). f`l < ack(k, list_add(l))"; +by (etac prim_rec.induct 1); by Safe_tac; by (DEPTH_SOLVE (ares_tac ([SC_case, CONST_case, PROJ_case, COMP_case, PREC_case, bexI, ballI] @ nat_typechecks) 1)); -qed "ack_bounds_primrec"; +qed "ack_bounds_prim_rec"; -Goal "~ (lam l:list(nat). list_case(0, %x xs. ack(x,x), l)) : primrec"; +Goal "~ (lam l:list(nat). list_case(0, %x xs. ack(x,x), l)) : prim_rec"; by (rtac notI 1); -by (etac (ack_bounds_primrec RS bexE) 1); +by (etac (ack_bounds_prim_rec RS bexE) 1); by (rtac lt_irrefl 1); by (dres_inst_tac [("x", "[x]")] bspec 1); by (Asm_simp_tac 1); -by (asm_full_simp_tac (simpset() addsimps [add_0_right]) 1); -qed "ack_not_primrec"; +by (Asm_full_simp_tac 1); +qed "ack_not_prim_rec"; diff -r 3eecc7fbfad8 -r e0f9d930e956 src/ZF/ex/Primrec.thy --- a/src/ZF/ex/Primrec.thy Mon Dec 28 16:50:37 1998 +0100 +++ b/src/ZF/ex/Primrec.thy Mon Dec 28 16:52:51 1998 +0100 @@ -3,7 +3,7 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge -Primitive Recursive Functions +Primitive Recursive Functions: the inductive definition Proof adopted from Nora Szasz, @@ -14,49 +14,20 @@ (Van Nostrand, 1964), page 250, exercise 11. *) -Primrec = List + +Primrec = Primrec_defs + consts - primrec :: i - SC :: i - CONST :: i=>i - PROJ :: i=>i - COMP :: [i,i]=>i - PREC :: [i,i]=>i - ACK :: i=>i - ack :: [i,i]=>i - -translations - "ack(x,y)" == "ACK(x) ` [y]" - -defs - - SC_def "SC == lam l:list(nat).list_case(0, %x xs. succ(x), l)" - - CONST_def "CONST(k) == lam l:list(nat).k" - - PROJ_def "PROJ(i) == lam l:list(nat). list_case(0, %x xs. x, drop(i,l))" - - COMP_def "COMP(g,fs) == lam l:list(nat). g ` map(%f. f`l, fs)" - - (*Note that g is applied first to PREC(f,g)`y and then to y!*) - PREC_def "PREC(f,g) == - lam l:list(nat). list_case(0, - %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)" - - ACK_def "ACK(i) == rec(i, SC, - %z r. PREC (CONST (r`[1]), COMP(r,[PROJ(0)])))" - + prim_rec :: i inductive - domains "primrec" <= "list(nat)->nat" + domains "prim_rec" <= "list(nat)->nat" intrs - SC "SC : primrec" - CONST "k: nat ==> CONST(k) : primrec" - PROJ "i: nat ==> PROJ(i) : primrec" - COMP "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec" - PREC "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec" + SC "SC : prim_rec" + CONST "k: nat ==> CONST(k) : prim_rec" + PROJ "i: nat ==> PROJ(i) : prim_rec" + COMP "[| g: prim_rec; fs: list(prim_rec) |] ==> COMP(g,fs): prim_rec" + PREC "[| 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, CONST_def, PROJ_def, COMP_def, PREC_def]" type_intrs "nat_typechecks @ list.intrs @ [lam_type, list_case_type, drop_type, map_type, apply_type, rec_type]" diff -r 3eecc7fbfad8 -r e0f9d930e956 src/ZF/ex/Primrec_defs.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/ex/Primrec_defs.ML Mon Dec 28 16:52:51 1998 +0100 @@ -0,0 +1,52 @@ +(* Title: ZF/ex/Primrec + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Primitive Recursive Functions: preliminary definitions +*) + +(*Theory TF redeclares map_type*) +val map_type = Context.thm "List.map_type"; + +val pr_typechecks = + nat_typechecks @ list.intrs @ + [lam_type, list_case_type, drop_type, map_type, + apply_type, rec_type]; + +(** Useful special cases of evaluation ***) + +simpset_ref() := simpset() setSolver (type_auto_tac pr_typechecks); + +Goalw [SC_def] + "[| x:nat; l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)"; +by (Asm_simp_tac 1); +qed "SC"; + +Goalw [CONST_def] + "[| l: list(nat) |] ==> CONST(k) ` l = k"; +by (Asm_simp_tac 1); +qed "CONST"; + +Goalw [PROJ_def] + "[| x: nat; l: list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x"; +by (Asm_simp_tac 1); +qed "PROJ_0"; + +Goalw [COMP_def] + "[| l: list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]"; +by (Asm_simp_tac 1); +qed "COMP_1"; + +Goalw [PREC_def] + "l: list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l"; +by (Asm_simp_tac 1); +qed "PREC_0"; + +Goalw [PREC_def] + "[| x:nat; l: list(nat) |] ==> \ +\ PREC(f,g) ` (Cons(succ(x),l)) = \ +\ g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))"; +by (Asm_simp_tac 1); +qed "PREC_succ"; + diff -r 3eecc7fbfad8 -r e0f9d930e956 src/ZF/ex/Primrec_defs.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/ex/Primrec_defs.thy Mon Dec 28 16:52:51 1998 +0100 @@ -0,0 +1,45 @@ +(* Title: ZF/ex/Primrec_defs.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Primitive Recursive Functions: preliminary definitions of the constructors + +[These must reside in a separate theory in order to be visible in the + con_defs part of prim_rec's inductive definition.] +*) + +Primrec_defs = Main + + +consts + SC :: i + CONST :: i=>i + PROJ :: i=>i + COMP :: [i,i]=>i + PREC :: [i,i]=>i + ACK :: i=>i + ack :: [i,i]=>i + +translations + "ack(x,y)" == "ACK(x) ` [y]" + +defs + + SC_def "SC == lam l:list(nat).list_case(0, %x xs. succ(x), l)" + + CONST_def "CONST(k) == lam l:list(nat).k" + + PROJ_def "PROJ(i) == lam l:list(nat). list_case(0, %x xs. x, drop(i,l))" + + COMP_def "COMP(g,fs) == lam l:list(nat). g ` List.map(%f. f`l, fs)" + + (*Note that g is applied first to PREC(f,g)`y and then to y!*) + PREC_def "PREC(f,g) == + lam l:list(nat). list_case(0, + %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)" + + ACK_def "ACK(i) == rec(i, SC, + %z r. PREC (CONST (r`[1]), COMP(r,[PROJ(0)])))" + + +end