--- 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";
--- 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
--- 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";
-
--- 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
--- 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";
--- 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"
- ("_ \\<midarrow>_\\<midarrow>_\\<longrightarrow> _" [81,81,81,81] 100)
- "op ||" ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "\\<parallel>" 10)
+ "_trans_of" :: "'s => 'a => ('a,'s)ioa => 's => bool"
+ ("_ \<midarrow>_\<midarrow>_\<longrightarrow> _" [81,81,81,81] 100)
+ "op ||" ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "\<parallel>" 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
-
--- 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";
-
-
-
-
-
-
-
--- 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
--- 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<<f_act exA
- is used! --> 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<<f_act exA
+ is used! --> 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);
--- 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
--- 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);
(* <== *)
--- 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
--- 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";
-
-
-
-
--- 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
--- 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];
-
-
-
-
--- 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
--- 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
--- 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];
--- 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> .--> [] <> <xt2 (plift (%a. a : acts))>"
-SF_def
+SF_def:
"SF A acts == [] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
-
+
-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
--- 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" ("\\<not> _" [40] 40)
- "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\\<and>" 35)
- "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\\<or>" 30)
- "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\\<longrightarrow>" 25)
+ "NOT" ::"'a predicate => 'a predicate" ("\<not> _" [40] 40)
+ "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<and>" 35)
+ "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<or>" 30)
+ "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<longrightarrow>" 25)
syntax (xsymbols)
- "satisfies" ::"'a => 'a predicate => bool" ("_ \\<Turnstile> _" [100,9] 8)
+ "satisfies" ::"'a => 'a predicate => bool" ("_ \<Turnstile> _" [100,9] 8)
syntax (HTML output)
- "NOT" ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)
- "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\\<and>" 35)
- "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\\<or>" 30)
+ "NOT" ::"'a predicate => 'a predicate" ("\<not> _" [40] 40)
+ "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<and>" 35)
+ "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<or>" 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
--- 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";
-
-
-
-
-
--- 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
--- 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];
-
-
--- 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
--- 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 => <x,y>##(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";
-
-
--- 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 => <x,y>##(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
--- 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<<y --> x=y";
@@ -609,7 +606,7 @@
Goal "! s. Forall P s --> t<<s --> 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<<s2";
by (res_inst_tac [("t","s1")] (seq.reach RS subst) 1);
@@ -940,15 +937,15 @@
qed"take_lemma_principle2";
-(* Note: in the following proofs the ordering of proof steps is very
+(* Note: in the following proofs the ordering of proof steps is very
important, as otherwise either (Forall Q s1) would be in the IH as
- assumption (then rule useless) or it is not possible to strengthen
+ assumption (then rule useless) or it is not possible to strengthen
the IH by doing a forall closure of the sequence t (then rule also useless).
- This is also the reason why the induction rule (nat_less_induct or nat_induct) has to
- to be imbuilt into the rule, as induction has to be done early and the take lemma
+ This is also the reason why the induction rule (nat_less_induct or nat_induct) has to
+ to be imbuilt into the rule, as induction has to be done early and the take lemma
has to be used in the trivial direction afterwards for the (Forall Q x) case. *)
-Goal
+Goal
"!! Q. [|!! s. [| Forall Q s; A s |] ==> (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 *)
--- 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" ("(_\<leadsto>_)" [66,65] 65)
- "@Consq" ::"'a => 'a Seq => 'a Seq" ("(_\\<leadsto>_)" [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
--- 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";
--- 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
--- 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";
-
-
-
-
--- 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
--- 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.
*)
--- 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" ("\\<box> (_)" [80] 80)
- "Diamond" ::"'a temporal => 'a temporal" ("\\<diamond> (_)" [80] 80)
- "Leadsto" ::"'a temporal => 'a temporal => 'a temporal" (infixr "\\<leadsto>" 22)
-
+ "Box" ::"'a temporal => 'a temporal" ("\<box> (_)" [80] 80)
+ "Diamond" ::"'a temporal => 'a temporal" ("\<diamond> (_)" [80] 80)
+ "Leadsto" ::"'a temporal => 'a temporal => 'a temporal" (infixr "\<leadsto>" 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
--- 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 *)
--- 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
-
--- 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