# HG changeset patch
# User nipkow
# Date 971348479 -7200
# Node ID 9e8b4bebc94029121a44a510b5b9c76dfb54bd56
# Parent  b52140d1a7bc29a31e19c48f9bd4549cacd0c5b5
induct -> lfp_induct

diff -r b52140d1a7bc -r 9e8b4bebc940 src/HOL/IMP/Denotation.ML
--- a/src/HOL/IMP/Denotation.ML	Thu Oct 12 12:26:30 2000 +0200
+++ b/src/HOL/IMP/Denotation.ML	Thu Oct 12 13:01:19 2000 +0200
@@ -46,7 +46,7 @@
 
 (* while *)
 by (strip_tac 1);
-by (etac (Gamma_mono RSN (2,induct)) 1);
+by (etac (Gamma_mono RSN (2,lfp_induct)) 1);
 by (rewtac Gamma_def);  
 by (Fast_tac 1);
 
diff -r b52140d1a7bc -r 9e8b4bebc940 src/HOL/IMP/Hoare.ML
--- a/src/HOL/IMP/Hoare.ML	Thu Oct 12 12:26:30 2000 +0200
+++ b/src/HOL/IMP/Hoare.ML	Thu Oct 12 13:01:19 2000 +0200
@@ -25,7 +25,7 @@
   by (Fast_tac 1);
  by (Fast_tac 1);
 by (EVERY' [rtac allI, rtac allI, rtac impI] 1);
-by (etac induct2 1);
+by (etac lfp_induct2 1);
  by (rtac Gamma_mono 1);
 by (rewtac Gamma_def);  
 by (Fast_tac 1);
@@ -85,7 +85,7 @@
 by (strip_tac 1);
 by (rtac mp 1);
  by (assume_tac 2);
-by (etac induct2 1);
+by (etac lfp_induct2 1);
 by (fast_tac (claset() addSIs [monoI]) 1);
 by (stac gfp_unfold 1);
  by (fast_tac (claset() addSIs [monoI]) 1);
diff -r b52140d1a7bc -r 9e8b4bebc940 src/HOL/Lfp.ML
--- a/src/HOL/Lfp.ML	Thu Oct 12 12:26:30 2000 +0200
+++ b/src/HOL/Lfp.ML	Thu Oct 12 13:01:19 2000 +0200
@@ -47,13 +47,13 @@
             rtac (Int_lower1 RS (mono RS monoD)),
             rtac (mono RS lfp_lemma2),
             rtac (CollectI RS subsetI), rtac indhyp, atac]);
-qed "induct";
+qed "lfp_induct";
 
-bind_thm ("induct2",
-  split_rule (read_instantiate [("a","(a,b)")] induct));
+bind_thm ("lfp_induct2",
+  split_rule (read_instantiate [("a","(a,b)")] lfp_induct));
 
 
-(** Definition forms of lfp_Tarski and induct, to control unfolding **)
+(** Definition forms of lfp_unfold and lfp_induct, to control unfolding **)
 
 Goal "[| h==lfp(f);  mono(f) |] ==> h = f(h)";
 by (auto_tac (claset() addSIs [lfp_unfold], simpset()));  
@@ -63,9 +63,9 @@
     "[| A == lfp(f);  mono(f);   a:A;                   \
 \       !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x)        \
 \    |] ==> P(a)";
-by (EVERY1 [rtac induct,        (*backtracking to force correct induction*)
+by (EVERY1 [rtac lfp_induct,        (*backtracking to force correct induction*)
             REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]);
-qed "def_induct";
+qed "def_lfp_induct";
 
 (*Monotonicity of lfp!*)
 val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)";
diff -r b52140d1a7bc -r 9e8b4bebc940 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Thu Oct 12 12:26:30 2000 +0200
+++ b/src/HOL/NatDef.ML	Thu Oct 12 13:01:19 2000 +0200
@@ -27,7 +27,7 @@
 val major::prems = Goal
     "[| i: Nat;  P(Zero_Rep);   \
 \       !!j. [| j: Nat; P(j) |] ==> P(Suc_Rep(j)) |]  ==> P(i)";
-by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_induct) 1);
+by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_lfp_induct) 1);
 by (blast_tac (claset() addIs prems) 1);
 qed "Nat_induct";
 
diff -r b52140d1a7bc -r 9e8b4bebc940 src/HOL/Real/PNat.ML
--- a/src/HOL/Real/PNat.ML	Thu Oct 12 12:26:30 2000 +0200
+++ b/src/HOL/Real/PNat.ML	Thu Oct 12 13:01:19 2000 +0200
@@ -33,7 +33,7 @@
 val major::prems = Goal
     "[| i: pnat;  P(1);   \
 \       !!j. [| j: pnat; P(j) |] ==> P(Suc(j)) |]  ==> P(i)";
-by (rtac ([pnat_def, pnat_fun_mono, major] MRS def_induct) 1);
+by (rtac ([pnat_def, pnat_fun_mono, major] MRS def_lfp_induct) 1);
 by (blast_tac (claset() addIs prems) 1);
 qed "PNat_induct";
 
diff -r b52140d1a7bc -r 9e8b4bebc940 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Oct 12 12:26:30 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Oct 12 13:01:19 2000 +0200
@@ -575,7 +575,7 @@
     val induct = prove_goalw_cterm [] (cterm_of sign
       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
         [rtac (impI RS allI) 1,
-         DETERM (etac (mono RS (fp_def RS def_induct)) 1),
+         DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1),
          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
          fold_goals_tac rec_sets_defs,
          (*This CollectE and disjE separates out the introduction rules*)
diff -r b52140d1a7bc -r 9e8b4bebc940 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Thu Oct 12 12:26:30 2000 +0200
+++ b/src/HOL/Trancl.ML	Thu Oct 12 13:01:19 2000 +0200
@@ -53,7 +53,7 @@
 \     !!x. P(x,x); \
 \     !!x y z.[| P(x,y); (x,y): r^*; (y,z): r |]  ==>  P(x,z) |] \
 \  ==>  P(a,b)";
-by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_induct) 1);
+by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_lfp_induct) 1);
 by (blast_tac (claset() addIs prems) 1);
 qed "rtrancl_full_induct";
 
diff -r b52140d1a7bc -r 9e8b4bebc940 src/HOL/ex/MT.ML
--- a/src/HOL/ex/MT.ML	Thu Oct 12 12:26:30 2000 +0200
+++ b/src/HOL/ex/MT.ML	Thu Oct 12 13:01:19 2000 +0200
@@ -65,7 +65,7 @@
   " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y) |] ==> \
 \   P(x)";
 by (cut_facts_tac prems 1);
-by (etac induct 1);
+by (etac lfp_induct 1);
 by (assume_tac 1);
 by (eresolve_tac prems 1);
 qed "lfp_ind2";