Replaced nat_ind_tac by induct_tac.
authorberghofe
Mon Aug 05 14:32:56 2002 +0200 (2002-08-05)
changeset 1345401e2496dee05
parent 13453 af96f2568406
child 13455 f88a91ff8ac6
Replaced nat_ind_tac by induct_tac.
src/HOLCF/FOCUS/Buffer.ML
src/HOLCF/FOCUS/Buffer_adm.ML
src/HOLCF/FOCUS/Stream_adm.ML
src/HOLCF/domain/theorems.ML
src/HOLCF/ex/Dagstuhl.ML
src/HOLCF/ex/Hoare.ML
src/HOLCF/ex/Loop.ML
src/HOLCF/ex/Stream.ML
     1.1 --- a/src/HOLCF/FOCUS/Buffer.ML	Mon Aug 05 14:30:06 2002 +0200
     1.2 +++ b/src/HOLCF/FOCUS/Buffer.ML	Mon Aug 05 14:32:56 2002 +0200
     1.3 @@ -160,7 +160,7 @@
     1.4  
     1.5  Goal "\\<forall>s f ff. f\\<in>BufEq \\<longrightarrow> ff\\<in>BufEq \\<longrightarrow> \
     1.6  \ s\\<in>BufAC_Asm \\<longrightarrow> stream_take n\\<cdot>(f\\<cdot>s) = stream_take n\\<cdot>(ff\\<cdot>s)";
     1.7 -by (nat_ind_tac "n" 1);
     1.8 +by (induct_tac "n" 1);
     1.9  by  (Simp_tac 1);
    1.10  by (strip_tac 1);
    1.11  by (dtac (BufAC_Asm_unfold RS iffD1) 1);
     2.1 --- a/src/HOLCF/FOCUS/Buffer_adm.ML	Mon Aug 05 14:30:06 2002 +0200
     2.2 +++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Mon Aug 05 14:32:56 2002 +0200
     2.3 @@ -112,7 +112,7 @@
     2.4  		\    (s,f\\<cdot>s):down_iterate BufAC_Cmt_F i";
     2.5  by (res_inst_tac [("x","%i. 2*i")] exI 1);
     2.6  by (rtac allI 1);
     2.7 -by (nat_ind_tac "i" 1);
     2.8 +by (induct_tac "i" 1);
     2.9  by ( Simp_tac 1);
    2.10  by (simp_tac (simpset() addsimps [add_commute]) 1);
    2.11  by (strip_tac 1);
     3.1 --- a/src/HOLCF/FOCUS/Stream_adm.ML	Mon Aug 05 14:30:06 2002 +0200
     3.2 +++ b/src/HOLCF/FOCUS/Stream_adm.ML	Mon Aug 05 14:32:56 2002 +0200
     3.3 @@ -60,7 +60,7 @@
     3.4  \ Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i";
     3.5  by (safe_tac HOL_cs);
     3.6  by (res_inst_tac [("x","i*ia")] exI 1);
     3.7 -by (nat_ind_tac "ia" 1);
     3.8 +by (induct_tac "ia" 1);
     3.9  by ( Simp_tac 1);
    3.10  by (Simp_tac 1);
    3.11  by (strip_tac 1);
    3.12 @@ -109,13 +109,13 @@
    3.13  "!!X. [|stream_antiP (F::(('a::flat stream)set => ('a stream set)))|]\
    3.14  \ ==> !i x y. x << y --> y:down_iterate F i --> x:down_iterate F i" (K [
    3.15  	rtac allI 1,
    3.16 -	nat_ind_tac "i" 1,
    3.17 +	induct_tac "i" 1,
    3.18  	 Simp_tac 1,
    3.19  	Simp_tac 1,
    3.20  	strip_tac 1,
    3.21  	etac allE 1 THEN etac all_dupE 1 THEN etac exE 1 THEN etac exE 1,
    3.22  	etac conjE 1,
    3.23 -	case_tac "#x < Fin ia" 1,
    3.24 +	case_tac "#x < Fin i" 1,
    3.25  	 fast_tac HOL_cs 1,
    3.26  	fold_goals_tac [thm "ile_def"],
    3.27  	mp_tac 1,
     4.1 --- a/src/HOLCF/domain/theorems.ML	Mon Aug 05 14:30:06 2002 +0200
     4.2 +++ b/src/HOLCF/domain/theorems.ML	Mon Aug 05 14:32:56 2002 +0200
     4.3 @@ -371,7 +371,7 @@
     4.4    val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
     4.5    val take_stricts=pg copy_take_defs(mk_trp(foldr' mk_conj(map(fn((dn,args),_)=>
     4.6              strict(dc_take dn $ %:"n")) eqs))) ([
     4.7 -                        nat_ind_tac "n" 1,
     4.8 +                        induct_tac "n" 1,
     4.9                           simp_tac iterate_Cprod_ss 1,
    4.10                          asm_simp_tac (iterate_Cprod_ss addsimps copy_rews)1]);
    4.11    val take_stricts' = rewrite_rule copy_take_defs take_stricts;
    4.12 @@ -385,7 +385,7 @@
    4.13           con_app2 con (app_rec_arg (fn n=>dc_take (nth_elem(n,dnames))$ %:"n"))
    4.14                                args)) cons) eqs)))) ([
    4.15                                  simp_tac iterate_Cprod_ss 1,
    4.16 -                                nat_ind_tac "n" 1,
    4.17 +                                induct_tac "n" 1,
    4.18                              simp_tac(iterate_Cprod_ss addsimps copy_con_rews) 1,
    4.19                                  asm_full_simp_tac (HOLCF_ss addsimps 
    4.20                                        (filter (has_fewer_prems 1) copy_rews)) 1,
    4.21 @@ -442,7 +442,7 @@
    4.22                               (dc_take dn $ %:"n" `%(x_name n)))) (fn prems => [
    4.23                                  quant_tac 1,
    4.24                                  simp_tac HOL_ss 1,
    4.25 -                                nat_ind_tac "n" 1,
    4.26 +                                induct_tac "n" 1,
    4.27                                  simp_tac (take_ss addsimps prems) 1,
    4.28                                  TRY(safe_tac HOL_cs)]
    4.29                                  @ flat(map (fn (cons,cases) => [
    4.30 @@ -494,7 +494,7 @@
    4.31           mk_disj(dc_take dn $ Bound 1 ` Bound 0 === UU,
    4.32                   dc_take dn $ Bound 1 ` Bound 0 === Bound 0))) 1 eqs)))) ([
    4.33                                  rtac allI 1,
    4.34 -                                nat_ind_tac "n" 1,
    4.35 +                                induct_tac "n" 1,
    4.36                                  simp_tac take_ss 1,
    4.37                          TRY(safe_tac(empty_cs addSEs[conjE] addSIs[conjI]))] @
    4.38                                  flat(mapn (fn n => fn (cons,cases) => [
    4.39 @@ -564,7 +564,7 @@
    4.40                                  (dc_take dn $ %:"n" `bnd_arg n 0 === 
    4.41                                  (dc_take dn $ %:"n" `bnd_arg n 1)))0 dnames))))))
    4.42                               ([ rtac impI 1,
    4.43 -                                nat_ind_tac "n" 1,
    4.44 +                                induct_tac "n" 1,
    4.45                                  simp_tac take_ss 1,
    4.46                                  safe_tac HOL_cs] @
    4.47                                  flat(mapn (fn n => fn x => [
     5.1 --- a/src/HOLCF/ex/Dagstuhl.ML	Mon Aug 05 14:30:06 2002 +0200
     5.2 +++ b/src/HOLCF/ex/Dagstuhl.ML	Mon Aug 05 14:32:56 2002 +0200
     5.3 @@ -31,7 +31,7 @@
     5.4  
     5.5  val prems = goal Dagstuhl.thy "YS = YYS";
     5.6  by (resolve_tac stream.take_lemmas 1);
     5.7 -by (nat_ind_tac "n" 1);
     5.8 +by (induct_tac "n" 1);
     5.9  by (simp_tac (simpset() addsimps stream.rews) 1);
    5.10  by (stac YS_def2 1);
    5.11  by (stac YYS_def2 1);
     6.1 --- a/src/HOLCF/ex/Hoare.ML	Mon Aug 05 14:30:06 2002 +0200
     6.2 +++ b/src/HOLCF/ex/Hoare.ML	Mon Aug 05 14:32:56 2002 +0200
     6.3 @@ -86,14 +86,14 @@
     6.4  
     6.5  Goal "(ALL m. m< Suc k --> b1$(iterate m g x)=TT) -->\
     6.6  \  p$(iterate k g x)=p$x";
     6.7 -by (nat_ind_tac "k" 1);
     6.8 +by (induct_tac "k" 1);
     6.9  by (Simp_tac 1);
    6.10  by (Simp_tac 1);
    6.11  by (strip_tac 1);
    6.12 -by (res_inst_tac [("s","p$(iterate k g x)")] trans 1);
    6.13 +by (res_inst_tac [("s","p$(iterate n g x)")] trans 1);
    6.14  by (rtac trans 1);
    6.15  by (rtac (p_def3 RS sym) 2);
    6.16 -by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
    6.17 +by (res_inst_tac [("s","TT"),("t","b1$(iterate n g x)")] ssubst 1);
    6.18  by (rtac mp 1);
    6.19  by (etac spec 1);
    6.20  by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
    6.21 @@ -108,14 +108,14 @@
    6.22  
    6.23  Goal "(ALL m. m< Suc k --> b1$(iterate m g x)=TT) --> \
    6.24  \ q$(iterate k g x)=q$x";
    6.25 -by (nat_ind_tac "k" 1);
    6.26 +by (induct_tac "k" 1);
    6.27  by (Simp_tac 1);
    6.28  by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
    6.29  by (strip_tac 1);
    6.30 -by (res_inst_tac [("s","q$(iterate k g x)")] trans 1);
    6.31 +by (res_inst_tac [("s","q$(iterate n g x)")] trans 1);
    6.32  by (rtac trans 1);
    6.33  by (rtac (q_def3 RS sym) 2);
    6.34 -by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
    6.35 +by (res_inst_tac [("s","TT"),("t","b1$(iterate n g x)")] ssubst 1);
    6.36  by (fast_tac HOL_cs 1);
    6.37  by (simp_tac HOLCF_ss 1);
    6.38  by (etac mp 1);
     7.1 --- a/src/HOLCF/ex/Loop.ML	Mon Aug 05 14:30:06 2002 +0200
     7.2 +++ b/src/HOLCF/ex/Loop.ML	Mon Aug 05 14:32:56 2002 +0200
     7.3 @@ -30,7 +30,7 @@
     7.4  qed "while_unfold";
     7.5  
     7.6  Goal "ALL x. while$b$g$x = while$b$g$(iterate k (step$b$g) x)";
     7.7 -by (nat_ind_tac "k" 1);
     7.8 +by (induct_tac "k" 1);
     7.9  by (simp_tac HOLCF_ss 1);
    7.10  by (rtac allI 1);
    7.11  by (rtac trans 1);
    7.12 @@ -86,26 +86,26 @@
    7.13  Goal "[| ALL x. INV x & b$x=TT & g$x~=UU --> INV (g$x);\
    7.14  \        EX y. b$y=FF; INV x |] \
    7.15  \     ==> iterate k (step$b$g) x ~=UU --> INV (iterate k (step$b$g) x)";
    7.16 -by (nat_ind_tac "k" 1);
    7.17 +by (induct_tac "k" 1);
    7.18  by (Asm_simp_tac 1);
    7.19  by (strip_tac 1);
    7.20  by (simp_tac (simpset() addsimps [step_def2]) 1);
    7.21 -by (res_inst_tac [("p","b$(iterate k (step$b$g) x)")] trE 1);
    7.22 +by (res_inst_tac [("p","b$(iterate n (step$b$g) x)")] trE 1);
    7.23  by (etac notE 1);
    7.24  by (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1);
    7.25  by (asm_simp_tac HOLCF_ss 1);
    7.26  by (rtac mp 1);
    7.27  by (etac spec 1);
    7.28  by (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] addsimps [loop_lemma2] ) 1);
    7.29 -by (res_inst_tac [("s","iterate (Suc k) (step$b$g) x"),
    7.30 -                  ("t","g$(iterate k (step$b$g) x)")] ssubst 1);
    7.31 +by (res_inst_tac [("s","iterate (Suc n) (step$b$g) x"),
    7.32 +                  ("t","g$(iterate n (step$b$g) x)")] ssubst 1);
    7.33  by (atac 2);
    7.34  by (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1);
    7.35  by (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] addsimps [loop_lemma2] ) 1);
    7.36  qed_spec_mp "loop_lemma3";
    7.37  
    7.38  Goal "ALL x. b$(iterate k (step$b$g) x)=FF --> while$b$g$x= iterate k (step$b$g) x";
    7.39 -by (nat_ind_tac "k" 1);
    7.40 +by (induct_tac "k" 1);
    7.41  by (Simp_tac 1);
    7.42  by (strip_tac 1);
    7.43  by (stac while_unfold 1);
     8.1 --- a/src/HOLCF/ex/Stream.ML	Mon Aug 05 14:30:06 2002 +0200
     8.2 +++ b/src/HOLCF/ex/Stream.ML	Mon Aug 05 14:32:56 2002 +0200
     8.3 @@ -454,7 +454,7 @@
     8.4  qed "slen_scons_eq_rev";
     8.5  
     8.6  Goal "!x. (Fin n < #x) = (stream_take n\\<cdot>x ~= x)";
     8.7 -by (nat_ind_tac "n" 1);
     8.8 +by (induct_tac "n" 1);
     8.9  by  (simp_tac(simpset() addsimps [slen_empty_eq, thm "Fin_0"]) 1);
    8.10  by  (Fast_tac 1);
    8.11  by (rtac allI 1);
    8.12 @@ -476,7 +476,7 @@
    8.13  qed "slen_take_lemma1";
    8.14  
    8.15  Goal "!x. ~stream_finite x --> #(stream_take i\\<cdot>x) = Fin i";
    8.16 -by (nat_ind_tac "i" 1);
    8.17 +by (induct_tac "i" 1);
    8.18  by  (simp_tac(simpset() addsimps [thm "Fin_0"]) 1);
    8.19  by (rtac allI 1);
    8.20  by (stream_case_tac "x" 1);
    8.21 @@ -515,7 +515,7 @@
    8.22  
    8.23  Goal "!(x::'a::flat stream) y. Fin n <= #x --> x << y --> \
    8.24  \ stream_take n\\<cdot>x = stream_take n\\<cdot>y";
    8.25 -by (nat_ind_tac "n" 1);
    8.26 +by (induct_tac "n" 1);
    8.27  by ( simp_tac(simpset() addsimps [slen_empty_eq]) 1);
    8.28  by (strip_tac 1);
    8.29  by (stream_case_tac "x" 1);
    8.30 @@ -553,7 +553,7 @@
    8.31  qed "slen_strict_mono";
    8.32  
    8.33  Goal "!x. Fin (i + j) <= #x --> Fin j <= #(iterate i rt x)";
    8.34 -by (nat_ind_tac "i" 1);
    8.35 +by (induct_tac "i" 1);
    8.36  by  (Simp_tac 1);
    8.37  by (strip_tac 1);
    8.38  by (stream_case_tac "x" 1);