--- a/src/HOL/Auth/All_Symmetric.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/Auth/All_Symmetric.thy Mon Jan 11 21:21:02 2016 +0100
@@ -4,7 +4,10 @@
text \<open>All keys are symmetric\<close>
-defs all_symmetric_def: "all_symmetric \<equiv> True"
+overloading all_symmetric \<equiv> all_symmetric
+begin
+ definition "all_symmetric \<equiv> True"
+end
lemma isSym_keys: "K \<in> symKeys"
by (simp add: symKeys_def all_symmetric_def invKey_symmetric)
--- a/src/HOL/Bali/Example.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/Bali/Example.thy Mon Jan 11 21:21:02 2016 +0100
@@ -141,12 +141,16 @@
lemma neq_Main_SXcpt [simp]: "Main\<noteq>SXcpt xn"
by (simp add: SXcpt_def)
+
subsubsection "classes and interfaces"
-defs
-
- Object_mdecls_def: "Object_mdecls \<equiv> []"
- SXcpt_mdecls_def: "SXcpt_mdecls \<equiv> []"
+overloading
+ Object_mdecls \<equiv> Object_mdecls
+ SXcpt_mdecls \<equiv> SXcpt_mdecls
+begin
+ definition "Object_mdecls \<equiv> []"
+ definition "SXcpt_mdecls \<equiv> []"
+end
axiomatization
foo :: mname
--- a/src/HOL/IMPP/EvenOdd.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/IMPP/EvenOdd.thy Mon Jan 11 21:21:02 2016 +0100
@@ -29,8 +29,10 @@
THEN Loc Res:==(%s. 1)
ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1)))"
-defs
- bodies_def: "bodies == [(Even,evn),(Odd,odd)]"
+overloading bodies \<equiv> bodies
+begin
+ definition "bodies == [(Even,evn),(Odd,odd)]"
+end
definition
Z_eq_Arg_plus :: "nat => nat assn" ("Z=Arg+_" [50]50) where
--- a/src/HOL/IMPP/Misc.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/IMPP/Misc.thy Mon Jan 11 21:21:02 2016 +0100
@@ -8,13 +8,29 @@
imports Hoare
begin
-defs
- newlocs_def: "newlocs == %x. undefined"
- setlocs_def: "setlocs s l' == case s of st g l => st g l'"
- getlocs_def: "getlocs s == case s of st g l => l"
- update_def: "update s vn v == case vn of
- Glb gn => (case s of st g l => st (g(gn:=v)) l)
- | Loc ln => (case s of st g l => st g (l(ln:=v)))"
+overloading
+ newlocs \<equiv> newlocs
+ setlocs \<equiv> setlocs
+ getlocs \<equiv> getlocs
+ update \<equiv> update
+begin
+
+definition newlocs :: locals
+ where "newlocs == %x. undefined"
+
+definition setlocs :: "state => locals => state"
+ where "setlocs s l' == case s of st g l => st g l'"
+
+definition getlocs :: "state => locals"
+ where "getlocs s == case s of st g l => l"
+
+definition update :: "state => vname => val => state"
+ where "update s vn v ==
+ case vn of
+ Glb gn => (case s of st g l => st (g(gn:=v)) l)
+ | Loc ln => (case s of st g l => st g (l(ln:=v)))"
+
+end
subsection "state access"
--- a/src/HOL/IOA/Asig.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/IOA/Asig.thy Mon Jan 11 21:21:02 2016 +0100
@@ -9,41 +9,31 @@
imports Main
begin
-type_synonym
- 'a signature = "('a set * 'a set * 'a set)"
+type_synonym 'a signature = "('a set * 'a set * 'a set)"
+
+definition "inputs" :: "'action signature => 'action set"
+ where asig_inputs_def: "inputs == fst"
-consts
- "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"
+definition "outputs" :: "'action signature => 'action set"
+ where asig_outputs_def: "outputs == (fst o snd)"
- is_asig ::"'action signature => bool"
- mk_ext_asig ::"'action signature => 'action signature"
-
-
-defs
+definition "internals" :: "'action signature => 'action set"
+ where 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)"
+definition "actions" :: "'action signature => 'action set"
+ where actions_def: "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
-actions_def:
- "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
-
-externals_def:
- "externals(asig) == (inputs(asig) Un outputs(asig))"
+definition externals :: "'action signature => 'action set"
+ where externals_def: "externals(asig) == (inputs(asig) Un outputs(asig))"
-is_asig_def:
- "is_asig(triple) ==
- ((inputs(triple) Int outputs(triple) = {}) &
- (outputs(triple) Int internals(triple) = {}) &
- (inputs(triple) Int internals(triple) = {}))"
+definition is_asig :: "'action signature => bool"
+ where "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(triple) == (inputs(triple), outputs(triple), {})"
+definition mk_ext_asig :: "'action signature => 'action signature"
+ where "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def
--- a/src/HOL/IOA/IOA.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/IOA/IOA.thy Mon Jan 11 21:21:02 2016 +0100
@@ -15,183 +15,148 @@
type_synonym ('a, 's) transition = "('s * 'a * 's)"
type_synonym ('a,'s) ioa = "'a signature * 's set * ('a, 's) transition set"
-consts
+(* IO automata *)
+
+definition state_trans :: "['action signature, ('action,'state)transition set] => bool"
+ where "state_trans asig R ==
+ (!triple. triple:R --> fst(snd(triple)):actions(asig)) &
+ (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
+
+definition asig_of :: "('action,'state)ioa => 'action signature"
+ where "asig_of == fst"
- (* IO automata *)
- state_trans::"['action signature, ('action,'state)transition set] => bool"
- asig_of ::"('action,'state)ioa => 'action signature"
- starts_of ::"('action,'state)ioa => 'state set"
- trans_of ::"('action,'state)ioa => ('action,'state)transition set"
- IOA ::"('action,'state)ioa => bool"
+definition starts_of :: "('action,'state)ioa => 'state set"
+ where "starts_of == (fst o snd)"
+
+definition trans_of :: "('action,'state)ioa => ('action,'state)transition set"
+ where "trans_of == (snd o snd)"
- (* Executions, schedules, and traces *)
+definition IOA :: "('action,'state)ioa => bool"
+ where "IOA(ioa) == (is_asig(asig_of(ioa)) &
+ (~ starts_of(ioa) = {}) &
+ state_trans (asig_of ioa) (trans_of ioa))"
+
+
+(* Executions, schedules, and traces *)
- is_execution_fragment ::"[('action,'state)ioa, ('action,'state)execution] => bool"
- has_execution ::"[('action,'state)ioa, ('action,'state)execution] => bool"
- executions :: "('action,'state)ioa => ('action,'state)execution set"
- mk_trace :: "[('action,'state)ioa, 'action oseq] => 'action oseq"
- reachable :: "[('action,'state)ioa, 'state] => bool"
- invariant :: "[('action,'state)ioa, 'state=>bool] => bool"
- has_trace :: "[('action,'state)ioa, 'action oseq] => bool"
- traces :: "('action,'state)ioa => 'action oseq set"
- NF :: "'a oseq => 'a oseq"
+(* An execution fragment is modelled with a pair of sequences:
+ the first is the action options, the second the state sequence.
+ Finite executions have None actions from some point on. *)
+definition is_execution_fragment :: "[('action,'state)ioa, ('action,'state)execution] => bool"
+ where "is_execution_fragment A ex ==
+ let act = fst(ex); state = snd(ex)
+ in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &
+ (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
+
+definition executions :: "('action,'state)ioa => ('action,'state)execution set"
+ where "executions(ioa) == {e. snd e 0:starts_of(ioa) & is_execution_fragment ioa e}"
- (* Composition of action signatures and automata *)
+
+definition reachable :: "[('action,'state)ioa, 'state] => bool"
+ where "reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)"
+
+definition invariant :: "[('action,'state)ioa, 'state=>bool] => bool"
+ where "invariant A P == (!s. reachable A s --> P(s))"
+
+
+(* Composition of action signatures and automata *)
+
+consts
compatible_asigs ::"('a => 'action signature) => bool"
asig_composition ::"('a => 'action signature) => 'action signature"
compatible_ioas ::"('a => ('action,'state)ioa) => bool"
ioa_composition ::"('a => ('action, 'state)ioa) =>('action,'a => 'state)ioa"
- (* binary composition of action signatures and automata *)
- compat_asigs ::"['action signature, 'action signature] => bool"
- asig_comp ::"['action signature, 'action signature] => 'action signature"
- compat_ioas ::"[('action,'s)ioa, ('action,'t)ioa] => bool"
- par ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "||" 10)
+
+(* binary composition of action signatures and automata *)
- (* Filtering and hiding *)
- filter_oseq :: "('a => bool) => 'a oseq => 'a oseq"
+definition compat_asigs ::"['action signature, 'action signature] => bool"
+ where "compat_asigs a1 a2 ==
+ (((outputs(a1) Int outputs(a2)) = {}) &
+ ((internals(a1) Int actions(a2)) = {}) &
+ ((internals(a2) Int actions(a1)) = {}))"
- restrict_asig :: "['a signature, 'a set] => 'a signature"
- restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
+definition compat_ioas ::"[('action,'s)ioa, ('action,'t)ioa] => bool"
+ where "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
- (* Notions of correctness *)
- ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool"
-
- (* Instantiation of abstract IOA by concrete actions *)
- rename:: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
+definition asig_comp :: "['action signature, 'action signature] => 'action signature"
+ where "asig_comp a1 a2 ==
+ (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),
+ (outputs(a1) Un outputs(a2)),
+ (internals(a1) Un internals(a2))))"
-defs
-
-state_trans_def:
- "state_trans asig R ==
- (!triple. triple:R --> fst(snd(triple)):actions(asig)) &
- (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
+definition par :: "[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "||" 10)
+ where "(ioa1 || ioa2) ==
+ (asig_comp (asig_of ioa1) (asig_of ioa2),
+ {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},
+ {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
+ in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) &
+ (if a:actions(asig_of(ioa1)) then
+ (fst(s),a,fst(t)):trans_of(ioa1)
+ else fst(t) = fst(s))
+ &
+ (if a:actions(asig_of(ioa2)) then
+ (snd(s),a,snd(t)):trans_of(ioa2)
+ else snd(t) = snd(s))})"
-asig_of_def: "asig_of == fst"
-starts_of_def: "starts_of == (fst o snd)"
-trans_of_def: "trans_of == (snd o snd)"
-
-ioa_def:
- "IOA(ioa) == (is_asig(asig_of(ioa)) &
- (~ starts_of(ioa) = {}) &
- state_trans (asig_of ioa) (trans_of ioa))"
-
-
-(* An execution fragment is modelled with a pair of sequences:
- * the first is the action options, the second the state sequence.
- * Finite executions have None actions from some point on.
- *******)
-is_execution_fragment_def:
- "is_execution_fragment A ex ==
- let act = fst(ex); state = snd(ex)
- in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &
- (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
-
-
-executions_def:
- "executions(ioa) == {e. snd e 0:starts_of(ioa) &
- is_execution_fragment ioa e}"
-
-
-reachable_def:
- "reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)"
-
-
-invariant_def: "invariant A P == (!s. reachable A s --> P(s))"
-
+(* Filtering and hiding *)
(* Restrict the trace to those members of the set s *)
-filter_oseq_def:
- "filter_oseq p s ==
+definition filter_oseq :: "('a => bool) => 'a oseq => 'a oseq"
+ where "filter_oseq p s ==
(%i. case s(i)
of None => None
| Some(x) => if p x then Some x else None)"
-
-mk_trace_def:
- "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))"
-
+definition mk_trace :: "[('action,'state)ioa, 'action oseq] => 'action oseq"
+ where "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))"
(* Does an ioa have an execution with the given trace *)
-has_trace_def:
- "has_trace ioa b ==
- (? ex:executions(ioa). b = mk_trace ioa (fst ex))"
+definition has_trace :: "[('action,'state)ioa, 'action oseq] => bool"
+ where "has_trace ioa b == (? ex:executions(ioa). b = mk_trace ioa (fst ex))"
-normal_form_def:
- "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &
+definition NF :: "'a oseq => 'a oseq"
+ where "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &
(!j. j ~: range(f) --> nf(j)= None) &
- (!i. nf(i)=None --> (nf (Suc i)) = None) "
+ (!i. nf(i)=None --> (nf (Suc i)) = None)"
(* All the traces of an ioa *)
-
- traces_def:
- "traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}"
-
-(*
- traces_def:
- "traces(ioa) == {tr. has_trace ioa tr}"
-*)
-
-compat_asigs_def:
- "compat_asigs a1 a2 ==
- (((outputs(a1) Int outputs(a2)) = {}) &
- ((internals(a1) Int actions(a2)) = {}) &
- ((internals(a2) Int actions(a1)) = {}))"
-
-
-compat_ioas_def:
- "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
+definition traces :: "('action,'state)ioa => 'action oseq set"
+ where "traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}"
-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:
- "(ioa1 || ioa2) ==
- (asig_comp (asig_of ioa1) (asig_of ioa2),
- {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},
- {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
- in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) &
- (if a:actions(asig_of(ioa1)) then
- (fst(s),a,fst(t)):trans_of(ioa1)
- else fst(t) = fst(s))
- &
- (if a:actions(asig_of(ioa2)) then
- (snd(s),a,snd(t)):trans_of(ioa2)
- else snd(t) = snd(s))})"
-
-
-restrict_asig_def:
- "restrict_asig asig actns ==
+definition restrict_asig :: "['a signature, 'a set] => 'a signature"
+ where "restrict_asig asig actns ==
(inputs(asig) Int actns, outputs(asig) Int actns,
internals(asig) Un (externals(asig) - actns))"
-
-restrict_def:
- "restrict ioa actns ==
+definition restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
+ where "restrict ioa actns ==
(restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))"
-ioa_implements_def:
- "ioa_implements ioa1 ioa2 ==
+
+(* Notions of correctness *)
+
+definition ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool"
+ where "ioa_implements ioa1 ioa2 ==
((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &
(outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) &
traces(ioa1) <= traces(ioa2))"
-rename_def:
-"rename ioa ren ==
- (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},
- {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},
- {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),
- 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)})"
+
+(* Instantiation of abstract IOA by concrete actions *)
+
+definition rename :: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
+ where "rename ioa ren ==
+ (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},
+ {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},
+ {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),
+ 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)})"
declare Let_def [simp]
@@ -206,7 +171,7 @@
lemma trans_in_actions:
"[| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))"
- apply (unfold ioa_def state_trans_def actions_def is_asig_def)
+ apply (unfold IOA_def state_trans_def actions_def is_asig_def)
apply (erule conjE)+
apply (erule allE, erule impE, assumption)
apply simp
--- a/src/HOL/Library/Old_Datatype.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/Library/Old_Datatype.thy Mon Jan 11 21:21:02 2016 +0100
@@ -26,80 +26,67 @@
type_synonym 'a item = "('a, unit) node set"
type_synonym ('a, 'b) dtree = "('a, 'b) node set"
-consts
- Push :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
-
- Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
- ndepth :: "('a, 'b) node => nat"
+definition Push :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
+ (*crude "lists" of nats -- needed for the constructions*)
+ where "Push == (%b h. case_nat b h)"
- Atom :: "('a + nat) => ('a, 'b) dtree"
- Leaf :: "'a => ('a, 'b) dtree"
- Numb :: "nat => ('a, 'b) dtree"
- Scons :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree"
- In0 :: "('a, 'b) dtree => ('a, 'b) dtree"
- In1 :: "('a, 'b) dtree => ('a, 'b) dtree"
- Lim :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree"
-
- ntrunc :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree"
-
- uprod :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
- usum :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
-
- Split :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
- Case :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
-
- dprod :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
- => (('a, 'b) dtree * ('a, 'b) dtree)set"
- dsum :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
- => (('a, 'b) dtree * ('a, 'b) dtree)set"
+definition Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
+ where "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
-defs
+(** operations on S-expressions -- sets of nodes **)
- Push_Node_def: "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
-
- (*crude "lists" of nats -- needed for the constructions*)
- Push_def: "Push == (%b h. case_nat b h)"
+(*S-expression constructors*)
+definition Atom :: "('a + nat) => ('a, 'b) dtree"
+ where "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
+definition Scons :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree"
+ where "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)"
- (** operations on S-expressions -- sets of nodes **)
+(*Leaf nodes, with arbitrary or nat labels*)
+definition Leaf :: "'a => ('a, 'b) dtree"
+ where "Leaf == Atom o Inl"
+definition Numb :: "nat => ('a, 'b) dtree"
+ where "Numb == Atom o Inr"
- (*S-expression constructors*)
- Atom_def: "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
- Scons_def: "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)"
-
- (*Leaf nodes, with arbitrary or nat labels*)
- Leaf_def: "Leaf == Atom o Inl"
- Numb_def: "Numb == Atom o Inr"
+(*Injections of the "disjoint sum"*)
+definition In0 :: "('a, 'b) dtree => ('a, 'b) dtree"
+ where "In0(M) == Scons (Numb 0) M"
+definition In1 :: "('a, 'b) dtree => ('a, 'b) dtree"
+ where "In1(M) == Scons (Numb 1) M"
- (*Injections of the "disjoint sum"*)
- In0_def: "In0(M) == Scons (Numb 0) M"
- In1_def: "In1(M) == Scons (Numb 1) M"
+(*Function spaces*)
+definition Lim :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree"
+ where "Lim f == \<Union>{z. ? x. z = Push_Node (Inl x) ` (f x)}"
- (*Function spaces*)
- Lim_def: "Lim f == \<Union>{z. ? x. z = Push_Node (Inl x) ` (f x)}"
+(*the set of nodes with depth less than k*)
+definition ndepth :: "('a, 'b) node => nat"
+ where "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
+definition ntrunc :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree"
+ where "ntrunc k N == {n. n:N & ndepth(n)<k}"
- (*the set of nodes with depth less than k*)
- ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
- ntrunc_def: "ntrunc k N == {n. n:N & ndepth(n)<k}"
+(*products and sums for the "universe"*)
+definition uprod :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
+ where "uprod A B == UN x:A. UN y:B. { Scons x y }"
+definition usum :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
+ where "usum A B == In0`A Un In1`B"
- (*products and sums for the "universe"*)
- uprod_def: "uprod A B == UN x:A. UN y:B. { Scons x y }"
- usum_def: "usum A B == In0`A Un In1`B"
+(*the corresponding eliminators*)
+definition Split :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
+ where "Split c M == THE u. EX x y. M = Scons x y & u = c x y"
- (*the corresponding eliminators*)
- Split_def: "Split c M == THE u. EX x y. M = Scons x y & u = c x y"
-
- Case_def: "Case c d M == THE u. (EX x . M = In0(x) & u = c(x))
- | (EX y . M = In1(y) & u = d(y))"
+definition Case :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
+ where "Case c d M == THE u. (EX x . M = In0(x) & u = c(x)) | (EX y . M = In1(y) & u = d(y))"
- (** equality for the "universe" **)
-
- dprod_def: "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
+(** equality for the "universe" **)
- dsum_def: "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un
- (UN (y,y'):s. {(In1(y),In1(y'))})"
+definition dprod :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
+ => (('a, 'b) dtree * ('a, 'b) dtree)set"
+ where "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
+definition dsum :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
+ => (('a, 'b) dtree * ('a, 'b) dtree)set"
+ where "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un (UN (y,y'):s. {(In1(y),In1(y'))})"
lemma apfst_convE:
--- a/src/HOL/MicroJava/DFA/Semilat.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy Mon Jan 11 21:21:02 2016 +0100
@@ -15,23 +15,26 @@
type_synonym 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
type_synonym 'a sl = "'a set \<times> 'a ord \<times> 'a binop"
-consts
- "lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
- "lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
- "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c"
-(*<*)
+definition lesub :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
+ where "lesub x r y \<longleftrightarrow> r x y"
+
+definition lesssub :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
+ where "lesssub x r y \<longleftrightarrow> lesub x r y \<and> x \<noteq> y"
+
+definition plussub :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c"
+ where "plussub x f y = f x y"
+
notation (ASCII)
"lesub" ("(_ /<='__ _)" [50, 1000, 51] 50) and
"lesssub" ("(_ /<'__ _)" [50, 1000, 51] 50) and
"plussub" ("(_ /+'__ _)" [65, 1000, 66] 65)
-(*>*)
+
notation
"lesub" ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
"lesssub" ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
"plussub" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
-(*<*)
+
(* allow \<sub> instead of \<bsub>..\<esub> *)
-
abbreviation (input)
lesub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
where "x \<sqsubseteq>\<^sub>r y == x \<sqsubseteq>\<^bsub>r\<^esub> y"
@@ -43,12 +46,6 @@
abbreviation (input)
plussub1 :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
where "x \<squnion>\<^sub>f y == x \<squnion>\<^bsub>f\<^esub> y"
-(*>*)
-
-defs
- lesub_def: "x \<sqsubseteq>\<^sub>r y \<equiv> r x y"
- lesssub_def: "x \<sqsubset>\<^sub>r y \<equiv> x \<sqsubseteq>\<^sub>r y \<and> x \<noteq> y"
- plussub_def: "x \<squnion>\<^sub>f y \<equiv> f x y"
definition ord :: "('a \<times> 'a) set \<Rightarrow> 'a ord" where
"ord r \<equiv> \<lambda>x y. (x,y) \<in> r"
--- a/src/HOL/MicroJava/J/Example.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/MicroJava/J/Example.thy Mon Jan 11 21:21:02 2016 +0100
@@ -82,31 +82,33 @@
declare Base_not_Xcpt [symmetric, simp]
declare Ext_not_Xcpt [symmetric, simp]
-consts
- foo_Base:: java_mb
- foo_Ext :: java_mb
- BaseC :: "java_mb cdecl"
- ExtC :: "java_mb cdecl"
- test :: stmt
- foo :: mname
- a :: loc
- b :: loc
+definition foo_Base :: java_mb
+ where "foo_Base == ([x],[],Skip,LAcc x)"
-defs
- foo_Base_def:"foo_Base == ([x],[],Skip,LAcc x)"
- BaseC_def:"BaseC == (Base, (Object,
+definition foo_Ext :: java_mb
+ where "foo_Ext == ([x],[],Expr( {Ext}Cast Ext
+ (LAcc x)..vee:=Lit (Intg Numeral1)),
+ Lit Null)"
+
+consts foo :: mname
+
+definition BaseC :: "java_mb cdecl"
+ where "BaseC == (Base, (Object,
[(vee, PrimT Boolean)],
[((foo,[Class Base]),Class Base,foo_Base)]))"
- foo_Ext_def:"foo_Ext == ([x],[],Expr( {Ext}Cast Ext
- (LAcc x)..vee:=Lit (Intg Numeral1)),
- Lit Null)"
- ExtC_def: "ExtC == (Ext, (Base ,
+
+definition ExtC :: "java_mb cdecl"
+ where "ExtC == (Ext, (Base ,
[(vee, PrimT Integer)],
[((foo,[Class Base]),Class Ext,foo_Ext)]))"
- test_def:"test == Expr(e::=NewC Ext);;
+definition test :: stmt
+ where "test == Expr(e::=NewC Ext);;
Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))"
+consts
+ a :: loc
+ b :: loc
abbreviation
NP :: xcpt where
--- a/src/HOL/MicroJava/J/TypeRel.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy Mon Jan 11 21:21:02 2016 +0100
@@ -176,14 +176,18 @@
by(rule finite_acyclic_wf_converse[OF finite_subcls1])
qed
-consts
- "method" :: "'c prog \<times> cname => ( sig \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
- field :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty )" (* ###curry *)
- fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
+definition "method" :: "'c prog \<times> cname => (sig \<rightharpoonup> cname \<times> ty \<times> 'c)"
+ \<comment> "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
+ where [code]: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
+ ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
-\<comment> "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
-defs method_def [code]: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
- ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
+definition fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list"
+ \<comment> "list of fields of a class, including inherited and hidden ones"
+ where [code]: "fields \<equiv> \<lambda>(G,C). class_rec G C [] (\<lambda>C fs ms ts.
+ map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
+
+definition field :: "'c prog \<times> cname => (vname \<rightharpoonup> cname \<times> ty)"
+ where [code]: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
method (G,C) = (if C = Object then empty else method (G,D)) ++
@@ -194,11 +198,6 @@
apply auto
done
-
-\<comment> "list of fields of a class, including inherited and hidden ones"
-defs fields_def [code]: "fields \<equiv> \<lambda>(G,C). class_rec G C [] (\<lambda>C fs ms ts.
- map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
-
lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
fields (G,C) =
map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
@@ -208,9 +207,6 @@
apply auto
done
-
-defs field_def [code]: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
-
lemma field_fields:
"field (G,C) fn = Some (fd, fT) \<Longrightarrow> map_of (fields (G,C)) (fn, fd) = Some fT"
apply (unfold field_def)
--- a/src/HOL/MicroJava/J/WellType.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy Mon Jan 11 21:21:02 2016 +0100
@@ -33,24 +33,20 @@
localT :: "'c env => (vname \<rightharpoonup> ty)"
where "localT == snd"
-consts
- more_spec :: "'c prog => (ty \<times> 'x) \<times> ty list =>
- (ty \<times> 'x) \<times> ty list => bool"
- appl_methds :: "'c prog => cname => sig => ((ty \<times> ty) \<times> ty list) set"
- max_spec :: "'c prog => cname => sig => ((ty \<times> ty) \<times> ty list) set"
+definition more_spec :: "'c prog \<Rightarrow> (ty \<times> 'x) \<times> ty list \<Rightarrow> (ty \<times> 'x) \<times> ty list \<Rightarrow> bool"
+ where "more_spec G == \<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>d\<preceq>d' \<and>
+ list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
-defs
- more_spec_def: "more_spec G == \<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>d\<preceq>d' \<and>
- list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
-
+definition appl_methds :: "'c prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> ((ty \<times> ty) \<times> ty list) set"
\<comment> "applicable methods, cf. 15.11.2.1"
- appl_methds_def: "appl_methds G C == \<lambda>(mn, pTs).
+ where "appl_methds G C == \<lambda>(mn, pTs).
{((Class md,rT),pTs') |md rT mb pTs'.
method (G,C) (mn, pTs') = Some (md,rT,mb) \<and>
list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'}"
+definition max_spec :: "'c prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> ((ty \<times> ty) \<times> ty list) set"
\<comment> "maximally specific methods, cf. 15.11.2.2"
- max_spec_def: "max_spec G C sig == {m. m \<in>appl_methds G C sig \<and>
+ where "max_spec G C sig == {m. m \<in>appl_methds G C sig \<and>
(\<forall>m'\<in>appl_methds G C sig.
more_spec G m' m --> m' = m)}"
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Mon Jan 11 21:21:02 2016 +0100
@@ -1273,10 +1273,20 @@
consts inverse :: "'a \<Rightarrow> 'a"
-defs (overloaded)
-inverse_bool: "inverse (b::bool) \<equiv> \<not> b"
-inverse_set: "inverse (S::'a set) \<equiv> -S"
-inverse_pair: "inverse p \<equiv> (inverse (fst p), inverse (snd p))"
+overloading inverse_bool \<equiv> "inverse :: bool \<Rightarrow> bool"
+begin
+ definition "inverse (b::bool) \<equiv> \<not> b"
+end
+
+overloading inverse_set \<equiv> "inverse :: 'a set \<Rightarrow> 'a set"
+begin
+ definition "inverse (S::'a set) \<equiv> -S"
+end
+
+overloading inverse_pair \<equiv> "inverse :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b"
+begin
+ definition "inverse_pair p \<equiv> (inverse (fst p), inverse (snd p))"
+end
lemma "inverse b"
nitpick [expect = genuine]
--- a/src/HOL/Nominal/Nominal.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/Nominal/Nominal.thy Mon Jan 11 21:21:02 2016 +0100
@@ -2416,11 +2416,15 @@
consts
fresh_star :: "'b \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp>* _" [100,100] 100)
-defs (overloaded)
- fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x\<in>xs. x\<sharp>c"
-
-defs (overloaded)
- fresh_star_list: "xs\<sharp>*c \<equiv> \<forall>x\<in>set xs. x\<sharp>c"
+overloading fresh_star_set \<equiv> "fresh_star :: 'b set \<Rightarrow> 'a \<Rightarrow> bool"
+begin
+ definition fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x::'b\<in>xs. x\<sharp>(c::'a)"
+end
+
+overloading frsh_star_list \<equiv> "fresh_star :: 'b list \<Rightarrow> 'a \<Rightarrow> bool"
+begin
+ definition fresh_star_list: "xs\<sharp>*c \<equiv> \<forall>x::'b\<in>set xs. x\<sharp>(c::'a)"
+end
lemmas fresh_star_def = fresh_star_list fresh_star_set
--- a/src/HOL/TLA/Buffer/Buffer.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/TLA/Buffer/Buffer.thy Mon Jan 11 21:21:02 2016 +0100
@@ -8,31 +8,35 @@
imports "../TLA"
begin
-consts
- (* actions *)
- BInit :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> stpred"
- Enq :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
- Deq :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
- Next :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
+(* actions *)
+
+definition BInit :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> stpred"
+ where "BInit ic q oc == PRED q = #[]"
- (* temporal formulas *)
- IBuffer :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
- Buffer :: "'a stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
+definition Enq :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
+ where "Enq ic q oc == ACT (ic$ \<noteq> $ic)
+ \<and> (q$ = $q @ [ ic$ ])
+ \<and> (oc$ = $oc)"
-defs
- BInit_def: "BInit ic q oc == PRED q = #[]"
- Enq_def: "Enq ic q oc == ACT (ic$ \<noteq> $ic)
- \<and> (q$ = $q @ [ ic$ ])
- \<and> (oc$ = $oc)"
- Deq_def: "Deq ic q oc == ACT ($q \<noteq> #[])
- \<and> (oc$ = hd< $q >)
- \<and> (q$ = tl< $q >)
- \<and> (ic$ = $ic)"
- Next_def: "Next ic q oc == ACT (Enq ic q oc \<or> Deq ic q oc)"
- IBuffer_def: "IBuffer ic q oc == TEMP Init (BInit ic q oc)
- \<and> \<box>[Next ic q oc]_(ic,q,oc)
- \<and> WF(Deq ic q oc)_(ic,q,oc)"
- Buffer_def: "Buffer ic oc == TEMP (\<exists>\<exists>q. IBuffer ic q oc)"
+definition Deq :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
+ where "Deq ic q oc == ACT ($q \<noteq> #[])
+ \<and> (oc$ = hd< $q >)
+ \<and> (q$ = tl< $q >)
+ \<and> (ic$ = $ic)"
+
+definition Next :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
+ where "Next ic q oc == ACT (Enq ic q oc \<or> Deq ic q oc)"
+
+
+(* temporal formulas *)
+
+definition IBuffer :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
+ where "IBuffer ic q oc == TEMP Init (BInit ic q oc)
+ \<and> \<box>[Next ic q oc]_(ic,q,oc)
+ \<and> WF(Deq ic q oc)_(ic,q,oc)"
+
+definition Buffer :: "'a stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
+ where "Buffer ic oc == TEMP (\<exists>\<exists>q. IBuffer ic q oc)"
(* ---------------------------- Data lemmas ---------------------------- *)
--- a/src/HOL/TLA/Init.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/TLA/Init.thy Mon Jan 11 21:21:02 2016 +0100
@@ -35,10 +35,17 @@
defs
Init_def: "sigma \<Turnstile> Init F == (first_world sigma) \<Turnstile> F"
-defs (overloaded)
- fw_temp_def: "first_world == \<lambda>sigma. sigma"
- fw_stp_def: "first_world == st1"
- fw_act_def: "first_world == \<lambda>sigma. (st1 sigma, st2 sigma)"
+overloading
+ fw_temp \<equiv> "first_world :: behavior \<Rightarrow> behavior"
+ fw_stp \<equiv> "first_world :: behavior \<Rightarrow> state"
+ fw_act \<equiv> "first_world :: behavior \<Rightarrow> state \<times> state"
+begin
+
+definition "first_world == \<lambda>sigma. sigma"
+definition "first_world == st1"
+definition "first_world == \<lambda>sigma. (st1 sigma, st2 sigma)"
+
+end
lemma const_simps [int_rewrite, simp]:
"\<turnstile> (Init #True) = #True"
--- a/src/HOL/TLA/Memory/Memory.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/TLA/Memory/Memory.thy Mon Jan 11 21:21:02 2016 +0100
@@ -12,122 +12,135 @@
type_synonym memType = "(Locs \<Rightarrow> Vals) stfun" (* intention: MemLocs \<Rightarrow> MemVals *)
type_synonym resType = "(PrIds \<Rightarrow> Vals) stfun"
-consts
- (* state predicates *)
- MInit :: "memType \<Rightarrow> Locs \<Rightarrow> stpred"
- PInit :: "resType \<Rightarrow> PrIds \<Rightarrow> stpred"
- (* auxiliary predicates: is there a pending read/write request for
- some process id and location/value? *)
- RdRequest :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> stpred"
- WrRequest :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> stpred"
+
+(* state predicates *)
+
+definition MInit :: "memType \<Rightarrow> Locs \<Rightarrow> stpred"
+ where "MInit mm l == PRED mm!l = #InitVal"
+
+definition PInit :: "resType \<Rightarrow> PrIds \<Rightarrow> stpred"
+ where "PInit rs p == PRED rs!p = #NotAResult"
+
+
+(* auxiliary predicates: is there a pending read/write request for
+ some process id and location/value? *)
+
+definition RdRequest :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> stpred"
+ where "RdRequest ch p l == PRED Calling ch p \<and> (arg<ch!p> = #(read l))"
+
+definition WrRequest :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> stpred"
+ where "WrRequest ch p l v == PRED Calling ch p \<and> (arg<ch!p> = #(write l v))"
+
+
+(* actions *)
+
+(* a read that doesn't raise BadArg *)
+definition GoodRead :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
+ where "GoodRead mm rs p l == ACT #l \<in> #MemLoc \<and> ((rs!p)$ = $(mm!l))"
+
+(* a read that raises BadArg *)
+definition BadRead :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
+ where "BadRead mm rs p l == ACT #l \<notin> #MemLoc \<and> ((rs!p)$ = #BadArg)"
- (* actions *)
- GoodRead :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
- BadRead :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
- ReadInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
- Read :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
- GoodWrite :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
- BadWrite :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
- WriteInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
- Write :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
- MemReturn :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
- MemFail :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
- RNext :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
- UNext :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+(* the read action with l visible *)
+definition ReadInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
+ where "ReadInner ch mm rs p l == ACT
+ $(RdRequest ch p l)
+ \<and> (GoodRead mm rs p l \<or> BadRead mm rs p l)
+ \<and> unchanged (rtrner ch ! p)"
+
+(* the read action with l quantified *)
+definition Read :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+ where "Read ch mm rs p == ACT (\<exists>l. ReadInner ch mm rs p l)"
- (* temporal formulas *)
- RPSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal"
- UPSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal"
- MSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> Locs \<Rightarrow> temporal"
- IRSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal"
- IUSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal"
+(* similar definitions for the write action *)
+definition GoodWrite :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
+ where "GoodWrite mm rs p l v ==
+ ACT #l \<in> #MemLoc \<and> #v \<in> #MemVal
+ \<and> ((mm!l)$ = #v) \<and> ((rs!p)$ = #OK)"
- RSpec :: "memChType \<Rightarrow> resType \<Rightarrow> temporal"
- USpec :: "memChType \<Rightarrow> temporal"
+definition BadWrite :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
+ where "BadWrite mm rs p l v == ACT
+ \<not> (#l \<in> #MemLoc \<and> #v \<in> #MemVal)
+ \<and> ((rs!p)$ = #BadArg) \<and> unchanged (mm!l)"
- (* memory invariant: in the paper, the invariant is hidden in the definition of
- the predicate S used in the implementation proof, but it is easier to verify
- at this level. *)
- MemInv :: "memType \<Rightarrow> Locs \<Rightarrow> stpred"
+definition WriteInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
+ where "WriteInner ch mm rs p l v == ACT
+ $(WrRequest ch p l v)
+ \<and> (GoodWrite mm rs p l v \<or> BadWrite mm rs p l v)
+ \<and> unchanged (rtrner ch ! p)"
-defs
- MInit_def: "MInit mm l == PRED mm!l = #InitVal"
- PInit_def: "PInit rs p == PRED rs!p = #NotAResult"
+definition Write :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
+ where "Write ch mm rs p l == ACT (\<exists>v. WriteInner ch mm rs p l v)"
+
- RdRequest_def: "RdRequest ch p l == PRED
- Calling ch p \<and> (arg<ch!p> = #(read l))"
- WrRequest_def: "WrRequest ch p l v == PRED
- Calling ch p \<and> (arg<ch!p> = #(write l v))"
- (* a read that doesn't raise BadArg *)
- GoodRead_def: "GoodRead mm rs p l == ACT
- #l \<in> #MemLoc \<and> ((rs!p)$ = $(mm!l))"
- (* a read that raises BadArg *)
- BadRead_def: "BadRead mm rs p l == ACT
- #l \<notin> #MemLoc \<and> ((rs!p)$ = #BadArg)"
- (* the read action with l visible *)
- ReadInner_def: "ReadInner ch mm rs p l == ACT
- $(RdRequest ch p l)
- \<and> (GoodRead mm rs p l \<or> BadRead mm rs p l)
- \<and> unchanged (rtrner ch ! p)"
- (* the read action with l quantified *)
- Read_def: "Read ch mm rs p == ACT (\<exists>l. ReadInner ch mm rs p l)"
+(* the return action *)
+definition MemReturn :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+ where "MemReturn ch rs p == ACT
+ ( ($(rs!p) \<noteq> #NotAResult)
+ \<and> ((rs!p)$ = #NotAResult)
+ \<and> Return ch p (rs!p))"
+
+(* the failure action of the unreliable memory *)
+definition MemFail :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+ where "MemFail ch rs p == ACT
+ $(Calling ch p)
+ \<and> ((rs!p)$ = #MemFailure)
+ \<and> unchanged (rtrner ch ! p)"
- (* similar definitions for the write action *)
- GoodWrite_def: "GoodWrite mm rs p l v == ACT
- #l \<in> #MemLoc \<and> #v \<in> #MemVal
- \<and> ((mm!l)$ = #v) \<and> ((rs!p)$ = #OK)"
- BadWrite_def: "BadWrite mm rs p l v == ACT
- \<not> (#l \<in> #MemLoc \<and> #v \<in> #MemVal)
- \<and> ((rs!p)$ = #BadArg) \<and> unchanged (mm!l)"
- WriteInner_def: "WriteInner ch mm rs p l v == ACT
- $(WrRequest ch p l v)
- \<and> (GoodWrite mm rs p l v \<or> BadWrite mm rs p l v)
- \<and> unchanged (rtrner ch ! p)"
- Write_def: "Write ch mm rs p l == ACT (\<exists>v. WriteInner ch mm rs p l v)"
+(* next-state relations for reliable / unreliable memory *)
+definition RNext :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+ where "RNext ch mm rs p == ACT
+ ( Read ch mm rs p
+ \<or> (\<exists>l. Write ch mm rs p l)
+ \<or> MemReturn ch rs p)"
+
+definition UNext :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+ where "UNext ch mm rs p == ACT (RNext ch mm rs p \<or> MemFail ch rs p)"
- (* the return action *)
- MemReturn_def: "MemReturn ch rs p == ACT
- ( ($(rs!p) \<noteq> #NotAResult)
- \<and> ((rs!p)$ = #NotAResult)
- \<and> Return ch p (rs!p))"
+
+(* temporal formulas *)
+
+definition RPSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal"
+ where "RPSpec ch mm rs p == TEMP
+ Init(PInit rs p)
+ \<and> \<box>[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
+ \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
+ \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
- (* the failure action of the unreliable memory *)
- MemFail_def: "MemFail ch rs p == ACT
- $(Calling ch p)
- \<and> ((rs!p)$ = #MemFailure)
- \<and> unchanged (rtrner ch ! p)"
- (* next-state relations for reliable / unreliable memory *)
- RNext_def: "RNext ch mm rs p == ACT
- ( Read ch mm rs p
- \<or> (\<exists>l. Write ch mm rs p l)
- \<or> MemReturn ch rs p)"
- UNext_def: "UNext ch mm rs p == ACT
- (RNext ch mm rs p \<or> MemFail ch rs p)"
+definition UPSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal"
+ where "UPSpec ch mm rs p == TEMP
+ Init(PInit rs p)
+ \<and> \<box>[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
+ \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
+ \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
+
+definition MSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> Locs \<Rightarrow> temporal"
+ where "MSpec ch mm rs l == TEMP
+ Init(MInit mm l)
+ \<and> \<box>[ \<exists>p. Write ch mm rs p l ]_(mm!l)"
+
+definition IRSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal"
+ where "IRSpec ch mm rs == TEMP
+ (\<forall>p. RPSpec ch mm rs p)
+ \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
- RPSpec_def: "RPSpec ch mm rs p == TEMP
- Init(PInit rs p)
- \<and> \<box>[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
- \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
- \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
- UPSpec_def: "UPSpec ch mm rs p == TEMP
- Init(PInit rs p)
- \<and> \<box>[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
- \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
- \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
- MSpec_def: "MSpec ch mm rs l == TEMP
- Init(MInit mm l)
- \<and> \<box>[ \<exists>p. Write ch mm rs p l ]_(mm!l)"
- IRSpec_def: "IRSpec ch mm rs == TEMP
- (\<forall>p. RPSpec ch mm rs p)
- \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
- IUSpec_def: "IUSpec ch mm rs == TEMP
- (\<forall>p. UPSpec ch mm rs p)
- \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
+definition IUSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal"
+ where "IUSpec ch mm rs == TEMP
+ (\<forall>p. UPSpec ch mm rs p)
+ \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
+
+definition RSpec :: "memChType \<Rightarrow> resType \<Rightarrow> temporal"
+ where "RSpec ch rs == TEMP (\<exists>\<exists>mm. IRSpec ch mm rs)"
- RSpec_def: "RSpec ch rs == TEMP (\<exists>\<exists>mm. IRSpec ch mm rs)"
- USpec_def: "USpec ch == TEMP (\<exists>\<exists>mm rs. IUSpec ch mm rs)"
+definition USpec :: "memChType \<Rightarrow> temporal"
+ where "USpec ch == TEMP (\<exists>\<exists>mm rs. IUSpec ch mm rs)"
- MemInv_def: "MemInv mm l == PRED #l \<in> #MemLoc \<longrightarrow> mm!l \<in> #MemVal"
+(* memory invariant: in the paper, the invariant is hidden in the definition of
+ the predicate S used in the implementation proof, but it is easier to verify
+ at this level. *)
+definition MemInv :: "memType \<Rightarrow> Locs \<Rightarrow> stpred"
+ where "MemInv mm l == PRED #l \<in> #MemLoc \<longrightarrow> mm!l \<in> #MemVal"
lemmas RM_action_defs =
MInit_def PInit_def RdRequest_def WrRequest_def MemInv_def
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy Mon Jan 11 21:21:02 2016 +0100
@@ -16,65 +16,78 @@
*)
type_synonym ('a,'r) channel =" (PrIds \<Rightarrow> ('a,'r) chan) stfun"
+
+(* data-level functions *)
+
consts
- (* data-level functions *)
cbit :: "('a,'r) chan \<Rightarrow> bit"
rbit :: "('a,'r) chan \<Rightarrow> bit"
arg :: "('a,'r) chan \<Rightarrow> 'a"
res :: "('a,'r) chan \<Rightarrow> 'r"
- (* state functions *)
- caller :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'a)) stfun"
- rtrner :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'r)) stfun"
+
+(* state functions *)
- (* state predicates *)
- Calling :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> stpred"
+definition caller :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'a)) stfun"
+ where "caller ch == \<lambda>s p. (cbit (ch s p), arg (ch s p))"
- (* actions *)
- ACall :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
- AReturn :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
+definition rtrner :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'r)) stfun"
+ where "rtrner ch == \<lambda>s p. (rbit (ch s p), res (ch s p))"
+
- (* temporal formulas *)
- PLegalCaller :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
- LegalCaller :: "('a,'r) channel \<Rightarrow> temporal"
- PLegalReturner :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
- LegalReturner :: "('a,'r) channel \<Rightarrow> temporal"
+(* slice through array-valued state function *)
- (* slice through array-valued state function *)
+consts
slice :: "('a \<Rightarrow> 'b) stfun \<Rightarrow> 'a \<Rightarrow> 'b stfun"
-
syntax
"_slice" :: "[lift, 'a] \<Rightarrow> lift" ("(_!_)" [70,70] 70)
-
- "_Call" :: "['a, 'b, lift] \<Rightarrow> lift" ("(Call _ _ _)" [90,90,90] 90)
- "_Return" :: "['a, 'b, lift] \<Rightarrow> lift" ("(Return _ _ _)" [90,90,90] 90)
-
translations
"_slice" == "CONST slice"
-
- "_Call" == "CONST ACall"
- "_Return" == "CONST AReturn"
-
defs
slice_def: "(PRED (x!i)) s == x s i"
- caller_def: "caller ch == \<lambda>s p. (cbit (ch s p), arg (ch s p))"
- rtrner_def: "rtrner ch == \<lambda>s p. (rbit (ch s p), res (ch s p))"
+
+(* state predicates *)
+
+definition Calling :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> stpred"
+ where "Calling ch p == PRED cbit< ch!p > \<noteq> rbit< ch!p >"
+
+
+(* actions *)
- Calling_def: "Calling ch p == PRED cbit< ch!p > \<noteq> rbit< ch!p >"
+consts
+ ACall :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
+ AReturn :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
+syntax
+ "_Call" :: "['a, 'b, lift] \<Rightarrow> lift" ("(Call _ _ _)" [90,90,90] 90)
+ "_Return" :: "['a, 'b, lift] \<Rightarrow> lift" ("(Return _ _ _)" [90,90,90] 90)
+translations
+ "_Call" == "CONST ACall"
+ "_Return" == "CONST AReturn"
+defs
Call_def: "(ACT Call ch p v) == ACT \<not> $Calling ch p
\<and> (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
\<and> (arg<ch!p>$ = $v)"
Return_def: "(ACT Return ch p v) == ACT $Calling ch p
\<and> (rbit<ch!p>$ = $cbit<ch!p>)
\<and> (res<ch!p>$ = $v)"
- PLegalCaller_def: "PLegalCaller ch p == TEMP
- Init(\<not> Calling ch p)
- \<and> \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"
- LegalCaller_def: "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)"
- PLegalReturner_def: "PLegalReturner ch p == TEMP
- \<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)"
- LegalReturner_def: "LegalReturner ch == TEMP (\<forall>p. PLegalReturner ch p)"
+
+
+(* temporal formulas *)
+
+definition PLegalCaller :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
+ where "PLegalCaller ch p == TEMP
+ Init(\<not> Calling ch p)
+ \<and> \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"
+
+definition LegalCaller :: "('a,'r) channel \<Rightarrow> temporal"
+ where "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)"
+
+definition PLegalReturner :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
+ where "PLegalReturner ch p == TEMP \<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)"
+
+definition LegalReturner :: "('a,'r) channel \<Rightarrow> temporal"
+ where "LegalReturner ch == TEMP (\<forall>p. PLegalReturner ch p)"
declare slice_def [simp]
--- a/src/HOL/TLA/Memory/RPC.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/TLA/Memory/RPC.thy Mon Jan 11 21:21:02 2016 +0100
@@ -12,63 +12,64 @@
type_synonym rpcRcvChType = "memChType"
type_synonym rpcStType = "(PrIds \<Rightarrow> rpcState) stfun"
-consts
- (* state predicates *)
- RPCInit :: "rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> stpred"
+
+(* state predicates *)
- (* actions *)
- RPCFwd :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
- RPCReject :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
- RPCFail :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
- RPCReply :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
- RPCNext :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+definition RPCInit :: "rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> stpred"
+ where "RPCInit rcv rst p == PRED ((rst!p = #rpcA) \<and> \<not>Calling rcv p)"
+
+
+(* actions *)
- (* temporal *)
- RPCIPSpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> temporal"
- RPCISpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> temporal"
-
-defs
- RPCInit_def: "RPCInit rcv rst p == PRED ((rst!p = #rpcA) \<and> \<not>Calling rcv p)"
+definition RPCFwd :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+ where "RPCFwd send rcv rst p == ACT
+ $(Calling send p)
+ \<and> $(rst!p) = # rpcA
+ \<and> IsLegalRcvArg<arg<$(send!p)>>
+ \<and> Call rcv p RPCRelayArg<arg<send!p>>
+ \<and> (rst!p)$ = # rpcB
+ \<and> unchanged (rtrner send!p)"
- RPCFwd_def: "RPCFwd send rcv rst p == ACT
- $(Calling send p)
- \<and> $(rst!p) = # rpcA
- \<and> IsLegalRcvArg<arg<$(send!p)>>
- \<and> Call rcv p RPCRelayArg<arg<send!p>>
- \<and> (rst!p)$ = # rpcB
- \<and> unchanged (rtrner send!p)"
+definition RPCReject :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+ where "RPCReject send rcv rst p == ACT
+ $(rst!p) = # rpcA
+ \<and> \<not>IsLegalRcvArg<arg<$(send!p)>>
+ \<and> Return send p #BadCall
+ \<and> unchanged ((rst!p), (caller rcv!p))"
- RPCReject_def: "RPCReject send rcv rst p == ACT
- $(rst!p) = # rpcA
- \<and> \<not>IsLegalRcvArg<arg<$(send!p)>>
- \<and> Return send p #BadCall
- \<and> unchanged ((rst!p), (caller rcv!p))"
+definition RPCFail :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+ where "RPCFail send rcv rst p == ACT
+ \<not>$(Calling rcv p)
+ \<and> Return send p #RPCFailure
+ \<and> (rst!p)$ = #rpcA
+ \<and> unchanged (caller rcv!p)"
- RPCFail_def: "RPCFail send rcv rst p == ACT
- \<not>$(Calling rcv p)
- \<and> Return send p #RPCFailure
- \<and> (rst!p)$ = #rpcA
- \<and> unchanged (caller rcv!p)"
+definition RPCReply :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+ where "RPCReply send rcv rst p == ACT
+ \<not>$(Calling rcv p)
+ \<and> $(rst!p) = #rpcB
+ \<and> Return send p res<rcv!p>
+ \<and> (rst!p)$ = #rpcA
+ \<and> unchanged (caller rcv!p)"
- RPCReply_def: "RPCReply send rcv rst p == ACT
- \<not>$(Calling rcv p)
- \<and> $(rst!p) = #rpcB
- \<and> Return send p res<rcv!p>
- \<and> (rst!p)$ = #rpcA
- \<and> unchanged (caller rcv!p)"
+definition RPCNext :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+ where "RPCNext send rcv rst p == ACT
+ ( RPCFwd send rcv rst p
+ \<or> RPCReject send rcv rst p
+ \<or> RPCFail send rcv rst p
+ \<or> RPCReply send rcv rst p)"
+
- RPCNext_def: "RPCNext send rcv rst p == ACT
- ( RPCFwd send rcv rst p
- \<or> RPCReject send rcv rst p
- \<or> RPCFail send rcv rst p
- \<or> RPCReply send rcv rst p)"
+(* temporal *)
- RPCIPSpec_def: "RPCIPSpec send rcv rst p == TEMP
- Init RPCInit rcv rst p
- \<and> \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
- \<and> WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
+definition RPCIPSpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> temporal"
+ where "RPCIPSpec send rcv rst p == TEMP
+ Init RPCInit rcv rst p
+ \<and> \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
+ \<and> WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
- RPCISpec_def: "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)"
+definition RPCISpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> temporal"
+ where "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)"
lemmas RPC_action_defs =
--- a/src/HOL/TLA/Memory/RPCParameters.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/TLA/Memory/RPCParameters.thy Mon Jan 11 21:21:02 2016 +0100
@@ -16,32 +16,28 @@
datatype rpcOp = memcall memOp | othercall Vals
datatype rpcState = rpcA | rpcB
-consts
- (* some particular return values *)
- RPCFailure :: Vals
- BadCall :: Vals
-
- (* Translate an rpc call to a memory call and test if the current argument
- is legal for the receiver (i.e., the memory). This can now be a little
- simpler than for the generic RPC component. RelayArg returns an arbitrary
- memory call for illegal arguments. *)
- IsLegalRcvArg :: "rpcOp \<Rightarrow> bool"
- RPCRelayArg :: "rpcOp \<Rightarrow> memOp"
-
-axiomatization where
+axiomatization RPCFailure :: Vals and BadCall :: Vals
+where
(* RPCFailure is different from MemVals and exceptions *)
RFNoMemVal: "RPCFailure \<notin> MemVal" and
NotAResultNotRF: "NotAResult \<noteq> RPCFailure" and
OKNotRF: "OK \<noteq> RPCFailure" and
BANotRF: "BadArg \<noteq> RPCFailure"
-defs
- IsLegalRcvArg_def: "IsLegalRcvArg ra ==
- case ra of (memcall m) \<Rightarrow> True
- | (othercall v) \<Rightarrow> False"
- RPCRelayArg_def: "RPCRelayArg ra ==
- case ra of (memcall m) \<Rightarrow> m
- | (othercall v) \<Rightarrow> undefined"
+(* Translate an rpc call to a memory call and test if the current argument
+ is legal for the receiver (i.e., the memory). This can now be a little
+ simpler than for the generic RPC component. RelayArg returns an arbitrary
+ memory call for illegal arguments. *)
+
+definition IsLegalRcvArg :: "rpcOp \<Rightarrow> bool"
+ where "IsLegalRcvArg ra ==
+ case ra of (memcall m) \<Rightarrow> True
+ | (othercall v) \<Rightarrow> False"
+
+definition RPCRelayArg :: "rpcOp \<Rightarrow> memOp"
+ where "RPCRelayArg ra ==
+ case ra of (memcall m) \<Rightarrow> m
+ | (othercall v) \<Rightarrow> undefined"
lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF
NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric]
--- a/src/HOL/TLA/Stfun.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/TLA/Stfun.thy Mon Jan 11 21:21:02 2016 +0100
@@ -40,15 +40,17 @@
"PRED P" => "(P::state \<Rightarrow> _)"
"_stvars" == "CONST stvars"
-defs
- (* Base variables may be assigned arbitrary (type-correct) values.
- Note that vs may be a tuple of variables. The correct identification
- of base variables is up to the user who must take care not to
- introduce an inconsistency. For example, "basevars (x,x)" would
- definitely be inconsistent.
- *)
- basevars_def: "stvars vs == range vs = UNIV"
-
+(* Base variables may be assigned arbitrary (type-correct) values.
+ Note that vs may be a tuple of variables. The correct identification
+ of base variables is up to the user who must take care not to
+ introduce an inconsistency. For example, "basevars (x,x)" would
+ definitely be inconsistent.
+*)
+overloading stvars \<equiv> stvars
+begin
+ definition stvars :: "(state \<Rightarrow> 'a) \<Rightarrow> bool"
+ where basevars_def: "stvars vs == range vs = UNIV"
+end
lemma basevars: "\<And>vs. basevars vs \<Longrightarrow> \<exists>u. vs u = c"
apply (unfold basevars_def)
--- a/src/HOL/ex/MT.thy Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/ex/MT.thy Mon Jan 11 21:21:02 2016 +0100
@@ -60,21 +60,7 @@
te_app :: "[TyEnv, ExVar] => Ty"
te_dom :: "TyEnv => ExVar set"
- eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set"
- eval_rel :: "((ValEnv * Ex) * Val) set"
- eval :: "[ValEnv, Ex, Val] => bool" ("_ |- _ ---> _" [36,0,36] 50)
-
- elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set"
- elab_rel :: "((TyEnv * Ex) * Ty) set"
- elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [36,0,36] 50)
-
isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50)
- isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _")
-
- hasty_fun :: "(Val * Ty) set => (Val * Ty) set"
- hasty_rel :: "(Val * Ty) set"
- hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50)
- hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35)
(*
Expression constructors must be injective, distinct and it must be possible
@@ -185,9 +171,8 @@
derived.
*)
-defs
- eval_fun_def:
- " eval_fun(s) ==
+definition eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set"
+ where "eval_fun(s) ==
{ pp.
(? ve c. pp=((ve,e_const(c)),v_const(c))) |
(? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve)) |
@@ -208,51 +193,56 @@
)
}"
- eval_rel_def: "eval_rel == lfp(eval_fun)"
- eval_def: "ve |- e ---> v == ((ve,e),v):eval_rel"
+definition eval_rel :: "((ValEnv * Ex) * Val) set"
+ where "eval_rel == lfp(eval_fun)"
+
+definition eval :: "[ValEnv, Ex, Val] => bool" ("_ |- _ ---> _" [36,0,36] 50)
+ where "ve |- e ---> v == ((ve,e),v) \<in> eval_rel"
(* The static semantics is defined in the same way as the dynamic
semantics. The relation te |- e ===> t express the expression e has the
type t in the type environment te.
*)
- elab_fun_def:
- "elab_fun(s) ==
- { pp.
- (? te c t. pp=((te,e_const(c)),t) & c isof t) |
- (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) |
- (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) |
- (? te f x e t1 t2.
- pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s
- ) |
- (? te e1 e2 t1 t2.
- pp=((te,e1 @@ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s
- )
- }"
+definition elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set"
+ where "elab_fun(s) ==
+ { pp.
+ (? te c t. pp=((te,e_const(c)),t) & c isof t) |
+ (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) |
+ (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) |
+ (? te f x e t1 t2.
+ pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s
+ ) |
+ (? te e1 e2 t1 t2.
+ pp=((te,e1 @@ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s
+ )
+ }"
- elab_rel_def: "elab_rel == lfp(elab_fun)"
- elab_def: "te |- e ===> t == ((te,e),t):elab_rel"
+definition elab_rel :: "((TyEnv * Ex) * Ty) set"
+ where "elab_rel == lfp(elab_fun)"
+
+definition elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [36,0,36] 50)
+ where "te |- e ===> t == ((te,e),t):elab_rel"
+
(* The original correspondence relation *)
- isof_env_def:
- " ve isofenv te ==
- ve_dom(ve) = te_dom(te) &
- ( ! x.
+definition isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _")
+ where "ve isofenv te ==
+ ve_dom(ve) = te_dom(te) &
+ (! x.
x:ve_dom(ve) -->
- (? c. ve_app ve x = v_const(c) & c isof te_app te x)
- )
- "
+ (? c. ve_app ve x = v_const(c) & c isof te_app te x))"
axiomatization where
isof_app: "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app c1 c2 isof t2"
-defs
+
(* The extented correspondence relation *)
- hasty_fun_def:
- " hasty_fun(r) ==
- { p.
+definition hasty_fun :: "(Val * Ty) set => (Val * Ty) set"
+ where "hasty_fun(r) ==
+ { p.
( ? c t. p = (v_const(c),t) & c isof t) |
( ? ev e ve t te.
p = (v_clos(<|ev,e,ve|>),t) &
@@ -260,15 +250,18 @@
ve_dom(ve) = te_dom(te) &
(! ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r)
)
- }
- "
+ }"
+
+definition hasty_rel :: "(Val * Ty) set"
+ where "hasty_rel == gfp(hasty_fun)"
- hasty_rel_def: "hasty_rel == gfp(hasty_fun)"
- hasty_def: "v hasty t == (v,t) : hasty_rel"
- hasty_env_def:
- " ve hastyenv te ==
- ve_dom(ve) = te_dom(te) &
- (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)"
+definition hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50)
+ where "v hasty t == (v,t) : hasty_rel"
+
+definition hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35)
+ where "ve hastyenv te ==
+ ve_dom(ve) = te_dom(te) &
+ (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)"
(* ############################################################ *)