Adapted to new datatype package.
--- a/src/HOLCF/Discrete0.thy Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/Discrete0.thy Fri Jul 24 13:44:27 1998 +0200
@@ -6,9 +6,9 @@
Discrete CPOs
*)
-Discrete0 = Cont +
+Discrete0 = Cont + Datatype +
-datatype 'a discr = Discr 'a
+datatype 'a discr = Discr "'a :: term"
instance discr :: (term)sq_ord
--- a/src/HOLCF/Discrete1.ML Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/Discrete1.ML Fri Jul 24 13:44:27 1998 +0200
@@ -13,7 +13,7 @@
Goalw [chain]
"!!S::nat=>('a::term)discr. chain S ==> S i = S 0";
-by (nat_ind_tac "i" 1);
+by (induct_tac "i" 1);
by (rtac refl 1);
by (etac subst 1);
by (rtac sym 1);
--- a/src/HOLCF/Fix.ML Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/Fix.ML Fri Jul 24 13:44:27 1998 +0200
@@ -12,24 +12,10 @@
(* derive inductive properties of iterate from primitive recursion *)
(* ------------------------------------------------------------------------ *)
-qed_goal "iterate_0" thy "iterate 0 F x = x"
- (fn prems =>
- [
- (resolve_tac (nat_recs iterate_def) 1)
- ]);
-
-qed_goal "iterate_Suc" thy "iterate (Suc n) F x = F`(iterate n F x)"
- (fn prems =>
- [
- (resolve_tac (nat_recs iterate_def) 1)
- ]);
-
-Addsimps [iterate_0, iterate_Suc];
-
qed_goal "iterate_Suc2" thy "iterate (Suc n) F x = iterate n F (F`x)"
(fn prems =>
[
- (nat_ind_tac "n" 1),
+ (induct_tac "n" 1),
(Simp_tac 1),
(stac iterate_Suc 1),
(stac iterate_Suc 1),
@@ -49,7 +35,7 @@
(cut_facts_tac prems 1),
(strip_tac 1),
(Simp_tac 1),
- (nat_ind_tac "i" 1),
+ (induct_tac "i" 1),
(Asm_simp_tac 1),
(Asm_simp_tac 1),
(etac monofun_cfun_arg 1)
@@ -103,7 +89,7 @@
(rtac chain_iterate 1),
(rtac ub_rangeI 1),
(strip_tac 1),
- (nat_ind_tac "i" 1),
+ (induct_tac "i" 1),
(Asm_simp_tac 1),
(Asm_simp_tac 1),
(res_inst_tac [("t","x")] subst 1),
@@ -120,7 +106,7 @@
(fn prems =>
[
(strip_tac 1),
- (nat_ind_tac "i" 1),
+ (induct_tac "i" 1),
(Asm_simp_tac 1),
(Asm_simp_tac 1),
(rtac (less_fun RS iffD2) 1),
@@ -141,7 +127,7 @@
(fn prems =>
[
(strip_tac 1),
- (nat_ind_tac "i" 1),
+ (induct_tac "i" 1),
(Asm_simp_tac 1),
(rtac (lub_const RS thelubI RS sym) 1),
(Asm_simp_tac 1),
@@ -185,7 +171,7 @@
[
(rtac monofunI 1),
(strip_tac 1),
- (nat_ind_tac "n" 1),
+ (induct_tac "n" 1),
(Asm_simp_tac 1),
(Asm_simp_tac 1),
(etac monofun_cfun_arg 1)
@@ -196,7 +182,7 @@
[
(rtac contlubI 1),
(strip_tac 1),
- (nat_ind_tac "n" 1),
+ (induct_tac "n" 1),
(Simp_tac 1),
(Simp_tac 1),
(res_inst_tac [("t","iterate n F (lub(range(%u. Y u)))"),
@@ -493,7 +479,7 @@
(etac admD 1),
(rtac chain_iterate 1),
(rtac allI 1),
- (nat_ind_tac "i" 1),
+ (induct_tac "i" 1),
(stac iterate_0 1),
(atac 1),
(stac iterate_Suc 1),
--- a/src/HOLCF/Fix.thy Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/Fix.thy Fri Jul 24 13:44:27 1998 +0200
@@ -18,9 +18,12 @@
adm :: "('a::cpo=>bool)=>bool"
admw :: "('a=>bool)=>bool"
+primrec
+ iterate_0 "iterate 0 F x = x"
+ iterate_Suc "iterate (Suc n) F x = F`(iterate n F x)"
+
defs
-iterate_def "iterate n F c == nat_rec c (%n x. F`x) n"
Ifix_def "Ifix F == lub(range(%i. iterate i F UU))"
fix_def "fix == (LAM f. Ifix f)"
--- a/src/HOLCF/IMP/Denotational.ML Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IMP/Denotational.ML Fri Jul 24 13:44:27 1998 +0200
@@ -18,7 +18,7 @@
Goalw [dlift_def]
"(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
-by (simp_tac (simpset() addsplits [split_lift_case]) 1);
+by (simp_tac (simpset() addsplits [Lift1.lift.split]) 1);
qed "dlift_is_Def";
Addsimps [dlift_is_Def];
@@ -29,7 +29,7 @@
qed_spec_mp "eval_implies_D";
Goal "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t";
-by (com.induct_tac "c" 1);
+by (induct_tac "c" 1);
by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
--- a/src/HOLCF/IMP/Denotational.thy Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IMP/Denotational.thy Fri Jul 24 13:44:27 1998 +0200
@@ -14,7 +14,7 @@
consts D :: "com => state discr -> state lift"
-primrec D com
+primrec
"D(SKIP) = (LAM s. Def(undiscr s))"
"D(X := a) = (LAM s. Def((undiscr s)[X := a(undiscr s)]))"
"D(c0 ; c1) = (dlift(D c1) oo (D c0))"
--- a/src/HOLCF/IOA/ABP/Abschannel_finite.thy Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/ABP/Abschannel_finite.thy Fri Jul 24 13:44:27 1998 +0200
@@ -28,7 +28,6 @@
reverse :: 'a list => 'a list
primrec
- reverse List.list
reverse_Nil "reverse([]) = []"
reverse_Cons "reverse(x#xs) = reverse(xs)@[x]"
--- a/src/HOLCF/IOA/ABP/Action.thy Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/ABP/Action.thy Fri Jul 24 13:44:27 1998 +0200
@@ -6,7 +6,7 @@
The set of all actions of the system
*)
-Action = Packet +
+Action = Packet + Datatype +
datatype 'm action = Next | S_msg ('m) | R_msg ('m)
| S_pkt ('m packet) | R_pkt ('m packet)
| S_ack (bool) | R_ack (bool)
--- a/src/HOLCF/IOA/ABP/Correctness.ML Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.ML Fri Jul 24 13:44:27 1998 +0200
@@ -46,10 +46,10 @@
by (rtac iffI 1);
by (subgoal_tac "(l~=[]) --> (reduce(l)~=[])" 1);
by (Fast_tac 1);
- by (List.list.induct_tac "l" 1);
+ by (induct_tac "l" 1);
by (Simp_tac 1);
by (Simp_tac 1);
- by (rtac (split_list_case RS iffD2) 1);
+ by (rtac (list.split RS iffD2) 1);
by (Asm_full_simp_tac 1);
by (REPEAT (rtac allI 1));
by (rtac impI 1);
@@ -60,7 +60,7 @@
val l_iff_red_nil = result();
Goal "s~=[] --> hd(s)=hd(reduce(s))";
-by (List.list.induct_tac "s" 1);
+by (induct_tac "s" 1);
by (Simp_tac 1);
by (case_tac "list =[]" 1);
by (Asm_full_simp_tac 1);
@@ -68,7 +68,7 @@
by (rotate 1 1);
by (asm_full_simp_tac list_ss 1);
by (Simp_tac 1);
-by (rtac (split_list_case RS iffD2) 1);
+by (rtac (list.split RS iffD2) 1);
by (asm_full_simp_tac list_ss 1);
by (REPEAT (rtac allI 1));
by (rtac impI 1);
@@ -80,7 +80,7 @@
(* to be used in the following Lemma *)
Goal "l~=[] --> reverse(reduce(l))~=[]";
-by (List.list.induct_tac "l" 1);
+by (induct_tac "l" 1);
by (Simp_tac 1);
by (case_tac "list =[]" 1);
by (asm_full_simp_tac (simpset() addsimps [reverse_Cons]) 1);
@@ -100,7 +100,7 @@
Goal "!!l.[| l~=[] |] ==> \
\ hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))";
by (Simp_tac 1);
- by (rtac (split_list_case RS iffD2) 1);
+ by (rtac (list.split RS iffD2) 1);
by (asm_full_simp_tac list_ss 1);
by (REPEAT (rtac allI 1));
by (rtac impI 1);
@@ -119,7 +119,7 @@
by (stac split_if 1);
by (rtac conjI 1);
(* --> *)
-by (List.list.induct_tac "l" 1);
+by (induct_tac "l" 1);
by (Simp_tac 1);
by (case_tac "list=[]" 1);
by (asm_full_simp_tac (simpset() addsimps [reverse_Nil,reverse_Cons]) 1);
@@ -132,7 +132,7 @@
by (asm_full_simp_tac (impl_ss addsimps [last_ind_on_first,l_iff_red_nil]) 1);
(* <-- *)
by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe,l_iff_red_nil]) 1);
-by (List.list.induct_tac "l" 1);
+by (induct_tac "l" 1);
by (Simp_tac 1);
by (case_tac "list=[]" 1);
by (cut_inst_tac [("l","list")] cons_not_nil 2);
@@ -174,7 +174,7 @@
(* ---------------- main-part ------------------- *)
by (REPEAT (rtac allI 1));
by (rtac imp_conj_lemma 1);
-by (abs_action.induct_tac "a" 1);
+by (induct_tac "a" 1);
(* ----------------- 2 cases ---------------------*)
by (ALLGOALS (simp_tac (simpset() addsimps [externals_def])));
(* fst case --------------------------------------*)
@@ -219,7 +219,7 @@
(* main-part *)
by (REPEAT (rtac allI 1));
by (rtac imp_conj_lemma 1);
-by (Action.action.induct_tac "a" 1);
+by (induct_tac "a" 1);
(* 7 cases *)
by (ALLGOALS (simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
qed"sender_unchanged";
@@ -235,7 +235,7 @@
(* main-part *)
by (REPEAT (rtac allI 1));
by (rtac imp_conj_lemma 1);
-by (Action.action.induct_tac "a" 1);
+by (induct_tac "a" 1);
(* 7 cases *)
by (ALLGOALS(simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
qed"receiver_unchanged";
@@ -250,7 +250,7 @@
(* main-part *)
by (REPEAT (rtac allI 1));
by (rtac imp_conj_lemma 1);
-by (Action.action.induct_tac "a" 1);
+by (induct_tac "a" 1);
(* 7 cases *)
by (ALLGOALS(simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
qed"env_unchanged";
@@ -259,7 +259,7 @@
Goal "compatible srch_ioa rsch_ioa";
by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
+by (induct_tac "x" 1);
by (ALLGOALS(Simp_tac));
val compat_single_ch = result();
@@ -267,7 +267,7 @@
Goal "compatible srch_fin_ioa rsch_fin_ioa";
by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
+by (induct_tac "x" 1);
by (ALLGOALS(Simp_tac));
val compat_single_fin_ch = result();
@@ -284,7 +284,7 @@
Int_def]) 1);
by (Simp_tac 1);
by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
+by (induct_tac "x" 1);
by (ALLGOALS Simp_tac);
val compat_rec = result();
@@ -293,7 +293,7 @@
by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
by (Simp_tac 1);
by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
+by (induct_tac "x" 1);
by (ALLGOALS Simp_tac);
val compat_rec_fin =result();
@@ -302,7 +302,7 @@
by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
by (Simp_tac 1);
by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
+by (induct_tac "x" 1);
by (ALLGOALS(Simp_tac));
val compat_sen=result();
@@ -311,7 +311,7 @@
by (simp_tac (ss addsimps [empty_def, compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
by (Simp_tac 1);
by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
+by (induct_tac "x" 1);
by (ALLGOALS(Simp_tac));
val compat_sen_fin =result();
@@ -320,7 +320,7 @@
by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
by (Simp_tac 1);
by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
+by (induct_tac "x" 1);
by (ALLGOALS(Simp_tac));
val compat_env=result();
@@ -329,7 +329,7 @@
by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
by (Simp_tac 1);
by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
+by (induct_tac "x" 1);
by (ALLGOALS Simp_tac);
val compat_env_fin=result();
--- a/src/HOLCF/IOA/ABP/Correctness.thy Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.thy Fri Jul 24 13:44:27 1998 +0200
@@ -17,7 +17,6 @@
system_fin_ioa :: "('m action, bool * 'm impl_state)ioa"
primrec
- reduce List.list
reduce_Nil "reduce [] = []"
reduce_Cons "reduce(x#xs) =
(case xs of
--- a/src/HOLCF/IOA/ABP/Lemmas.ML Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/ABP/Lemmas.ML Fri Jul 24 13:44:27 1998 +0200
@@ -45,13 +45,13 @@
val list_ss = simpset_of List.thy;
goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
-by (List.list.induct_tac "l" 1);
+by (induct_tac "l" 1);
by (simp_tac list_ss 1);
by (simp_tac list_ss 1);
val hd_append =result();
goal List.thy "l ~= [] --> (? x xs. l = (x#xs))";
- by (List.list.induct_tac "l" 1);
+ by (induct_tac "l" 1);
by (simp_tac list_ss 1);
by (Fast_tac 1);
qed"cons_not_nil";
--- a/src/HOLCF/IOA/NTP/Action.thy Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Action.thy Fri Jul 24 13:44:27 1998 +0200
@@ -6,7 +6,7 @@
The set of all actions of the system
*)
-Action = Packet +
+Action = Packet + Datatype +
datatype 'm action = S_msg ('m) | R_msg ('m)
| S_pkt ('m packet) | R_pkt ('m packet)
| S_ack (bool) | R_ack (bool)
--- a/src/HOLCF/IOA/NTP/Correctness.ML Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Correctness.ML Fri Jul 24 13:44:27 1998 +0200
@@ -44,7 +44,7 @@
restrict_asig_def, Spec.sig_def]
@asig_projections)) 1);
- by (Action.action.induct_tac "a" 1);
+ by (induct_tac "a" 1);
by (ALLGOALS(simp_tac (simpset() addsimps [actions_def]@asig_projections)));
(* 2 *)
by (simp_tac (simpset() addsimps impl_ioas) 1);
@@ -76,7 +76,7 @@
by (REPEAT(rtac allI 1));
by (rtac imp_conj_lemma 1); (* from lemmas.ML *)
-by (Action.action.induct_tac "a" 1);
+by (induct_tac "a" 1);
by (asm_simp_tac (ss' addsplits [split_if]) 1);
by (forward_tac [inv4] 1);
by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
--- a/src/HOLCF/IOA/NTP/Impl.ML Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Impl.ML Fri Jul 24 13:44:27 1998 +0200
@@ -41,7 +41,7 @@
\ | a:actions(receiver_asig) \
\ | a:actions(srch_asig) \
\ | a:actions(rsch_asig)";
- by (Action.action.induct_tac "a" 1);
+ by (induct_tac "a" 1);
by (ALLGOALS (Simp_tac));
Addsimps [result()];
@@ -160,7 +160,7 @@
1);
by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
- by (Action.action.induct_tac "a" 1);
+ by (induct_tac "a" 1);
(* 10 cases. First 4 are simple, since state doesn't change *)
@@ -221,7 +221,7 @@
@ sender_projections @ impl_ioas))) 1);
by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
- by (Action.action.induct_tac "a" 1);
+ by (induct_tac "a" 1);
val tac3 = asm_full_simp_tac (ss addsimps [inv3_def] addsplits [split_if]);
@@ -287,7 +287,7 @@
@ sender_projections @ impl_ioas))) 1);
by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
- by (Action.action.induct_tac "a" 1);
+ by (induct_tac "a" 1);
val tac4 = asm_full_simp_tac (ss addsimps [inv4_def]
setloop (split_tac [split_if]));
--- a/src/HOLCF/IOA/NTP/Lemmas.ML Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Lemmas.ML Fri Jul 24 13:44:27 1998 +0200
@@ -36,7 +36,7 @@
(* Arithmetic *)
goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
-by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [split_nat_case]) 1);
+by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1);
by (Blast_tac 1);
qed "pred_suc";
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Fri Jul 24 13:44:27 1998 +0200
@@ -878,9 +878,9 @@
\ --> seq_take n`(x @@ (t>>y1)) = seq_take n`(x @@ (t>>y2)))";
by (Seq_induct_tac "x" [] 1);
by (strip_tac 1);
-by (res_inst_tac [("n","n")] natE 1);
+by (exhaust_tac "n" 1);
by Auto_tac;
-by (res_inst_tac [("n","n")] natE 1);
+by (exhaust_tac "n" 1);
by Auto_tac;
qed"take_reduction1";
@@ -900,9 +900,9 @@
\ --> seq_take n`(x @@ (t>>y1)) << seq_take n`(x @@ (t>>y2)))";
by (Seq_induct_tac "x" [] 1);
by (strip_tac 1);
-by (res_inst_tac [("n","n")] natE 1);
+by (exhaust_tac "n" 1);
by Auto_tac;
-by (res_inst_tac [("n","n")] natE 1);
+by (exhaust_tac "n" 1);
by Auto_tac;
qed"take_reduction_less1";
--- a/src/HOLCF/IOA/meta_theory/TrivEx.ML Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TrivEx.ML Fri Jul 24 13:44:27 1998 +0200
@@ -23,7 +23,7 @@
by (simp_tac (simpset() addsimps [trans_of_def,
C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
by (simp_tac (simpset() addsimps [h_abs_def]) 1);
-by (action.induct_tac "a" 1);
+by (induct_tac "a" 1);
by Auto_tac;
qed"h_abs_is_abstraction";
--- a/src/HOLCF/IOA/meta_theory/TrivEx2.ML Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TrivEx2.ML Fri Jul 24 13:44:27 1998 +0200
@@ -23,7 +23,7 @@
by (simp_tac (simpset() addsimps [trans_of_def,
C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
by (simp_tac (simpset() addsimps [h_abs_def]) 1);
-by (action.induct_tac "a" 1);
+by (induct_tac "a" 1);
by Auto_tac;
qed"h_abs_is_abstraction";
@@ -32,7 +32,7 @@
Goalw [xt2_def,plift,option_lift]
"(xt2 (plift afun)) (s,a,t) = (afun a)";
(* !!!!!!!!!!!!! Occurs check !!!! *)
-by (option.induct_tac "a" 1);
+by (induct_tac "a" 1);
*)
--- a/src/HOLCF/Lift1.thy Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/Lift1.thy Fri Jul 24 13:44:27 1998 +0200
@@ -6,7 +6,7 @@
Lifting types of class term to flat pcpo's
*)
-Lift1 = Cprod3 +
+Lift1 = Cprod3 + Datatype +
default term
--- a/src/HOLCF/Porder.ML Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/Porder.ML Fri Jul 24 13:44:27 1998 +0200
@@ -32,7 +32,7 @@
( fn prems =>
[
(cut_facts_tac prems 1),
- (nat_ind_tac "y" 1),
+ (induct_tac "y" 1),
(rtac impI 1),
(etac less_zeroE 1),
(stac less_Suc_eq 1),
@@ -224,7 +224,7 @@
(cut_facts_tac prems 1),
(rtac chainI 1),
(rtac allI 1),
- (nat_ind_tac "i" 1),
+ (induct_tac "i" 1),
(Asm_simp_tac 1),
(Asm_simp_tac 1)
]);
@@ -235,7 +235,7 @@
[
(cut_facts_tac prems 1),
(rtac allI 1),
- (nat_ind_tac "j" 1),
+ (induct_tac "j" 1),
(Asm_simp_tac 1),
(Asm_simp_tac 1)
]);
--- a/src/HOLCF/ex/Hoare.ML Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/ex/Hoare.ML Fri Jul 24 13:44:27 1998 +0200
@@ -183,7 +183,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (res_inst_tac [("n","k")] natE 1),
+ (exhaust_tac "k" 1),
(hyp_subst_tac 1),
(Simp_tac 1),
(strip_tac 1),
@@ -199,7 +199,7 @@
(atac 1),
(rtac trans 1),
(rtac p_def3 1),
- (res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1),
+ (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1),
(rtac (hoare_lemma8 RS spec RS mp) 1),
(atac 1),
(atac 1),
@@ -220,7 +220,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (res_inst_tac [("n","k")] natE 1),
+ (exhaust_tac "k" 1),
(hyp_subst_tac 1),
(Simp_tac 1),
(strip_tac 1),
@@ -238,7 +238,7 @@
(atac 1),
(rtac trans 1),
(rtac p_def3 1),
- (res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1),
+ (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1),
(rtac (hoare_lemma8 RS spec RS mp) 1),
(atac 1),
(atac 1),
@@ -381,7 +381,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (res_inst_tac [("n","k")] natE 1),
+ (exhaust_tac "k" 1),
(hyp_subst_tac 1),
(strip_tac 1),
(Simp_tac 1),
@@ -394,7 +394,7 @@
(atac 1),
(rtac trans 1),
(rtac q_def3 1),
- (res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1),
+ (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1),
(rtac (hoare_lemma8 RS spec RS mp) 1),
(atac 1),
(atac 1),
@@ -410,7 +410,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (res_inst_tac [("n","k")] natE 1),
+ (exhaust_tac "k" 1),
(hyp_subst_tac 1),
(Simp_tac 1),
(strip_tac 1),
@@ -427,7 +427,7 @@
(atac 1),
(rtac trans 1),
(rtac q_def3 1),
- (res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1),
+ (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1),
(rtac (hoare_lemma8 RS spec RS mp) 1),
(atac 1),
(atac 1),