--- a/src/HOL/UNITY/Lift.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOL/UNITY/Lift.ML Fri Jan 29 16:23:56 1999 +0100
@@ -37,7 +37,6 @@
(*The order in which they are applied seems to be critical...*)
val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4];
-
val metric_simps = [metric_def, vimage_def];
@@ -109,7 +108,7 @@
by (constrains_tac 1);
by (ALLGOALS Clarify_tac);
by (REPEAT_FIRST distinct_tac);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [zle_imp_zle_zadd])));
+by Auto_tac;
qed "bounded";
@@ -246,8 +245,6 @@
by Auto_tac;
by (REPEAT_FIRST (eresolve_tac mov_metrics));
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls)));
-(** LEVEL 5 **)
-by (dres_inst_tac [("w1","Min")] (zle_iff_zadd RS iffD1) 1);
by (Blast_tac 1);
qed "E_thm16a";
@@ -260,8 +257,6 @@
by Auto_tac;
by (REPEAT_FIRST (eresolve_tac mov_metrics));
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls)));
-(** LEVEL 5 **)
-by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1);
by (Blast_tac 1);
qed "E_thm16b";
--- a/src/HOLCF/IOA/Storage/Correctness.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/Storage/Correctness.ML Fri Jan 29 16:23:56 1999 +0100
@@ -28,7 +28,7 @@
(* ---------------- main-part ------------------- *)
by (REPEAT (rtac allI 1));
-br imp_conj_lemma 1;
+by (rtac imp_conj_lemma 1);
ren "k b used c k' b' a" 1;
by (induct_tac "a" 1);
by (ALLGOALS (simp_tac (simpset() addsimps [sim_relation_def,
@@ -37,13 +37,13 @@
(* NEW *)
by (res_inst_tac [("x","(used,True)")] exI 1);
by (Asm_full_simp_tac 1);
-br transition_is_ex 1;
+by (rtac transition_is_ex 1);
by (simp_tac (simpset() addsimps [
Spec.ioa_def,Spec.trans_def,trans_of_def])1);
(* LOC *)
by (res_inst_tac [("x","(used Un {k},False)")] exI 1);
by (Asm_full_simp_tac 1);
-br transition_is_ex 1;
+by (rtac transition_is_ex 1);
by (simp_tac (simpset() addsimps [
Spec.ioa_def,Spec.trans_def,trans_of_def])1);
by (Fast_tac 1);
@@ -51,8 +51,8 @@
by (res_inst_tac [("x","(used - {nat},c)")] exI 1);
by (Asm_full_simp_tac 1);
by (SELECT_GOAL (safe_tac set_cs) 1);
-auto();
-br transition_is_ex 1;
+by Auto_tac;
+by (rtac transition_is_ex 1);
by (simp_tac (simpset() addsimps [
Spec.ioa_def,Spec.trans_def,trans_of_def])1);
qed"issimulation";
@@ -61,14 +61,14 @@
Goalw [ioa_implements_def]
"impl_ioa =<| spec_ioa";
-br conjI 1;
+by (rtac conjI 1);
by (simp_tac (simpset() addsimps [Impl.sig_def,Spec.sig_def,
Impl.ioa_def,Spec.ioa_def, asig_outputs_def,asig_of_def,
asig_inputs_def]) 1);
-br trace_inclusion_for_simulations 1;
+by (rtac trace_inclusion_for_simulations 1);
by (simp_tac (simpset() addsimps [Impl.sig_def,Spec.sig_def,
Impl.ioa_def,Spec.ioa_def, externals_def,asig_outputs_def,asig_of_def,
asig_inputs_def]) 1);
-br issimulation 1;
+by (rtac issimulation 1);
qed"implementation";
--- a/src/HOLCF/IOA/meta_theory/Abstraction.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML Fri Jan 29 16:23:56 1999 +0100
@@ -57,7 +57,7 @@
Goalw [cex_abs_def]
- "!!h.[| is_abstraction h C A |] ==>\
+ "[| is_abstraction h C A |] ==>\
\ !s. reachable C s & is_exec_frag C (s,xs) \
\ --> is_exec_frag A (cex_abs h (s,xs))";
@@ -72,7 +72,7 @@
qed_spec_mp"exec_frag_abstraction";
-Goal "!!A. is_abstraction h C A ==> weakeningIOA A C h";
+Goal "is_abstraction h C A ==> weakeningIOA A C h";
by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def])1);
by Auto_tac;
by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
@@ -85,7 +85,7 @@
qed"abs_is_weakening";
-Goal "!!A. [|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] \
+Goal "[|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] \
\ ==> validIOA C P";
by (dtac abs_is_weakening 1);
by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def,
@@ -117,7 +117,7 @@
Goalw [is_live_abstraction_def]
- "!!A. [|is_live_abstraction h (C,L) (A,M); \
+ "[|is_live_abstraction h (C,L) (A,M); \
\ validLIOA (A,M) Q; temp_strengthening Q P h |] \
\ ==> validLIOA (C,L) P";
by Auto_tac;
@@ -130,7 +130,7 @@
Goalw [is_live_abstraction_def]
- "!!A. [|is_live_abstraction h (C,L) (A,M); \
+ "[|is_live_abstraction h (C,L) (A,M); \
\ validLIOA (A,M) (H1 .--> Q); temp_strengthening Q P h; \
\ temp_weakening H1 H2 h; validLIOA (C,L) H2 |] \
\ ==> validLIOA (C,L) P";
@@ -151,14 +151,14 @@
Goalw [is_abstraction_def,is_ref_map_def]
-"!! h. is_abstraction h C A ==> is_ref_map h C A";
+"is_abstraction h C A ==> is_ref_map h C A";
by (safe_tac set_cs);
by (res_inst_tac[("x","(a,h t)>>nil")] exI 1);
by (asm_full_simp_tac (simpset() addsimps [move_def])1);
qed"abstraction_is_ref_map";
-Goal "!! h. [| inp(C)=inp(A); out(C)=out(A); \
+Goal "[| inp(C)=inp(A); out(C)=out(A); \
\ is_abstraction h C A |] \
\ ==> C =<| A";
by (asm_full_simp_tac (simpset() addsimps [ioa_implements_def]) 1);
@@ -179,7 +179,7 @@
(* Reduces to Filter (Map fst x) = Filter (Map fst (Map (%(a,t). (a,x)) x),
that is to special Map Lemma *)
Goalw [cex_abs_def,mk_trace_def,filter_act_def]
- "!! f. ext C = ext A \
+ "ext C = ext A \
\ ==> mk_trace C`xs = mk_trace A`(snd (cex_abs f (s,xs)))";
by (Asm_full_simp_tac 1);
by (pair_induct_tac "xs" [] 1);
@@ -190,7 +190,7 @@
is_live_abstraction includes temp_strengthening which is necessarily based
on cex_abs and not on corresp_ex. Thus, the proof is redoone in a more specific
way for cex_abs *)
-Goal "!! h. [| inp(C)=inp(A); out(C)=out(A); \
+Goal "[| inp(C)=inp(A); out(C)=out(A); \
\ is_live_abstraction h (C,M) (A,L) |] \
\ ==> live_implements (C,M) (A,L)";
@@ -223,7 +223,7 @@
(* FIX: NAch Traces.ML bringen *)
Goalw [ioa_implements_def]
-"!! A. [| A =<| B; B =<| C|] ==> A =<| C";
+"[| A =<| B; B =<| C|] ==> A =<| C";
by Auto_tac;
qed"implements_trans";
@@ -234,7 +234,7 @@
(* Abstraction Rules for Automata *)
(* ---------------------------------------------------------------- *)
-Goal "!! C. [| inp(C)=inp(A); out(C)=out(A); \
+Goal "[| inp(C)=inp(A); out(C)=out(A); \
\ inp(Q)=inp(P); out(Q)=out(P); \
\ is_abstraction h1 C A; \
\ A =<| Q ; \
@@ -250,7 +250,7 @@
qed"AbsRuleA1";
-Goal "!! C. [| inp(C)=inp(A); out(C)=out(A); \
+Goal "[| inp(C)=inp(A); out(C)=out(A); \
\ inp(Q)=inp(P); out(Q)=out(P); \
\ is_live_abstraction h1 (C,LC) (A,LA); \
\ live_implements (A,LA) (Q,LQ) ; \
@@ -276,28 +276,28 @@
(* ---------------------------------------------------------------- *)
Goalw [temp_strengthening_def]
-"!! h. [| temp_strengthening P1 Q1 h; \
+"[| temp_strengthening P1 Q1 h; \
\ temp_strengthening P2 Q2 h |] \
\ ==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h";
by Auto_tac;
qed"strength_AND";
Goalw [temp_strengthening_def]
-"!! h. [| temp_strengthening P1 Q1 h; \
+"[| temp_strengthening P1 Q1 h; \
\ temp_strengthening P2 Q2 h |] \
\ ==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h";
by Auto_tac;
qed"strength_OR";
Goalw [temp_strengthening_def]
-"!! h. [| temp_weakening P Q h |] \
+"[| temp_weakening P Q h |] \
\ ==> temp_strengthening (.~ P) (.~ Q) h";
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
by Auto_tac;
qed"strength_NOT";
Goalw [temp_strengthening_def]
-"!! h. [| temp_weakening P1 Q1 h; \
+"[| temp_weakening P1 Q1 h; \
\ temp_strengthening P2 Q2 h |] \
\ ==> temp_strengthening (P1 .--> P2) (Q1 .--> Q2) h";
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
@@ -310,28 +310,28 @@
(* ---------------------------------------------------------------- *)
Goal
-"!! h. [| temp_weakening P1 Q1 h; \
+"[| temp_weakening P1 Q1 h; \
\ temp_weakening P2 Q2 h |] \
\ ==> temp_weakening (P1 .& P2) (Q1 .& Q2) h";
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
qed"weak_AND";
Goal
-"!! h. [| temp_weakening P1 Q1 h; \
+"[| temp_weakening P1 Q1 h; \
\ temp_weakening P2 Q2 h |] \
\ ==> temp_weakening (P1 .| P2) (Q1 .| Q2) h";
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
qed"weak_OR";
Goalw [temp_strengthening_def]
-"!! h. [| temp_strengthening P Q h |] \
+"[| temp_strengthening P Q h |] \
\ ==> temp_weakening (.~ P) (.~ Q) h";
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
by Auto_tac;
qed"weak_NOT";
Goalw [temp_strengthening_def]
-"!! h. [| temp_strengthening P1 Q1 h; \
+"[| temp_strengthening P1 Q1 h; \
\ temp_weakening P2 Q2 h |] \
\ ==> temp_weakening (P1 .--> P2) (Q1 .--> Q2) h";
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
@@ -373,7 +373,7 @@
(* important property of ex2seq: can be shiftet, as defined "pointwise" *)
Goalw [tsuffix_def,suffix_def]
-"!!s. tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')";
+"tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')";
by Auto_tac;
by (dtac ex2seqConc 1);
by Auto_tac;
@@ -395,7 +395,7 @@
properties carry over *)
Goalw [tsuffix_def,suffix_def,cex_absSeq_def]
-"!! s. tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)";
+"tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)";
by Auto_tac;
by (asm_full_simp_tac (simpset() addsimps [Mapnil])1);
by (asm_full_simp_tac (simpset() addsimps [MapUU])1);
@@ -406,7 +406,7 @@
Goalw [temp_strengthening_def,state_strengthening_def, temp_sat_def,
satisfies_def,Box_def]
-"!! h. [| temp_strengthening P Q h |]\
+"[| temp_strengthening P Q h |]\
\ ==> temp_strengthening ([] P) ([] Q) h";
by (clarify_tac set_cs 1);
by (forward_tac [ex2seq_tsuffix] 1);
@@ -420,7 +420,7 @@
Goalw [temp_strengthening_def,state_strengthening_def,
temp_sat_def,satisfies_def,Init_def,unlift_def]
-"!! h. [| state_strengthening P Q h |]\
+"[| state_strengthening P Q h |]\
\ ==> temp_strengthening (Init P) (Init Q) h";
by (safe_tac set_cs);
by (pair_tac "ex" 1);
@@ -464,7 +464,7 @@
(* important property of ex2seq: can be shiftet, as defined "pointwise" *)
-Goal "!!ex. [| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL`(ex2seq ex) = ex2seq ex')";
+Goal "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL`(ex2seq ex) = ex2seq ex')";
by (pair_tac "ex" 1);
by (Seq_case_simp_tac "y" 1);
by (pair_tac "a" 1);
@@ -483,7 +483,7 @@
Goalw [temp_strengthening_def,state_strengthening_def,
temp_sat_def, satisfies_def,Next_def]
-"!! h. [| temp_strengthening P Q h |]\
+"[| temp_strengthening P Q h |]\
\ ==> temp_strengthening (Next P) (Next Q) h";
by (Asm_full_simp_tac 1);
by (safe_tac set_cs);
@@ -494,7 +494,7 @@
(* cons case *)
by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU,
ex2seq_abs_cex,cex_absSeq_TL RS sym, ex2seqnilTL])1);
-be conjE 1;
+by (etac conjE 1);
by (dtac TLex2seq 1);
by (assume_tac 1);
by Auto_tac;
@@ -508,7 +508,7 @@
Goal
-"!! h. [| state_weakening P Q h |]\
+"[| state_weakening P Q h |]\
\ ==> temp_weakening (Init P) (Init Q) h";
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2,
state_weakening_def2, temp_sat_def,satisfies_def,Init_def,unlift_def])1);
@@ -525,7 +525,7 @@
Goalw [Diamond_def]
-"!! h. [| temp_strengthening P Q h |]\
+"[| temp_strengthening P Q h |]\
\ ==> temp_strengthening (<> P) (<> Q) h";
by (rtac strength_NOT 1);
by (rtac weak_Box 1);
@@ -533,7 +533,7 @@
qed"strength_Diamond";
Goalw [Leadsto_def]
-"!! h. [| temp_weakening P1 P2 h;\
+"[| temp_weakening P1 P2 h;\
\ temp_strengthening Q1 Q2 h |]\
\ ==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h";
by (rtac strength_Box 1);
@@ -548,7 +548,7 @@
Goalw [Diamond_def]
-"!! h. [| temp_weakening P Q h |]\
+"[| temp_weakening P Q h |]\
\ ==> temp_weakening (<> P) (<> Q) h";
by (rtac weak_NOT 1);
by (rtac strength_Box 1);
@@ -556,7 +556,7 @@
qed"weak_Diamond";
Goalw [Leadsto_def]
-"!! h. [| temp_strengthening P1 P2 h;\
+"[| temp_strengthening P1 P2 h;\
\ temp_weakening Q1 Q2 h |]\
\ ==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h";
by (rtac weak_Box 1);
--- a/src/HOLCF/IOA/meta_theory/Asig.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/Asig.ML Fri Jan 29 16:23:56 1999 +0100
@@ -6,8 +6,6 @@
Action signatures
*)
-open Asig;
-
val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def];
Goal
@@ -17,23 +15,23 @@
by (simp_tac (simpset() addsimps asig_projections) 1);
qed "asig_triple_proj";
-Goal "!!a.[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
+Goal "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
qed"int_and_ext_is_act";
-Goal "!!a.[|a:externals(S)|] ==> a:actions(S)";
+Goal "[|a:externals(S)|] ==> a:actions(S)";
by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
qed"ext_is_act";
-Goal "!!a.[|a:internals S|] ==> a:actions S";
+Goal "[|a:internals S|] ==> a:actions S";
by (asm_full_simp_tac (simpset() addsimps [asig_internals_def,actions_def]) 1);
qed"int_is_act";
-Goal "!!a.[|a:inputs S|] ==> a:actions S";
+Goal "[|a:inputs S|] ==> a:actions S";
by (asm_full_simp_tac (simpset() addsimps [asig_inputs_def,actions_def]) 1);
qed"inp_is_act";
-Goal "!!a.[|a:outputs S|] ==> a:actions S";
+Goal "[|a:outputs S|] ==> a:actions S";
by (asm_full_simp_tac (simpset() addsimps [asig_outputs_def,actions_def]) 1);
qed"out_is_act";
@@ -41,19 +39,19 @@
by (fast_tac (claset() addSIs [ext_is_act]) 1 );
qed"ext_and_act";
-Goal "!!S. [|is_asig S;x: actions S|] ==> (x~:externals S) = (x: internals S)";
+Goal "[|is_asig S;x: actions S|] ==> (x~:externals S) = (x: internals S)";
by (asm_full_simp_tac (simpset() addsimps [actions_def,is_asig_def,externals_def]) 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (Blast_tac 1);
qed"not_ext_is_int";
-Goal "!!S. is_asig S ==> (x~:externals S) = (x: internals S | x~:actions S)";
+Goal "is_asig S ==> (x~:externals S) = (x: internals S | x~:actions S)";
by (asm_full_simp_tac (simpset() addsimps [actions_def,is_asig_def,externals_def]) 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (Blast_tac 1);
qed"not_ext_is_int_or_not_act";
Goalw [externals_def,actions_def,is_asig_def]
- "!! x. [| is_asig (S); x:internals S |] ==> x~:externals S";
+ "[| is_asig (S); x:internals S |] ==> x~:externals S";
by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (Blast_tac 1);
qed"int_is_not_ext";
--- a/src/HOLCF/IOA/meta_theory/Automata.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML Fri Jan 29 16:23:56 1999 +0100
@@ -9,12 +9,9 @@
(* this modification of the simpset is local to this file *)
Delsimps [split_paired_Ex];
-
-open reachable;
-
val ioa_projections = [asig_of_def, starts_of_def, trans_of_def,wfair_of_def,sfair_of_def];
-(* ----------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
section "asig_of, starts_of, trans_of";
@@ -29,7 +26,7 @@
qed "ioa_triple_proj";
Goalw [is_trans_of_def,actions_def, is_asig_def]
- "!!A. [| is_trans_of A; (s1,a,s2):trans_of(A) |] ==> a:act A";
+ "[| is_trans_of A; (s1,a,s2):trans_of(A) |] ==> a:act A";
by (REPEAT(etac conjE 1));
by (EVERY1[etac allE, etac impE, atac]);
by (Asm_full_simp_tac 1);
@@ -55,7 +52,7 @@
qed "trans_of_par";
-(* ----------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
section "actions and par";
@@ -107,7 +104,7 @@
asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1);
qed"internals_of_par";
-(* ---------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------ *)
section "actions and compatibility";
@@ -117,50 +114,50 @@
qed"compat_commute";
Goalw [externals_def,actions_def,compatible_def]
- "!! a. [| compatible A1 A2; a:ext A1|] ==> a~:int A2";
+ "[| compatible A1 A2; a:ext A1|] ==> a~:int A2";
by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (Blast_tac 1);
qed"ext1_is_not_int2";
(* just commuting the previous one: better commute compatible *)
Goalw [externals_def,actions_def,compatible_def]
- "!! a. [| compatible A2 A1 ; a:ext A1|] ==> a~:int A2";
+ "[| compatible A2 A1 ; a:ext A1|] ==> a~:int A2";
by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (Blast_tac 1);
qed"ext2_is_not_int1";
bind_thm("ext1_ext2_is_not_act2",ext1_is_not_int2 RS int_and_ext_is_act);
bind_thm("ext1_ext2_is_not_act1",ext2_is_not_int1 RS int_and_ext_is_act);
Goalw [externals_def,actions_def,compatible_def]
- "!! x. [| compatible A B; x:int A |] ==> x~:ext B";
+ "[| compatible A B; x:int A |] ==> x~:ext B";
by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (Blast_tac 1);
qed"intA_is_not_extB";
Goalw [externals_def,actions_def,compatible_def,is_asig_def,asig_of_def]
-"!! a. [| compatible A B; a:int A |] ==> a ~: act B";
+"[| compatible A B; a:int A |] ==> a ~: act B";
by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (Blast_tac 1);
qed"intA_is_not_actB";
(* the only one that needs disjointness of outputs and of internals and _all_ acts *)
Goalw [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def,
compatible_def,is_asig_def,asig_of_def]
-"!! a. [| compatible A B; a:out A ;a:act B|] ==> a : inp B";
+"[| compatible A B; a:out A ;a:act B|] ==> a : inp B";
by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (Blast_tac 1);
qed"outAactB_is_inpB";
(* needed for propagation of input_enabledness from A,B to A||B *)
Goalw [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def,
compatible_def,is_asig_def,asig_of_def]
-"!! a. [| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B";
+"[| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B";
by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (Blast_tac 1);
qed"inpAAactB_is_inpBoroutB";
-(* ---------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
section "input_enabledness and par";
@@ -169,7 +166,7 @@
1. inpAAactB_is_inpBoroutB ie. internals are really hidden.
2. inputs_of_par: outputs are no longer inputs of par. This is important here *)
Goalw [input_enabled_def]
-"!!A. [| compatible A B; input_enabled A; input_enabled B|] \
+"[| compatible A B; input_enabled A; input_enabled B|] \
\ ==> input_enabled (A||B)";
by (asm_full_simp_tac (simpset()addsimps[Let_def,inputs_of_par,trans_of_par])1);
by (safe_tac set_cs);
@@ -232,7 +229,7 @@
by (Asm_full_simp_tac 1);
qed"input_enabled_par";
-(* ---------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
section "invariants";
@@ -252,21 +249,23 @@
val [p1,p2] = goal thy
"[| !!s. s : starts_of(A) ==> P(s); \
-\ !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
+\ !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
\ |] ==> invariant A P";
by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1);
qed "invariantI1";
-val [p1,p2] = goalw thy [invariant_def]
-"[| invariant A P; reachable A s |] ==> P(s)";
- br(p2 RS (p1 RS spec RS mp))1;
+Goalw [invariant_def] "[| invariant A P; reachable A s |] ==> P(s)";
+by (Blast_tac 1);
qed "invariantE";
-(* ---------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
section "restrict";
+val reachable_0 = reachable.reachable_0
+and reachable_n = reachable.reachable_n;
+
Goal "starts_of(restrict ioa acts) = starts_of(ioa) & \
\ trans_of(restrict ioa acts) = trans_of(ioa)";
by (simp_tac (simpset() addsimps ([restrict_def]@ioa_projections)) 1);
@@ -300,18 +299,18 @@
by (simp_tac (simpset() addsimps [cancel_restrict_a,cancel_restrict_b,acts_restrict]) 1);
qed"cancel_restrict";
-(* ---------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
section "rename";
-Goal "!!f. s -a--(rename C f)-> t ==> (? x. Some(x) = f(a) & s -x--C-> t)";
+Goal "s -a--(rename C f)-> t ==> (? x. Some(x) = f(a) & s -x--C-> t)";
by (asm_full_simp_tac (simpset() addsimps [Let_def,rename_def,trans_of_def]) 1);
qed"trans_rename";
-Goal "!!s.[| reachable (rename C g) s |] ==> reachable C s";
+Goal "[| reachable (rename C g) s |] ==> reachable C s";
by (etac reachable.induct 1);
by (rtac reachable_0 1);
by (asm_full_simp_tac (simpset() addsimps [rename_def]@ioa_projections) 1);
@@ -324,49 +323,49 @@
-(* ---------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
section "trans_of(A||B)";
-Goal "!!A.[|(s,a,t):trans_of (A||B); a:act A|] \
+Goal "[|(s,a,t):trans_of (A||B); a:act A|] \
\ ==> (fst s,a,fst t):trans_of A";
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
qed"trans_A_proj";
-Goal "!!A.[|(s,a,t):trans_of (A||B); a:act B|] \
+Goal "[|(s,a,t):trans_of (A||B); a:act B|] \
\ ==> (snd s,a,snd t):trans_of B";
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
qed"trans_B_proj";
-Goal "!!A.[|(s,a,t):trans_of (A||B); a~:act A|]\
+Goal "[|(s,a,t):trans_of (A||B); a~:act A|]\
\ ==> fst s = fst t";
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
qed"trans_A_proj2";
-Goal "!!A.[|(s,a,t):trans_of (A||B); a~:act B|]\
+Goal "[|(s,a,t):trans_of (A||B); a~:act B|]\
\ ==> snd s = snd t";
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
qed"trans_B_proj2";
-Goal "!!A.(s,a,t):trans_of (A||B) \
+Goal "(s,a,t):trans_of (A||B) \
\ ==> a :act A | a :act B";
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
qed"trans_AB_proj";
-Goal "!!A. [|a:act A;a:act B;\
+Goal "[|a:act A;a:act B;\
\ (fst s,a,fst t):trans_of A;(snd s,a,snd t):trans_of B|]\
\ ==> (s,a,t):trans_of (A||B)";
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
qed"trans_AB";
-Goal "!!A. [|a:act A;a~:act B;\
+Goal "[|a:act A;a~:act B;\
\ (fst s,a,fst t):trans_of A;snd s=snd t|]\
\ ==> (s,a,t):trans_of (A||B)";
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
qed"trans_A_notB";
-Goal "!!A. [|a~:act A;a:act B;\
+Goal "[|a~:act A;a:act B;\
\ (snd s,a,snd t):trans_of B;fst s=fst t|]\
\ ==> (s,a,t):trans_of (A||B)";
by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
@@ -397,7 +396,7 @@
qed "trans_of_par4";
-(* ---------------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
section "proof obligation generator for IOA requirements";
@@ -407,12 +406,12 @@
qed"is_trans_of_par";
Goalw [is_trans_of_def]
-"!!A. is_trans_of A ==> is_trans_of (restrict A acts)";
+"is_trans_of A ==> is_trans_of (restrict A acts)";
by (asm_simp_tac (simpset() addsimps [cancel_restrict,acts_restrict])1);
qed"is_trans_of_restrict";
Goalw [is_trans_of_def,restrict_def,restrict_asig_def]
-"!!A. is_trans_of A ==> is_trans_of (rename A f)";
+"is_trans_of A ==> is_trans_of (rename A f)";
by (asm_full_simp_tac
(simpset() addsimps [Let_def,actions_def,trans_of_def, asig_internals_def,
asig_outputs_def,asig_inputs_def,externals_def,
@@ -420,31 +419,29 @@
by (Blast_tac 1);
qed"is_trans_of_rename";
-Goal "!! A. [| is_asig_of A; is_asig_of B; compatible A B|] \
+Goal "[| is_asig_of A; is_asig_of B; compatible A B|] \
\ ==> is_asig_of (A||B)";
by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,asig_of_par,
asig_comp_def,compatible_def,asig_internals_def,asig_outputs_def,
asig_inputs_def,actions_def,is_asig_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [asig_of_def]) 1);
by Auto_tac;
-by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
qed"is_asig_of_par";
Goalw [is_asig_of_def,is_asig_def,asig_of_def,restrict_def,restrict_asig_def,
asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,o_def]
-"!! A. is_asig_of A ==> is_asig_of (restrict A f)";
+"is_asig_of A ==> is_asig_of (restrict A f)";
by (Asm_full_simp_tac 1);
by Auto_tac;
-by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
qed"is_asig_of_restrict";
-Goal "!! A. is_asig_of A ==> is_asig_of (rename A f)";
+Goal "is_asig_of A ==> is_asig_of (rename A f)";
by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,
rename_def,rename_set_def,asig_internals_def,asig_outputs_def,
asig_inputs_def,actions_def,is_asig_def,asig_of_def]) 1);
by Auto_tac;
by (ALLGOALS(dres_inst_tac [("s","Some ?x")] sym THEN' Asm_full_simp_tac));
-by (ALLGOALS(best_tac (set_cs addEs [equalityCE])));
+by (ALLGOALS(Blast_tac));
qed"is_asig_of_rename";
@@ -453,28 +450,26 @@
Goalw [compatible_def]
-"!! A. [|compatible A B; compatible A C |]==> compatible A (B||C)";
+"[|compatible A B; compatible A C |]==> compatible A (B||C)";
by (asm_full_simp_tac (simpset() addsimps [internals_of_par,
outputs_of_par,actions_of_par]) 1);
by Auto_tac;
-by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
qed"compatible_par";
(* better derive by previous one and compat_commute *)
Goalw [compatible_def]
-"!! A. [|compatible A C; compatible B C |]==> compatible (A||B) C";
+"[|compatible A C; compatible B C |]==> compatible (A||B) C";
by (asm_full_simp_tac (simpset() addsimps [internals_of_par,
outputs_of_par,actions_of_par]) 1);
by Auto_tac;
-by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
qed"compatible_par2";
Goalw [compatible_def]
-"!! A. [| compatible A B; (ext B - S) Int ext A = {}|] \
+"[| compatible A B; (ext B - S) Int ext A = {}|] \
\ ==> compatible A (restrict B S)";
by (asm_full_simp_tac (simpset() addsimps [ioa_triple_proj,asig_triple_proj,
externals_def,restrict_def,restrict_asig_def,actions_def]) 1);
-by (auto_tac (claset() addEs [equalityCE],simpset()));
+by Auto_tac;
qed"compatible_restrict";
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML Fri Jan 29 16:23:56 1999 +0100
@@ -66,7 +66,7 @@
by (Simp_tac 1);
qed"mkex2_nil";
-Goal "!!x.[| x:act A; x~:act B; HD`exA=Def a|] \
+Goal "[| x:act A; x~:act B; HD`exA=Def a|] \
\ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
\ (x,snd a,t) >> (mkex2 A B`sch`(TL`exA)`exB) (snd a) t";
by (rtac trans 1);
@@ -75,7 +75,7 @@
by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
qed"mkex2_cons_1";
-Goal "!!x.[| x~:act A; x:act B; HD`exB=Def b|] \
+Goal "[| x~:act A; x:act B; HD`exB=Def b|] \
\ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
\ (x,s,snd b) >> (mkex2 A B`sch`exA`(TL`exB)) s (snd b)";
by (rtac trans 1);
@@ -84,7 +84,7 @@
by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
qed"mkex2_cons_2";
-Goal "!!x.[| x:act A; x:act B; HD`exA=Def a;HD`exB=Def b|] \
+Goal "[| x:act A; x:act B; HD`exA=Def a;HD`exB=Def b|] \
\ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
\ (x,snd a,snd b) >> \
\ (mkex2 A B`sch`(TL`exA)`(TL`exB)) (snd a) (snd b)";
@@ -109,7 +109,7 @@
by (simp_tac (simpset() addsimps [mkex_def]) 1);
qed"mkex_nil";
-Goal "!!x.[| x:act A; x~:act B |] \
+Goal "[| x:act A; x~:act B |] \
\ ==> mkex A B (x>>sch) (s,a>>exA) (t,exB) = \
\ ((s,t), (x,snd a,t) >> snd (mkex A B sch (snd a,exA) (t,exB)))";
by (simp_tac (simpset() addsimps [mkex_def]) 1);
@@ -117,7 +117,7 @@
by Auto_tac;
qed"mkex_cons_1";
-Goal "!!x.[| x~:act A; x:act B |] \
+Goal "[| x~:act A; x:act B |] \
\ ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) = \
\ ((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))";
by (simp_tac (simpset() addsimps [mkex_def]) 1);
@@ -125,7 +125,7 @@
by Auto_tac;
qed"mkex_cons_2";
-Goal "!!x.[| x:act A; x:act B |] \
+Goal "[| x:act A; x:act B |] \
\ ==> mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) = \
\ ((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))";
by (simp_tac (simpset() addsimps [mkex_def]) 1);
@@ -277,7 +277,7 @@
qed"stutterA_mkex";
-Goal "!! sch.[| \
+Goal "[| \
\ Forall (%x. x:act (A||B)) sch ; \
\ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\
\ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \
@@ -308,7 +308,7 @@
qed"stutterB_mkex";
-Goal "!! sch.[| \
+Goal "[| \
\ Forall (%x. x:act (A||B)) sch ; \
\ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\
\ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Fri Jan 29 16:23:56 1999 +0100
@@ -60,7 +60,7 @@
by (Simp_tac 1);
qed"mksch_nil";
-Goal "!!x.[|x:act A;x~:act B|] \
+Goal "[|x:act A;x~:act B|] \
\ ==> mksch A B`(x>>tr)`schA`schB = \
\ (Takewhile (%a. a:int A)`schA) \
\ @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a. a:int A)`schA)) \
@@ -71,7 +71,7 @@
by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"mksch_cons1";
-Goal "!!x.[|x~:act A;x:act B|] \
+Goal "[|x~:act A;x:act B|] \
\ ==> mksch A B`(x>>tr)`schA`schB = \
\ (Takewhile (%a. a:int B)`schB) \
\ @@ (x>>(mksch A B`tr`schA`(TL`(Dropwhile (%a. a:int B)`schB)) \
@@ -82,7 +82,7 @@
by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"mksch_cons2";
-Goal "!!x.[|x:act A;x:act B|] \
+Goal "[|x:act A;x:act B|] \
\ ==> mksch A B`(x>>tr)`schA`schB = \
\ (Takewhile (%a. a:int A)`schA) \
\ @@ ((Takewhile (%a. a:int B)`schB) \
@@ -199,7 +199,7 @@
(* safe-tac makes too many case distinctions with this lemma in the next proof *)
Delsimps [FiniteConc];
-Goal "!! tr. [| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==> \
+Goal "[| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==> \
\ ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y & \
\ Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr & \
\ Filter (%a. a:ext B)`y = Filter (%a. a:act B)`tr &\
@@ -272,7 +272,7 @@
(* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *)
Delsimps [FilterConc];
-Goal " !!bs. [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==> \
+Goal " [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==> \
\! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs &\
\ Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) \
\ --> (? y1 y2. (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) & \
@@ -326,7 +326,7 @@
Delsimps [FilterConc];
-Goal " !!as. [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==> \
+Goal " [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==> \
\! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) as &\
\ Filter (%a. a:ext A)`x = Filter (%a. a:act A)`(as @@ z) \
\ --> (? x1 x2. (mksch A B`(as @@ z)`x`y) = (x1 @@ (mksch A B`z`x2`y)) & \
@@ -379,7 +379,7 @@
(*
-Goal "!! y.Finite y ==> ! z tr. Forall (%a.a:ext (A||B)) tr & \
+Goal "Finite y ==> ! z tr. Forall (%a.a:ext (A||B)) tr & \
\ y = z @@ mksch A B`tr`a`b\
\ --> Finite tr";
by (etac Seq_Finite_ind 1);
--- a/src/HOLCF/IOA/meta_theory/Compositionality.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML Fri Jan 29 16:23:56 1999 +0100
@@ -8,7 +8,7 @@
-Goal "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA";
+Goal "[|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA";
by Auto_tac;
qed"compatibility_consequence3";
@@ -27,12 +27,11 @@
(* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A) *)
-Goal "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA";
+Goal "[|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA";
by Auto_tac;
qed"compatibility_consequence4";
-Goal
-"!! A B. [| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \
+Goal "[| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \
\ Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
by (rtac ForallPFilterQR 1);
by (assume_tac 2);
@@ -48,8 +47,7 @@
-Goal "!! A1 A2 B1 B2. \
-\ [| is_trans_of A1; is_trans_of A2; is_trans_of B1; is_trans_of B2;\
+Goal "[| is_trans_of A1; is_trans_of A2; is_trans_of B1; is_trans_of B2;\
\ is_asig_of A1; is_asig_of A2; \
\ is_asig_of B1; is_asig_of B2; \
\ compatible A1 B1; compatible A2 B2; \
--- a/src/HOLCF/IOA/meta_theory/Deadlock.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML Fri Jan 29 16:23:56 1999 +0100
@@ -10,14 +10,14 @@
input actions may always be added to a schedule
**********************************************************************************)
-Goal "!! sch. [| Filter (%x. x:act A)`sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
+Goal "[| Filter (%x. x:act A)`sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
\ ==> Filter (%x. x:act A)`sch @@ a>>nil : schedules A";
by (asm_full_simp_tac (simpset() addsimps [schedules_def,has_schedule_def]) 1);
by (safe_tac set_cs);
by (forward_tac [inp_is_act] 1);
by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
by (pair_tac "ex" 1);
-ren "sch s ex" 1;
+ren "s ex" 1;
by (subgoal_tac "Finite ex" 1);
by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 2);
by (rtac (Map2Finite RS iffD1) 2);
@@ -51,7 +51,7 @@
and distributivity of is_exec_frag over @@
**********************************************************************************)
Delsplits [split_if];
-Goal "!! sch. [| a : local A; Finite sch; sch : schedules (A||B); \
+Goal "[| a : local A; Finite sch; sch : schedules (A||B); \
\ Filter (%x. x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
\ ==> (sch @@ a>>nil) : schedules (A||B)";
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.ML Fri Jan 29 16:23:56 1999 +0100
@@ -10,7 +10,7 @@
Delsimps [split_paired_Ex];
Goalw [live_implements_def]
-"!! A. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] \
+"[| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] \
\ ==> live_implements (A,LA) (C,LC)";
by Auto_tac;
qed"live_implements_trans";
@@ -24,7 +24,7 @@
(* ---------------------------------------------------------------- *)
-Goal "!! f. [| inp(C)=inp(A); out(C)=out(A); \
+Goal "[| inp(C)=inp(A); out(C)=out(A); \
\ is_live_ref_map f (C,M) (A,L) |] \
\ ==> live_implements (C,M) (A,L)";
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Fri Jan 29 16:23:56 1999 +0100
@@ -62,7 +62,7 @@
section"properties of move";
Goalw [is_ref_map_def]
- "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
+ "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
\ move A (@x. move A x (f s) a (f t)) (f s) a (f t)";
by (subgoal_tac "? ex. move A ex (f s) a (f t)" 1);
@@ -73,7 +73,7 @@
qed"move_is_move";
Goal
- "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
+ "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
\ is_exec_frag A (f s,@x. move A x (f s) a (f t))";
by (cut_inst_tac [] move_is_move 1);
by (REPEAT (assume_tac 1));
@@ -81,7 +81,7 @@
qed"move_subprop1";
Goal
- "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
+ "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
\ Finite ((@x. move A x (f s) a (f t)))";
by (cut_inst_tac [] move_is_move 1);
by (REPEAT (assume_tac 1));
@@ -89,7 +89,7 @@
qed"move_subprop2";
Goal
- "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
+ "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
\ laststate (f s,@x. move A x (f s) a (f t)) = (f t)";
by (cut_inst_tac [] move_is_move 1);
by (REPEAT (assume_tac 1));
@@ -97,7 +97,7 @@
qed"move_subprop3";
Goal
- "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
+ "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
\ mk_trace A`((@x. move A x (f s) a (f t))) = \
\ (if a:ext A then a>>nil else nil)";
@@ -131,7 +131,7 @@
------------------------------------------------------- *)
Delsplits[split_if];
Goalw [corresp_ex_def]
- "!!f.[|is_ref_map f C A; ext C = ext A|] ==> \
+ "[|is_ref_map f C A; ext C = ext A|] ==> \
\ !s. reachable C s & is_exec_frag C (s,xs) --> \
\ mk_trace C`xs = mk_trace A`(snd (corresp_ex A f (s,xs)))";
@@ -180,7 +180,7 @@
Goalw [corresp_ex_def]
- "!!f.[| is_ref_map f C A |] ==>\
+ "[| is_ref_map f C A |] ==>\
\ !s. reachable C s & is_exec_frag C (s,xs) \
\ --> is_exec_frag A (corresp_ex A f (s,xs))";
@@ -221,7 +221,7 @@
Goalw [traces_def]
- "!!f. [| ext C = ext A; is_ref_map f C A |] \
+ "[| ext C = ext A; is_ref_map f C A |] \
\ ==> traces C <= traces A";
by (simp_tac(simpset() addsimps [has_trace_def2])1);
@@ -260,15 +260,13 @@
qed"fininf";
-Goal
-"is_wfair A W (s,ex) = \
+Goal "is_wfair A W (s,ex) = \
\ (fin_often (%x. ~Enabled A W (snd x)) ex --> inf_often (%x. fst x :W) ex)";
by (asm_full_simp_tac (simpset() addsimps [is_wfair_def,fin_often_def])1);
by Auto_tac;
qed"WF_alt";
-Goal
-"!! ex. [|is_wfair A W (s,ex); inf_often (%x. Enabled A W (snd x)) ex; \
+Goal "[|is_wfair A W (s,ex); inf_often (%x. Enabled A W (snd x)) ex; \
\ en_persistent A W|] \
\ ==> inf_often (%x. fst x :W) ex";
by (dtac persistent 1);
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Fri Jan 29 16:23:56 1999 +0100
@@ -15,21 +15,21 @@
section "transitions and moves";
-Goal"!!f. s -a--A-> t ==> ? ex. move A ex s a t";
+Goal "s -a--A-> t ==> ? ex. move A ex s a t";
by (res_inst_tac [("x","(a,t)>>nil")] exI 1);
by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
qed"transition_is_ex";
-Goal"!!f. (~a:ext A) & s=t ==> ? ex. move A ex s a t";
+Goal "(~a:ext A) & s=t ==> ? ex. move A ex s a t";
by (res_inst_tac [("x","nil")] exI 1);
by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
qed"nothing_is_ex";
-Goal"!!f. (s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A) \
+Goal "(s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A) \
\ ==> ? ex. move A ex s a s''";
by (res_inst_tac [("x","(a,s')>>(a',s'')>>nil")] exI 1);
@@ -37,8 +37,7 @@
qed"ei_transitions_are_ex";
-Goal
-"!!f. (s1 -a1--A-> s2) & (s2 -a2--A-> s3) & (s3 -a3--A-> s4) &\
+Goal "(s1 -a1--A-> s2) & (s2 -a2--A-> s3) & (s3 -a3--A-> s4) &\
\ (~a2:ext A) & (~a3:ext A) ==> \
\ ? ex. move A ex s1 a1 s4";
@@ -53,7 +52,7 @@
Goalw [is_weak_ref_map_def,is_ref_map_def]
- "!!f. [| ext C = ext A; \
+ "[| ext C = ext A; \
\ is_weak_ref_map f C A |] ==> is_ref_map f C A";
by (safe_tac set_cs);
by (case_tac "a:ext A" 1);
@@ -69,7 +68,7 @@
val lemma = result();
Delsplits [split_if];
-Goal "!!f.[| is_weak_ref_map f C A |]\
+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);
--- a/src/HOLCF/IOA/meta_theory/Seq.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.ML Fri Jan 29 16:23:56 1999 +0100
@@ -47,7 +47,7 @@
qed"smap_UU";
Goal
-"!!x.[|x~=UU|] ==> smap`f`(x##xs)= (f`x)##smap`f`xs";
+"[|x~=UU|] ==> smap`f`(x##xs)= (f`x)##smap`f`xs";
by (rtac trans 1);
by (stac smap_unfold 1);
by (Asm_full_simp_tac 1);
@@ -74,7 +74,7 @@
qed"sfilter_UU";
Goal
-"!!x. x~=UU ==> sfilter`P`(x##xs)= \
+"x~=UU ==> sfilter`P`(x##xs)= \
\ (If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)";
by (rtac trans 1);
by (stac sfilter_unfold 1);
@@ -102,7 +102,7 @@
qed"sforall2_UU";
Goal
-"!!x. x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)";
+"x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)";
by (rtac trans 1);
by (stac sforall2_unfold 1);
by (Asm_full_simp_tac 1);
@@ -131,7 +131,7 @@
qed"stakewhile_UU";
Goal
-"!!x. x~=UU ==> stakewhile`P`(x##xs) = \
+"x~=UU ==> stakewhile`P`(x##xs) = \
\ (If P`x then x##(stakewhile`P`xs) else nil fi)";
by (rtac trans 1);
by (stac stakewhile_unfold 1);
@@ -160,7 +160,7 @@
qed"sdropwhile_UU";
Goal
-"!!x. x~=UU ==> sdropwhile`P`(x##xs) = \
+"x~=UU ==> sdropwhile`P`(x##xs) = \
\ (If P`x then sdropwhile`P`xs else x##xs fi)";
by (rtac trans 1);
by (stac sdropwhile_unfold 1);
@@ -191,7 +191,7 @@
qed"slast_UU";
Goal
-"!!x. x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)";
+"x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)";
by (rtac trans 1);
by (stac slast_unfold 1);
by (Asm_full_simp_tac 1);
@@ -281,20 +281,20 @@
by (Simp_tac 1);
qed"szip_UU1";
-Goal "!!x. x~=nil ==> szip`x`UU=UU";
+Goal "x~=nil ==> szip`x`UU=UU";
by (stac szip_unfold 1);
by (Asm_full_simp_tac 1);
by (res_inst_tac [("x","x")] seq.casedist 1);
by (REPEAT (Asm_full_simp_tac 1));
qed"szip_UU2";
-Goal "!!x. x~=UU ==> szip`(x##xs)`nil=UU";
+Goal "x~=UU ==> szip`(x##xs)`nil=UU";
by (rtac trans 1);
by (stac szip_unfold 1);
by (REPEAT (Asm_full_simp_tac 1));
qed"szip_cons_nil";
-Goal "!!x.[| x~=UU; y~=UU|] ==> szip`(x##xs)`(y##ys) = <x,y>##szip`xs`ys";
+Goal "[| x~=UU; y~=UU|] ==> szip`(x##xs)`(y##ys) = <x,y>##szip`xs`ys";
by (rtac trans 1);
by (stac szip_unfold 1);
by (REPEAT (Asm_full_simp_tac 1));
@@ -317,13 +317,13 @@
section "scons, nil";
Goal
- "!!x. [|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)";
+ "[|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)";
by (rtac iffI 1);
by (etac (hd seq.injects) 1);
by Auto_tac;
qed"scons_inject_eq";
-Goal "!!x. nil<<x ==> nil=x";
+Goal "nil<<x ==> nil=x";
by (res_inst_tac [("x","x")] seq.casedist 1);
by (hyp_subst_tac 1);
by (etac antisym_less 1);
@@ -416,7 +416,7 @@
by (fast_tac (HOL_cs addSDs seq.injects) 1);
qed"Finite_cons_a";
-Goal "!!x. a~=UU ==>(Finite (a##x)) = (Finite x)";
+Goal "a~=UU ==>(Finite (a##x)) = (Finite x)";
by (rtac iffI 1);
by (rtac (Finite_cons_a RS mp RS mp RS mp) 1);
by (REPEAT (assume_tac 1));
@@ -448,8 +448,7 @@
]);
-Goal
-"!!P.[|P(UU);P(nil);\
+Goal "!!P.[|P(UU);P(nil);\
\ !! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)\
\ |] ==> seq_finite(s) --> P(s)";
by (rtac seq_finite_ind_lemma 1);
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Fri Jan 29 16:23:56 1999 +0100
@@ -167,7 +167,7 @@
by (Simp_tac 1);
qed"Zip_UU1";
-Goal "!! x. x~=nil ==> Zip`x`UU =UU";
+Goal "x~=nil ==> Zip`x`UU =UU";
by (stac Zip_unfold 1);
by (Simp_tac 1);
by (res_inst_tac [("x","x")] seq.casedist 1);
@@ -384,11 +384,11 @@
qed"Finite_Cons";
Addsimps [Finite_Cons];
-Goal "!! x. Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)";
+Goal "Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)";
by (Seq_Finite_induct_tac 1);
qed"FiniteConc_1";
-Goal "!! z. Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)";
+Goal "Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)";
by (Seq_Finite_induct_tac 1);
(* nil*)
by (strip_tac 1);
@@ -415,11 +415,11 @@
Addsimps [FiniteConc];
-Goal "!! s. Finite s ==> Finite (Map f`s)";
+Goal "Finite s ==> Finite (Map f`s)";
by (Seq_Finite_induct_tac 1);
qed"FiniteMap1";
-Goal "!! s. Finite s ==> ! t. (s = Map f`t) --> Finite t";
+Goal "Finite s ==> ! t. (s = Map f`t) --> Finite t";
by (Seq_Finite_induct_tac 1);
by (strip_tac 1);
by (Seq_case_simp_tac "t" 1);
@@ -438,7 +438,7 @@
qed"Map2Finite";
-Goal "!! s. Finite s ==> Finite (Filter P`s)";
+Goal "Finite s ==> Finite (Filter P`s)";
by (Seq_Finite_induct_tac 1);
qed"FiniteFilter";
@@ -519,11 +519,11 @@
section "Last";
-Goal "!! s. Finite s ==> s~=nil --> Last`s~=UU";
+Goal "Finite s ==> s~=nil --> Last`s~=UU";
by (Seq_Finite_induct_tac 1);
qed"Finite_Last1";
-Goal "!! s. Finite s ==> Last`s=UU --> s=nil";
+Goal "Finite s ==> Last`s=UU --> s=nil";
by (Seq_Finite_induct_tac 1);
by (fast_tac HOL_cs 1);
qed"Finite_Last2";
@@ -587,7 +587,7 @@
by (Seq_induct_tac "x" [Forall_def,sforall_def] 1);
qed"Forall_Conc_impl";
-Goal "!! x. Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)";
+Goal "Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)";
by (Seq_Finite_induct_tac 1);
qed"Forall_Conc";
@@ -619,7 +619,7 @@
bind_thm ("Forall_prefixclosed",Forall_prefix RS spec RS mp RS mp);
-Goal "!! h. [| Finite h; Forall P s; s= h @@ t |] ==> Forall P t";
+Goal "[| Finite h; Forall P s; s= h @@ t |] ==> Forall P t";
by Auto_tac;
qed"Forall_postfixclosed";
@@ -658,7 +658,7 @@
(* holds also in other direction *)
-Goal "!! P. ~Finite ys & Forall (%x. ~P x) ys \
+Goal "~Finite ys & Forall (%x. ~P x) ys \
\ --> Filter P`ys = UU ";
by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
qed"ForallnPFilterPUU1";
@@ -685,7 +685,7 @@
(* inverse of ForallnPFilterPUU. proved by 2 lemmas because of adm problems *)
-Goal "!! ys. Finite ys ==> Filter P`ys ~= UU";
+Goal "Finite ys ==> Filter P`ys ~= UU";
by (Seq_Finite_induct_tac 1);
qed"FilterUU_nFinite_lemma1";
@@ -693,7 +693,7 @@
by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
qed"FilterUU_nFinite_lemma2";
-Goal "!! P. Filter P`ys = UU ==> \
+Goal "Filter P`ys = UU ==> \
\ (Forall (%x. ~P x) ys & ~Finite ys)";
by (rtac conjI 1);
by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1);
@@ -775,7 +775,7 @@
bind_thm("TakewhileConc",TakewhileConc1 RS mp);
-Goal "!! s. Finite s ==> Forall P s --> Dropwhile P`(s @@ t) = Dropwhile P`t";
+Goal "Finite s ==> Forall P s --> Dropwhile P`(s @@ t) = Dropwhile P`t";
by (Seq_Finite_induct_tac 1);
qed"DropwhileConc1";
@@ -804,7 +804,7 @@
by (Asm_full_simp_tac 1);
qed"divide_Seq_lemma";
-Goal "!! x. (x>>xs) << Filter P`y \
+Goal "(x>>xs) << Filter P`y \
\ ==> y = ((Takewhile (%a. ~ P a)`y) @@ (x >> TL`(Dropwhile (%a.~P a)`y))) \
\ & Finite (Takewhile (%a. ~ P a)`y) & P x";
by (rtac (divide_Seq_lemma RS mp) 1);
@@ -820,7 +820,7 @@
qed"nForall_HDFilter";
-Goal "!!y. ~Forall P y \
+Goal "~Forall P y \
\ ==> ? x. y= (Takewhile P`y @@ (x >> TL`(Dropwhile P`y))) & \
\ Finite (Takewhile P`y) & (~ P x)";
by (dtac (nForall_HDFilter RS mp) 1);
@@ -831,7 +831,7 @@
qed"divide_Seq2";
-Goal "!! y. ~Forall P y \
+Goal "~Forall P y \
\ ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)";
by (cut_inst_tac [] divide_Seq2 1);
(*Auto_tac no longer proves it*)
@@ -864,7 +864,7 @@
qed"take_reduction1";
-Goal "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 = seq_take k`y2|] \
+Goal "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k`y1 = seq_take k`y2|] \
\ ==> seq_take n`(x @@ (s>>y1)) = seq_take n`(y @@ (t>>y2))";
by (auto_tac (claset() addSIs [take_reduction1 RS spec RS mp],simpset()));
@@ -1117,13 +1117,13 @@
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
qed"Filter_lemma1";
-Goal "!! s. Finite s ==> \
+Goal "Finite s ==> \
\ (Forall (%x. (~P x) | (~ Q x)) s \
\ --> Filter P`(Filter Q`s) = nil)";
by (Seq_Finite_induct_tac 1);
qed"Filter_lemma2";
-Goal "!! s. Finite s ==> \
+Goal "Finite s ==> \
\ Forall (%x. (~P x) | (~ Q x)) s \
\ --> Filter (%x. P x & Q x)`s = nil";
by (Seq_Finite_induct_tac 1);
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Fri Jan 29 16:23:56 1999 +0100
@@ -61,7 +61,7 @@
(* ---------------------------------------------------------------- *)
Goalw [Cut_def]
-"!! s. [| Forall (%a.~ P a) s; Finite s|] \
+"[| Forall (%a.~ P a) s; Finite s|] \
\ ==> Cut P s =nil";
by (subgoal_tac "Filter P`s = nil" 1);
by (asm_simp_tac (simpset() addsimps [oraclebuild_nil]) 1);
@@ -70,7 +70,7 @@
qed"Cut_nil";
Goalw [Cut_def]
-"!! s. [| Forall (%a.~ P a) s; ~Finite s|] \
+"[| Forall (%a.~ P a) s; ~Finite s|] \
\ ==> Cut P s =UU";
by (subgoal_tac "Filter P`s= UU" 1);
by (asm_simp_tac (simpset() addsimps [oraclebuild_UU]) 1);
@@ -79,7 +79,7 @@
qed"Cut_UU";
Goalw [Cut_def]
-"!! s. [| P t; Forall (%x.~ P x) ss; Finite ss|] \
+"[| P t; Forall (%x.~ P x) ss; Finite ss|] \
\ ==> Cut P (ss @@ (t>> rs)) \
\ = ss @@ (t >> Cut P rs)";
@@ -200,7 +200,7 @@
Goalw [schedules_def,has_schedule_def]
- "!! sch. [|sch : schedules A ; tr = Filter (%a. a:ext A)`sch|] \
+ "[|sch : schedules A ; tr = Filter (%a. a:ext A)`sch|] \
\ ==> ? sch. sch : schedules A & \
\ tr = Filter (%a. a:ext A)`sch &\
\ LastActExtsch A sch";
@@ -239,7 +239,7 @@
(* ---------------------------------------------------------------- *)
Goalw [LastActExtsch_def]
- "!! A. [| LastActExtsch A sch; Filter (%x. x:ext A)`sch = nil |] \
+ "[| LastActExtsch A sch; Filter (%x. x:ext A)`sch = nil |] \
\ ==> sch=nil";
by (dtac FilternPnilForallP 1);
by (etac conjE 1);
@@ -249,7 +249,7 @@
qed"LastActExtimplnil";
Goalw [LastActExtsch_def]
- "!! A. [| LastActExtsch A sch; Filter (%x. x:ext A)`sch = UU |] \
+ "[| LastActExtsch A sch; Filter (%x. x:ext A)`sch = UU |] \
\ ==> sch=UU";
by (dtac FilternPUUForallP 1);
by (etac conjE 1);
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Fri Jan 29 16:23:56 1999 +0100
@@ -69,7 +69,7 @@
Delsimps [Let_def];
Goalw [is_simulation_def]
- "!!f. [|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==>\
+ "[|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==>\
\ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
\ (t,T'): R & move A (@ex2. move A ex2 s' a T') s' a T'";
@@ -99,7 +99,7 @@
Addsimps [Let_def];
Goal
- "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
+ "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
\ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
\ is_exec_frag A (s',@x. move A x s' a T')";
by (cut_inst_tac [] move_is_move_sim 1);
@@ -108,7 +108,7 @@
qed"move_subprop1_sim";
Goal
- "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
+ "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
\ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
\ Finite (@x. move A x s' a T')";
by (cut_inst_tac [] move_is_move_sim 1);
@@ -117,7 +117,7 @@
qed"move_subprop2_sim";
Goal
- "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
+ "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
\ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
\ laststate (s',@x. move A x s' a T') = T'";
by (cut_inst_tac [] move_is_move_sim 1);
@@ -126,7 +126,7 @@
qed"move_subprop3_sim";
Goal
- "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
+ "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
\ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
\ mk_trace A`((@x. move A x s' a T')) = \
\ (if a:ext A then a>>nil else nil)";
@@ -136,7 +136,7 @@
qed"move_subprop4_sim";
Goal
- "!!f. [|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
+ "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
\ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
\ (t,T'):R";
by (cut_inst_tac [] move_is_move_sim 1);
@@ -158,7 +158,7 @@
Delsplits[split_if];
Goal
- "!!f.[|is_simulation R C A; ext C = ext A|] ==> \
+ "[|is_simulation R C A; ext C = ext A|] ==> \
\ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> \
\ mk_trace C`ex = mk_trace A`((corresp_ex_simC A R`ex) s')";
@@ -188,7 +188,7 @@
Goal
- "!!f.[| is_simulation R C A |] ==>\
+ "[| is_simulation R C A |] ==>\
\ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R \
\ --> is_exec_frag A (s',(corresp_ex_simC A R`ex) s')";
@@ -240,7 +240,7 @@
S':= @s'. (s,s'):R & s':starts_of A, where s:starts_of C *)
Goal
-"!!C. [| is_simulation R C A; s:starts_of C |] \
+"[| is_simulation R C A; s:starts_of C |] \
\ ==> let S' = @s'. (s,s'):R & s':starts_of A in \
\ (s,S'):R & S':starts_of A";
by (asm_full_simp_tac (simpset() addsimps [is_simulation_def,
@@ -259,7 +259,7 @@
Goalw [traces_def]
- "!!f. [| ext C = ext A; is_simulation R C A |] \
+ "[| ext C = ext A; is_simulation R C A |] \
\ ==> traces C <= traces A";
by (simp_tac(simpset() addsimps [has_trace_def2])1);
--- a/src/HOLCF/IOA/meta_theory/TL.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/TL.ML Fri Jan 29 16:23:56 1999 +0100
@@ -50,7 +50,7 @@
qed"reflT";
-Goal "!!x. [| suffix y x ; suffix z y |] ==> suffix z x";
+Goal "[| suffix y x ; suffix z y |] ==> suffix z x";
by (asm_full_simp_tac (simpset() addsimps [suffix_def])1);
by Auto_tac;
by (res_inst_tac [("x","s1 @@ s1a")] exI 1);
@@ -79,21 +79,21 @@
(* TLA Rules by Lamport *)
(* ---------------------------------------------------------------- *)
-Goal "!! P. validT P ==> validT ([] P)";
+Goal "validT P ==> validT ([] P)";
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Box_def,tsuffix_def])1);
qed"STL1a";
-Goal "!! P. valid P ==> validT (Init P)";
+Goal "valid P ==> validT (Init P)";
by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,Init_def])1);
qed"STL1b";
-Goal "!! P. valid P ==> validT ([] (Init P))";
+Goal "valid P ==> validT ([] (Init P))";
by (rtac STL1a 1);
by (etac STL1b 1);
qed"STL1";
(* Note that unlift and HD is not at all used !!! *)
-Goal "!! P. valid (P .--> Q) ==> validT ([] (Init P) .--> [] (Init Q))";
+Goal "valid (P .--> Q) ==> validT ([] (Init P) .--> [] (Init Q))";
by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,IMPLIES_def,Box_def,Init_def])1);
qed"STL4";
@@ -158,11 +158,11 @@
-Goal "!! P. [| validT (P .--> Q); validT P |] ==> validT Q";
+Goal "[| validT (P .--> Q); validT P |] ==> validT Q";
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,IMPLIES_def])1);
qed"ModusPonens";
(* works only if validT is defined without restriction to s~=UU, s~=nil *)
-Goal "!! P. validT P ==> validT (Next P)";
+Goal "validT P ==> validT (Next P)";
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Next_def])1);
(* qed"NextTauto"; *)
--- a/src/HOLCF/IOA/meta_theory/TLS.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.ML Fri Jan 29 16:23:56 1999 +0100
@@ -86,21 +86,21 @@
after the translation via ex2seq !! *)
Goalw [Init_def,Next_def,temp_sat_def,satisfies_def,IMPLIES_def,AND_def]
- "!! A. [| ! s a t. (P s) & s-a--A-> t --> (Q t) |]\
+ "[| ! s a t. (P s) & s-a--A-> t --> (Q t) |]\
\ ==> ex |== (Init (%(s,a,t). P s) .& Init (%(s,a,t). s -a--A-> t) \
\ .--> (Next (Init (%(s,a,t).Q s))))";
by (clarify_tac set_cs 1);
by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
(* TL = UU *)
-br conjI 1;
+by (rtac conjI 1);
by (pair_tac "ex" 1);
by (Seq_case_simp_tac "y" 1);
by (pair_tac "a" 1);
by (Seq_case_simp_tac "s" 1);
by (pair_tac "a" 1);
(* TL = nil *)
-br conjI 1;
+by (rtac conjI 1);
by (pair_tac "ex" 1);
by (Seq_case_simp_tac "y" 1);
by (asm_full_simp_tac (simpset() addsimps [unlift_def])1);