24584

1 
(* Title: FOLP/ex/Nat.ML

0

2 
ID: $Id$

1459

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

4 
Copyright 1992 University of Cambridge


5 
*)


6 

5061

7 
Goal "?p : ~ (Suc(k) = k)";

0

8 
by (res_inst_tac [("n","k")] induct 1);


9 
by (rtac notI 1);


10 
by (etac Suc_neq_0 1);


11 
by (rtac notI 1);


12 
by (etac notE 1);


13 
by (etac Suc_inject 1);


14 
val Suc_n_not_n = result();


15 


16 

5061

17 
Goal "?p : (k+m)+n = k+(m+n)";

0

18 
prths ([induct] RL [topthm()]); (*prints all 14 next states!*)


19 
by (rtac induct 1);


20 
back();


21 
back();


22 
back();


23 
back();


24 
back();


25 
back();


26 

5061

27 
Goalw [add_def] "?p : 0+n = n";

0

28 
by (rtac rec_0 1);


29 
val add_0 = result();


30 

5061

31 
Goalw [add_def] "?p : Suc(m)+n = Suc(m+n)";

0

32 
by (rtac rec_Suc 1);


33 
val add_Suc = result();


34 


35 
(*

17480

36 
val nat_congs = mk_congs (the_context ()) ["Suc", "op +"];

0

37 
prths nat_congs;


38 
*)

17480

39 
val prems = goal (the_context ()) "p: x=y ==> ?p : Suc(x) = Suc(y)";

0

40 
by (resolve_tac (prems RL [subst]) 1);


41 
by (rtac refl 1);


42 
val Suc_cong = result();


43 

17480

44 
val prems = goal (the_context ()) "[ p : a=x; q: b=y ] ==> ?p : a+b=x+y";


45 
by (resolve_tac (prems RL [subst]) 1 THEN resolve_tac (prems RL [subst]) 1 THEN

0

46 
rtac refl 1);


47 
val Plus_cong = result();


48 


49 
val nat_congs = [Suc_cong,Plus_cong];


50 


51 

17480

52 
val add_ss = FOLP_ss addcongs nat_congs

1459

53 
addrews [add_0, add_Suc];

0

54 

5061

55 
Goal "?p : (k+m)+n = k+(m+n)";

0

56 
by (res_inst_tac [("n","k")] induct 1);


57 
by (SIMP_TAC add_ss 1);


58 
by (ASM_SIMP_TAC add_ss 1);


59 
val add_assoc = result();


60 

5061

61 
Goal "?p : m+0 = m";

0

62 
by (res_inst_tac [("n","m")] induct 1);


63 
by (SIMP_TAC add_ss 1);


64 
by (ASM_SIMP_TAC add_ss 1);


65 
val add_0_right = result();


66 

5061

67 
Goal "?p : m+Suc(n) = Suc(m+n)";

0

68 
by (res_inst_tac [("n","m")] induct 1);


69 
by (ALLGOALS (ASM_SIMP_TAC add_ss));


70 
val add_Suc_right = result();


71 


72 
(*mk_typed_congs appears not to work with FOLP's version of subst*)
