Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Replaced nat_ind_tac by induct_tac.
authorberghofe
Mon, 05 Aug 2002 14:32:56 +0200
changeset 13454 01e2496dee05
parent 13453 af96f2568406
child 13455 f88a91ff8ac6
Replaced nat_ind_tac by induct_tac.
src/HOLCF/FOCUS/Buffer.ML file | annotate | diff | comparison | revisions
src/HOLCF/FOCUS/Buffer_adm.ML file | annotate | diff | comparison | revisions
src/HOLCF/FOCUS/Stream_adm.ML file | annotate | diff | comparison | revisions
src/HOLCF/domain/theorems.ML file | annotate | diff | comparison | revisions
src/HOLCF/ex/Dagstuhl.ML file | annotate | diff | comparison | revisions
src/HOLCF/ex/Hoare.ML file | annotate | diff | comparison | revisions
src/HOLCF/ex/Loop.ML file | annotate | diff | comparison | revisions
src/HOLCF/ex/Stream.ML file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/FOCUS/Buffer.ML	Mon Aug 05 14:30:06 2002 +0200
+++ b/src/HOLCF/FOCUS/Buffer.ML	Mon Aug 05 14:32:56 2002 +0200
@@ -160,7 +160,7 @@
 
 Goal "\\<forall>s f ff. f\\<in>BufEq \\<longrightarrow> ff\\<in>BufEq \\<longrightarrow> \
 \ s\\<in>BufAC_Asm \\<longrightarrow> stream_take n\\<cdot>(f\\<cdot>s) = stream_take n\\<cdot>(ff\\<cdot>s)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by  (Simp_tac 1);
 by (strip_tac 1);
 by (dtac (BufAC_Asm_unfold RS iffD1) 1);
--- a/src/HOLCF/FOCUS/Buffer_adm.ML	Mon Aug 05 14:30:06 2002 +0200
+++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Mon Aug 05 14:32:56 2002 +0200
@@ -112,7 +112,7 @@
 		\    (s,f\\<cdot>s):down_iterate BufAC_Cmt_F i";
 by (res_inst_tac [("x","%i. 2*i")] exI 1);
 by (rtac allI 1);
-by (nat_ind_tac "i" 1);
+by (induct_tac "i" 1);
 by ( Simp_tac 1);
 by (simp_tac (simpset() addsimps [add_commute]) 1);
 by (strip_tac 1);
--- a/src/HOLCF/FOCUS/Stream_adm.ML	Mon Aug 05 14:30:06 2002 +0200
+++ b/src/HOLCF/FOCUS/Stream_adm.ML	Mon Aug 05 14:32:56 2002 +0200
@@ -60,7 +60,7 @@
 \ Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i";
 by (safe_tac HOL_cs);
 by (res_inst_tac [("x","i*ia")] exI 1);
-by (nat_ind_tac "ia" 1);
+by (induct_tac "ia" 1);
 by ( Simp_tac 1);
 by (Simp_tac 1);
 by (strip_tac 1);
@@ -109,13 +109,13 @@
 "!!X. [|stream_antiP (F::(('a::flat stream)set => ('a stream set)))|]\
 \ ==> !i x y. x << y --> y:down_iterate F i --> x:down_iterate F i" (K [
 	rtac allI 1,
-	nat_ind_tac "i" 1,
+	induct_tac "i" 1,
 	 Simp_tac 1,
 	Simp_tac 1,
 	strip_tac 1,
 	etac allE 1 THEN etac all_dupE 1 THEN etac exE 1 THEN etac exE 1,
 	etac conjE 1,
-	case_tac "#x < Fin ia" 1,
+	case_tac "#x < Fin i" 1,
 	 fast_tac HOL_cs 1,
 	fold_goals_tac [thm "ile_def"],
 	mp_tac 1,
--- a/src/HOLCF/domain/theorems.ML	Mon Aug 05 14:30:06 2002 +0200
+++ b/src/HOLCF/domain/theorems.ML	Mon Aug 05 14:32:56 2002 +0200
@@ -371,7 +371,7 @@
   val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
   val take_stricts=pg copy_take_defs(mk_trp(foldr' mk_conj(map(fn((dn,args),_)=>
             strict(dc_take dn $ %:"n")) eqs))) ([
-                        nat_ind_tac "n" 1,
+                        induct_tac "n" 1,
                          simp_tac iterate_Cprod_ss 1,
                         asm_simp_tac (iterate_Cprod_ss addsimps copy_rews)1]);
   val take_stricts' = rewrite_rule copy_take_defs take_stricts;
@@ -385,7 +385,7 @@
          con_app2 con (app_rec_arg (fn n=>dc_take (nth_elem(n,dnames))$ %:"n"))
                               args)) cons) eqs)))) ([
                                 simp_tac iterate_Cprod_ss 1,
-                                nat_ind_tac "n" 1,
+                                induct_tac "n" 1,
                             simp_tac(iterate_Cprod_ss addsimps copy_con_rews) 1,
                                 asm_full_simp_tac (HOLCF_ss addsimps 
                                       (filter (has_fewer_prems 1) copy_rews)) 1,
@@ -442,7 +442,7 @@
                              (dc_take dn $ %:"n" `%(x_name n)))) (fn prems => [
                                 quant_tac 1,
                                 simp_tac HOL_ss 1,
-                                nat_ind_tac "n" 1,
+                                induct_tac "n" 1,
                                 simp_tac (take_ss addsimps prems) 1,
                                 TRY(safe_tac HOL_cs)]
                                 @ flat(map (fn (cons,cases) => [
@@ -494,7 +494,7 @@
          mk_disj(dc_take dn $ Bound 1 ` Bound 0 === UU,
                  dc_take dn $ Bound 1 ` Bound 0 === Bound 0))) 1 eqs)))) ([
                                 rtac allI 1,
-                                nat_ind_tac "n" 1,
+                                induct_tac "n" 1,
                                 simp_tac take_ss 1,
                         TRY(safe_tac(empty_cs addSEs[conjE] addSIs[conjI]))] @
                                 flat(mapn (fn n => fn (cons,cases) => [
@@ -564,7 +564,7 @@
                                 (dc_take dn $ %:"n" `bnd_arg n 0 === 
                                 (dc_take dn $ %:"n" `bnd_arg n 1)))0 dnames))))))
                              ([ rtac impI 1,
-                                nat_ind_tac "n" 1,
+                                induct_tac "n" 1,
                                 simp_tac take_ss 1,
                                 safe_tac HOL_cs] @
                                 flat(mapn (fn n => fn x => [
--- a/src/HOLCF/ex/Dagstuhl.ML	Mon Aug 05 14:30:06 2002 +0200
+++ b/src/HOLCF/ex/Dagstuhl.ML	Mon Aug 05 14:32:56 2002 +0200
@@ -31,7 +31,7 @@
 
 val prems = goal Dagstuhl.thy "YS = YYS";
 by (resolve_tac stream.take_lemmas 1);
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (simp_tac (simpset() addsimps stream.rews) 1);
 by (stac YS_def2 1);
 by (stac YYS_def2 1);
--- a/src/HOLCF/ex/Hoare.ML	Mon Aug 05 14:30:06 2002 +0200
+++ b/src/HOLCF/ex/Hoare.ML	Mon Aug 05 14:32:56 2002 +0200
@@ -86,14 +86,14 @@
 
 Goal "(ALL m. m< Suc k --> b1$(iterate m g x)=TT) -->\
 \  p$(iterate k g x)=p$x";
-by (nat_ind_tac "k" 1);
+by (induct_tac "k" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (strip_tac 1);
-by (res_inst_tac [("s","p$(iterate k g x)")] trans 1);
+by (res_inst_tac [("s","p$(iterate n g x)")] trans 1);
 by (rtac trans 1);
 by (rtac (p_def3 RS sym) 2);
-by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate n g x)")] ssubst 1);
 by (rtac mp 1);
 by (etac spec 1);
 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
@@ -108,14 +108,14 @@
 
 Goal "(ALL m. m< Suc k --> b1$(iterate m g x)=TT) --> \
 \ q$(iterate k g x)=q$x";
-by (nat_ind_tac "k" 1);
+by (induct_tac "k" 1);
 by (Simp_tac 1);
 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
 by (strip_tac 1);
-by (res_inst_tac [("s","q$(iterate k g x)")] trans 1);
+by (res_inst_tac [("s","q$(iterate n g x)")] trans 1);
 by (rtac trans 1);
 by (rtac (q_def3 RS sym) 2);
-by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate n g x)")] ssubst 1);
 by (fast_tac HOL_cs 1);
 by (simp_tac HOLCF_ss 1);
 by (etac mp 1);
--- a/src/HOLCF/ex/Loop.ML	Mon Aug 05 14:30:06 2002 +0200
+++ b/src/HOLCF/ex/Loop.ML	Mon Aug 05 14:32:56 2002 +0200
@@ -30,7 +30,7 @@
 qed "while_unfold";
 
 Goal "ALL x. while$b$g$x = while$b$g$(iterate k (step$b$g) x)";
-by (nat_ind_tac "k" 1);
+by (induct_tac "k" 1);
 by (simp_tac HOLCF_ss 1);
 by (rtac allI 1);
 by (rtac trans 1);
@@ -86,26 +86,26 @@
 Goal "[| ALL x. INV x & b$x=TT & g$x~=UU --> INV (g$x);\
 \        EX y. b$y=FF; INV x |] \
 \     ==> iterate k (step$b$g) x ~=UU --> INV (iterate k (step$b$g) x)";
-by (nat_ind_tac "k" 1);
+by (induct_tac "k" 1);
 by (Asm_simp_tac 1);
 by (strip_tac 1);
 by (simp_tac (simpset() addsimps [step_def2]) 1);
-by (res_inst_tac [("p","b$(iterate k (step$b$g) x)")] trE 1);
+by (res_inst_tac [("p","b$(iterate n (step$b$g) x)")] trE 1);
 by (etac notE 1);
 by (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1);
 by (asm_simp_tac HOLCF_ss 1);
 by (rtac mp 1);
 by (etac spec 1);
 by (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] addsimps [loop_lemma2] ) 1);
-by (res_inst_tac [("s","iterate (Suc k) (step$b$g) x"),
-                  ("t","g$(iterate k (step$b$g) x)")] ssubst 1);
+by (res_inst_tac [("s","iterate (Suc n) (step$b$g) x"),
+                  ("t","g$(iterate n (step$b$g) x)")] ssubst 1);
 by (atac 2);
 by (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1);
 by (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] addsimps [loop_lemma2] ) 1);
 qed_spec_mp "loop_lemma3";
 
 Goal "ALL x. b$(iterate k (step$b$g) x)=FF --> while$b$g$x= iterate k (step$b$g) x";
-by (nat_ind_tac "k" 1);
+by (induct_tac "k" 1);
 by (Simp_tac 1);
 by (strip_tac 1);
 by (stac while_unfold 1);
--- a/src/HOLCF/ex/Stream.ML	Mon Aug 05 14:30:06 2002 +0200
+++ b/src/HOLCF/ex/Stream.ML	Mon Aug 05 14:32:56 2002 +0200
@@ -454,7 +454,7 @@
 qed "slen_scons_eq_rev";
 
 Goal "!x. (Fin n < #x) = (stream_take n\\<cdot>x ~= x)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by  (simp_tac(simpset() addsimps [slen_empty_eq, thm "Fin_0"]) 1);
 by  (Fast_tac 1);
 by (rtac allI 1);
@@ -476,7 +476,7 @@
 qed "slen_take_lemma1";
 
 Goal "!x. ~stream_finite x --> #(stream_take i\\<cdot>x) = Fin i";
-by (nat_ind_tac "i" 1);
+by (induct_tac "i" 1);
 by  (simp_tac(simpset() addsimps [thm "Fin_0"]) 1);
 by (rtac allI 1);
 by (stream_case_tac "x" 1);
@@ -515,7 +515,7 @@
 
 Goal "!(x::'a::flat stream) y. Fin n <= #x --> x << y --> \
 \ stream_take n\\<cdot>x = stream_take n\\<cdot>y";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by ( simp_tac(simpset() addsimps [slen_empty_eq]) 1);
 by (strip_tac 1);
 by (stream_case_tac "x" 1);
@@ -553,7 +553,7 @@
 qed "slen_strict_mono";
 
 Goal "!x. Fin (i + j) <= #x --> Fin j <= #(iterate i rt x)";
-by (nat_ind_tac "i" 1);
+by (induct_tac "i" 1);
 by  (Simp_tac 1);
 by (strip_tac 1);
 by (stream_case_tac "x" 1);
isabelle