--- a/src/HOL/IOA/Solve.ML Thu Jul 08 13:38:41 1999 +0200
+++ b/src/HOL/IOA/Solve.ML Thu Jul 08 13:42:31 1999 +0200
@@ -73,13 +73,13 @@
\ (fst ex), \
\ %i. fst (snd ex i))")] bexI 1);
(* fst(s) is in projected execution *)
- by (Simp_tac 1);
- by (fast_tac (claset() delSWrapper"split_all_tac")1);
+ by (Force_tac 1);
(* projected execution is indeed an execution *)
by (asm_full_simp_tac
- (simpset() addsimps [executions_def,is_execution_fragment_def,
- par_def,starts_of_def,trans_of_def,filter_oseq_def]
- addsplits [option.split]) 1);
+ (simpset() delcongs [if_weak_cong]
+ addsimps [executions_def,is_execution_fragment_def,
+ par_def,starts_of_def,trans_of_def,filter_oseq_def]
+ addsplits [option.split]) 1);
qed"comp1_reachable";
@@ -93,23 +93,25 @@
\ (fst ex), \
\ %i. snd (snd ex i))")] bexI 1);
(* fst(s) is in projected execution *)
- by (Simp_tac 1);
- by (fast_tac (claset() delSWrapper"split_all_tac")1);
+ by (Force_tac 1);
(* projected execution is indeed an execution *)
by (asm_full_simp_tac
- (simpset() addsimps [executions_def,is_execution_fragment_def,
- par_def,starts_of_def,trans_of_def,filter_oseq_def]
- addsplits [option.split]) 1);
+ (simpset() delcongs [if_weak_cong]
+ addsimps [executions_def,is_execution_fragment_def,
+ par_def,starts_of_def,trans_of_def,filter_oseq_def]
+ addsplits [option.split]) 1);
qed"comp2_reachable";
-Delsplits [split_if];
+Delsplits [split_if]; Delcongs [if_weak_cong];
-(* Composition of possibility-mappings *)
-Goalw [is_weak_pmap_def] "[| is_weak_pmap f C1 A1 & \
-\ externals(asig_of(A1))=externals(asig_of(C1)) &\
-\ is_weak_pmap g C2 A2 & \
-\ externals(asig_of(A2))=externals(asig_of(C2)) & \
-\ compat_ioas C1 C2 & compat_ioas A1 A2 |] \
+(* THIS THEOREM IS NEVER USED (lcp)
+ Composition of possibility-mappings *)
+Goalw [is_weak_pmap_def]
+ "[| is_weak_pmap f C1 A1; \
+\ externals(asig_of(A1))=externals(asig_of(C1));\
+\ is_weak_pmap g C2 A2; \
+\ externals(asig_of(A2))=externals(asig_of(C2)); \
+\ compat_ioas C1 C2; compat_ioas A1 A2 |] \
\ ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)";
by (rtac conjI 1);
(* start_states *)
@@ -117,7 +119,6 @@
(* transitions *)
by (REPEAT (rtac allI 1));
by (rtac imp_conj_lemma 1);
-by (REPEAT(etac conjE 1));
by (simp_tac (simpset() addsimps [externals_of_par_extra]) 1);
by (simp_tac (simpset() addsimps [par_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1);
@@ -144,8 +145,8 @@
by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong]
addsplits [split_if]) 1);
by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
- asm_full_simp_tac(simpset() addsimps[comp1_reachable,
- comp2_reachable])1));
+ asm_full_simp_tac(simpset() addsimps[comp1_reachable,
+ comp2_reachable])1));
qed"fxg_is_weak_pmap_of_product_IOA";
@@ -210,3 +211,4 @@
qed"rename_through_pmap";
Addsplits [split_if];
+Addcongs [if_weak_cong];
--- a/src/HOL/UNITY/Lift.ML Thu Jul 08 13:38:41 1999 +0200
+++ b/src/HOL/UNITY/Lift.ML Thu Jul 08 13:42:31 1999 +0200
@@ -32,8 +32,12 @@
val mov_metric4 = read_instantiate_sg (sign_of thy)
[("P", "(?x <= metric ?n ?s)")] rev_mp;
+val mov_metric5 = read_instantiate_sg (sign_of thy)
+ [("P", "?x ~= metric ?n ?s")] rev_mp;
+
(*The order in which they are applied seems to be critical...*)
-val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4];
+val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4,
+ mov_metric5];
val metric_simps = [metric_def, vimage_def];
@@ -302,12 +306,15 @@
by Auto_tac;
qed "E_thm11";
+val metric_tac = REPEAT (FIRSTGOAL (eresolve_tac mov_metrics))
+ THEN auto_tac (claset(), simpset() addsimps metric_simps);
+
(*lem_lift_3_5*)
Goal
"Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
\ LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})";
by (ensures_tac "request_act" 1);
-by (auto_tac (claset(), simpset() addsimps metric_simps));
+by metric_tac;
qed "E_thm13";
(*lem_lift_3_6*)
@@ -316,15 +323,14 @@
\ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
\ LeadsTo (opened Int Req n Int {s. metric n s = N})";
by (ensures_tac "open_act" 1);
-by (REPEAT_FIRST (eresolve_tac mov_metrics));
-by (auto_tac (claset(), simpset() addsimps metric_simps));
+by metric_tac;
qed "E_thm14";
(*lem_lift_3_7*)
Goal "Lift : (opened Int Req n Int {s. metric n s = N}) \
\ LeadsTo (closed Int Req n Int {s. metric n s = N})";
by (ensures_tac "close_act" 1);
-by (auto_tac (claset(), simpset() addsimps metric_simps));
+by metric_tac;
qed "E_thm15";
@@ -339,11 +345,10 @@
qed "lift_3_Req";
-
(*Now we observe that our integer metric is really a natural number*)
Goal "Lift : Always {s. #0 <= metric n s}";
by (rtac (bounded RS Always_weaken) 1);
-by (auto_tac (claset(), simpset() addsimps metric_simps));
+by metric_tac;
qed "Always_nonneg";
val R_thm11 = [Always_nonneg, E_thm11] MRS Always_LeadsTo_weaken;
--- a/src/HOL/ex/Fib.ML Thu Jul 08 13:38:41 1999 +0200
+++ b/src/HOL/ex/Fib.ML Thu Jul 08 13:42:31 1999 +0200
@@ -53,8 +53,8 @@
(*Concrete Mathematics, page 278: Cassini's identity*)
Goal "fib (Suc (Suc n)) * fib n = \
-\ (if n mod 2 = 0 then (fib(Suc n) * fib(Suc n)) - 1 \
-\ else Suc (fib(Suc n) * fib(Suc n)))";
+\ (if n mod 2 = 0 then (fib(Suc n) * fib(Suc n)) - 1 \
+\ else Suc (fib(Suc n) * fib(Suc n)))";
by (res_inst_tac [("u","n")] fib.induct 1);
by (res_inst_tac [("P", "%z. ?ff(x) * z = ?kk(x)")] (fib_Suc_Suc RS ssubst) 3);
by (stac (read_instantiate [("x", "Suc(Suc ?n)")] fib_Suc_Suc) 3);
@@ -63,11 +63,10 @@
by (ALLGOALS (*using [fib_Suc_Suc] here results in a longer proof!*)
(asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2,
mod_less, mod_Suc])));
-by (ALLGOALS
- (asm_full_simp_tac
- (simpset() addsimps add_ac @ mult_ac @
- [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2,
- mod_less, mod_Suc])));
+by (asm_full_simp_tac
+ (simpset() addsimps [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2,
+ mod_less, mod_Suc]) 2);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [fib_Suc_Suc])));
qed "fib_Cassini";
--- a/src/HOLCF/IOA/ABP/Correctness.ML Thu Jul 08 13:38:41 1999 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.ML Thu Jul 08 13:42:31 1999 +0200
@@ -33,8 +33,6 @@
asig_projections @ set_lemmas;
Addsimps hom_ioas;
-Addsimps [reduce_Nil,reduce_Cons];
-
(* auxiliary function *)
@@ -43,70 +41,27 @@
(* lemmas about reduce *)
Goal "(reduce(l)=[]) = (l=[])";
- by (rtac iffI 1);
- by (subgoal_tac "(l~=[]) --> (reduce(l)~=[])" 1);
- by (Fast_tac 1);
- by (induct_tac "l" 1);
- by (Simp_tac 1);
- by (Simp_tac 1);
- by (rtac (list.split RS iffD2) 1);
- by (Asm_full_simp_tac 1);
- by (REPEAT (rtac allI 1));
- by (rtac impI 1);
- by (hyp_subst_tac 1);
- by (stac split_if 1);
- by (Asm_full_simp_tac 1);
- by (Asm_full_simp_tac 1);
+by (induct_tac "l" 1);
+by (auto_tac (claset(), simpset() addsplits [list.split]));
val l_iff_red_nil = result();
Goal "s~=[] --> hd(s)=hd(reduce(s))";
by (induct_tac "s" 1);
-by (Simp_tac 1);
-by (case_tac "list =[]" 1);
-by (Asm_full_simp_tac 1);
-(* main case *)
-by (rotate 1 1);
-by (asm_full_simp_tac list_ss 1);
-by (Simp_tac 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);
-by (stac split_if 1);
-by (REPEAT(hyp_subst_tac 1));
-by (etac subst 1);
-by (Simp_tac 1);
+by (auto_tac (claset(), simpset() addsplits [list.split]));
qed"hd_is_reduce_hd";
(* to be used in the following Lemma *)
Goal "l~=[] --> reverse(reduce(l))~=[]";
by (induct_tac "l" 1);
-by (Simp_tac 1);
-by (case_tac "list =[]" 1);
-by (asm_full_simp_tac (simpset() addsimps [reverse_Cons]) 1);
-(* main case *)
-by (rotate 1 1);
-by (Asm_full_simp_tac 1);
-by (cut_inst_tac [("l","list")] cons_not_nil 1);
-by (Asm_full_simp_tac 1);
-by (REPEAT (etac exE 1));
-by (Asm_simp_tac 1);
-by (stac split_if 1);
-by (hyp_subst_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [reverse_Cons]) 1);
-qed"rev_red_not_nil";
+by (auto_tac (claset(), simpset() addsplits [list.split]));
+qed_spec_mp "rev_red_not_nil";
(* shows applicability of the induction hypothesis of the following Lemma 1 *)
-Goal "!!l.[| l~=[] |] ==> \
-\ hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))";
+Goal "l~=[] ==> hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))";
by (Simp_tac 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);
- by (stac split_if 1);
- by (asm_full_simp_tac (list_ss addsimps [reverse_Cons,hd_append,
- (rev_red_not_nil RS mp)]) 1);
+ by (asm_full_simp_tac (list_ss addsplits [list.split]
+ addsimps [reverse_Cons,hd_append,
+ rev_red_not_nil]) 1);
qed"last_ind_on_first";
val impl_ss = simpset() delsimps [reduce_Cons];
@@ -145,21 +100,14 @@
(* Main Lemma 2 for R_pkt in showing that reduce is refinement *)
-Goal
- "!! s. [| s~=[] |] ==> \
+Goal "s~=[] ==> \
\ if hd(s)=hd(tl(s)) & tl(s)~=[] then \
\ reduce(tl(s))=reduce(s) else \
\ reduce(tl(s))=tl(reduce(s))";
by (cut_inst_tac [("l","s")] cons_not_nil 1);
by (Asm_full_simp_tac 1);
by (REPEAT (etac exE 1));
-by (Asm_full_simp_tac 1);
-by (stac split_if 1);
-by (rtac conjI 1);
-by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe]) 2);
-by (Step_tac 1);
-by (ALLGOALS (cut_inst_tac [("l","xs")] cons_not_nil));
-by (Auto_tac);
+by (auto_tac (claset(), simpset() addsplits [list.split]));
val reduce_tl =result();
@@ -167,16 +115,17 @@
C h a n n e l A b s t r a c t i o n
*******************************************************************)
-Delsplits [split_if];
-Goal
- "is_weak_ref_map reduce ch_ioa ch_fin_ioa";
+Delsplits [split_if];
+
+Goal "is_weak_ref_map reduce ch_ioa ch_fin_ioa";
by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
(* ---------------- main-part ------------------- *)
by (REPEAT (rtac allI 1));
by (rtac imp_conj_lemma 1);
by (induct_tac "a" 1);
(* ----------------- 2 cases ---------------------*)
-by (ALLGOALS (simp_tac (simpset() addsimps [externals_def])));
+by (ALLGOALS (simp_tac (simpset() delcongs [if_weak_cong]
+ addsimps [externals_def])));
(* fst case --------------------------------------*)
by (rtac impI 1);
by (rtac disjI2 1);
@@ -194,14 +143,14 @@
by (etac reduce_tl 1);
qed"channel_abstraction";
-Goal
- "is_weak_ref_map reduce srch_ioa srch_fin_ioa";
+Addsplits [split_if];
+
+Goal "is_weak_ref_map reduce srch_ioa srch_fin_ioa";
by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
qed"sender_abstraction";
-Goal
- "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa";
+Goal "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa";
by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
qed"receiver_abstraction";
@@ -209,52 +158,34 @@
(* 3 thms that do not hold generally! The lucky restriction here is
the absence of internal actions. *)
-Goal
- "is_weak_ref_map (%id. id) sender_ioa sender_ioa";
+Goal "is_weak_ref_map (%id. id) sender_ioa sender_ioa";
by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
-by (TRY(
- (rtac conjI 1) THEN
-(* start states *)
- (Fast_tac 1)));
(* main-part *)
by (REPEAT (rtac allI 1));
-by (rtac imp_conj_lemma 1);
by (induct_tac "a" 1);
(* 7 cases *)
-by (ALLGOALS (simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
+by (ALLGOALS (simp_tac (simpset() addsimps [externals_def])));
qed"sender_unchanged";
(* 2 copies of before *)
-Goal
- "is_weak_ref_map (%id. id) receiver_ioa receiver_ioa";
+Goal "is_weak_ref_map (%id. id) receiver_ioa receiver_ioa";
by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
-by (TRY(
- (rtac conjI 1) THEN
- (* start states *)
- (Fast_tac 1)));
(* main-part *)
by (REPEAT (rtac allI 1));
-by (rtac imp_conj_lemma 1);
by (induct_tac "a" 1);
(* 7 cases *)
-by (ALLGOALS(simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
+by (ALLGOALS(simp_tac (simpset() addsimps [externals_def])));
qed"receiver_unchanged";
-Goal
- "is_weak_ref_map (%id. id) env_ioa env_ioa";
+Goal "is_weak_ref_map (%id. id) env_ioa env_ioa";
by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
-by (TRY(
- (rtac conjI 1) THEN
-(* start states *)
- (Fast_tac 1)));
(* main-part *)
by (REPEAT (rtac allI 1));
-by (rtac imp_conj_lemma 1);
by (induct_tac "a" 1);
(* 7 cases *)
-by (ALLGOALS(simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
+by (ALLGOALS(simp_tac (simpset() addsimps [externals_def])));
qed"env_unchanged";
-Addsplits [split_if];
+
Goal "compatible srch_ioa rsch_ioa";
by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
@@ -335,8 +266,7 @@
(* lemmata about externals of channels *)
-Goal
- "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) & \
+Goal "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) & \
\ externals(asig_of(rsch_fin_ioa)) = externals(asig_of(rsch_ioa))";
by (simp_tac (simpset() addsimps [externals_def]) 1);
val ext_single_ch = result();
@@ -363,8 +293,7 @@
(* FIX: this proof should be done with compositionality on trace level, not on
weak_ref_map level, as done here with fxg_is_weak_ref_map_of_product_IOA
-Goal
- "is_weak_ref_map abs system_ioa system_fin_ioa";
+Goal "is_weak_ref_map abs system_ioa system_fin_ioa";
by (simp_tac (impl_ss delsimps ([srch_ioa_def, rsch_ioa_def, srch_fin_ioa_def,
rsch_fin_ioa_def] @ env_ioas @ impl_ioas)
--- a/src/HOLCF/IOA/NTP/Correctness.ML Thu Jul 08 13:38:41 1999 +0200
+++ b/src/HOLCF/IOA/NTP/Correctness.ML Thu Jul 08 13:42:31 1999 +0200
@@ -64,13 +64,13 @@
Receiver.rbit_def, Receiver.rq_def, Receiver.rsending_def];
-
(* Proof of correctness *)
Goalw [Spec.ioa_def, is_weak_ref_map_def]
"is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig)) \
\ spec_ioa";
-by (simp_tac (simpset() delsplits [split_if] addsimps
- [Correctness.hom_def, cancel_restrict, externals_lemma]) 1);
+by (simp_tac (simpset() delcongs [if_weak_cong] delsplits [split_if]
+ addsimps [Correctness.hom_def, cancel_restrict,
+ externals_lemma]) 1);
by (rtac conjI 1);
by (simp_tac ss' 1);
by (asm_simp_tac (simpset() addsimps sels) 1);
@@ -78,25 +78,16 @@
by (rtac imp_conj_lemma 1); (* from lemmas.ML *)
by (induct_tac "a" 1);
-by (asm_simp_tac (ss' addsplits [split_if]) 1);
+by (ALLGOALS (asm_simp_tac ss'));
by (forward_tac [inv4] 1);
-by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
-by (simp_tac ss' 1);
-by (simp_tac ss' 1);
-by (simp_tac ss' 1);
-by (simp_tac ss' 1);
-by (simp_tac ss' 1);
-by (simp_tac ss' 1);
-by (simp_tac ss' 1);
+by (Force_tac 1);
-by (asm_simp_tac ss' 1);
by (forward_tac [inv4] 1);
by (forward_tac [inv2] 1);
by (etac disjE 1);
by (Asm_simp_tac 1);
-by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
+by (Force_tac 1);
-by (asm_simp_tac ss' 1);
by (forward_tac [inv2] 1);
by (etac disjE 1);
@@ -104,14 +95,14 @@
by (case_tac "sq(sen(s))=[]" 1);
by (asm_full_simp_tac ss' 1);
-by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1);
+by (blast_tac (claset() addSDs [add_leD1 RS leD]) 1);
by (case_tac "m = hd(sq(sen(s)))" 1);
-by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
+by (Force_tac 1);
by (Asm_full_simp_tac 1);
-by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1);
+by (blast_tac (claset() addSDs [add_leD1 RS leD]) 1);
by (Asm_full_simp_tac 1);
qed"ntp_correct";
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML Thu Jul 08 13:38:41 1999 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Thu Jul 08 13:42:31 1999 +0200
@@ -67,9 +67,10 @@
by (fast_tac (claset() addDs prems) 1);
val lemma = result();
-Delsplits [split_if];
-Goal "[| is_weak_ref_map f C A |]\
-\ ==> (is_weak_ref_map f (rename C g) (rename A g))";
+Delsplits [split_if]; Delcongs [if_weak_cong];
+
+Goal "[| is_weak_ref_map f C A |] \
+\ ==> (is_weak_ref_map f (rename C g) (rename A g))";
by (asm_full_simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
by (rtac conjI 1);
(* 1: start states *)
@@ -104,12 +105,9 @@
by (forward_tac [reachable_rename] 1);
by (Asm_full_simp_tac 1);
(* x is internal *)
-by (simp_tac (simpset() addcongs [conj_cong]) 1);
-by (rtac impI 1);
-by (etac conjE 1);
by (forward_tac [reachable_rename] 1);
by Auto_tac;
qed"rename_through_pmap";
-Addsplits [split_if];
+Addsplits [split_if]; Addcongs [if_weak_cong];