# HG changeset patch # User mueller # Date 912094676 -3600 # Node ID 44290b71a85f358106201e7bf4d561c35c4620d6 # Parent cd19eaa90f4584735e6f2aeae8ecc02af15d4d2f tuning to assimiliate it with PhD; diff -r cd19eaa90f45 -r 44290b71a85f src/HOLCF/IOA/meta_theory/Abstraction.ML --- 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 *) (* ---------------------------------------------------------------- *) diff -r cd19eaa90f45 -r 44290b71a85f src/HOLCF/IOA/meta_theory/Abstraction.thy --- 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" diff -r cd19eaa90f45 -r 44290b71a85f src/HOLCF/IOA/meta_theory/Automata.ML --- 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, diff -r cd19eaa90f45 -r 44290b71a85f src/HOLCF/IOA/meta_theory/CompoScheds.ML --- 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 *) diff -r cd19eaa90f45 -r 44290b71a85f src/HOLCF/IOA/meta_theory/Compositionality.ML --- 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; diff -r cd19eaa90f45 -r 44290b71a85f src/HOLCF/IOA/meta_theory/LiveIOA.ML --- 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 diff -r cd19eaa90f45 -r 44290b71a85f src/HOLCF/IOA/meta_theory/Pred.thy --- 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 + diff -r cd19eaa90f45 -r 44290b71a85f src/HOLCF/IOA/meta_theory/RefCorrectness.thy --- 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))" diff -r cd19eaa90f45 -r 44290b71a85f src/HOLCF/IOA/meta_theory/Seq.ML --- 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"; - -*) - diff -r cd19eaa90f45 -r 44290b71a85f src/HOLCF/IOA/meta_theory/Seq.thy --- 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 => ##(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)" diff -r cd19eaa90f45 -r 44290b71a85f src/HOLCF/IOA/meta_theory/Sequence.ML --- 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); diff -r cd19eaa90f45 -r 44290b71a85f src/HOLCF/IOA/meta_theory/ShortExecutions.ML --- 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); diff -r cd19eaa90f45 -r 44290b71a85f src/HOLCF/IOA/meta_theory/TL.ML --- 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; diff -r cd19eaa90f45 -r 44290b71a85f src/HOLCF/IOA/meta_theory/TL.thy --- 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 - *) diff -r cd19eaa90f45 -r 44290b71a85f src/HOLCF/IOA/meta_theory/TLS.ML --- 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 *) (* ---------------------------------------------------------- *) diff -r cd19eaa90f45 -r 44290b71a85f src/HOLCF/IOA/meta_theory/TLS.thy --- 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 diff -r cd19eaa90f45 -r 44290b71a85f src/HOLCF/IOA/meta_theory/Traces.thy --- 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 "\\" 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)