# HG changeset patch # User wenzelm # Date 1125674639 -7200 # Node ID 41eee2e7b465972f51de92eea8337590cc074838 # Parent 148c241d2492991637c0016db54273efe95796d7 converted specifications to Isar theories; diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/Abstraction.ML --- a/src/HOLCF/IOA/meta_theory/Abstraction.ML Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML Fri Sep 02 17:23:59 2005 +0200 @@ -1,8 +1,6 @@ (* Title: HOLCF/IOA/meta_theory/Abstraction.thy ID: $Id$ Author: Olaf Müller - -Abstraction Theory -- tailored for I/O automata. *) section "cex_abs"; diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/Abstraction.thy --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,15 +1,15 @@ (* Title: HOLCF/IOA/meta_theory/Abstraction.thy ID: $Id$ Author: Olaf Müller +*) -Abstraction Theory -- tailored for I/O automata. -*) +header {* Abstraction Theory -- tailored for I/O automata *} - -Abstraction = LiveIOA + +theory Abstraction +imports LiveIOA +begin -default type - +defaultsort type consts @@ -18,9 +18,9 @@ is_abstraction ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" - weakeningIOA :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool" - temp_weakening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" - temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" + weakeningIOA :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool" + temp_weakening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" + temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" state_weakening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" state_strengthening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" @@ -30,53 +30,55 @@ defs -is_abstraction_def - "is_abstraction f C A == - (!s:starts_of(C). f(s):starts_of(A)) & - (!s t a. reachable C s & s -a--C-> t +is_abstraction_def: + "is_abstraction f C A == + (!s:starts_of(C). f(s):starts_of(A)) & + (!s t a. reachable C s & s -a--C-> t --> (f s) -a--A-> (f t))" -is_live_abstraction_def - "is_live_abstraction h CL AM == +is_live_abstraction_def: + "is_live_abstraction h CL AM == is_abstraction h (fst CL) (fst AM) & temp_weakening (snd AM) (snd CL) h" -cex_abs_def +cex_abs_def: "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))" (* equals cex_abs on Sequneces -- after ex2seq application -- *) -cex_absSeq_def +cex_absSeq_def: "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))$s" -weakeningIOA_def +weakeningIOA_def: "weakeningIOA A C h == ! ex. ex : executions C --> cex_abs h ex : executions A" -temp_weakening_def +temp_weakening_def: "temp_weakening Q P h == temp_strengthening (.~ Q) (.~ P) h" -temp_strengthening_def +temp_strengthening_def: "temp_strengthening Q P h == ! ex. (cex_abs h ex |== Q) --> (ex |== P)" -state_weakening_def +state_weakening_def: "state_weakening Q P h == state_strengthening (.~Q) (.~P) h" -state_strengthening_def +state_strengthening_def: "state_strengthening Q P h == ! s t a. Q (h(s),a,h(t)) --> P (s,a,t)" -rules +axioms (* thm about ex2seq which is not provable by induction as ex2seq is not continous *) -ex2seq_abs_cex - "ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)" +ex2seq_abs_cex: + "ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)" (* analog to the proved thm strength_Box - proof skipped as trivial *) -weak_Box -"temp_weakening P Q h +weak_Box: +"temp_weakening P Q h ==> temp_weakening ([] P) ([] Q) h" (* analog to the proved thm strength_Next - proof skipped as trivial *) -weak_Next -"temp_weakening P Q h +weak_Next: +"temp_weakening P Q h ==> temp_weakening (Next P) (Next Q) h" -end \ No newline at end of file +ML {* use_legacy_bindings (the_context ()) *} + +end diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/Asig.ML --- a/src/HOLCF/IOA/meta_theory/Asig.ML Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Asig.ML Fri Sep 02 17:23:59 2005 +0200 @@ -1,8 +1,6 @@ (* Title: HOL/IOA/meta_theory/Asig.ML ID: $Id$ Author: Olaf Müller, Tobias Nipkow & Konrad Slind - -Action signatures. *) val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def]; @@ -37,7 +35,7 @@ Goal "(x: actions S & x : externals S) = (x: externals S)"; by (fast_tac (claset() addSIs [ext_is_act]) 1 ); qed"ext_and_act"; - + 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 (Blast_tac 1); @@ -53,4 +51,3 @@ by (Asm_full_simp_tac 1); by (Blast_tac 1); qed"int_is_not_ext"; - diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/Asig.thy --- a/src/HOLCF/IOA/meta_theory/Asig.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Asig.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,47 +1,52 @@ (* Title: HOL/IOA/meta_theory/Asig.thy ID: $Id$ Author: Olaf Müller, Tobias Nipkow & Konrad Slind - -Action signatures. *) -Asig = Main + +header {* Action signatures *} -types +theory Asig +imports Main +begin -'a signature = "('a set * 'a set * 'a set)" +types + 'a signature = "('a set * 'a set * 'a set)" consts - actions,inputs,outputs,internals,externals,locals - ::"'action signature => 'action set" + actions :: "'action signature => 'action set" + inputs :: "'action signature => 'action set" + outputs :: "'action signature => 'action set" + internals :: "'action signature => 'action set" + externals :: "'action signature => 'action set" + locals :: "'action signature => 'action set" is_asig ::"'action signature => bool" mk_ext_asig ::"'action signature => 'action signature" - defs -asig_inputs_def "inputs == fst" -asig_outputs_def "outputs == (fst o snd)" -asig_internals_def "internals == (snd o snd)" +asig_inputs_def: "inputs == fst" +asig_outputs_def: "outputs == (fst o snd)" +asig_internals_def: "internals == (snd o snd)" -actions_def +actions_def: "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))" -externals_def +externals_def: "externals(asig) == (inputs(asig) Un outputs(asig))" -locals_def +locals_def: "locals asig == ((internals asig) Un (outputs asig))" -is_asig_def - "is_asig(triple) == - ((inputs(triple) Int outputs(triple) = {}) & - (outputs(triple) Int internals(triple) = {}) & +is_asig_def: + "is_asig(triple) == + ((inputs(triple) Int outputs(triple) = {}) & + (outputs(triple) Int internals(triple) = {}) & (inputs(triple) Int internals(triple) = {}))" -mk_ext_asig_def +mk_ext_asig_def: "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})" +ML {* use_legacy_bindings (the_context ()) *} -end +end diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/Automata.ML --- a/src/HOLCF/IOA/meta_theory/Automata.ML Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Automata.ML Fri Sep 02 17:23:59 2005 +0200 @@ -1,8 +1,6 @@ (* Title: HOLCF/IOA/meta_theory/Automata.ML ID: $Id$ Author: Olaf Mueller, Tobias Nipkow, Konrad Slind - -The I/O automata of Lynch and Tuttle. *) (* this modification of the simpset is local to this file *) @@ -37,14 +35,14 @@ qed "starts_of_par"; Goal -"trans_of(A || B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) \ +"trans_of(A || B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) \ \ in (a:act A | a:act B) & \ -\ (if a:act A then \ -\ (fst(s),a,fst(t)):trans_of(A) \ -\ else fst(t) = fst(s)) \ -\ & \ -\ (if a:act B then \ -\ (snd(s),a,snd(t)):trans_of(B) \ +\ (if a:act A then \ +\ (fst(s),a,fst(t)):trans_of(A) \ +\ else fst(t) = fst(s)) \ +\ & \ +\ (if a:act B then \ +\ (snd(s),a,snd(t)):trans_of(B) \ \ else snd(t) = snd(s))}"; by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1); @@ -56,7 +54,7 @@ section "actions and par"; -Goal +Goal "actions(asig_comp a b) = actions(a) Un actions(b)"; by (simp_tac (simpset() addsimps ([actions_def,asig_comp_def]@asig_projections)) 1); @@ -73,24 +71,24 @@ \ (ext A1) Un (ext A2)"; by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_of_par,asig_comp_def, asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1); -by (rtac set_ext 1); +by (rtac set_ext 1); by (fast_tac set_cs 1); -qed"externals_of_par"; +qed"externals_of_par"; Goal "act (A1||A2) = \ \ (act A1) Un (act A2)"; by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def, asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1); -by (rtac set_ext 1); +by (rtac set_ext 1); by (fast_tac set_cs 1); -qed"actions_of_par"; +qed"actions_of_par"; Goal "inp (A1||A2) =\ \ ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))"; by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def, asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1); qed"inputs_of_par"; - + Goal "out (A1||A2) =\ \ (out A1) Un (out A2)"; by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def, @@ -105,7 +103,7 @@ (* ------------------------------------------------------------------------ *) -section "actions and compatibility"; +section "actions and compatibility"; Goal"compatible A B = compatible B A"; by (asm_full_simp_tac (simpset() addsimps [compatible_def,Int_commute]) 1); @@ -158,13 +156,13 @@ (* ------------------------------------------------------------------------- *) -section "input_enabledness and par"; +section "input_enabledness and par"; -(* ugly case distinctions. Heart of proof: +(* ugly case distinctions. Heart of proof: 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] +Goalw [input_enabled_def] "[| 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); @@ -232,7 +230,7 @@ section "invariants"; -val [p1,p2] = goalw thy [invariant_def] +val [p1,p2] = goalw (the_context ()) [invariant_def] "[| !!s. s:starts_of(A) ==> P(s); \ \ !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \ \ ==> invariant A P"; @@ -246,7 +244,7 @@ qed"invariantI"; -val [p1,p2] = goal thy +val [p1,p2] = goal (the_context ()) "[| !!s. s : starts_of(A) ==> P(s); \ \ !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \ \ |] ==> invariant A P"; @@ -254,7 +252,7 @@ qed "invariantI1"; Goalw [invariant_def] "[| invariant A P; reachable A s |] ==> P(s)"; -by (Blast_tac 1); +by (Blast_tac 1); qed "invariantE"; (* ------------------------------------------------------------------------- *) @@ -375,7 +373,7 @@ trans_B_proj2,trans_AB_proj]; -Goal +Goal "((s,a,t) : trans_of(A || B || C || D)) = \ \ ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) | \ \ a:actions(asig_of(D))) & \ @@ -397,24 +395,24 @@ (* ------------------------------------------------------------------------- *) -section "proof obligation generator for IOA requirements"; +section "proof obligation generator for IOA requirements"; (* without assumptions on A and B because is_trans_of is also incorporated in ||def *) Goalw [is_trans_of_def] "is_trans_of (A||B)"; by (simp_tac (simpset() addsimps [Let_def,actions_of_par,trans_of_par]) 1); qed"is_trans_of_par"; -Goalw [is_trans_of_def] +Goalw [is_trans_of_def] "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] +Goalw [is_trans_of_def,restrict_def,restrict_asig_def] "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, - asig_of_def,rename_def,rename_set_def]) 1); + asig_outputs_def,asig_inputs_def,externals_def, + asig_of_def,rename_def,rename_set_def]) 1); by (Blast_tac 1); qed"is_trans_of_rename"; @@ -428,7 +426,7 @@ 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] + asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,o_def] "is_asig_of A ==> is_asig_of (restrict A f)"; by (Asm_full_simp_tac 1); by Auto_tac; @@ -438,7 +436,7 @@ 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 Auto_tac; by (ALLGOALS(dres_inst_tac [("s","Some ?x")] sym THEN' Asm_full_simp_tac)); by (ALLGOALS(Blast_tac)); qed"is_asig_of_rename"; @@ -450,7 +448,7 @@ Goalw [compatible_def] "[|compatible A B; compatible A C |]==> compatible A (B||C)"; -by (asm_full_simp_tac (simpset() addsimps [internals_of_par, +by (asm_full_simp_tac (simpset() addsimps [internals_of_par, outputs_of_par,actions_of_par]) 1); by Auto_tac; qed"compatible_par"; @@ -458,7 +456,7 @@ (* better derive by previous one and compat_commute *) Goalw [compatible_def] "[|compatible A C; compatible B C |]==> compatible (A||B) C"; -by (asm_full_simp_tac (simpset() addsimps [internals_of_par, +by (asm_full_simp_tac (simpset() addsimps [internals_of_par, outputs_of_par,actions_of_par]) 1); by Auto_tac; qed"compatible_par2"; diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/Automata.thy --- a/src/HOLCF/IOA/meta_theory/Automata.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,22 +1,22 @@ (* Title: HOLCF/IOA/meta_theory/Automata.thy ID: $Id$ Author: Olaf Müller, Konrad Slind, Tobias Nipkow +*) -The I/O automata of Lynch and Tuttle in HOLCF. -*) - - -Automata = Asig + +header {* The I/O automata of Lynch and Tuttle in HOLCF *} -default type - +theory Automata +imports Asig +begin + +defaultsort type + types - ('a,'s)transition = "'s * 'a * 's" - ('a,'s)ioa = "'a signature * 's set * ('a,'s)transition set * - (('a set) set) * (('a set) set)" + ('a, 's) transition = "'s * 'a * 's" + ('a, 's) ioa = "'a signature * 's set * ('a,'s)transition set * ('a set set) * ('a set set)" consts - + (* IO automata *) asig_of ::"('a,'s)ioa => 'a signature" @@ -26,10 +26,10 @@ sfair_of ::"('a,'s)ioa => ('a set) set" is_asig_of ::"('a,'s)ioa => bool" - is_starts_of ::"('a,'s)ioa => bool" - is_trans_of ::"('a,'s)ioa => bool" - input_enabled ::"('a,'s)ioa => bool" - IOA ::"('a,'s)ioa => bool" + is_starts_of ::"('a,'s)ioa => bool" + is_trans_of ::"('a,'s)ioa => bool" + input_enabled ::"('a,'s)ioa => bool" + IOA ::"('a,'s)ioa => bool" (* constraints for fair IOA *) @@ -41,7 +41,7 @@ enabled ::"('a,'s)ioa => 'a => 's => bool" Enabled ::"('a,'s)ioa => 'a set => 's => bool" - (* action set keeps enabled until probably disabled by itself *) + (* action set keeps enabled until probably disabled by itself *) en_persistent :: "('a,'s)ioa => 'a set => bool" @@ -61,7 +61,7 @@ (* hiding and restricting *) hide_asig :: "['a signature, 'a set] => 'a signature" - hide :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa" + "hide" :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa" restrict_asig :: "['a signature, 'a set] => 'a signature" restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa" @@ -70,7 +70,7 @@ rename :: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa" -syntax +syntax "_trans_of" :: "'s => 'a => ('a,'s)ioa => 's => bool" ("_ -_--_-> _" [81,81,81,81] 100) "reachable" :: "[('a,'s)ioa, 's] => bool" @@ -84,15 +84,15 @@ syntax (xsymbols) - "_trans_of" :: "'s => 'a => ('a,'s)ioa => 's => bool" - ("_ \\_\\_\\ _" [81,81,81,81] 100) - "op ||" ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "\\" 10) + "_trans_of" :: "'s => 'a => ('a,'s)ioa => 's => bool" + ("_ \_\_\ _" [81,81,81,81] 100) + "op ||" ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "\" 10) -inductive "reachable C" - intrs - reachable_0 "s:(starts_of C) ==> s : reachable C" - reachable_n "[|s:reachable C; (s,a,t):trans_of C|] ==> t:reachable C" +inductive "reachable C" + intros + reachable_0: "s:(starts_of C) ==> s : reachable C" + reachable_n: "[|s:reachable C; (s,a,t):trans_of C|] ==> t:reachable C" translations @@ -105,72 +105,68 @@ "out A" == "outputs (asig_of A)" "local A" == "locals (asig_of A)" - - defs (* --------------------------------- IOA ---------------------------------*) +asig_of_def: "asig_of == fst" +starts_of_def: "starts_of == (fst o snd)" +trans_of_def: "trans_of == (fst o snd o snd)" +wfair_of_def: "wfair_of == (fst o snd o snd o snd)" +sfair_of_def: "sfair_of == (snd o snd o snd o snd)" + +is_asig_of_def: + "is_asig_of A == is_asig (asig_of A)" + +is_starts_of_def: + "is_starts_of A == (~ starts_of A = {})" + +is_trans_of_def: + "is_trans_of A == + (!triple. triple:(trans_of A) --> fst(snd(triple)):actions(asig_of A))" + +input_enabled_def: + "input_enabled A == + (!a. (a:inputs(asig_of A)) --> (!s1. ? s2. (s1,a,s2):(trans_of A)))" -asig_of_def "asig_of == fst" -starts_of_def "starts_of == (fst o snd)" -trans_of_def "trans_of == (fst o snd o snd)" -wfair_of_def "wfair_of == (fst o snd o snd o snd)" -sfair_of_def "sfair_of == (snd o snd o snd o snd)" - -is_asig_of_def - "is_asig_of A == is_asig (asig_of A)" - -is_starts_of_def - "is_starts_of A == (~ starts_of A = {})" - -is_trans_of_def - "is_trans_of A == - (!triple. triple:(trans_of A) --> fst(snd(triple)):actions(asig_of A))" - -input_enabled_def - "input_enabled A == - (!a. (a:inputs(asig_of A)) --> (!s1. ? s2. (s1,a,s2):(trans_of A)))" - - -ioa_def - "IOA A == (is_asig_of A & - is_starts_of A & +ioa_def: + "IOA A == (is_asig_of A & + is_starts_of A & is_trans_of A & input_enabled A)" -invariant_def "invariant A P == (!s. reachable A s --> P(s))" +invariant_def: "invariant A P == (!s. reachable A s --> P(s))" (* ------------------------- parallel composition --------------------------*) -compatible_def - "compatible A B == - (((out A Int out B) = {}) & - ((int A Int act B) = {}) & +compatible_def: + "compatible A B == + (((out A Int out B) = {}) & + ((int A Int act B) = {}) & ((int B Int act A) = {}))" -asig_comp_def - "asig_comp a1 a2 == - (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)), - (outputs(a1) Un outputs(a2)), +asig_comp_def: + "asig_comp a1 a2 == + (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)), + (outputs(a1) Un outputs(a2)), (internals(a1) Un internals(a2))))" -par_def - "(A || B) == - (asig_comp (asig_of A) (asig_of B), - {pr. fst(pr):starts_of(A) & snd(pr):starts_of(B)}, - {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) - in (a:act A | a:act B) & - (if a:act A then - (fst(s),a,fst(t)):trans_of(A) - else fst(t) = fst(s)) - & - (if a:act B then - (snd(s),a,snd(t)):trans_of(B) +par_def: + "(A || B) == + (asig_comp (asig_of A) (asig_of B), + {pr. fst(pr):starts_of(A) & snd(pr):starts_of(B)}, + {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) + in (a:act A | a:act B) & + (if a:act A then + (fst(s),a,fst(t)):trans_of(A) + else fst(t) = fst(s)) + & + (if a:act B then + (snd(s),a,snd(t)):trans_of(B) else snd(t) = snd(s))}, wfair_of A Un wfair_of B, sfair_of A Un sfair_of B)" @@ -178,84 +174,84 @@ (* ------------------------ hiding -------------------------------------------- *) -restrict_asig_def - "restrict_asig asig actns == - (inputs(asig) Int actns, - outputs(asig) Int actns, +restrict_asig_def: + "restrict_asig asig actns == + (inputs(asig) Int actns, + outputs(asig) Int actns, internals(asig) Un (externals(asig) - actns))" -(* Notice that for wfair_of and sfair_of nothing has to be changed, as - changes from the outputs to the internals does not touch the locals as +(* Notice that for wfair_of and sfair_of nothing has to be changed, as + changes from the outputs to the internals does not touch the locals as a whole, which is of importance for fairness only *) -restrict_def - "restrict A actns == - (restrict_asig (asig_of A) actns, - starts_of A, +restrict_def: + "restrict A actns == + (restrict_asig (asig_of A) actns, + starts_of A, trans_of A, wfair_of A, sfair_of A)" -hide_asig_def - "hide_asig asig actns == - (inputs(asig) - actns, - outputs(asig) - actns, +hide_asig_def: + "hide_asig asig actns == + (inputs(asig) - actns, + outputs(asig) - actns, internals(asig) Un actns)" -hide_def - "hide A actns == - (hide_asig (asig_of A) actns, - starts_of A, +hide_def: + "hide A actns == + (hide_asig (asig_of A) actns, + starts_of A, trans_of A, wfair_of A, sfair_of A)" (* ------------------------- renaming ------------------------------------------- *) - -rename_set_def - "rename_set A ren == {b. ? x. Some x = ren b & x : A}" + +rename_set_def: + "rename_set A ren == {b. ? x. Some x = ren b & x : A}" -rename_def -"rename ioa ren == - ((rename_set (inp ioa) ren, - rename_set (out ioa) ren, - rename_set (int ioa) ren), - starts_of ioa, - {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) - in +rename_def: +"rename ioa ren == + ((rename_set (inp ioa) ren, + rename_set (out ioa) ren, + rename_set (int ioa) ren), + starts_of ioa, + {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) + in ? x. Some(x) = ren(a) & (s,x,t):trans_of ioa}, {rename_set s ren | s. s: wfair_of ioa}, {rename_set s ren | s. s: sfair_of ioa})" (* ------------------------- fairness ----------------------------- *) -fairIOA_def - "fairIOA A == (! S : wfair_of A. S<= local A) & +fairIOA_def: + "fairIOA A == (! S : wfair_of A. S<= local A) & (! S : sfair_of A. S<= local A)" -input_resistant_def - "input_resistant A == ! W : sfair_of A. ! s a t. +input_resistant_def: + "input_resistant A == ! W : sfair_of A. ! s a t. reachable A s & reachable A t & a:inp A & Enabled A W s & s -a--A-> t --> Enabled A W t" -enabled_def +enabled_def: "enabled A a s == ? t. s-a--A-> t" -Enabled_def +Enabled_def: "Enabled A W s == ? w:W. enabled A w s" -en_persistent_def - "en_persistent A W == ! s a t. Enabled A W s & - a ~:W & - s -a--A-> t +en_persistent_def: + "en_persistent A W == ! s a t. Enabled A W s & + a ~:W & + s -a--A-> t --> Enabled A W t" -was_enabled_def +was_enabled_def: "was_enabled A a t == ? s. s-a--A-> t" -set_was_enabled_def +set_was_enabled_def: "set_was_enabled A W t == ? w:W. was_enabled A w t" +ML {* use_legacy_bindings (the_context ()) *} end - diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/CompoExecs.ML --- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML Fri Sep 02 17:23:59 2005 +0200 @@ -1,11 +1,9 @@ (* Title: HOLCF/IOA/meta_theory/CompoExecs.ML ID: $Id$ Author: Olaf Müller +*) -Compositionality on Execution level. -*) - -Delsimps (ex_simps @ all_simps); +Delsimps (ex_simps @ all_simps); Delsimps [split_paired_All]; (* ----------------------------------------------------------------------------------- *) @@ -65,8 +63,8 @@ qed"Filter_ex2_nil"; Goal "Filter_ex2 sig$(at >> xs) = \ -\ (if (fst at:actions sig) \ -\ then at >> (Filter_ex2 sig$xs) \ +\ (if (fst at:actions sig) \ +\ then at >> (Filter_ex2 sig$xs) \ \ else Filter_ex2 sig$xs)"; by (asm_full_simp_tac (simpset() addsimps [Filter_ex2_def]) 1); @@ -80,7 +78,7 @@ Goal "stutter2 sig = (LAM ex. (%s. case ex of \ \ nil => TT \ -\ | x##xs => (flift1 \ +\ | x##xs => (flift1 \ \ (%p.(If Def ((fst p)~:actions sig) \ \ then Def (s=(snd p)) \ \ else TT fi) \ @@ -106,7 +104,7 @@ Goal "(stutter2 sig$(at>>xs)) s = \ \ ((if (fst at)~:actions sig then Def (s=snd at) else TT) \ -\ andalso (stutter2 sig$xs) (snd at))"; +\ andalso (stutter2 sig$xs) (snd at))"; by (rtac trans 1); by (stac stutter2_unfold 1); by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def,If_and_if]) 1); @@ -175,7 +173,7 @@ Goal "!s. is_exec_frag (A||B) (s,xs) \ \ --> stutter (asig_of A) (fst s,ProjA2$xs) &\ -\ stutter (asig_of B) (snd s,ProjB2$xs)"; +\ stutter (asig_of B) (snd s,ProjB2$xs)"; by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1); (* main case *) @@ -194,7 +192,7 @@ by (pair_induct_tac "xs" [Forall_def,sforall_def,is_exec_frag_def] 1); (* main case *) by (safe_tac set_cs); -by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2 @ +by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2 @ [actions_asig_comp,asig_of_par]) 1)); qed"lemma_1_1c"; @@ -203,7 +201,7 @@ (* Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B) *) (* ----------------------------------------------------------------------- *) -Goal +Goal "!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)$(ProjA2$xs)) &\ \ is_exec_frag B (snd s,Filter_ex2 (asig_of B)$(ProjB2$xs)) &\ \ stutter (asig_of A) (fst s,(ProjA2$xs)) & \ @@ -229,7 +227,7 @@ (* ------------------------------------------------------------------ *) -Goal +Goal "(ex:executions(A||B)) =\ \(Filter_ex (asig_of A) (ProjA ex) : executions A &\ \ Filter_ex (asig_of B) (ProjB ex) : executions B &\ @@ -263,10 +261,3 @@ by (rtac set_ext 1); by (asm_full_simp_tac (simpset() addsimps [compositionality_ex,actions_of_par]) 1); qed"compositionality_ex_modules"; - - - - - - - diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/CompoExecs.thy --- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,69 +1,70 @@ (* Title: HOLCF/IOA/meta_theory/CompoExecs.thy ID: $Id$ Author: Olaf Müller +*) -Compositionality on Execution level. -*) +header {* Compositionality on Execution level *} -CompoExecs = Traces + +theory CompoExecs +imports Traces +begin - -consts +consts ProjA ::"('a,'s * 't)execution => ('a,'s)execution" ProjA2 ::"('a,'s * 't)pairs -> ('a,'s)pairs" ProjB ::"('a,'s * 't)execution => ('a,'t)execution" ProjB2 ::"('a,'s * 't)pairs -> ('a,'t)pairs" Filter_ex ::"'a signature => ('a,'s)execution => ('a,'s)execution" - Filter_ex2 ::"'a signature => ('a,'s)pairs -> ('a,'s)pairs" - stutter ::"'a signature => ('a,'s)execution => bool" + Filter_ex2 ::"'a signature => ('a,'s)pairs -> ('a,'s)pairs" + stutter ::"'a signature => ('a,'s)execution => bool" stutter2 ::"'a signature => ('a,'s)pairs -> ('s => tr)" par_execs ::"[('a,'s)execution_module,('a,'t)execution_module] => ('a,'s*'t)execution_module" -defs +defs -ProjA_def - "ProjA ex == (fst (fst ex), ProjA2$(snd ex))" +ProjA_def: + "ProjA ex == (fst (fst ex), ProjA2$(snd ex))" -ProjB_def - "ProjB ex == (snd (fst ex), ProjB2$(snd ex))" +ProjB_def: + "ProjB ex == (snd (fst ex), ProjB2$(snd ex))" -ProjA2_def +ProjA2_def: "ProjA2 == Map (%x.(fst x,fst(snd x)))" -ProjB2_def +ProjB2_def: "ProjB2 == Map (%x.(fst x,snd(snd x)))" - + -Filter_ex_def +Filter_ex_def: "Filter_ex sig ex == (fst ex,Filter_ex2 sig$(snd ex))" -Filter_ex2_def +Filter_ex2_def: "Filter_ex2 sig == Filter (%x. fst x:actions sig)" -stutter_def +stutter_def: "stutter sig ex == ((stutter2 sig$(snd ex)) (fst ex) ~= FF)" -stutter2_def - "stutter2 sig ==(fix$(LAM h ex. (%s. case ex of +stutter2_def: + "stutter2 sig ==(fix$(LAM h ex. (%s. case ex of nil => TT - | x##xs => (flift1 + | x##xs => (flift1 (%p.(If Def ((fst p)~:actions sig) - then Def (s=(snd p)) + then Def (s=(snd p)) else TT fi) - andalso (h$xs) (snd p)) + andalso (h$xs) (snd p)) $x) - )))" + )))" -par_execs_def - "par_execs ExecsA ExecsB == - let exA = fst ExecsA; sigA = snd ExecsA; - exB = fst ExecsB; sigB = snd ExecsB +par_execs_def: + "par_execs ExecsA ExecsB == + let exA = fst ExecsA; sigA = snd ExecsA; + exB = fst ExecsB; sigB = snd ExecsB in ( {ex. Filter_ex sigA (ProjA ex) : exA} Int {ex. Filter_ex sigB (ProjB ex) : exB} @@ -72,4 +73,6 @@ Int {ex. Forall (%x. fst x:(actions sigA Un actions sigB)) (snd ex)}, asig_comp sigA sigB)" -end \ No newline at end of file +ML {* use_legacy_bindings (the_context ()) *} + +end diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/CompoScheds.ML --- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML Fri Sep 02 17:23:59 2005 +0200 @@ -1,11 +1,7 @@ (* Title: HOLCF/IOA/meta_theory/CompoScheds.ML ID: $Id$ Author: Olaf Müller - -Compositionality on Schedule level. -*) - - +*) Addsimps [surjective_pairing RS sym]; @@ -20,7 +16,7 @@ (* ---------------------------------------------------------------- *) -bind_thm ("mkex2_unfold", fix_prover2 thy mkex2_def +bind_thm ("mkex2_unfold", fix_prover2 (the_context ()) mkex2_def "mkex2 A B = (LAM sch exA exB. (%s t. case sch of \ \ nil => nil \ \ | x##xs => \ @@ -41,7 +37,7 @@ \ UU => UU \ \ | Def a => \ \ (y,(snd a,t))>>(mkex2 A B$xs$(TL$exA)$exB) (snd a) t) \ -\ ) \ +\ ) \ \ else \ \ (if y:act B then \ \ (case HD$exB of \ @@ -117,7 +113,7 @@ qed"mkex_cons_1"; Goal "[| x~:act A; x:act B |] \ -\ ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) = \ +\ ==> 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); by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1); @@ -166,7 +162,7 @@ (* Lemma_2_2 : State-projections do not affect filter_act *) (* --------------------------------------------------------------------- *) -Goal +Goal "filter_act$(ProjA2$xs) =filter_act$xs &\ \ filter_act$(ProjB2$xs) =filter_act$xs"; @@ -178,7 +174,7 @@ (* Schedules of A||B have only A- or B-actions *) (* --------------------------------------------------------------------- *) -(* 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 *) @@ -188,13 +184,13 @@ by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1); (* main case *) by (safe_tac set_cs); -by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2 @ +by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2 @ [actions_asig_comp,asig_of_par]) 1)); qed"sch_actions_in_AorB"; (* --------------------------------------------------------------------------*) - section "Lemmas for <=="; + section "Lemmas for <=="; (* ---------------------------------------------------------------------------*) (*--------------------------------------------------------------------------- @@ -210,7 +206,7 @@ by (Seq_induct_tac "sch" [Filter_def,Forall_def,sforall_def,mkex_def] 1); -(* main case *) +(* main case *) (* splitting into 4 cases according to a:A, a:B *) by (Asm_full_simp_tac 1); by (safe_tac set_cs); @@ -218,13 +214,13 @@ (* Case y:A, y:B *) by (Seq_case_simp_tac "exA" 1); (* Case exA=UU, Case exA=nil*) -(* These UU and nil cases are the only places where the assumption filter A sch< to generate a contradiction using ~a>>ss<< UU(nil), using theorems +(* These UU and nil cases are the only places where the assumption filter A sch< to generate a contradiction using ~a>>ss<< UU(nil), using theorems Cons_not_less_UU and Cons_not_less_nil *) by (Seq_case_simp_tac "exB" 1); (* Case exA=a>>x, exB=b>>y *) -(* here it is important that Seq_case_simp_tac uses no !full!_simp_tac for the cons case, - as otherwise mkex_cons_3 would not be rewritten without use of rotate_tac: then tactic +(* here it is important that Seq_case_simp_tac uses no !full!_simp_tac for the cons case, + as otherwise mkex_cons_3 would not be rewritten without use of rotate_tac: then tactic would not be generally applicable *) by (Asm_full_simp_tac 1); @@ -243,8 +239,8 @@ (* generalizing the proof above to a tactic *) -fun mkex_induct_tac sch exA exB = - EVERY1[Seq_induct_tac sch [Filter_def,Forall_def,sforall_def,mkex_def,stutter_def], +fun mkex_induct_tac sch exA exB = + EVERY1[Seq_induct_tac sch [Filter_def,Forall_def,sforall_def,mkex_def,stutter_def], Asm_full_simp_tac, SELECT_GOAL (safe_tac set_cs), Seq_case_simp_tac exA, @@ -323,7 +319,7 @@ (*--------------------------------------------------------------------------- - Filter of mkex(sch,exA,exB) to A after projection onto A is exA + Filter of mkex(sch,exA,exB) to A after projection onto A is exA -- using zip$(proj1$exA)$(proj2$exA) instead of exA -- -- because of admissibility problems -- structural induction @@ -342,7 +338,7 @@ (*--------------------------------------------------------------------------- zip$(proj1$y)$(proj2$y) = y (using the lift operations) - lemma for admissibility problems + lemma for admissibility problems --------------------------------------------------------------------------- *) Goal "Zip$(Map fst$y)$(Map snd$y) = y"; @@ -351,8 +347,8 @@ (*--------------------------------------------------------------------------- - filter A$sch = proj1$ex --> zip$(filter A$sch)$(proj2$ex) = ex - lemma for eliminating non admissible equations in assumptions + filter A$sch = proj1$ex --> zip$(filter A$sch)$(proj2$ex) = ex + lemma for eliminating non admissible equations in assumptions --------------------------------------------------------------------------- *) Goal "!! sch ex. \ @@ -363,7 +359,7 @@ qed"trick_against_eq_in_ass"; (*--------------------------------------------------------------------------- - Filter of mkex(sch,exA,exB) to A after projection onto A is exA + Filter of mkex(sch,exA,exB) to A after projection onto A is exA using the above trick --------------------------------------------------------------------------- *) @@ -383,10 +379,10 @@ by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [filter_mkex_is_exA_tmp]) 1); qed"filter_mkex_is_exA"; - + (*--------------------------------------------------------------------------- - Filter of mkex(sch,exA,exB) to B after projection onto B is exB + Filter of mkex(sch,exA,exB) to B after projection onto B is exB -- using zip$(proj1$exB)$(proj2$exB) instead of exB -- -- because of admissibility problems -- structural induction @@ -407,7 +403,7 @@ (*--------------------------------------------------------------------------- - Filter of mkex(sch,exA,exB) to A after projection onto B is exB + Filter of mkex(sch,exA,exB) to A after projection onto B is exB using the above trick --------------------------------------------------------------------------- *) @@ -450,19 +446,19 @@ (* Main Theorem *) (* ------------------------------------------------------------------ *) -Goal +Goal "(sch : schedules (A||B)) = \ \ (Filter (%a. a:act A)$sch : schedules A &\ \ Filter (%a. a:act B)$sch : schedules B &\ \ Forall (%x. x:act (A||B)) sch)"; by (simp_tac (simpset() addsimps [schedules_def, has_schedule_def]) 1); -by (safe_tac set_cs); -(* ==> *) +by (safe_tac set_cs); +(* ==> *) by (res_inst_tac [("x","Filter_ex (asig_of A) (ProjA ex)")] bexI 1); by (asm_full_simp_tac (simpset() addsimps [compositionality_ex]) 2); by (simp_tac (simpset() addsimps [Filter_ex_def,ProjA_def, - lemma_2_1a,lemma_2_1b]) 1); + lemma_2_1a,lemma_2_1b]) 1); by (res_inst_tac [("x","Filter_ex (asig_of B) (ProjB ex)")] bexI 1); by (asm_full_simp_tac (simpset() addsimps [compositionality_ex]) 2); by (simp_tac (simpset() addsimps [Filter_ex_def,ProjB_def, @@ -485,7 +481,7 @@ (* mkex is an execution -- use compositionality on ex-level *) by (asm_full_simp_tac (simpset() addsimps [compositionality_ex]) 1); -by (asm_full_simp_tac (simpset() addsimps +by (asm_full_simp_tac (simpset() addsimps [stutter_mkex_on_A, stutter_mkex_on_B, filter_mkex_is_exB,filter_mkex_is_exA]) 1); by (pair_tac "exA" 1); diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/CompoScheds.thy --- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,59 +1,58 @@ (* Title: HOLCF/IOA/meta_theory/CompoScheds.thy ID: $Id$ Author: Olaf Müller +*) -Compositionality on Schedule level. -*) +header {* Compositionality on Schedule level *} -CompoScheds = CompoExecs + - - +theory CompoScheds +imports CompoExecs +begin consts mkex ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq => - ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution" - mkex2 ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> - ('a,'s)pairs -> ('a,'t)pairs -> + ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution" + mkex2 ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> + ('a,'s)pairs -> ('a,'t)pairs -> ('s => 't => ('a,'s*'t)pairs)" par_scheds ::"['a schedule_module,'a schedule_module] => 'a schedule_module" - defs -mkex_def - "mkex A B sch exA exB == +mkex_def: + "mkex A B sch exA exB == ((fst exA,fst exB), (mkex2 A B$sch$(snd exA)$(snd exB)) (fst exA) (fst exB))" -mkex2_def - "mkex2 A B == (fix$(LAM h sch exA exB. (%s t. case sch of +mkex2_def: + "mkex2 A B == (fix$(LAM h sch exA exB. (%s t. case sch of nil => nil - | x##xs => - (case x of + | x##xs => + (case x of UU => UU - | Def y => - (if y:act A then - (if y:act B then + | Def y => + (if y:act A then + (if y:act B then (case HD$exA of UU => UU | Def a => (case HD$exB of UU => UU - | Def b => + | Def b => (y,(snd a,snd b))>> (h$xs$(TL$exA)$(TL$exB)) (snd a) (snd b))) else (case HD$exA of UU => UU - | Def a => + | Def a => (y,(snd a,t))>>(h$xs$(TL$exA)$exB) (snd a) t) ) - else - (if y:act B then + else + (if y:act B then (case HD$exB of UU => UU - | Def b => + | Def b => (y,(s,snd b))>>(h$xs$exA$(TL$exB)) s (snd b)) else UU @@ -61,14 +60,16 @@ ) ))))" -par_scheds_def - "par_scheds SchedsA SchedsB == - let schA = fst SchedsA; sigA = snd SchedsA; - schB = fst SchedsB; sigB = snd SchedsB +par_scheds_def: + "par_scheds SchedsA SchedsB == + let schA = fst SchedsA; sigA = snd SchedsA; + schB = fst SchedsB; sigB = snd SchedsB in ( {sch. Filter (%a. a:actions sigA)$sch : schA} Int {sch. Filter (%a. a:actions sigB)$sch : schB} Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch}, asig_comp sigA sigB)" +ML {* use_legacy_bindings (the_context ()) *} + end diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/CompoTraces.ML --- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Fri Sep 02 17:23:59 2005 +0200 @@ -1,9 +1,7 @@ (* Title: HOLCF/IOA/meta_theory/CompoTraces.ML - ID: $Id$ + ID: $Id$ Author: Olaf Müller - -Compositionality on Trace level. -*) +*) simpset_ref () := simpset() setmksym (K NONE); @@ -11,15 +9,15 @@ section "mksch rewrite rules"; (* ---------------------------------------------------------------- *) -bind_thm ("mksch_unfold", fix_prover2 thy mksch_def +bind_thm ("mksch_unfold", fix_prover2 (the_context ()) mksch_def "mksch A B = (LAM tr schA schB. case tr of \ \ nil => nil\ \ | x##xs => \ -\ (case x of \ +\ (case x of \ \ UU => UU \ \ | Def y => \ \ (if y:act A then \ -\ (if y:act B then \ +\ (if y:act B then \ \ ((Takewhile (%a. a:int A)$schA) \ \ @@(Takewhile (%a. a:int B)$schB) \ \ @@(y>>(mksch A B$xs \ @@ -33,7 +31,7 @@ \ $schB))) \ \ ) \ \ else \ -\ (if y:act B then \ +\ (if y:act B then \ \ ((Takewhile (%a. a:int B)$schB) \ \ @@ (y>>(mksch A B$xs \ \ $schA \ @@ -103,11 +101,11 @@ (* ---------------------------------------------------------------------------- *) - section"Lemmata for ==>"; + section"Lemmata for ==>"; (* ---------------------------------------------------------------------------- *) -(* Consequence out of ext1_ext2_is_not_act1(2), which in turn are consequences out of - the compatibility of IOA, in particular out of the condition that internals are +(* Consequence out of ext1_ext2_is_not_act1(2), which in turn are consequences out of + the compatibility of IOA, in particular out of the condition that internals are really hidden. *) Goal "(eB & ~eA --> ~A) --> \ @@ -125,18 +123,18 @@ (* ---------------------------------------------------------------------------- *) - section"Lemmata for <=="; + section"Lemmata for <=="; (* ---------------------------------------------------------------------------- *) -(* Lemma for substitution of looping assumption in another specific assumption *) -val [p1,p2] = goal thy "[| f << (g x) ; x=(h x) |] ==> f << g (h x)"; +(* Lemma for substitution of looping assumption in another specific assumption *) +val [p1,p2] = goal (the_context ()) "[| f << (g x) ; x=(h x) |] ==> f << g (h x)"; by (cut_facts_tac [p1] 1); by (etac (p2 RS subst) 1); qed"subst_lemma1"; -(* Lemma for substitution of looping assumption in another specific assumption *) -val [p1,p2] = goal thy "[| (f x) = y >> g; x=(h x) |] ==> (f (h x)) = y >> g"; +(* Lemma for substitution of looping assumption in another specific assumption *) +val [p1,p2] = goal (the_context ()) "[| (f x) = y >> g; x=(h x) |] ==> (f (h x)) = y >> g"; by (cut_facts_tac [p1] 1); by (etac (p2 RS subst) 1); qed"subst_lemma2"; @@ -145,7 +143,7 @@ Goal "!!A B. compatible A B ==> \ \ ! schA schB. Forall (%x. x:act (A||B)) tr \ \ --> Forall (%x. x:act (A||B)) (mksch A B$tr$schA$schB)"; -by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); +by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); by (safe_tac set_cs); by (asm_full_simp_tac (simpset() addsimps [actions_of_par]) 1); by (case_tac "a:act A" 1); @@ -214,7 +212,7 @@ back(); by (REPEAT (etac conjE 1)); (* Finite (tw iA x) and Finite (tw iB y) *) -by (asm_full_simp_tac (simpset() addsimps +by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,FiniteConc]) 1); (* now for conclusion IH applicable, but assumptions have to be transformed *) by (dres_inst_tac [("x","x"), @@ -232,7 +230,7 @@ by (REPEAT (etac conjE 1)); (* Finite (tw iB y) *) -by (asm_full_simp_tac (simpset() addsimps +by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,FiniteConc]) 1); (* now for conclusion IH applicable, but assumptions have to be transformed *) by (dres_inst_tac [("x","y"), @@ -247,7 +245,7 @@ by (REPEAT (etac conjE 1)); (* Finite (tw iA x) *) -by (asm_full_simp_tac (simpset() addsimps +by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,FiniteConc]) 1); (* now for conclusion IH applicable, but assumptions have to be transformed *) by (dres_inst_tac [("x","x"), @@ -258,7 +256,7 @@ addsimps [not_ext_is_int_or_not_act,ForallTL,ForallDropwhile]) 1); (* a~: act B; a~: act A *) -by (fast_tac (claset() addSIs [ext_is_act] +by (fast_tac (claset() addSIs [ext_is_act] addss (simpset() addsimps [externals_of_par]) ) 1); qed_spec_mp"FiniteL_mksch"; @@ -266,7 +264,7 @@ (* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *) -Delsimps [FilterConc]; +Delsimps [FilterConc]; 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 &\ @@ -295,31 +293,31 @@ by (dres_inst_tac [("x","y"), ("g","Filter (%a. a:act B)$(s@@z)")] subst_lemma2 1); by (assume_tac 1); -Addsimps [FilterConc]; +Addsimps [FilterConc]; by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act]) 1); (* apply IH *) by (eres_inst_tac [("x","TL$(Dropwhile (%a. a:int B)$y)")] allE 1); by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile])1); by (REPEAT (etac exE 1)); by (REPEAT (etac conjE 1)); -by (Asm_full_simp_tac 1); +by (Asm_full_simp_tac 1); (* for replacing IH in conclusion *) -by (rotate_tac ~2 1); -by (Asm_full_simp_tac 1); +by (rotate_tac ~2 1); +by (Asm_full_simp_tac 1); (* instantiate y1a and y2a *) by (res_inst_tac [("x","Takewhile (%a. a:int B)$y @@ a>>y1")] exI 1); by (res_inst_tac [("x","y2")] exI 1); (* elminate all obligations up to two depending on Conc_assoc *) by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, intA_is_not_actB, - int_is_act,int_is_not_ext]) 1); -by (simp_tac (simpset() addsimps [Conc_assoc]) 1); + int_is_act,int_is_not_ext]) 1); +by (simp_tac (simpset() addsimps [Conc_assoc]) 1); qed_spec_mp "reduceA_mksch1"; bind_thm("reduceA_mksch",conjI RSN (6,conjI RSN (5,reduceA_mksch1))); (* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *) -Delsimps [FilterConc]; +Delsimps [FilterConc]; Goal " [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==> \ @@ -349,24 +347,24 @@ by (dres_inst_tac [("x","x"), ("g","Filter (%a. a:act A)$(s@@z)")] subst_lemma2 1); by (assume_tac 1); -Addsimps [FilterConc]; +Addsimps [FilterConc]; by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act]) 1); (* apply IH *) by (eres_inst_tac [("x","TL$(Dropwhile (%a. a:int A)$x)")] allE 1); by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile])1); by (REPEAT (etac exE 1)); by (REPEAT (etac conjE 1)); -by (Asm_full_simp_tac 1); +by (Asm_full_simp_tac 1); (* for replacing IH in conclusion *) -by (rotate_tac ~2 1); -by (Asm_full_simp_tac 1); +by (rotate_tac ~2 1); +by (Asm_full_simp_tac 1); (* instantiate y1a and y2a *) by (res_inst_tac [("x","Takewhile (%a. a:int A)$x @@ a>>x1")] exI 1); by (res_inst_tac [("x","x2")] exI 1); (* elminate all obligations up to two depending on Conc_assoc *) by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, intA_is_not_actB, - int_is_act,int_is_not_ext]) 1); -by (simp_tac (simpset() addsimps [Conc_assoc]) 1); + int_is_act,int_is_not_ext]) 1); +by (simp_tac (simpset() addsimps [Conc_assoc]) 1); qed_spec_mp"reduceB_mksch1"; bind_thm("reduceB_mksch",conjI RSN (6,conjI RSN (5,reduceB_mksch1))); @@ -397,7 +395,7 @@ by (case_tac "s:act B" 1); by (rotate_tac ~2 1); by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc,nil_is_Conc2]) 1); -by (fast_tac (claset() addSIs [ext_is_act] +by (fast_tac (claset() addSIs [ext_is_act] addss (simpset() addsimps [externals_of_par]) ) 1); (* main case *) by (Seq_case_simp_tac "tr" 1); @@ -455,13 +453,13 @@ *) - + (*------------------------------------------------------------------------------------- *) section"Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr"; (* structural induction ------------------------------------------------------------------------------------- *) -Goal +Goal "!! A B. [| compatible A B; compatible B A;\ \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \ \ ! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \ @@ -472,7 +470,7 @@ by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); -(* main case *) +(* main case *) (* splitting into 4 cases according to a:A, a:B *) by (Asm_full_simp_tac 1); by (safe_tac set_cs); @@ -483,7 +481,7 @@ back(); by (REPEAT (etac conjE 1)); (* filtering internals of A in schA and of B in schB is nil *) -by (asm_full_simp_tac (simpset() addsimps +by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act, externals_of_par, intA_is_not_extB,int_is_not_ext]) 1); (* conclusion of IH ok, but assumptions of IH have to be transformed *) @@ -499,7 +497,7 @@ by (ftac divide_Seq 1); by (REPEAT (etac conjE 1)); (* filtering internals of A is nil *) -by (asm_full_simp_tac (simpset() addsimps +by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act, externals_of_par, intA_is_not_extB,int_is_not_ext]) 1); by (dres_inst_tac [("x","schA")] subst_lemma1 1); @@ -511,7 +509,7 @@ by (ftac divide_Seq 1); by (REPEAT (etac conjE 1)); (* filtering internals of A is nil *) -by (asm_full_simp_tac (simpset() addsimps +by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act, externals_of_par, intA_is_not_extB,int_is_not_ext]) 1); by (dres_inst_tac [("x","schB")] subst_lemma1 1); @@ -521,7 +519,7 @@ ForallTL,ForallDropwhile]) 1); (* Case a~:A, a~:B *) -by (fast_tac (claset() addSIs [ext_is_act] +by (fast_tac (claset() addSIs [ext_is_act] addss (simpset() addsimps [externals_of_par]) ) 1); qed"FilterA_mksch_is_tr"; @@ -534,7 +532,7 @@ ********************************************************************** (*--------------------------------------------------------------------------- - Filter of mksch(tr,schA,schB) to A is schA + Filter of mksch(tr,schA,schB) to A is schA take lemma --------------------------------------------------------------------------- *) @@ -616,7 +614,7 @@ by (etac ForallQFilterPnil 2); by (assume_tac 2); by (Fast_tac 2); - + (* bring in divide Seq for s *) by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1); by (REPEAT (etac conjE 1)); @@ -639,7 +637,7 @@ (* now conclusion fulfills induction hypothesis, but assumptions are not ready *) (* -nacessary anymore ???????????????? +nacessary anymore ???????????????? by (rotate_tac ~10 1); *) @@ -666,8 +664,8 @@ (*--------------------------------------------------------------------------- *) - section" Filter of mksch(tr,schA,schB) to A is schA -- take lemma proof"; - + section" Filter of mksch(tr,schA,schB) to A is schA -- take lemma proof"; + (* --------------------------------------------------------------------------- *) @@ -772,7 +770,7 @@ by (etac ForallQFilterPnil 2); by (assume_tac 2); by (Fast_tac 2); - + (* bring in divide Seq for s *) by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1); by (REPEAT (etac conjE 1)); @@ -860,7 +858,7 @@ by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext]) 1); -(* f A (tw iB schB2) = nil *) +(* f A (tw iB schB2) = nil *) by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext,not_ext_is_int_or_not_act, intA_is_not_actB]) 1); @@ -907,7 +905,7 @@ (*--------------------------------------------------------------------------- *) section" Filter of mksch(tr,schA,schB) to B is schB -- take lemma proof"; - + (* --------------------------------------------------------------------------- *) @@ -1014,7 +1012,7 @@ by (etac ForallQFilterPnil 2); by (assume_tac 2); by (Fast_tac 2); - + (* bring in divide Seq for s *) by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1); by (REPEAT (etac conjE 1)); @@ -1073,7 +1071,7 @@ by (etac ForallQFilterPnil 2); by (assume_tac 2); by (Fast_tac 2); - + (* bring in divide Seq for s *) by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1); by (REPEAT (etac conjE 1)); @@ -1102,7 +1100,7 @@ by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext]) 1); -(* f B (tw iA schA2) = nil *) +(* f B (tw iA schA2) = nil *) by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext,not_ext_is_int_or_not_act, intA_is_not_actB]) 1); @@ -1149,8 +1147,8 @@ (* ------------------------------------------------------------------ *) section"COMPOSITIONALITY on TRACE Level -- Main Theorem"; (* ------------------------------------------------------------------ *) - -Goal + +Goal "!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \ \ is_asig(asig_of A); is_asig(asig_of B)|] \ \ ==> (tr: traces(A||B)) = \ @@ -1160,8 +1158,8 @@ by (simp_tac (simpset() addsimps [traces_def,has_trace_def]) 1); by (safe_tac set_cs); - -(* ==> *) + +(* ==> *) (* There is a schedule of A *) by (res_inst_tac [("x","Filter (%a. a:act A)$sch")] bexI 1); by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 2); @@ -1172,7 +1170,7 @@ by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 2); by (asm_full_simp_tac (simpset() addsimps [compatibility_consequence2, externals_of_par,ext1_ext2_is_not_act2]) 1); -(* Traces of A||B have only external actions from A or B *) +(* Traces of A||B have only external actions from A or B *) by (rtac ForallPFilterP 1); (* <== *) diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/CompoTraces.thy --- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,11 +1,13 @@ (* Title: HOLCF/IOA/meta_theory/CompoTraces.thy ID: $Id$ Author: Olaf Müller - -Compositionality on Trace level. *) -CompoTraces = CompoScheds + ShortExecutions + +header {* Compositionality on Trace level *} + +theory CompoTraces +imports CompoScheds ShortExecutions +begin consts @@ -15,7 +17,7 @@ defs -mksch_def +mksch_def: "mksch A B == (fix$(LAM h tr schA schB. case tr of nil => nil | x##xs => @@ -50,7 +52,7 @@ )))" -par_traces_def +par_traces_def: "par_traces TracesA TracesB == let trA = fst TracesA; sigA = snd TracesA; trB = fst TracesB; sigB = snd TracesB @@ -60,12 +62,12 @@ Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr}, asig_comp sigA sigB)" -rules +axioms - -finiteR_mksch +finiteR_mksch: "Finite (mksch A B$tr$x$y) --> Finite tr" +ML {* use_legacy_bindings (the_context ()) *} end diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/Compositionality.ML --- a/src/HOLCF/IOA/meta_theory/Compositionality.ML Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML Fri Sep 02 17:23:59 2005 +0200 @@ -1,25 +1,21 @@ (* Title: HOLCF/IOA/meta_theory/Compositionality.ML ID: $Id$ Author: Olaf Müller - -Compositionality of I/O automata -*) - - +*) Goal "[|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA"; by Auto_tac; qed"compatibility_consequence3"; -Goal +Goal "!! A B. [| compatible A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \ \ Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr"; by (rtac ForallPFilterQR 1); (* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q$tr = Filter R$tr *) by (assume_tac 2); by (rtac compatibility_consequence3 1); -by (REPEAT (asm_full_simp_tac (simpset() +by (REPEAT (asm_full_simp_tac (simpset() addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1)); qed"Filter_actAisFilter_extA"; @@ -35,7 +31,7 @@ by (rtac ForallPFilterQR 1); by (assume_tac 2); by (rtac compatibility_consequence4 1); -by (REPEAT (asm_full_simp_tac (simpset() +by (REPEAT (asm_full_simp_tac (simpset() addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1)); qed"Filter_actAisFilter_extA2"; @@ -78,7 +74,3 @@ by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [Filter_actAisFilter_extA2]) 1); qed"compositionality"; - - - - diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/Compositionality.thy --- a/src/HOLCF/IOA/meta_theory/Compositionality.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Compositionality.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,8 +1,11 @@ (* Title: HOLCF/IOA/meta_theory/Compositionality.thy ID: $Id$ Author: Olaf Müller +*) -Compositionality of I/O automata. -*) +header {* Compositionality of I/O automata *} +theory Compositionality +imports CompoTraces +begin -Compositionality = CompoTraces +end diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/Deadlock.ML --- a/src/HOLCF/IOA/meta_theory/Deadlock.ML Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML Fri Sep 02 17:23:59 2005 +0200 @@ -1,9 +1,7 @@ (* Title: HOLCF/IOA/meta_theory/Deadlock.ML ID: $Id$ Author: Olaf Müller - -Deadlock freedom of I/O Automata. -*) +*) (******************************************************************************** input actions may always be added to a schedule @@ -83,7 +81,3 @@ qed"IOA_deadlock_free"; Addsplits [split_if]; - - - - diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/Deadlock.thy --- a/src/HOLCF/IOA/meta_theory/Deadlock.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Deadlock.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,8 +1,12 @@ (* Title: HOLCF/IOA/meta_theory/Deadlock.thy ID: $Id$ Author: Olaf Müller +*) -Deadlock freedom of I/O Automata. -*) +header {* Deadlock freedom of I/O Automata *} -Deadlock = RefCorrectness + CompoScheds +theory Deadlock +imports RefCorrectness CompoScheds +begin + +end diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/IOA.thy --- a/src/HOLCF/IOA/meta_theory/IOA.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/IOA.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,8 +1,12 @@ (* Title: HOLCF/IOA/meta_theory/IOA.thy ID: $Id$ Author: Olaf Müller +*) -The theory of I/O automata in HOLCF. -*) - -IOA = SimCorrectness + Compositionality + Deadlock +header {* The theory of I/O automata in HOLCF *} + +theory IOA +imports SimCorrectness Compositionality Deadlock +begin + +end diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/LiveIOA.ML --- a/src/HOLCF/IOA/meta_theory/LiveIOA.ML Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.ML Fri Sep 02 17:23:59 2005 +0200 @@ -1,8 +1,6 @@ (* Title: HOLCF/IOA/meta_theory/LiveIOA.ML ID: $Id$ Author: Olaf Müller - -Live I/O Automata. *) Delsimps [split_paired_Ex]; diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/LiveIOA.thy --- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,18 +1,19 @@ (* Title: HOLCF/IOA/meta_theory/LiveIOA.thy ID: $Id$ Author: Olaf Müller +*) -Live I/O automata -- specified by temproal formulas. -*) - -LiveIOA = TLS + +header {* Live I/O automata -- specified by temproal formulas *} -default type +theory LiveIOA +imports TLS +begin + +defaultsort type types + ('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp" - ('a,'s)live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp" - consts validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp => bool" @@ -25,36 +26,37 @@ live_implements :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" is_live_ref_map :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" - + defs -validLIOA_def +validLIOA_def: "validLIOA AL P == validIOA (fst AL) ((snd AL) .--> P)" -WF_def +WF_def: "WF A acts == <> [] <%(s,a,t) . Enabled A acts s> .--> [] <> " -SF_def +SF_def: "SF A acts == [] <> <%(s,a,t) . Enabled A acts s> .--> [] <> " - + -liveexecutions_def +liveexecutions_def: "liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}" -livetraces_def +livetraces_def: "livetraces AP == {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}" -live_implements_def - "live_implements CL AM == (inp (fst CL) = inp (fst AM)) & +live_implements_def: + "live_implements CL AM == (inp (fst CL) = inp (fst AM)) & (out (fst CL) = out (fst AM)) & livetraces CL <= livetraces AM" -is_live_ref_map_def - "is_live_ref_map f CL AM == - is_ref_map f (fst CL ) (fst AM) & - (! exec : executions (fst CL). (exec |== (snd CL)) --> +is_live_ref_map_def: + "is_live_ref_map f CL AM == + is_ref_map f (fst CL ) (fst AM) & + (! exec : executions (fst CL). (exec |== (snd CL)) --> ((corresp_ex (fst AM) f exec) |== (snd AM)))" +ML {* use_legacy_bindings (the_context ()) *} -end \ No newline at end of file +end diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/Pred.thy --- a/src/HOLCF/IOA/meta_theory/Pred.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,22 +1,23 @@ (* Title: HOLCF/IOA/meta_theory/Pred.thy ID: $Id$ Author: Olaf Müller +*) -Logical Connectives lifted to predicates. -*) - -Pred = Main + +header {* Logical Connectives lifted to predicates *} -default type +theory Pred +imports Main +begin + +defaultsort type types - -'a predicate = "'a => bool" + 'a predicate = "'a => bool" consts satisfies ::"'a => 'a predicate => bool" ("_ |= _" [100,9] 8) -valid ::"'a predicate => bool" (* ("|-") *) +valid ::"'a predicate => bool" (* ("|-") *) NOT ::"'a predicate => 'a predicate" (".~ _" [40] 40) AND ::"'a predicate => 'a predicate => 'a predicate" (infixr ".&" 35) @@ -31,41 +32,41 @@ "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "-->" 25) syntax (xsymbols output) - "NOT" ::"'a predicate => 'a predicate" ("\\ _" [40] 40) - "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\\" 35) - "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\\" 30) - "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\\" 25) + "NOT" ::"'a predicate => 'a predicate" ("\ _" [40] 40) + "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\" 35) + "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\" 30) + "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\" 25) syntax (xsymbols) - "satisfies" ::"'a => 'a predicate => bool" ("_ \\ _" [100,9] 8) + "satisfies" ::"'a => 'a predicate => bool" ("_ \ _" [100,9] 8) syntax (HTML output) - "NOT" ::"'a predicate => 'a predicate" ("\\ _" [40] 40) - "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\\" 35) - "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\\" 30) + "NOT" ::"'a predicate => 'a predicate" ("\ _" [40] 40) + "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\" 35) + "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\" 30) defs -satisfies_def - "s |= P == P s" +satisfies_def: + "s |= P == P s" (* priority einfuegen, da clash mit |=, wenn graphisches Symbol *) -valid_def +valid_def: "valid P == (! s. (s |= P))" - -NOT_def +NOT_def: "NOT P s == ~ (P s)" -AND_def +AND_def: "(P .& Q) s == (P s) & (Q s)" - -OR_def +OR_def: "(P .| Q) s == (P s) | (Q s)" -IMPLIES_def +IMPLIES_def: "(P .--> Q) s == (P s) --> (Q s)" +ML {* use_legacy_bindings (the_context ()) *} + end diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/RefCorrectness.ML --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Fri Sep 02 17:23:59 2005 +0200 @@ -1,12 +1,9 @@ (* Title: HOLCF/IOA/meta_theory/RefCorrectness.ML ID: $Id$ Author: Olaf Müller - -Correctness of Refinement Mappings in HOLCF/IOA. *) - (* -------------------------------------------------------------------------------- *) section "corresp_ex"; @@ -126,23 +123,23 @@ (* ------------------------------------------------------ - Lemma 1 :Traces coincide + Lemma 1 :Traces coincide ------------------------------------------------------- *) Delsplits[split_if]; Goalw [corresp_ex_def] - "[|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)))"; by (pair_induct_tac "xs" [is_exec_frag_def] 1); -(* cons case *) +(* cons case *) by (safe_tac set_cs); by (asm_full_simp_tac (simpset() addsimps [mk_traceConc]) 1); by (forward_tac [reachable.reachable_n] 1); by (assume_tac 1); by (eres_inst_tac [("x","y")] allE 1); by (Asm_full_simp_tac 1); -by (asm_full_simp_tac (simpset() addsimps [move_subprop4] +by (asm_full_simp_tac (simpset() addsimps [move_subprop4] addsplits [split_if]) 1); qed"lemma_1"; Addsplits[split_if]; @@ -158,9 +155,9 @@ (* Lemma 2.1 *) (* -------------------------------------------------- *) -Goal +Goal "Finite xs --> \ -\(!s .is_exec_frag A (s,xs) & is_exec_frag A (t,ys) & \ +\(!s .is_exec_frag A (s,xs) & is_exec_frag A (t,ys) & \ \ t = laststate (s,xs) \ \ --> is_exec_frag A (s,xs @@ ys))"; @@ -181,7 +178,7 @@ Goalw [corresp_ex_def] "[| 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))"; +\ --> is_exec_frag A (corresp_ex A f (s,xs))"; by (Asm_full_simp_tac 1); by (pair_induct_tac "xs" [is_exec_frag_def] 1); @@ -221,30 +218,30 @@ Goalw [traces_def] "[| ext C = ext A; is_ref_map f C A |] \ -\ ==> traces C <= traces A"; +\ ==> traces C <= traces A"; by (simp_tac(simpset() addsimps [has_trace_def2])1); by (safe_tac set_cs); (* give execution of abstract automata *) by (res_inst_tac[("x","corresp_ex A f ex")] bexI 1); - + (* Traces coincide, Lemma 1 *) by (pair_tac "ex" 1); by (etac (lemma_1 RS spec RS mp) 1); by (REPEAT (atac 1)); by (asm_full_simp_tac (simpset() addsimps [executions_def,reachable.reachable_0]) 1); - + (* corresp_ex is execution, Lemma 2 *) by (pair_tac "ex" 1); by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1); - (* start state *) + (* start state *) by (rtac conjI 1); by (asm_full_simp_tac (simpset() addsimps [is_ref_map_def,corresp_ex_def]) 1); (* is-execution-fragment *) by (etac (lemma_2 RS spec RS mp) 1); by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1); -qed"trace_inclusion"; +qed"trace_inclusion"; (* -------------------------------------------------------------------------------- *) @@ -290,11 +287,11 @@ by (etac (lemma_1 RS spec RS mp) 1); by (REPEAT (atac 1)); by (asm_full_simp_tac (simpset() addsimps [executions_def,reachable.reachable_0]) 1); - + (* corresp_ex is execution, Lemma 2 *) by (pair_tac "ex" 1); by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1); - (* start state *) + (* start state *) by (rtac conjI 1); by (asm_full_simp_tac (simpset() addsimps [is_ref_map_def,corresp_ex_def]) 1); (* is-execution-fragment *) @@ -320,11 +317,11 @@ by (simp_tac (simpset() addsimps [externals_def])1); by (SELECT_GOAL (auto_tac (claset(),simpset()))1); by (asm_full_simp_tac (simpset() addsimps [executions_def,reachable.reachable_0]) 1); - + (* corresp_ex is execution, Lemma 2 *) by (pair_tac "ex" 1); by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1); - (* start state *) + (* start state *) by (rtac conjI 1); by (asm_full_simp_tac (simpset() addsimps [is_ref_map_def,corresp_ex_def]) 1); (* is-execution-fragment *) @@ -334,8 +331,3 @@ (* Fairness *) by Auto_tac; qed"fair_trace_inclusion2"; - - - - - diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/RefCorrectness.thy --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,16 +1,17 @@ (* Title: HOLCF/IOA/meta_theory/RefCorrectness.thy ID: $Id$ Author: Olaf Müller - -Correctness of Refinement Mappings in HOLCF/IOA. *) +header {* Correctness of Refinement Mappings in HOLCF/IOA *} -RefCorrectness = RefMappings + - +theory RefCorrectness +imports RefMappings +begin + consts - corresp_ex ::"('a,'s2)ioa => ('s1 => 's2) => + corresp_ex ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution" corresp_exC ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs -> ('s1 => ('a,'s2)pairs)" @@ -18,39 +19,39 @@ defs -corresp_ex_def +corresp_ex_def: "corresp_ex A f ex == (f (fst ex),(corresp_exC A f$(snd ex)) (fst ex))" -corresp_exC_def - "corresp_exC A f == (fix$(LAM h ex. (%s. case ex of +corresp_exC_def: + "corresp_exC A f == (fix$(LAM h ex. (%s. case ex of nil => nil | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr))) @@ ((h$xs) (snd pr))) $x) )))" - -is_fair_ref_map_def - "is_fair_ref_map f C A == + +is_fair_ref_map_def: + "is_fair_ref_map f C A == is_ref_map f C A & (! ex : executions(C). fair_ex C ex --> fair_ex A (corresp_ex A f ex))" -rules +axioms (* Axioms for fair trace inclusion proof support, not for the correctness proof - of refinement mappings ! + of refinement mappings! Note: Everything is superseded by LiveIOA.thy! *) -corresp_laststate +corresp_laststate: "Finite ex ==> laststate (corresp_ex A f (s,ex)) = f (laststate (s,ex))" -corresp_Finite +corresp_Finite: "Finite (snd (corresp_ex A f (s,ex))) = Finite ex" -FromAtoC +FromAtoC: "fin_often (%x. P (snd x)) (snd (corresp_ex A f (s,ex))) ==> fin_often (%y. P (f (snd y))) ex" -FromCtoA +FromCtoA: "inf_often (%y. P (fst y)) ex ==> inf_often (%x. P (fst x)) (snd (corresp_ex A f (s,ex)))" @@ -58,12 +59,14 @@ an index i from which on no W in ex. But W inf enabled, ie at least once after i W is enabled. As W does not occur after i and W is enabling_persistent, W keeps enabled until infinity, ie. indefinitely *) -persistent +persistent: "[|inf_often (%x. Enabled A W (snd x)) ex; en_persistent A W|] ==> inf_often (%x. fst x :W) ex | fin_often (%x. ~Enabled A W (snd x)) ex" -infpostcond +infpostcond: "[| is_exec_frag A (s,ex); inf_often (%x. fst x:W) ex|] ==> inf_often (% x. set_was_enabled A W (snd x)) ex" -end \ No newline at end of file +ML {* use_legacy_bindings (the_context ()) *} + +end diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/RefMappings.ML --- a/src/HOLCF/IOA/meta_theory/RefMappings.ML Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Fri Sep 02 17:23:59 2005 +0200 @@ -1,8 +1,6 @@ (* Title: HOLCF/IOA/meta_theory/RefMappings.ML ID: $Id$ Author: Olaf Müller - -Refinement Mappings in HOLCF/IOA. *) @@ -16,7 +14,7 @@ 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 "(~a:ext A) & s=t ==> ? ex. move A ex s a t"; @@ -36,7 +34,7 @@ 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"; - + by (res_inst_tac [("x","(a1,s2)>>(a2,s3)>>(a3,s4)>>nil")] exI 1); by (asm_full_simp_tac (simpset() addsimps [move_def]) 1); qed"eii_transitions_are_ex"; @@ -105,5 +103,3 @@ by Auto_tac; qed"rename_through_pmap"; Addsplits [split_if]; Addcongs [if_weak_cong]; - - diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/RefMappings.thy --- a/src/HOLCF/IOA/meta_theory/RefMappings.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,45 +1,46 @@ (* Title: HOLCF/IOA/meta_theory/RefMappings.thy ID: $Id$ Author: Olaf Müller - -Refinement Mappings in HOLCF/IOA. *) -RefMappings = Traces + +header {* Refinement Mappings in HOLCF/IOA *} -default type +theory RefMappings +imports Traces +begin + +defaultsort type consts - move ::"[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" is_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" is_weak_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" - + defs - -move_def - "move ioa ex s a t == - (is_exec_frag ioa (s,ex) & Finite ex & - laststate (s,ex)=t & +move_def: + "move ioa ex s a t == + (is_exec_frag ioa (s,ex) & Finite ex & + laststate (s,ex)=t & mk_trace ioa$ex = (if a:ext(ioa) then a>>nil else nil))" -is_ref_map_def - "is_ref_map f C A == - (!s:starts_of(C). f(s):starts_of(A)) & - (!s t a. reachable C s & - s -a--C-> t +is_ref_map_def: + "is_ref_map f C A == + (!s:starts_of(C). f(s):starts_of(A)) & + (!s t a. reachable C s & + s -a--C-> t --> (? ex. move A ex (f s) a (f t)))" - -is_weak_ref_map_def - "is_weak_ref_map f C A == - (!s:starts_of(C). f(s):starts_of(A)) & - (!s t a. reachable C s & - s -a--C-> t - --> (if a:ext(C) + +is_weak_ref_map_def: + "is_weak_ref_map f C A == + (!s:starts_of(C). f(s):starts_of(A)) & + (!s t a. reachable C s & + s -a--C-> t + --> (if a:ext(C) then (f s) -a--A-> (f t) - else (f s)=(f t)))" + else (f s)=(f t)))" +ML {* use_legacy_bindings (the_context ()) *} end diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/Seq.ML --- a/src/HOLCF/IOA/meta_theory/Seq.ML Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Seq.ML Fri Sep 02 17:23:59 2005 +0200 @@ -1,9 +1,9 @@ (* Title: HOLCF/IOA/meta_theory/Seq.ML ID: $Id$ Author: Olaf Mller -*) +*) -Addsimps (sfinite.intrs @ seq.rews); +Addsimps (sfinite.intros @ seq.rews); (* Instead of adding UU_neq_nil every equation UU~=x could be changed to x~=UU *) @@ -30,23 +30,23 @@ (* smap *) (* ----------------------------------------------------------- *) -bind_thm ("smap_unfold", fix_prover2 thy smap_def +bind_thm ("smap_unfold", fix_prover2 (the_context ()) smap_def "smap = (LAM f tr. case tr of \ \ nil => nil \ \ | x##xs => f$x ## smap$f$xs)"); -Goal "smap$f$nil=nil"; +Goal "smap$f$nil=nil"; by (stac smap_unfold 1); by (Simp_tac 1); qed"smap_nil"; -Goal "smap$f$UU=UU"; +Goal "smap$f$UU=UU"; by (stac smap_unfold 1); by (Simp_tac 1); qed"smap_UU"; -Goal -"[|x~=UU|] ==> smap$f$(x##xs)= (f$x)##smap$f$xs"; +Goal +"[|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); @@ -57,7 +57,7 @@ (* sfilter *) (* ----------------------------------------------------------- *) -bind_thm ("sfilter_unfold", fix_prover2 thy sfilter_def +bind_thm ("sfilter_unfold", fix_prover2 (the_context ()) sfilter_def "sfilter = (LAM P tr. case tr of \ \ nil => nil \ \ | x##xs => If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)"); @@ -72,7 +72,7 @@ by (Simp_tac 1); qed"sfilter_UU"; -Goal +Goal "x~=UU ==> sfilter$P$(x##xs)= \ \ (If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)"; by (rtac trans 1); @@ -85,22 +85,22 @@ (* sforall2 *) (* ----------------------------------------------------------- *) -bind_thm ("sforall2_unfold", fix_prover2 thy sforall2_def +bind_thm ("sforall2_unfold", fix_prover2 (the_context ()) sforall2_def "sforall2 = (LAM P tr. case tr of \ \ nil => TT \ \ | x##xs => (P$x andalso sforall2$P$xs))"); -Goal "sforall2$P$nil=TT"; +Goal "sforall2$P$nil=TT"; by (stac sforall2_unfold 1); by (Simp_tac 1); qed"sforall2_nil"; -Goal "sforall2$P$UU=UU"; +Goal "sforall2$P$UU=UU"; by (stac sforall2_unfold 1); by (Simp_tac 1); qed"sforall2_UU"; -Goal +Goal "x~=UU ==> sforall2$P$(x##xs)= ((P$x) andalso sforall2$P$xs)"; by (rtac trans 1); by (stac sforall2_unfold 1); @@ -114,22 +114,22 @@ (* ----------------------------------------------------------- *) -bind_thm ("stakewhile_unfold", fix_prover2 thy stakewhile_def +bind_thm ("stakewhile_unfold", fix_prover2 (the_context ()) stakewhile_def "stakewhile = (LAM P tr. case tr of \ \ nil => nil \ \ | x##xs => (If P$x then x##(stakewhile$P$xs) else nil fi))"); -Goal "stakewhile$P$nil=nil"; +Goal "stakewhile$P$nil=nil"; by (stac stakewhile_unfold 1); by (Simp_tac 1); qed"stakewhile_nil"; -Goal "stakewhile$P$UU=UU"; +Goal "stakewhile$P$UU=UU"; by (stac stakewhile_unfold 1); by (Simp_tac 1); qed"stakewhile_UU"; -Goal +Goal "x~=UU ==> stakewhile$P$(x##xs) = \ \ (If P$x then x##(stakewhile$P$xs) else nil fi)"; by (rtac trans 1); @@ -143,22 +143,22 @@ (* ----------------------------------------------------------- *) -bind_thm ("sdropwhile_unfold", fix_prover2 thy sdropwhile_def +bind_thm ("sdropwhile_unfold", fix_prover2 (the_context ()) sdropwhile_def "sdropwhile = (LAM P tr. case tr of \ \ nil => nil \ \ | x##xs => (If P$x then sdropwhile$P$xs else tr fi))"); -Goal "sdropwhile$P$nil=nil"; +Goal "sdropwhile$P$nil=nil"; by (stac sdropwhile_unfold 1); by (Simp_tac 1); qed"sdropwhile_nil"; -Goal "sdropwhile$P$UU=UU"; +Goal "sdropwhile$P$UU=UU"; by (stac sdropwhile_unfold 1); by (Simp_tac 1); qed"sdropwhile_UU"; -Goal +Goal "x~=UU ==> sdropwhile$P$(x##xs) = \ \ (If P$x then sdropwhile$P$xs else x##xs fi)"; by (rtac trans 1); @@ -173,23 +173,23 @@ (* ----------------------------------------------------------- *) -bind_thm ("slast_unfold", fix_prover2 thy slast_def +bind_thm ("slast_unfold", fix_prover2 (the_context ()) slast_def "slast = (LAM tr. case tr of \ \ nil => UU \ \ | x##xs => (If is_nil$xs then x else slast$xs fi))"); -Goal "slast$nil=UU"; +Goal "slast$nil=UU"; by (stac slast_unfold 1); by (Simp_tac 1); qed"slast_nil"; -Goal "slast$UU=UU"; +Goal "slast$UU=UU"; by (stac slast_unfold 1); by (Simp_tac 1); qed"slast_UU"; -Goal +Goal "x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs fi)"; by (rtac trans 1); by (stac slast_unfold 1); @@ -202,18 +202,18 @@ (* sconc *) (* ----------------------------------------------------------- *) -bind_thm ("sconc_unfold", fix_prover2 thy sconc_def +bind_thm ("sconc_unfold", fix_prover2 (the_context ()) sconc_def "sconc = (LAM t1 t2. case t1 of \ \ nil => t2 \ \ | x##xs => x ## (xs @@ t2))"); -Goal "nil @@ y = y"; +Goal "nil @@ y = y"; by (stac sconc_unfold 1); by (Simp_tac 1); qed"sconc_nil"; -Goal "UU @@ y=UU"; +Goal "UU @@ y=UU"; by (stac sconc_unfold 1); by (Simp_tac 1); qed"sconc_UU"; @@ -233,22 +233,22 @@ (* sflat *) (* ----------------------------------------------------------- *) -bind_thm ("sflat_unfold", fix_prover2 thy sflat_def +bind_thm ("sflat_unfold", fix_prover2 (the_context ()) sflat_def "sflat = (LAM tr. case tr of \ \ nil => nil \ \ | x##xs => x @@ sflat$xs)"); -Goal "sflat$nil=nil"; +Goal "sflat$nil=nil"; by (stac sflat_unfold 1); by (Simp_tac 1); qed"sflat_nil"; -Goal "sflat$UU=UU"; +Goal "sflat$UU=UU"; by (stac sflat_unfold 1); by (Simp_tac 1); qed"sflat_UU"; -Goal "sflat$(x##xs)= x@@(sflat$xs)"; +Goal "sflat$(x##xs)= x@@(sflat$xs)"; by (rtac trans 1); by (stac sflat_unfold 1); by (Asm_full_simp_tac 1); @@ -263,24 +263,24 @@ (* szip *) (* ----------------------------------------------------------- *) -bind_thm ("szip_unfold", fix_prover2 thy szip_def +bind_thm ("szip_unfold", fix_prover2 (the_context ()) szip_def "szip = (LAM t1 t2. case t1 of \ \ nil => nil \ \ | x##xs => (case t2 of \ \ nil => UU \ \ | y##ys => ##(szip$xs$ys)))"); -Goal "szip$nil$y=nil"; +Goal "szip$nil$y=nil"; by (stac szip_unfold 1); by (Simp_tac 1); qed"szip_nil"; -Goal "szip$UU$y=UU"; +Goal "szip$UU$y=UU"; by (stac szip_unfold 1); by (Simp_tac 1); qed"szip_UU1"; -Goal "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); @@ -304,10 +304,10 @@ smap_UU,smap_nil,smap_cons, sforall2_UU,sforall2_nil,sforall2_cons, slast_UU,slast_nil,slast_cons, - stakewhile_UU, stakewhile_nil, stakewhile_cons, + stakewhile_UU, stakewhile_nil, stakewhile_cons, sdropwhile_UU, sdropwhile_nil, sdropwhile_cons, sflat_UU,sflat_nil,sflat_cons, - szip_UU1,szip_UU2,szip_nil,szip_cons_nil,szip_cons]; + szip_UU1,szip_UU2,szip_nil,szip_cons_nil,szip_cons]; @@ -315,7 +315,7 @@ section "scons, nil"; -Goal +Goal "[|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)"; by (rtac iffI 1); by (etac (hd seq.injects) 1); @@ -436,7 +436,7 @@ (*-------------------------------- *) -qed_goalw "seq_finite_ind_lemma" thy [seq.finite_def] +qed_goalw "seq_finite_ind_lemma" (the_context ()) [seq.finite_def] "(!!n. P(seq_take n$s)) ==> seq_finite(s) -->P(s)" (fn prems => [ @@ -455,5 +455,3 @@ by (assume_tac 1); by (Asm_full_simp_tac 1); qed"seq_finite_ind"; - - diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/Seq.thy --- a/src/HOLCF/IOA/meta_theory/Seq.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Seq.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,26 +1,26 @@ (* Title: HOLCF/IOA/meta_theory/Seq.thy ID: $Id$ Author: Olaf Müller +*) -Partial, Finite and Infinite Sequences (lazy lists), modeled as domain. -*) - +header {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *} -Seq = HOLCF + Inductive + - -domain 'a seq = nil | "##" (HD::'a) (lazy TL::'a seq) (infixr 65) +theory Seq +imports HOLCF +begin +domain 'a seq = nil | "##" (HD :: 'a) (lazy TL :: "'a seq") (infixr 65) -consts - sfilter :: "('a -> tr) -> 'a seq -> 'a seq" +consts + sfilter :: "('a -> tr) -> 'a seq -> 'a seq" smap :: "('a -> 'b) -> 'a seq -> 'b seq" sforall :: "('a -> tr) => 'a seq => bool" sforall2 :: "('a -> tr) -> 'a seq -> tr" slast :: "'a seq -> 'a" sconc :: "'a seq -> 'a seq -> 'a seq" - sdropwhile, - stakewhile ::"('a -> tr) -> 'a seq -> 'a seq" - szip ::"'a seq -> 'b seq -> ('a*'b) seq" + sdropwhile ::"('a -> tr) -> 'a seq -> 'a seq" + stakewhile ::"('a -> tr) -> 'a seq -> 'a seq" + szip ::"'a seq -> 'b seq -> ('a*'b) seq" sflat :: "('a seq) seq -> 'a seq" sfinite :: "'a seq set" @@ -31,90 +31,105 @@ sproj :: "nat => 'a seq => 'a seq" syntax - "@@" :: "'a seq => 'a seq => 'a seq" (infixr 65) + "@@" :: "'a seq => 'a seq => 'a seq" (infixr 65) "Finite" :: "'a seq => bool" translations - "xs @@ ys" == "sconc$xs$ys" + "xs @@ ys" == "sconc $ xs $ ys" "Finite x" == "x:sfinite" "~(Finite x)" =="x~:sfinite" -defs - - +defs (* f not possible at lhs, as "pattern matching" only for % x arguments, f cannot be written at rhs in front, as fix_eq3 does not apply later *) -smap_def - "smap == (fix$(LAM h f tr. case tr of +smap_def: + "smap == (fix$(LAM h f tr. case tr of nil => nil | x##xs => f$x ## h$f$xs))" -sfilter_def - "sfilter == (fix$(LAM h P t. case t of - nil => nil - | x##xs => If P$x +sfilter_def: + "sfilter == (fix$(LAM h P t. case t of + nil => nil + | x##xs => If P$x then x##(h$P$xs) else h$P$xs - fi))" -sforall_def - "sforall P t == (sforall2$P$t ~=FF)" + fi))" +sforall_def: + "sforall P t == (sforall2$P$t ~=FF)" -sforall2_def - "sforall2 == (fix$(LAM h P t. case t of - nil => TT - | x##xs => P$x andalso h$P$xs))" - -sconc_def - "sconc == (fix$(LAM h t1 t2. case t1 of +sforall2_def: + "sforall2 == (fix$(LAM h P t. case t of + nil => TT + | x##xs => P$x andalso h$P$xs))" + +sconc_def: + "sconc == (fix$(LAM h t1 t2. case t1 of nil => t2 | x##xs => x##(h$xs$t2)))" -slast_def - "slast == (fix$(LAM h t. case t of - nil => UU - | x##xs => (If is_nil$xs +slast_def: + "slast == (fix$(LAM h t. case t of + nil => UU + | x##xs => (If is_nil$xs then x else h$xs fi)))" -stakewhile_def - "stakewhile == (fix$(LAM h P t. case t of - nil => nil - | x##xs => If P$x +stakewhile_def: + "stakewhile == (fix$(LAM h P t. case t of + nil => nil + | x##xs => If P$x then x##(h$P$xs) else nil - fi))" -sdropwhile_def - "sdropwhile == (fix$(LAM h P t. case t of - nil => nil - | x##xs => If P$x + fi))" +sdropwhile_def: + "sdropwhile == (fix$(LAM h P t. case t of + nil => nil + | x##xs => If P$x then h$P$xs else t - fi))" -sflat_def - "sflat == (fix$(LAM h t. case t of - nil => nil - | x##xs => x @@ (h$xs)))" + fi))" +sflat_def: + "sflat == (fix$(LAM h t. case t of + nil => nil + | x##xs => x @@ (h$xs)))" -szip_def - "szip == (fix$(LAM h t1 t2. case t1 of +szip_def: + "szip == (fix$(LAM h t1 t2. case t1 of nil => nil - | x##xs => (case t2 of - nil => UU + | x##xs => (case t2 of + nil => UU | y##ys => ##(h$xs$ys))))" -Partial_def +Partial_def: "Partial x == (seq_finite x) & ~(Finite x)" -Infinite_def +Infinite_def: "Infinite x == ~(seq_finite x)" -inductive "sfinite" - intrs - sfinite_0 "nil:sfinite" - sfinite_n "[|tr:sfinite;a~=UU|] ==> (a##tr) : sfinite" +inductive "sfinite" + intros + sfinite_0: "nil:sfinite" + sfinite_n: "[|tr:sfinite;a~=UU|] ==> (a##tr) : sfinite" +ML {* use_legacy_bindings (the_context ()) *} +ML {* +structure seq = +struct + open seq + val injects = [injects] + val inverts = [inverts] + val finites = [finites] + val take_lemmas = [take_lemmas] +end +structure sfinite = +struct + open sfinite + val elim = elims + val elims = [elims] +end +*} end diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/Sequence.ML --- a/src/HOLCF/IOA/meta_theory/Sequence.ML Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Fri Sep 02 17:23:59 2005 +0200 @@ -1,11 +1,8 @@ (* Title: HOLCF/IOA/meta_theory/Sequence.ML ID: $Id$ Author: Olaf Mller - -Theorems about Sequences over flat domains with lifted elements. *) - Addsimps [andalso_and,andalso_or]; (* ----------------------------------------------------------------------------------- *) @@ -40,7 +37,7 @@ by (simp_tac (simpset() addsimps [Filter_def]) 1); qed"Filter_nil"; -Goal "Filter P$(x>>xs)= (if P x then x>>(Filter P$xs) else Filter P$xs)"; +Goal "Filter P$(x>>xs)= (if P x then x>>(Filter P$xs) else Filter P$xs)"; by (simp_tac (simpset() addsimps [Filter_def, Consq_def,flift2_def,If_and_if]) 1); qed"Filter_cons"; @@ -66,7 +63,7 @@ (* ---------------------------------------------------------------- *) -Goal "(x>>xs) @@ y = x>>(xs @@y)"; +Goal "(x>>xs) @@ y = x>>(xs @@y)"; by (simp_tac (simpset() addsimps [Consq_def]) 1); qed"Conc_cons"; @@ -82,7 +79,7 @@ by (simp_tac (simpset() addsimps [Takewhile_def]) 1); qed"Takewhile_nil"; -Goal "Takewhile P$(x>>xs)= (if P x then x>>(Takewhile P$xs) else nil)"; +Goal "Takewhile P$(x>>xs)= (if P x then x>>(Takewhile P$xs) else nil)"; by (simp_tac (simpset() addsimps [Takewhile_def, Consq_def,flift2_def,If_and_if]) 1); qed"Takewhile_cons"; @@ -98,7 +95,7 @@ by (simp_tac (simpset() addsimps [Dropwhile_def]) 1); qed"Dropwhile_nil"; -Goal "Dropwhile P$(x>>xs)= (if P x then Dropwhile P$xs else x>>xs)"; +Goal "Dropwhile P$(x>>xs)= (if P x then Dropwhile P$xs else x>>xs)"; by (simp_tac (simpset() addsimps [Dropwhile_def, Consq_def,flift2_def,If_and_if]) 1); qed"Dropwhile_cons"; @@ -115,7 +112,7 @@ by (simp_tac (simpset() addsimps [Last_def]) 1); qed"Last_nil"; -Goal "Last$(x>>xs)= (if xs=nil then Def x else Last$xs)"; +Goal "Last$(x>>xs)= (if xs=nil then Def x else Last$xs)"; by (simp_tac (simpset() addsimps [Last_def, Consq_def]) 1); by (res_inst_tac [("x","xs")] seq.casedist 1); by (Asm_simp_tac 1); @@ -135,7 +132,7 @@ by (simp_tac (simpset() addsimps [Flat_def]) 1); qed"Flat_nil"; -Goal "Flat$(x##xs)= x @@ (Flat$xs)"; +Goal "Flat$(x##xs)= x @@ (Flat$xs)"; by (simp_tac (simpset() addsimps [Flat_def, Consq_def]) 1); qed"Flat_cons"; @@ -146,7 +143,7 @@ Goal "Zip = (LAM t1 t2. case t1 of \ \ nil => nil \ -\ | x##xs => (case t2 of \ +\ | x##xs => (case t2 of \ \ nil => UU \ \ | y##ys => (case x of \ \ UU => UU \ @@ -177,12 +174,12 @@ by (Simp_tac 1); qed"Zip_nil"; -Goal "Zip$(x>>xs)$nil= UU"; +Goal "Zip$(x>>xs)$nil= UU"; by (stac Zip_unfold 1); by (simp_tac (simpset() addsimps [Consq_def]) 1); qed"Zip_cons_nil"; -Goal "Zip$(x>>xs)$(y>>ys)= (x,y) >> Zip$xs$ys"; +Goal "Zip$(x>>xs)$(y>>ys)= (x,y) >> Zip$xs$ys"; by (rtac trans 1); by (stac Zip_unfold 1); by (Simp_tac 1); @@ -194,7 +191,7 @@ smap_UU,smap_nil,smap_cons, sforall2_UU,sforall2_nil,sforall2_cons, slast_UU,slast_nil,slast_cons, - stakewhile_UU, stakewhile_nil, stakewhile_cons, + stakewhile_UU, stakewhile_nil, stakewhile_cons, sdropwhile_UU, sdropwhile_nil, sdropwhile_cons, sflat_UU,sflat_nil,sflat_cons, szip_UU1,szip_UU2,szip_nil,szip_cons_nil,szip_cons]; @@ -205,7 +202,7 @@ Forall_UU,Forall_nil,Forall_cons, Last_UU,Last_nil,Last_cons, Conc_cons, - Takewhile_UU, Takewhile_nil, Takewhile_cons, + Takewhile_UU, Takewhile_nil, Takewhile_cons, Dropwhile_UU, Dropwhile_nil, Dropwhile_cons, Zip_UU1,Zip_UU2,Zip_nil,Zip_cons_nil,Zip_cons]; @@ -238,7 +235,7 @@ qed"Seq_cases"; fun Seq_case_tac s i = res_inst_tac [("x",s)] Seq_cases i - THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2); + THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2); (* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *) fun Seq_case_simp_tac s i = Seq_case_tac s i THEN Asm_simp_tac (i+2) @@ -337,7 +334,7 @@ by (assume_tac 1); by (def_tac 1); by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1); -qed"Seq_Finite_ind"; +qed"Seq_Finite_ind"; (* rws are definitions to be unfolded for admissibility check *) @@ -349,13 +346,13 @@ THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac i))); fun pair_tac s = res_inst_tac [("p",s)] PairE - THEN' hyp_subst_tac THEN' Asm_full_simp_tac; + THEN' hyp_subst_tac THEN' Asm_full_simp_tac; (* induction on a sequence of pairs with pairsplitting and simplification *) -fun pair_induct_tac s rws i = - res_inst_tac [("x",s)] Seq_induct i - THEN pair_tac "a" (i+3) - THEN (REPEAT_DETERM (CHANGED (Simp_tac (i+1)))) +fun pair_induct_tac s rws i = + res_inst_tac [("x",s)] Seq_induct i + THEN pair_tac "a" (i+3) + THEN (REPEAT_DETERM (CHANGED (Simp_tac (i+1)))) THEN simp_tac (simpset() addsimps rws) i; @@ -448,7 +445,7 @@ section "admissibility"; (* Finite x is proven to be adm: Finite_flat shows that there are only chains of length one. - Then the assumption that an _infinite_ chain exists (from admI2) is set to a contradiction + Then the assumption that an _infinite_ chain exists (from admI2) is set to a contradiction to Finite_flat *) Goal "!! (x:: 'a Seq). Finite x ==> !y. Finite (y:: 'a Seq) & x< x=y"; @@ -609,7 +606,7 @@ Goal "! s. Forall P s --> t< Forall P t"; by (Seq_induct_tac "t" [Forall_def,sforall_def] 1); -by (strip_tac 1); +by (strip_tac 1); by (Seq_case_simp_tac "sa" 1); by (Asm_full_simp_tac 1); by Auto_tac; @@ -791,16 +788,16 @@ \ --> y = ((Takewhile (%x. ~P x)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y))) \ \ & Finite (Takewhile (%x. ~ P x)$y) & P x"; -(* FIX: pay attention: is only admissible with chain-finite package to be added to +(* FIX: pay attention: is only admissible with chain-finite package to be added to adm test and Finite f x admissibility *) by (Seq_induct_tac "y" [] 1); by (rtac adm_all 1); -by (Asm_full_simp_tac 1); +by (Asm_full_simp_tac 1); by (case_tac "P a" 1); - by (Asm_full_simp_tac 1); + by (Asm_full_simp_tac 1); by (Blast_tac 1); (* ~ P a *) -by (Asm_full_simp_tac 1); +by (Asm_full_simp_tac 1); qed"divide_Seq_lemma"; Goal "(x>>xs) << Filter P$y \ @@ -808,12 +805,12 @@ \ & Finite (Takewhile (%a. ~ P a)$y) & P x"; by (rtac (divide_Seq_lemma RS mp) 1); by (dres_inst_tac [("f","HD"),("x","x>>xs")] monofun_cfun_arg 1); -by (Asm_full_simp_tac 1); +by (Asm_full_simp_tac 1); qed"divide_Seq"; - + Goal "~Forall P y --> (? x. HD$(Filter (%a. ~P a)$y) = Def x)"; -(* Pay attention: is only admissible with chain-finite package to be added to +(* Pay attention: is only admissible with chain-finite package to be added to adm test *) by (Seq_induct_tac "y" [Forall_def,sforall_def] 1); qed"nForall_HDFilter"; @@ -851,7 +848,7 @@ by Auto_tac; qed"seq_take_lemma"; -Goal +Goal " ! n. ((! k. k < n --> seq_take k$y1 = seq_take k$y2) \ \ --> seq_take n$(x @@ (t>>y1)) = seq_take n$(x @@ (t>>y2)))"; by (Seq_induct_tac "x" [] 1); @@ -870,10 +867,10 @@ qed"take_reduction"; (* ------------------------------------------------------------------ - take-lemma and take_reduction for << instead of = + take-lemma and take_reduction for << instead of = ------------------------------------------------------------------ *) -Goal +Goal " ! n. ((! k. k < n --> seq_take k$y1 << seq_take k$y2) \ \ --> seq_take n$(x @@ (t>>y1)) << seq_take n$(x @@ (t>>y2)))"; by (Seq_induct_tac "x" [] 1); @@ -891,7 +888,7 @@ qed"take_reduction_less"; -val prems = goalw thy [seq.take_def] +val prems = goalw (the_context ()) [seq.take_def] "(!! n. seq_take n$s1 << seq_take n$s2) ==> s1< (f s) = (g s) ; \ \ !! s1 s2 y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);\ \ Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \ @@ -970,7 +967,7 @@ qed"take_lemma_induct"; -Goal +Goal "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \ \ !! s1 s2 y n. [| ! t m. m < n --> A t --> seq_take m$(f t) = seq_take m$(g t);\ \ Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \ @@ -1022,7 +1019,7 @@ end; -Goal +Goal "!! Q. [|!! s h1 h2. [| Forall Q s; A s h1 h2|] ==> (f s h1 h2) = (g s h1 h2) ; \ \ !! s1 s2 y n. [| ! t h1 h2 m. m < n --> (A t h1 h2) --> seq_take m$(f t h1 h2) = seq_take m$(g t h1 h2);\ \ Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) h1 h2|] \ @@ -1046,7 +1043,7 @@ -Goal +Goal "!! Q. [|!! s. Forall Q s ==> P ((f s) = (g s)) ; \ \ !! s1 s2 y n. [| ! t m. m < n --> P (seq_take m$(f t) = seq_take m$(g t));\ \ Forall Q s1; Finite s1; ~ Q y|] \ @@ -1075,7 +1072,7 @@ *) -Goal +Goal "!! Q. [| A UU ==> (f UU) = (g UU) ; \ \ A nil ==> (f nil) = (g nil) ; \ \ !! s y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);\ @@ -1107,8 +1104,8 @@ Delsimps [FilterPQ]; -(* In general: How to do this case without the same adm problems - as for the entire proof ? *) +(* In general: How to do this case without the same adm problems + as for the entire proof ? *) Goal "Forall (%x.~(P x & Q x)) s \ \ --> Filter P$(Filter Q$s) =\ \ Filter (%x. P x & Q x)$s"; @@ -1130,7 +1127,7 @@ Goal "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s"; -by (res_inst_tac [("A1","%x. True") +by (res_inst_tac [("A1","%x. True") ,("Q1","%x.~(P x & Q x)"),("x1","s")] (take_lemma_induct RS mp) 1); (* better support for A = %x. True *) diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/Sequence.thy --- a/src/HOLCF/IOA/meta_theory/Sequence.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Fri Sep 02 17:23:59 2005 +0200 @@ -3,13 +3,15 @@ Author: Olaf Müller Sequences over flat domains with lifted elements. -*) - -Sequence = Seq + +*) -default type +theory Sequence +imports Seq +begin -types 'a Seq = ('a::type lift)seq +defaultsort type + +types 'a Seq = "'a::type lift seq" consts @@ -18,8 +20,8 @@ Map ::"('a => 'b) => 'a Seq -> 'b Seq" Forall ::"('a => bool) => 'a Seq => bool" Last ::"'a Seq -> 'a lift" - Dropwhile, - Takewhile ::"('a => bool) => 'a Seq -> 'a Seq" + Dropwhile ::"('a => bool) => 'a Seq -> 'a Seq" + Takewhile ::"('a => bool) => 'a Seq -> 'a Seq" Zip ::"'a Seq -> 'b Seq -> ('a * 'b) Seq" Flat ::"('a Seq) seq -> 'a Seq" @@ -29,63 +31,59 @@ "@Consq" ::"'a => 'a Seq => 'a Seq" ("(_/>>_)" [66,65] 65) (* list Enumeration *) - "_totlist" :: args => 'a Seq ("[(_)!]") - "_partlist" :: args => 'a Seq ("[(_)?]") + "_totlist" :: "args => 'a Seq" ("[(_)!]") + "_partlist" :: "args => 'a Seq" ("[(_)?]") syntax (xsymbols) + "@Consq" ::"'a => 'a Seq => 'a Seq" ("(_\_)" [66,65] 65) - "@Consq" ::"'a => 'a Seq => 'a Seq" ("(_\\_)" [66,65] 65) - translations - "a>>s" == "Consq a$s" "[x, xs!]" == "x>>[xs!]" "[x!]" == "x>>nil" "[x, xs?]" == "x>>[xs?]" - "[x?]" == "x>>UU" + "[x?]" == "x>>UU" defs +Consq_def: "Consq a == LAM s. Def a ## s" -Consq_def "Consq a == LAM s. Def a ## s" +Filter_def: "Filter P == sfilter$(flift2 P)" -Filter_def "Filter P == sfilter$(flift2 P)" +Map_def: "Map f == smap$(flift2 f)" -Map_def "Map f == smap$(flift2 f)" - -Forall_def "Forall P == sforall (flift2 P)" +Forall_def: "Forall P == sforall (flift2 P)" -Last_def "Last == slast" +Last_def: "Last == slast" -Dropwhile_def "Dropwhile P == sdropwhile$(flift2 P)" +Dropwhile_def: "Dropwhile P == sdropwhile$(flift2 P)" -Takewhile_def "Takewhile P == stakewhile$(flift2 P)" +Takewhile_def: "Takewhile P == stakewhile$(flift2 P)" -Flat_def "Flat == sflat" +Flat_def: "Flat == sflat" -Zip_def - "Zip == (fix$(LAM h t1 t2. case t1 of +Zip_def: + "Zip == (fix$(LAM h t1 t2. case t1 of nil => nil - | x##xs => (case t2 of - nil => UU - | y##ys => (case x of + | x##xs => (case t2 of + nil => UU + | y##ys => (case x of UU => UU - | Def a => (case y of + | Def a => (case y of UU => UU | Def b => Def (a,b)##(h$xs$ys))))))" -Filter2_def "Filter2 P == (fix$(LAM h t. case t of +Filter2_def: "Filter2 P == (fix$(LAM h t. case t of nil => nil - | x##xs => (case x of UU => UU | Def y => (if P y + | x##xs => (case x of UU => UU | Def y => (if P y then x##(h$xs) - else h$xs))))" + else h$xs))))" -rules - +axioms -- {* for test purposes should be deleted FIX !! *} (* FIXME *) + adm_all: "adm f" -(* for test purposes should be deleted FIX !! *) -adm_all "adm f" +ML {* use_legacy_bindings (the_context ()) *} end diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/SimCorrectness.ML --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Fri Sep 02 17:23:59 2005 +0200 @@ -1,12 +1,8 @@ (* Title: HOLCF/IOA/meta_theory/SimCorrectness.ML ID: $Id$ Author: Olaf Müller - -Correctness of Simulations in HOLCF/IOA. *) - - (* -------------------------------------------------------------------------------- *) section "corresp_ex_sim"; @@ -45,7 +41,7 @@ Goal "(corresp_ex_simC A R$((a,t)>>xs)) s = \ \ (let T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' \ \ in \ -\ (@cex. move A cex s a T') \ +\ (@cex. move A cex s a T') \ \ @@ ((corresp_ex_simC A R$xs) T'))"; by (rtac trans 1); by (stac corresp_ex_simC_unfold 1); @@ -75,13 +71,13 @@ (* Does not perform conditional rewriting on assumptions automatically as usual. Instantiate all variables per hand. Ask Tobias?? *) by (subgoal_tac "? t' ex. (t,t'):R & move A ex s' a t'" 1); -by (Asm_full_simp_tac 2); +by (Asm_full_simp_tac 2); by (etac conjE 2); by (eres_inst_tac [("x","s")] allE 2); by (eres_inst_tac [("x","s'")] allE 2); by (eres_inst_tac [("x","t")] allE 2); by (eres_inst_tac [("x","a")] allE 2); -by (Asm_full_simp_tac 2); +by (Asm_full_simp_tac 2); (* Go on as usual *) by (etac exE 1); by (dres_inst_tac [("x","t'"), @@ -152,30 +148,30 @@ (* ------------------------------------------------------ - Lemma 1 :Traces coincide + Lemma 1 :Traces coincide ------------------------------------------------------- *) Delsplits[split_if]; -Goal - "[|is_simulation R C A; ext C = ext A|] ==> \ +Goal + "[|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')"; by (pair_induct_tac "ex" [is_exec_frag_def] 1); -(* cons case *) -by (safe_tac set_cs); +(* cons case *) +by (safe_tac set_cs); ren "ex a t s s'" 1; by (asm_full_simp_tac (simpset() addsimps [mk_traceConc]) 1); by (forward_tac [reachable.reachable_n] 1); by (assume_tac 1); by (eres_inst_tac [("x","t")] allE 1); by (eres_inst_tac [("x", - "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")] + "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")] allE 1); by (Asm_full_simp_tac 1); -by (asm_full_simp_tac (simpset() addsimps +by (asm_full_simp_tac (simpset() addsimps [rewrite_rule [Let_def] move_subprop5_sim, - rewrite_rule [Let_def] move_subprop4_sim] + rewrite_rule [Let_def] move_subprop4_sim] addsplits [split_if]) 1); qed_spec_mp"traces_coincide_sim"; Addsplits[split_if]; @@ -186,10 +182,10 @@ (* ----------------------------------------------------------- *) -Goal +Goal "[| 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')"; +\ --> is_exec_frag A (s',(corresp_ex_simC A R$ex) s')"; by (Asm_full_simp_tac 1); by (pair_induct_tac "ex" [is_exec_frag_def] 1); @@ -197,7 +193,7 @@ by (safe_tac set_cs); ren "ex a t s s'" 1; by (res_inst_tac [("t", - "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")] + "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")] lemma_2_1 1); (* Finite *) @@ -214,12 +210,12 @@ (* reachable_n looping, therefore apply it manually *) by (eres_inst_tac [("x","t")] allE 1); by (eres_inst_tac [("x", - "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")] + "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")] allE 1); by (Asm_full_simp_tac 1); by (forward_tac [reachable.reachable_n] 1); by (assume_tac 1); -by (asm_full_simp_tac (simpset() addsimps +by (asm_full_simp_tac (simpset() addsimps [rewrite_rule [Let_def] move_subprop5_sim]) 1); (* laststate *) by (etac ((rewrite_rule [Let_def] move_subprop3_sim) RS sym) 1); @@ -234,11 +230,11 @@ (* -------------------------------------------------------------------------------- *) (* generate condition (s,S'):R & S':starts_of A, the first being intereting - for the induction cases concerning the two lemmas correpsim_is_execution and - traces_coincide_sim, the second for the start state case. + for the induction cases concerning the two lemmas correpsim_is_execution and + traces_coincide_sim, the second for the start state case. S':= @s'. (s,s'):R & s':starts_of A, where s:starts_of C *) -Goal +Goal "[| 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"; @@ -259,14 +255,14 @@ Goalw [traces_def] "[| ext C = ext A; is_simulation R C A |] \ -\ ==> traces C <= traces A"; +\ ==> traces C <= traces A"; by (simp_tac(simpset() addsimps [has_trace_def2])1); by (safe_tac set_cs); (* give execution of abstract automata *) by (res_inst_tac[("x","corresp_ex_sim A R ex")] bexI 1); - + (* Traces coincide, Lemma 1 *) by (pair_tac "ex" 1); ren "s ex" 1; @@ -275,13 +271,13 @@ by (REPEAT (atac 1)); by (asm_full_simp_tac (simpset() addsimps [executions_def, reachable.reachable_0,sim_starts1]) 1); - + (* corresp_ex_sim is execution, Lemma 2 *) by (pair_tac "ex" 1); by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1); ren "s ex" 1; - (* start state *) + (* start state *) by (rtac conjI 1); by (asm_full_simp_tac (simpset() addsimps [sim_starts2, corresp_ex_sim_def]) 1); @@ -291,8 +287,4 @@ by (res_inst_tac [("s","s")] correspsim_is_execution 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0,sim_starts1]) 1); -qed"trace_inclusion_for_simulations"; - - - - +qed"trace_inclusion_for_simulations"; diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/SimCorrectness.thy --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,16 +1,17 @@ (* Title: HOLCF/IOA/meta_theory/SimCorrectness.thy ID: $Id$ Author: Olaf Müller - -Correctness of Simulations in HOLCF/IOA. *) +header {* Correctness of Simulations in HOLCF/IOA *} -SimCorrectness = Simulations + - +theory SimCorrectness +imports Simulations +begin + consts - corresp_ex_sim ::"('a,'s2)ioa => (('s1 *'s2)set) => + corresp_ex_sim ::"('a,'s2)ioa => (('s1 *'s2)set) => ('a,'s1)execution => ('a,'s2)execution" (* Note: s2 instead of s1 in last argument type !! *) corresp_ex_simC ::"('a,'s2)ioa => (('s1 * 's2)set) => ('a,'s1)pairs @@ -18,21 +19,23 @@ defs - -corresp_ex_sim_def + +corresp_ex_sim_def: "corresp_ex_sim A R ex == let S'= (@s'.(fst ex,s'):R & s': starts_of A) - in + in (S',(corresp_ex_simC A R$(snd ex)) S')" -corresp_ex_simC_def - "corresp_ex_simC A R == (fix$(LAM h ex. (%s. case ex of +corresp_ex_simC_def: + "corresp_ex_simC A R == (fix$(LAM h ex. (%s. case ex of nil => nil | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr); - T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' + T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' in (@cex. move A cex s a T') @@ ((h$xs) T')) $x) )))" - -end \ No newline at end of file + +ML {* use_legacy_bindings (the_context ()) *} + +end diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/Simulations.ML --- a/src/HOLCF/IOA/meta_theory/Simulations.ML Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Simulations.ML Fri Sep 02 17:23:59 2005 +0200 @@ -1,12 +1,8 @@ (* Title: HOLCF/IOA/meta_theory/Simulations.ML ID: $Id$ Author: Olaf Müller - -Simulations in HOLCF/IOA. *) - - Goal "(A~={}) = (? x. x:A)"; by (safe_tac set_cs); by Auto_tac; @@ -29,7 +25,3 @@ "!! f. is_ref_map f C A ==> is_simulation {p. (snd p) = f (fst p)} C A"; by (Asm_full_simp_tac 1); qed"ref_map_is_simulation"; - - - - diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/Simulations.thy --- a/src/HOLCF/IOA/meta_theory/Simulations.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Simulations.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,13 +1,15 @@ (* Title: HOLCF/IOA/meta_theory/Simulations.thy ID: $Id$ Author: Olaf Müller - -Simulations in HOLCF/IOA. *) -Simulations = RefCorrectness + +header {* Simulations in HOLCF/IOA *} -default type +theory Simulations +imports RefCorrectness +begin + +defaultsort type consts @@ -20,44 +22,46 @@ defs -is_simulation_def - "is_simulation R C A == - (!s:starts_of C. R``{s} Int starts_of A ~= {}) & - (!s s' t a. reachable C s & +is_simulation_def: + "is_simulation R C A == + (!s:starts_of C. R``{s} Int starts_of A ~= {}) & + (!s s' t a. reachable C s & s -a--C-> t & - (s,s') : R + (s,s') : R --> (? t' ex. (t,t'):R & move A ex s' a t'))" -is_backward_simulation_def - "is_backward_simulation R C A == - (!s:starts_of C. R``{s} <= starts_of A) & - (!s t t' a. reachable C s & +is_backward_simulation_def: + "is_backward_simulation R C A == + (!s:starts_of C. R``{s} <= starts_of A) & + (!s t t' a. reachable C s & s -a--C-> t & - (t,t') : R + (t,t') : R --> (? ex s'. (s,s'):R & move A ex s' a t'))" -is_forw_back_simulation_def - "is_forw_back_simulation R C A == - (!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) & - (!s S' t a. reachable C s & +is_forw_back_simulation_def: + "is_forw_back_simulation R C A == + (!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) & + (!s S' t a. reachable C s & s -a--C-> t & - (s,S') : R + (s,S') : R --> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t')))" -is_back_forw_simulation_def - "is_back_forw_simulation R C A == - (!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) & - (!s t T' a. reachable C s & +is_back_forw_simulation_def: + "is_back_forw_simulation R C A == + (!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) & + (!s t T' a. reachable C s & s -a--C-> t & - (t,T') : R + (t,T') : R --> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t')))" -is_history_relation_def - "is_history_relation R C A == is_simulation R C A & +is_history_relation_def: + "is_history_relation R C A == is_simulation R C A & is_ref_map (%x.(@y. (x,y):(R^-1))) A C" -is_prophecy_relation_def - "is_prophecy_relation R C A == is_backward_simulation R C A & +is_prophecy_relation_def: + "is_prophecy_relation R C A == is_backward_simulation R C A & is_ref_map (%x.(@y. (x,y):(R^-1))) A C" - + +ML {* use_legacy_bindings (the_context ()) *} + end diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/TL.ML --- a/src/HOLCF/IOA/meta_theory/TL.ML Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/TL.ML Fri Sep 02 17:23:59 2005 +0200 @@ -1,8 +1,6 @@ (* Title: HOLCF/IOA/meta_theory/TL.ML ID: $Id$ Author: Olaf Müller - -Temporal Logic. *) diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/TL.thy --- a/src/HOLCF/IOA/meta_theory/TL.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/TL.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,22 +1,21 @@ (* Title: HOLCF/IOA/meta_theory/TLS.thy ID: $Id$ Author: Olaf Müller +*) -A General Temporal Logic. -*) - -TL = Pred + Sequence + +header {* A General Temporal Logic *} -default type +theory TL +imports Pred Sequence +begin + +defaultsort type types - -'a temporal = 'a Seq predicate - - -consts + 'a temporal = "'a Seq predicate" +consts suffix :: "'a Seq => 'a Seq => bool" tsuffix :: "'a Seq => 'a Seq => bool" @@ -28,45 +27,46 @@ Box ::"'a temporal => 'a temporal" ("[] (_)" [80] 80) Diamond ::"'a temporal => 'a temporal" ("<> (_)" [80] 80) -Next ::"'a temporal => 'a temporal" +Next ::"'a temporal => 'a temporal" Leadsto ::"'a temporal => 'a temporal => 'a temporal" (infixr "~>" 22) syntax (xsymbols) - "Box" ::"'a temporal => 'a temporal" ("\\ (_)" [80] 80) - "Diamond" ::"'a temporal => 'a temporal" ("\\ (_)" [80] 80) - "Leadsto" ::"'a temporal => 'a temporal => 'a temporal" (infixr "\\" 22) - + "Box" ::"'a temporal => 'a temporal" ("\ (_)" [80] 80) + "Diamond" ::"'a temporal => 'a temporal" ("\ (_)" [80] 80) + "Leadsto" ::"'a temporal => 'a temporal => 'a temporal" (infixr "\" 22) + defs - -unlift_def - "unlift x == (case x of +unlift_def: + "unlift x == (case x of UU => arbitrary | Def y => y)" (* this means that for nil and UU the effect is unpredictable *) -Init_def - "Init P s == (P (unlift (HD$s)))" +Init_def: + "Init P s == (P (unlift (HD$s)))" -suffix_def - "suffix s2 s == ? s1. (Finite s1 & s = s1 @@ s2)" +suffix_def: + "suffix s2 s == ? s1. (Finite s1 & s = s1 @@ s2)" -tsuffix_def +tsuffix_def: "tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s" -Box_def +Box_def: "([] P) s == ! s2. tsuffix s2 s --> P s2" -Next_def +Next_def: "(Next P) s == if (TL$s=UU | TL$s=nil) then (P s) else P (TL$s)" -Diamond_def +Diamond_def: "<> P == .~ ([] (.~ P))" -Leadsto_def - "P ~> Q == ([] (P .--> (<> Q)))" +Leadsto_def: + "P ~> Q == ([] (P .--> (<> Q)))" -validT_def +validT_def: "validT P == ! s. s~=UU & s~=nil --> (s |= P)" -end \ No newline at end of file +ML {* use_legacy_bindings (the_context ()) *} + +end diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/TLS.ML --- a/src/HOLCF/IOA/meta_theory/TLS.ML Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/TLS.ML Fri Sep 02 17:23:59 2005 +0200 @@ -1,8 +1,6 @@ (* Title: HOLCF/IOA/meta_theory/TLS.ML ID: $Id$ Author: Olaf Müller - -Temporal Logic of Steps -- tailored for I/O automata. *) (* global changes to simpset() and claset(), repeated from Traces.ML *) diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/TLS.thy --- a/src/HOLCF/IOA/meta_theory/TLS.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,27 +1,26 @@ (* Title: HOLCF/IOA/meta_theory/TLS.thy ID: $Id$ Author: Olaf Müller +*) -Temporal Logic of Steps -- tailored for I/O automata. -*) +header {* Temporal Logic of Steps -- tailored for I/O automata *} - -TLS = IOA + TL + +theory TLS +imports IOA TL +begin -default type +defaultsort type types + ('a, 's) ioa_temp = "('a option,'s)transition temporal" + ('a, 's) step_pred = "('a option,'s)transition predicate" + 's state_pred = "'s predicate" - ('a,'s)ioa_temp = "('a option,'s)transition temporal" - ('a,'s)step_pred = "('a option,'s)transition predicate" - 's state_pred = "'s predicate" - consts - option_lift :: "('a => 'b) => 'b => ('a option => 'b)" plift :: "('a => bool) => ('a option => bool)" - + temp_sat :: "('a,'s)execution => ('a,'s)ioa_temp => bool" (infixr "|==" 22) xt1 :: "'s predicate => ('a,'s)step_pred" xt2 :: "'a option predicate => ('a,'s)step_pred" @@ -32,63 +31,61 @@ mkfin :: "'a Seq => 'a Seq" ex2seq :: "('a,'s)execution => ('a option,'s)transition Seq" -ex2seqC :: "('a,'s)pairs -> ('s => ('a option,'s)transition Seq)" +ex2seqC :: "('a,'s)pairs -> ('s => ('a option,'s)transition Seq)" defs -mkfin_def +mkfin_def: "mkfin s == if Partial s then @t. Finite t & s = t @@ UU else s" -option_lift_def +option_lift_def: "option_lift f s y == case y of None => s | Some x => (f x)" -(* plift is used to determine that None action is always false in +(* plift is used to determine that None action is always false in transition predicates *) -plift_def +plift_def: "plift P == option_lift P False" -temp_sat_def +temp_sat_def: "ex |== P == ((ex2seq ex) |= P)" -xt1_def +xt1_def: "xt1 P tr == P (fst tr)" -xt2_def +xt2_def: "xt2 P tr == P (fst (snd tr))" -ex2seq_def +ex2seq_def: "ex2seq ex == ((ex2seqC $(mkfin (snd ex))) (fst ex))" -ex2seqC_def - "ex2seqC == (fix$(LAM h ex. (%s. case ex of +ex2seqC_def: + "ex2seqC == (fix$(LAM h ex. (%s. case ex of nil => (s,None,s)>>nil | x##xs => (flift1 (%pr. - (s,Some (fst pr), snd pr)>> (h$xs) (snd pr)) + (s,Some (fst pr), snd pr)>> (h$xs) (snd pr)) $x) )))" -validTE_def +validTE_def: "validTE P == ! ex. (ex |== P)" -validIOA_def +validIOA_def: "validIOA A P == ! ex : executions A . (ex |== P)" +axioms -rules - -mkfin_UU +mkfin_UU: "mkfin UU = nil" -mkfin_nil +mkfin_nil: "mkfin nil =nil" -mkfin_cons +mkfin_cons: "(mkfin (a>>s)) = (a>>(mkfin s))" - +ML {* use_legacy_bindings (the_context ()) *} end - diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/Traces.thy --- a/src/HOLCF/IOA/meta_theory/Traces.thy Fri Sep 02 15:54:47 2005 +0200 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy Fri Sep 02 17:23:59 2005 +0200 @@ -1,16 +1,17 @@ (* Title: HOLCF/IOA/meta_theory/Traces.thy ID: $Id$ Author: Olaf Müller +*) -Executions and Traces of I/O automata in HOLCF. -*) +header {* Executions and Traces of I/O automata in HOLCF *} - -Traces = Sequence + Automata + +theory Traces +imports Sequence Automata +begin -default type - -types +defaultsort type + +types ('a,'s)pairs = "('a * 's) Seq" ('a,'s)execution = "'s * ('a,'s)pairs" 'a trace = "'a Seq" @@ -18,21 +19,21 @@ ('a,'s)execution_module = "('a,'s)execution set * 'a signature" 'a schedule_module = "'a trace set * 'a signature" 'a trace_module = "'a trace set * 'a signature" - + consts (* Executions *) - is_exec_fragC ::"('a,'s)ioa => ('a,'s)pairs -> 's => tr" - is_exec_frag, + is_exec_fragC ::"('a,'s)ioa => ('a,'s)pairs -> 's => tr" + is_exec_frag ::"[('a,'s)ioa, ('a,'s)execution] => bool" has_execution ::"[('a,'s)ioa, ('a,'s)execution] => bool" executions :: "('a,'s)ioa => ('a,'s)execution set" (* Schedules and traces *) filter_act ::"('a,'s)pairs -> 'a trace" - has_schedule, + has_schedule :: "[('a,'s)ioa, 'a trace] => bool" has_trace :: "[('a,'s)ioa, 'a trace] => bool" - schedules, + schedules :: "('a,'s)ioa => 'a trace set" traces :: "('a,'s)ioa => 'a trace set" mk_trace :: "('a,'s)ioa => ('a,'s)pairs -> 'a trace" @@ -52,12 +53,12 @@ fair_ex ::"('a,'s)ioa => ('a,'s)execution => bool" (* fair behavior sets *) - + fairexecutions ::"('a,'s)ioa => ('a,'s)execution set" fairtraces ::"('a,'s)ioa => 'a trace set" (* Notions of implementation *) - "=<|" :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr 12) + "=<|" :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr 12) fair_implements :: "('a,'s1)ioa => ('a,'s2)ioa => bool" (* Execution, schedule and trace modules *) @@ -72,124 +73,125 @@ (* ------------------- Executions ------------------------------ *) -is_exec_frag_def +is_exec_frag_def: "is_exec_frag A ex == ((is_exec_fragC A$(snd ex)) (fst ex) ~= FF)" -is_exec_fragC_def - "is_exec_fragC A ==(fix$(LAM h ex. (%s. case ex of +is_exec_fragC_def: + "is_exec_fragC A ==(fix$(LAM h ex. (%s. case ex of nil => TT - | x##xs => (flift1 - (%p. Def ((s,p):trans_of A) andalso (h$xs) (snd p)) + | x##xs => (flift1 + (%p. Def ((s,p):trans_of A) andalso (h$xs) (snd p)) $x) - )))" + )))" -executions_def - "executions ioa == {e. ((fst e) : starts_of(ioa)) & +executions_def: + "executions ioa == {e. ((fst e) : starts_of(ioa)) & is_exec_frag ioa e}" (* ------------------- Schedules ------------------------------ *) -filter_act_def +filter_act_def: "filter_act == Map fst" -has_schedule_def - "has_schedule ioa sch == +has_schedule_def: + "has_schedule ioa sch == (? ex:executions ioa. sch = filter_act$(snd ex))" -schedules_def +schedules_def: "schedules ioa == {sch. has_schedule ioa sch}" (* ------------------- Traces ------------------------------ *) -has_trace_def - "has_trace ioa tr == +has_trace_def: + "has_trace ioa tr == (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))$sch)" - -traces_def + +traces_def: "traces ioa == {tr. has_trace ioa tr}" -mk_trace_def - "mk_trace ioa == LAM tr. +mk_trace_def: + "mk_trace ioa == LAM tr. Filter (%a. a:ext(ioa))$(filter_act$tr)" (* ------------------- Fair Traces ------------------------------ *) -laststate_def +laststate_def: "laststate ex == case Last$(snd ex) of UU => fst ex | Def at => snd at" -inf_often_def +inf_often_def: "inf_often P s == Infinite (Filter P$s)" (* filtering P yields a finite or partial sequence *) -fin_often_def +fin_often_def: "fin_often P s == ~inf_often P s" -(* 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: Is this the right model? +(* 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: 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) +wfair_ex_def: + "wfair_ex A ex == ! W : wfair_of A. + if Finite (snd ex) then ~Enabled A W (laststate ex) else is_wfair A W ex" -is_wfair_def +is_wfair_def: "is_wfair A W ex == (inf_often (%x. fst x:W) (snd ex) | inf_often (%x.~Enabled A W (snd x)) (snd ex))" -sfair_ex_def +sfair_ex_def: "sfair_ex A ex == ! W : sfair_of A. - if Finite (snd ex) + if Finite (snd ex) then ~Enabled A W (laststate ex) else is_sfair A W ex" -is_sfair_def +is_sfair_def: "is_sfair A W ex == (inf_often (%x. fst x:W) (snd ex) | fin_often (%x. Enabled A W (snd x)) (snd ex))" -fair_ex_def +fair_ex_def: "fair_ex A ex == wfair_ex A ex & sfair_ex A ex" -fairexecutions_def +fairexecutions_def: "fairexecutions A == {ex. ex:executions A & fair_ex A ex}" -fairtraces_def +fairtraces_def: "fairtraces A == {mk_trace A$(snd ex) | ex. ex:fairexecutions A}" (* ------------------- Implementation ------------------------------ *) -ioa_implements_def - "ioa1 =<| ioa2 == - (((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) & +ioa_implements_def: + "ioa1 =<| ioa2 == + (((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) & (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) & traces(ioa1) <= traces(ioa2))" -fair_implements_def +fair_implements_def: "fair_implements C A == inp(C) = inp(A) & out(C)=out(A) & fairtraces(C) <= fairtraces(A)" (* ------------------- Modules ------------------------------ *) -Execs_def +Execs_def: "Execs A == (executions A, asig_of A)" -Scheds_def +Scheds_def: "Scheds A == (schedules A, asig_of A)" -Traces_def +Traces_def: "Traces A == (traces A,asig_of A)" +ML {* use_legacy_bindings (the_context ()) *} -end \ No newline at end of file +end