--- a/src/HOLCF/IOA/meta_theory/Abstraction.ML Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML Thu Nov 26 16:37:56 1998 +0100
@@ -185,29 +185,6 @@
by (pair_induct_tac "xs" [] 1);
qed"traces_coincide_abs";
-(*
-FIX: Is this needed anywhere?
-
-Goalw [cex_abs_def]
- "!!f.[| is_abstraction h C A |] ==>\
-\ !s. reachable C s & is_exec_frag C (s,xs) \
-\ --> is_exec_frag A (cex_abs h (s,xs))";
-
-by (Asm_full_simp_tac 1);
-by (pair_induct_tac "xs" [is_exec_frag_def] 1);
-(* main case *)
-by (safe_tac set_cs);
-(* Stepd correspond to each other *)
-by (asm_full_simp_tac (simpset() addsimps [is_abstraction_def])1);
-(* IH *)
-(* reachable_n looping, therefore apply it manually *)
-by (eres_inst_tac [("x","y")] allE 1);
-by (Asm_full_simp_tac 1);
-by (forward_tac [reachable.reachable_n] 1);
-by (assume_tac 1);
-by (Asm_full_simp_tac 1);
-qed_spec_mp"correp_is_exec_abs";
-*)
(* Does not work with abstraction_is_ref_map as proof of abs_safety, because
is_live_abstraction includes temp_strengthening which is necessarily based
@@ -403,6 +380,8 @@
qed"ex2seq_tsuffix";
+(* FIX: NAch Sequence.ML bringen *)
+
Goal "(Map f`s = nil) = (s=nil)";
by (Seq_case_simp_tac "s" 1);
qed"Mapnil";
@@ -540,26 +519,6 @@
qed"weak_Init";
-(*
-
-(* analog to strengthening thm above, with analog lemmas used *)
-
-Goalw [state_weakening_def]
-"!! h. [| temp_weakening P Q h |]\
-\ ==> temp_weakening ([] P) ([] Q) h";
-by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2,
- temp_sat_def,satisfies_def,Box_def])1);
-
-(* analog to strengthening thm above, with analog lemmas used *)
-
-Goalw [state_weakening_def]
-"!! h. [| temp_weakening P Q h |]\
-\ ==> temp_weakening (Next P) (Next Q) h";
-by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2,
- temp_sat_def,satisfies_def,Next_def])1);
-
-*)
-
(* ---------------------------------------------------------------- *)
(* Localizing Temproal Strengthenings - 3 *)
(* ---------------------------------------------------------------- *)
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Thu Nov 26 16:37:56 1998 +0100
@@ -70,12 +70,12 @@
ex2seq_abs_cex
"ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)"
-(* analog to the proved thm strength_Box *)
+(* analog to the proved thm strength_Box - proof skipped as trivial *)
weak_Box
"temp_weakening P Q h
==> temp_weakening ([] P) ([] Q) h"
-(* analog to the proved thm strength_Next *)
+(* analog to the proved thm strength_Next - proof skipped as trivial *)
weak_Next
"temp_weakening P Q h
==> temp_weakening (Next P) (Next Q) h"
--- a/src/HOLCF/IOA/meta_theory/Automata.ML Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML Thu Nov 26 16:37:56 1998 +0100
@@ -460,7 +460,7 @@
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
qed"compatible_par";
-(* FIX: better derive by previous one and compat_commute *)
+(* better derive by previous one and compat_commute *)
Goalw [compatible_def]
"!! A. [|compatible A C; compatible B C |]==> compatible (A||B) C";
by (asm_full_simp_tac (simpset() addsimps [internals_of_par,
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML Thu Nov 26 16:37:56 1998 +0100
@@ -179,7 +179,7 @@
(* Schedules of A||B have only A- or B-actions *)
(* --------------------------------------------------------------------- *)
-(* FIX: very similar to lemma_1_1c, but it is not checking if every action element of
+(* very similar to lemma_1_1c, but it is not checking if every action element of
an ex is in A or B, but after projecting it onto the action schedule. Of course, this
is the same proposition, but we cannot change this one, when then rather lemma_1_1c *)
--- a/src/HOLCF/IOA/meta_theory/Compositionality.ML Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML Thu Nov 26 16:37:56 1998 +0100
@@ -25,8 +25,7 @@
qed"Filter_actAisFilter_extA";
-(* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A)
- or even better A||B= B||A, FIX *)
+(* 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";
by Auto_tac;
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.ML Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.ML Thu Nov 26 16:37:56 1998 +0100
@@ -56,18 +56,3 @@
(*
-
-(* Classical Fairness and Fairness by Temporal Formula coincide *)
-
-Goal "!! ex. Finite (snd ex) ==> \
-\ (ex |== WF A acts) = (~ Enabled A acts (laststate ex))";
-
-In 3 steps:
-
-1) []<>P and <>[]P mean both P (Last`s)
-2) Transform this to executions and laststate
-3) plift is used to show that plift (laststate ex) : acts == False.
-
-
-
-*)
\ No newline at end of file
--- a/src/HOLCF/IOA/meta_theory/Pred.thy Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Pred.thy Thu Nov 26 16:37:56 1998 +0100
@@ -1,14 +1,10 @@
-(* Title: HOLCF/IOA/meta_theory/TLS.thy
+(* Title: HOLCF/IOA/meta_theory/Pred.thy
ID: $Id$
Author: Olaf M"uller
Copyright 1997 TU Muenchen
Logical Connectives lifted to predicates.
-ToDo:
-
-<--> einfuehren.
-
*)
Pred = Arith +
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Thu Nov 26 16:37:56 1998 +0100
@@ -39,7 +39,8 @@
rules
(* Axioms for fair trace inclusion proof support, not for the correctness proof
- of refeinment mappings ! *)
+ of refinement mappings !
+ Note: Everything is superseded by LiveIOA.thy! *)
corresp_laststate
"Finite ex ==> laststate (corresp_ex A f (s,ex)) = f (laststate (s,ex))"
--- a/src/HOLCF/IOA/meta_theory/Seq.ML Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.ML Thu Nov 26 16:37:56 1998 +0100
@@ -376,7 +376,6 @@
by (simp_tac (simpset() addsimps [sforall_def]) 1);
by (res_inst_tac[("x","x")] seq.ind 1);
(* adm *)
-(* FIX should be refined in _one_ tactic *)
by (simp_tac (simpset() addsimps [adm_trick_1]) 1);
(* base cases *)
by (Simp_tac 1);
@@ -460,63 +459,3 @@
qed"seq_finite_ind";
-
-
-(*
-(* -----------------------------------------------------------------
- Fr"uhere Herleitung des endlichen Induktionsprinzips
- aus dem seq_finite Induktionsprinzip.
- Problem bei admissibility von Finite-->seq_finite!
- Deshalb Finite jetzt induktiv und nicht mehr rekursiv definiert!
- ------------------------------------------------------------------ *)
-
-Goal "seq_finite nil";
-by (simp_tac (simpset() addsimps [seq.sfinite_def]) 1);
-by (res_inst_tac [("x","Suc 0")] exI 1);
-by (simp_tac (simpset() addsimps seq.rews) 1);
-qed"seq_finite_nil";
-
-Goal "seq_finite UU";
-by (simp_tac (simpset() addsimps [seq.sfinite_def]) 1);
-qed"seq_finite_UU";
-
-Addsimps[seq_finite_nil,seq_finite_UU];
-
-goal HOL.thy "(B-->A) --> (A--> (B-->C))--> (B--> C)";
-by (fast_tac HOL_cs 1);
-qed"logic_lemma";
-
-
-Goal "!!P.[| P nil; \
-\ !!a t. [|a~=UU;Finite t; P t|] ==> P (a##t)|]\
-\ ==> Finite x --> P x";
-
-by (rtac (logic_lemma RS mp RS mp) 1);
-by (rtac trf_impl_tf 1);
-by (rtac seq_finite_ind 1);
-by (simp_tac (simpset() addsimps [Finite_def]) 1);
-by (simp_tac (simpset() addsimps [Finite_def]) 1);
-by (asm_full_simp_tac (simpset() addsimps [Finite_def]) 1);
-qed"Finite_ind";
-
-
-Goal "Finite tr --> seq_finite tr";
-by (rtac seq.ind 1);
-(* adm *)
-(* hier grosses Problem !!!!!!!!!!!!!!! *)
-
-by (simp_tac (simpset() addsimps [Finite_def]) 2);
-by (simp_tac (simpset() addsimps [Finite_def]) 2);
-
-(* main case *)
-by (asm_full_simp_tac (simpset() addsimps [Finite_def,seq.sfinite_def]) 2);
-by (rtac impI 2);
-by (rotate_tac 2 2);
-by (Asm_full_simp_tac 2);
-by (etac exE 2);
-by (res_inst_tac [("x","Suc n")] exI 2);
-by (asm_full_simp_tac (simpset() addsimps seq.rews) 2);
-qed"tf_is_trf";
-
-*)
-
--- a/src/HOLCF/IOA/meta_theory/Seq.thy Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy Thu Nov 26 16:37:56 1998 +0100
@@ -104,16 +104,6 @@
| x##xs => (case t2 of
nil => UU
| y##ys => <x,y>##(h`xs`ys))))"
-
-(*
-nproj_def
- "nproj == (%n tr.HD`(iterate n TL tr))"
-
-
-sproj_def
- "sproj == (%n tr.iterate n TL tr)"
-*)
-
Partial_def
"Partial x == (seq_finite x) & ~(Finite x)"
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Thu Nov 26 16:37:56 1998 +0100
@@ -188,8 +188,6 @@
by (rtac trans 1);
by (stac Zip_unfold 1);
by (Simp_tac 1);
-(* FIX: Why Simp_tac 2 times. Does continuity in simpflication make job sometimes not
- completely ready ? *)
by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"Zip_cons";
@@ -214,25 +212,6 @@
Zip_UU1,Zip_UU2,Zip_nil,Zip_cons_nil,Zip_cons];
-(*
-
-Can Filter with HOL predicate directly be defined as fixpoint ?
-
-Goal "Filter2 P = (LAM tr. case tr of \
- \ nil => nil \
- \ | x##xs => (case x of Undef => UU | Def y => \
-\ (if P y then y>>(Filter2 P`xs) else Filter2 P`xs)))";
-by (rtac trans 1);
-by (rtac fix_eq2 1);
-by (rtac Filter2_def 1);
-by (rtac beta_cfun 1);
-by (Simp_tac 1);
-
-is also possible, if then else has to be proven continuous and it would be nice if a case for
-Seq would be available.
-
-*)
-
(* ------------------------------------------------------------------------------------- *)
@@ -524,7 +503,7 @@
Addsimps [nilConc];
-(* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
+(* should be same as nil_is_Conc2 when all nils are turned to right side !! *)
Goal "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)";
by (Seq_case_simp_tac "x" 1);
by Auto_tac;
@@ -1155,7 +1134,7 @@
by (res_inst_tac [("A1","%x. True")
,("Q1","%x.~(P x & Q x)"),("x1","s")]
(take_lemma_induct RS mp) 1);
-(* FIX: better support for A = %x. True *)
+(* better support for A = %x. True *)
by (Fast_tac 3);
by (asm_full_simp_tac (simpset() addsimps [Filter_lemma1]) 1);
by (asm_full_simp_tac (simpset() addsimps [Filter_lemma2,Filter_lemma3]) 1);
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Thu Nov 26 16:37:56 1998 +0100
@@ -179,36 +179,6 @@
-(*
-
-Goal "Finite s --> (? y. s = Cut P s @@ y)";
-by (strip_tac 1);
-by (rtac exI 1);
-by (resolve_tac seq.take_lemmas 1);
-by (rtac mp 1);
-by (assume_tac 2);
-by (thin_tac' 1 1);
-by (res_inst_tac [("x","s")] spec 1);
-by (rtac less_induct 1);
-by (strip_tac 1);
-ren "na n s" 1;
-by (case_tac "Forall (%x. ~ P x) s" 1);
-by (rtac (seq_take_lemma RS iffD2 RS spec) 1);
-by (asm_full_simp_tac (simpset() addsimps [Cut_nil]) 1);
-(* main case *)
-by (dtac divide_Seq3 1);
-by (REPEAT (etac exE 1));
-by (REPEAT (etac conjE 1));
-by (hyp_subst_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,Conc_assoc]) 1);
-by (rtac take_reduction 1);
-
-qed_spec_mp"Cut_prefixcl_Finite";
-
-*)
-
-
-
Goal "!!ex .is_exec_frag A (s,ex) ==> is_exec_frag A (s,Cut P ex)";
by (case_tac "Finite ex" 1);
by (cut_inst_tac [("s","ex"),("P","P")] Cut_prefixcl_Finite 1);
--- a/src/HOLCF/IOA/meta_theory/TL.ML Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/TL.ML Thu Nov 26 16:37:56 1998 +0100
@@ -11,7 +11,7 @@
by (rtac ext 1);
by (simp_tac (simpset() addsimps [Diamond_def,NOT_def,Box_def])1);
by Auto_tac;
-qed"simple_try";
+qed"simple";
Goal "nil |= [] P";
by (asm_full_simp_tac (simpset() addsimps [satisfies_def,
@@ -73,27 +73,6 @@
qed"normalT";
-(*
-Goal "s |= <> F .& <> G .--> (<> (F .& <> G) .| <> (G .& <> F))";
-by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,AND_def,OR_def,Diamond_def2])1);
-by (rtac impI 1);
-by (etac conjE 1);
-by (etac exE 1);
-by (etac exE 1);
-
-
-by (rtac disjI1 1);
-
-Goal "!!s. [| tsuffix s1 s ; tsuffix s2 s|] ==> tsuffix s2 s1 | tsuffix s1 s2";
-by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1);
-by (REPEAT (etac conjE 1));
-by (REPEAT (etac exE 1));
-by (REPEAT (etac conjE 1));
-by (hyp_subst_tac 1);
-
-*)
-
-
section "TLA Rules by Lamport";
(* ---------------------------------------------------------------- *)
@@ -113,8 +92,6 @@
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))";
by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,IMPLIES_def,Box_def,Init_def])1);
@@ -175,7 +152,6 @@
by (Asm_full_simp_tac 1);
by Auto_tac;
-
by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1);
by Auto_tac;
--- a/src/HOLCF/IOA/meta_theory/TL.thy Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/TL.thy Thu Nov 26 16:37:56 1998 +0100
@@ -5,8 +5,6 @@
A General Temporal Logic
-Version 2: Interface directly after Sequeces, i.e. predicates and predicate transformers are in HOL
-
*)
--- a/src/HOLCF/IOA/meta_theory/TLS.ML Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.ML Thu Nov 26 16:37:56 1998 +0100
@@ -4,7 +4,7 @@
Copyright 1997 TU Muenchen
Temporal Logic of Steps -- tailored for I/O automata
-*)
+*)
(* global changes to simpset() and claset(), repeated from Traces.ML *)
Delsimps (ex_simps @ all_simps);
@@ -70,8 +70,6 @@
Addsimps [ex2seq_UU,ex2seq_nil, ex2seq_cons];
-
-
Goal "ex2seq exec ~= UU & ex2seq exec ~= nil";
by (pair_tac "exec" 1);
by (Seq_case_simp_tac "y" 1);
@@ -79,9 +77,6 @@
qed"ex2seq_nUUnnil";
-Goal "ex |== [] P .--> P";
-
-
(* ----------------------------------------------------------- *)
(* Interface TL -- TLS *)
(* ---------------------------------------------------------- *)
--- a/src/HOLCF/IOA/meta_theory/TLS.thy Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy Thu Nov 26 16:37:56 1998 +0100
@@ -42,8 +42,6 @@
"mkfin s == if Partial s then @t. Finite t & s = t @@ UU
else s"
-(* should be in Option as option_lift1, and option_map should be renamed to
- option_lift2 *)
option_lift_def
"option_lift f s y == case y of None => s | Some x => (f x)"
@@ -78,6 +76,8 @@
validIOA_def
"validIOA A P == ! ex : executions A . (ex |== P)"
+
+
rules
mkfin_UU
--- a/src/HOLCF/IOA/meta_theory/Traces.thy Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy Thu Nov 26 16:37:56 1998 +0100
@@ -66,13 +66,6 @@
Scheds :: "('a,'s)ioa => 'a schedule_module"
Traces :: "('a,'s)ioa => 'a trace_module"
-(*
-(* FIX: introduce good symbol *)
-syntax (symbols)
-
- "op <<|" ::"[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr "\\<parallel>" 10)
-*)
-
defs
@@ -144,7 +137,8 @@
(* Note that partial execs cannot be wfair as the inf_often predicate in the
else branch prohibits it. However they can be sfair in the case when all W
- are only finitely often enabled: FIX Is this the right model? *)
+ are only finitely often enabled: Is this the right model?
+ See LiveIOA for solution conforming with the literature and superseding this one *)
wfair_ex_def
"wfair_ex A ex == ! W : wfair_of A.
if Finite (snd ex)