--- a/src/CCL/CCL.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/CCL/CCL.thy Tue Jan 12 20:05:53 2016 +0100
@@ -320,17 +320,17 @@
apply blast
done
-lemma POgenXH:
- "<t,t'> : POgen(R) \<longleftrightarrow> t= bot | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
- (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> <a,a'> : R \<and> <b,b'> : R) |
+lemma POgenXH:
+ "<t,t'> : POgen(R) \<longleftrightarrow> t= bot | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
+ (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> <a,a'> : R \<and> <b,b'> : R) |
(EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. <f(x),f'(x)> : R))"
apply (unfold POgen_def SIM_def)
apply (rule iff_refl [THEN XHlemma2])
done
-lemma poXH:
- "t [= t' \<longleftrightarrow> t=bot | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
- (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> a [= a' \<and> b [= b') |
+lemma poXH:
+ "t [= t' \<longleftrightarrow> t=bot | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
+ (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> a [= a' \<and> b [= b') |
(EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. f(x) [= f'(x)))"
apply (simp add: PO_iff del: ex_simps)
apply (rule POgen_mono
@@ -438,18 +438,18 @@
apply blast
done
-lemma EQgenXH:
- "<t,t'> : EQgen(R) \<longleftrightarrow> (t=bot \<and> t'=bot) | (t=true \<and> t'=true) |
- (t=false \<and> t'=false) |
- (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> <a,a'> : R \<and> <b,b'> : R) |
+lemma EQgenXH:
+ "<t,t'> : EQgen(R) \<longleftrightarrow> (t=bot \<and> t'=bot) | (t=true \<and> t'=true) |
+ (t=false \<and> t'=false) |
+ (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> <a,a'> : R \<and> <b,b'> : R) |
(EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x.<f(x),f'(x)> : R))"
apply (unfold EQgen_def SIM_def)
apply (rule iff_refl [THEN XHlemma2])
done
-lemma eqXH:
- "t=t' \<longleftrightarrow> (t=bot \<and> t'=bot) | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
- (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> a=a' \<and> b=b') |
+lemma eqXH:
+ "t=t' \<longleftrightarrow> (t=bot \<and> t'=bot) | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
+ (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> a=a' \<and> b=b') |
(EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. f(x)=f'(x)))"
apply (subgoal_tac "<t,t'> : EQ \<longleftrightarrow>
(t=bot \<and> t'=bot) | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
--- a/src/CCL/Set.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/CCL/Set.thy Tue Jan 12 20:05:53 2016 +0100
@@ -9,62 +9,18 @@
typedecl 'a set
instance set :: ("term") "term" ..
-consts
- Collect :: "['a \<Rightarrow> o] \<Rightarrow> 'a set" (*comprehension*)
- Compl :: "('a set) \<Rightarrow> 'a set" (*complement*)
- Int :: "['a set, 'a set] \<Rightarrow> 'a set" (infixl "Int" 70)
- Un :: "['a set, 'a set] \<Rightarrow> 'a set" (infixl "Un" 65)
- Union :: "(('a set)set) \<Rightarrow> 'a set" (*...of a set*)
- Inter :: "(('a set)set) \<Rightarrow> 'a set" (*...of a set*)
- UNION :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set" (*general*)
- INTER :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set" (*general*)
- Ball :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o" (*bounded quants*)
- Bex :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o" (*bounded quants*)
- mono :: "['a set \<Rightarrow> 'b set] \<Rightarrow> o" (*monotonicity*)
- mem :: "['a, 'a set] \<Rightarrow> o" (infixl ":" 50) (*membership*)
- subset :: "['a set, 'a set] \<Rightarrow> o" (infixl "<=" 50)
- singleton :: "'a \<Rightarrow> 'a set" ("{_}")
- empty :: "'a set" ("{}")
+
+subsection \<open>Set comprehension and membership\<close>
+
+axiomatization Collect :: "['a \<Rightarrow> o] \<Rightarrow> 'a set"
+ and mem :: "['a, 'a set] \<Rightarrow> o" (infixl ":" 50)
+where mem_Collect_iff: "(a : Collect(P)) \<longleftrightarrow> P(a)"
+ and set_extension: "A = B \<longleftrightarrow> (ALL x. x:A \<longleftrightarrow> x:B)"
syntax
- "_Coll" :: "[idt, o] \<Rightarrow> 'a set" ("(1{_./ _})") (*collection*)
-
- (* Big Intersection / Union *)
-
- "_INTER" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set" ("(INT _:_./ _)" [0, 0, 0] 10)
- "_UNION" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set" ("(UN _:_./ _)" [0, 0, 0] 10)
-
- (* Bounded Quantifiers *)
-
- "_Ball" :: "[idt, 'a set, o] \<Rightarrow> o" ("(ALL _:_./ _)" [0, 0, 0] 10)
- "_Bex" :: "[idt, 'a set, o] \<Rightarrow> o" ("(EX _:_./ _)" [0, 0, 0] 10)
-
+ "_Coll" :: "[idt, o] \<Rightarrow> 'a set" ("(1{_./ _})")
translations
- "{x. P}" == "CONST Collect(\<lambda>x. P)"
- "INT x:A. B" == "CONST INTER(A, \<lambda>x. B)"
- "UN x:A. B" == "CONST UNION(A, \<lambda>x. B)"
- "ALL x:A. P" == "CONST Ball(A, \<lambda>x. P)"
- "EX x:A. P" == "CONST Bex(A, \<lambda>x. P)"
-
-axiomatization where
- mem_Collect_iff: "(a : {x. P(x)}) \<longleftrightarrow> P(a)" and
- set_extension: "A = B \<longleftrightarrow> (ALL x. x:A \<longleftrightarrow> x:B)"
-
-defs
- Ball_def: "Ball(A, P) == ALL x. x:A \<longrightarrow> P(x)"
- Bex_def: "Bex(A, P) == EX x. x:A \<and> P(x)"
- mono_def: "mono(f) == (ALL A B. A <= B \<longrightarrow> f(A) <= f(B))"
- subset_def: "A <= B == ALL x:A. x:B"
- singleton_def: "{a} == {x. x=a}"
- empty_def: "{} == {x. False}"
- Un_def: "A Un B == {x. x:A | x:B}"
- Int_def: "A Int B == {x. x:A \<and> x:B}"
- Compl_def: "Compl(A) == {x. \<not>x:A}"
- INTER_def: "INTER(A, B) == {y. ALL x:A. y: B(x)}"
- UNION_def: "UNION(A, B) == {y. EX x:A. y: B(x)}"
- Inter_def: "Inter(S) == (INT x:S. x)"
- Union_def: "Union(S) == (UN x:S. x)"
-
+ "{x. P}" == "CONST Collect(\<lambda>x. P)"
lemma CollectI: "P(a) \<Longrightarrow> a : {x. P(x)}"
apply (rule mem_Collect_iff [THEN iffD2])
@@ -85,6 +41,19 @@
subsection \<open>Bounded quantifiers\<close>
+definition Ball :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o"
+ where "Ball(A, P) == ALL x. x:A \<longrightarrow> P(x)"
+
+definition Bex :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o"
+ where "Bex(A, P) == EX x. x:A \<and> P(x)"
+
+syntax
+ "_Ball" :: "[idt, 'a set, o] \<Rightarrow> o" ("(ALL _:_./ _)" [0, 0, 0] 10)
+ "_Bex" :: "[idt, 'a set, o] \<Rightarrow> o" ("(EX _:_./ _)" [0, 0, 0] 10)
+translations
+ "ALL x:A. P" == "CONST Ball(A, \<lambda>x. P)"
+ "EX x:A. P" == "CONST Bex(A, \<lambda>x. P)"
+
lemma ballI: "(\<And>x. x:A \<Longrightarrow> P(x)) \<Longrightarrow> ALL x:A. P(x)"
by (simp add: Ball_def)
@@ -107,8 +76,7 @@
lemma ball_rew: "(ALL x:A. True) \<longleftrightarrow> True"
by (blast intro: ballI)
-
-subsection \<open>Congruence rules\<close>
+subsubsection \<open>Congruence rules\<close>
lemma ball_cong:
"\<lbrakk>A = A'; \<And>x. x:A' \<Longrightarrow> P(x) \<longleftrightarrow> P'(x)\<rbrakk> \<Longrightarrow>
@@ -121,6 +89,52 @@
by (blast intro: bexI elim: bexE)
+subsection \<open>Further operations\<close>
+
+definition subset :: "['a set, 'a set] \<Rightarrow> o" (infixl "<=" 50)
+ where "A <= B == ALL x:A. x:B"
+
+definition mono :: "['a set \<Rightarrow> 'b set] \<Rightarrow> o"
+ where "mono(f) == (ALL A B. A <= B \<longrightarrow> f(A) <= f(B))"
+
+definition singleton :: "'a \<Rightarrow> 'a set" ("{_}")
+ where "{a} == {x. x=a}"
+
+definition empty :: "'a set" ("{}")
+ where "{} == {x. False}"
+
+definition Un :: "['a set, 'a set] \<Rightarrow> 'a set" (infixl "Un" 65)
+ where "A Un B == {x. x:A | x:B}"
+
+definition Int :: "['a set, 'a set] \<Rightarrow> 'a set" (infixl "Int" 70)
+ where "A Int B == {x. x:A \<and> x:B}"
+
+definition Compl :: "('a set) \<Rightarrow> 'a set"
+ where "Compl(A) == {x. \<not>x:A}"
+
+
+subsection \<open>Big Intersection / Union\<close>
+
+definition INTER :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set"
+ where "INTER(A, B) == {y. ALL x:A. y: B(x)}"
+
+definition UNION :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set"
+ where "UNION(A, B) == {y. EX x:A. y: B(x)}"
+
+syntax
+ "_INTER" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set" ("(INT _:_./ _)" [0, 0, 0] 10)
+ "_UNION" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set" ("(UN _:_./ _)" [0, 0, 0] 10)
+translations
+ "INT x:A. B" == "CONST INTER(A, \<lambda>x. B)"
+ "UN x:A. B" == "CONST UNION(A, \<lambda>x. B)"
+
+definition Inter :: "(('a set)set) \<Rightarrow> 'a set"
+ where "Inter(S) == (INT x:S. x)"
+
+definition Union :: "(('a set)set) \<Rightarrow> 'a set"
+ where "Union(S) == (UN x:S. x)"
+
+
subsection \<open>Rules for subsets\<close>
lemma subsetI: "(\<And>x. x:A \<Longrightarrow> x:B) \<Longrightarrow> A <= B"
--- a/src/CCL/Term.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/CCL/Term.thy Tue Jan 12 20:05:53 2016 +0100
@@ -9,48 +9,69 @@
imports CCL
begin
-consts
+definition one :: "i"
+ where "one == true"
- one :: "i"
+definition "if" :: "[i,i,i]\<Rightarrow>i" ("(3if _/ then _/ else _)" [0,0,60] 60)
+ where "if b then t else u == case(b, t, u, \<lambda> x y. bot, \<lambda>v. bot)"
- "if" :: "[i,i,i]\<Rightarrow>i" ("(3if _/ then _/ else _)" [0,0,60] 60)
+definition inl :: "i\<Rightarrow>i"
+ where "inl(a) == <true,a>"
- inl :: "i\<Rightarrow>i"
- inr :: "i\<Rightarrow>i"
- "when" :: "[i,i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i"
+definition inr :: "i\<Rightarrow>i"
+ where "inr(b) == <false,b>"
+
+definition split :: "[i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
+ where "split(t,f) == case(t, bot, bot, f, \<lambda>u. bot)"
- split :: "[i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
- fst :: "i\<Rightarrow>i"
- snd :: "i\<Rightarrow>i"
- thd :: "i\<Rightarrow>i"
+definition "when" :: "[i,i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i"
+ where "when(t,f,g) == split(t, \<lambda>b x. if b then f(x) else g(x))"
+
+definition fst :: "i\<Rightarrow>i"
+ where "fst(t) == split(t, \<lambda>x y. x)"
- zero :: "i"
- succ :: "i\<Rightarrow>i"
- ncase :: "[i,i,i\<Rightarrow>i]\<Rightarrow>i"
- nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
+definition snd :: "i\<Rightarrow>i"
+ where "snd(t) == split(t, \<lambda>x y. y)"
+
+definition thd :: "i\<Rightarrow>i"
+ where "thd(t) == split(t, \<lambda>x p. split(p, \<lambda>y z. z))"
+
+definition zero :: "i"
+ where "zero == inl(one)"
- nil :: "i" ("([])")
- cons :: "[i,i]\<Rightarrow>i" (infixr "$" 80)
- lcase :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
- lrec :: "[i,i,[i,i,i]\<Rightarrow>i]\<Rightarrow>i"
+definition succ :: "i\<Rightarrow>i"
+ where "succ(n) == inr(n)"
+
+definition ncase :: "[i,i,i\<Rightarrow>i]\<Rightarrow>i"
+ where "ncase(n,b,c) == when(n, \<lambda>x. b, \<lambda>y. c(y))"
- "let" :: "[i,i\<Rightarrow>i]\<Rightarrow>i"
- letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
- letrec2 :: "[[i,i,i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
- letrec3 :: "[[i,i,i,i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+
+no_syntax
+ "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
+
+definition "let" :: "[i,i\<Rightarrow>i]\<Rightarrow>i"
+ where "let(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
syntax
- "_let" :: "[id,i,i]\<Rightarrow>i" ("(3let _ be _/ in _)"
- [0,0,60] 60)
+ "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
- "_letrec" :: "[id,id,i,i]\<Rightarrow>i" ("(3letrec _ _ be _/ in _)"
- [0,0,0,60] 60)
+definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+ where "letrec(h, b) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)"
+
+definition letrec2 :: "[[i,i,i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+ where "letrec2 (h, f) ==
+ letrec (\<lambda>p g'. split(p,\<lambda>x y. h(x,y,\<lambda>u v. g'(<u,v>))), \<lambda>g'. f(\<lambda>x y. g'(<x,y>)))"
- "_letrec2" :: "[id,id,id,i,i]\<Rightarrow>i" ("(3letrec _ _ _ be _/ in _)"
- [0,0,0,0,60] 60)
+definition letrec3 :: "[[i,i,i,i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+ where "letrec3 (h, f) ==
+ letrec (\<lambda>p g'. split(p,\<lambda>x xs. split(xs,\<lambda>y z. h(x,y,z,\<lambda>u v w. g'(<u,<v,w>>)))),
+ \<lambda>g'. f(\<lambda>x y z. g'(<x,<y,z>>)))"
- "_letrec3" :: "[id,id,id,id,i,i]\<Rightarrow>i" ("(3letrec _ _ _ _ be _/ in _)"
- [0,0,0,0,0,60] 60)
+syntax
+ "_let" :: "[id,i,i]\<Rightarrow>i" ("(3let _ be _/ in _)" [0,0,60] 60)
+ "_letrec" :: "[id,id,i,i]\<Rightarrow>i" ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60)
+ "_letrec2" :: "[id,id,id,i,i]\<Rightarrow>i" ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60)
+ "_letrec3" :: "[id,id,id,id,i,i]\<Rightarrow>i" ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60)
ML \<open>
(** Quantifier translations: variable binding **)
@@ -107,42 +128,24 @@
(@{const_syntax letrec3}, K letrec3_tr')]
\<close>
-consts
- napply :: "[i\<Rightarrow>i,i,i]\<Rightarrow>i" ("(_ ^ _ ` _)" [56,56,56] 56)
+
+definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
+ where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
+
+definition nil :: "i" ("([])")
+ where "[] == inl(one)"
-defs
- one_def: "one == true"
- if_def: "if b then t else u == case(b, t, u, \<lambda> x y. bot, \<lambda>v. bot)"
- inl_def: "inl(a) == <true,a>"
- inr_def: "inr(b) == <false,b>"
- when_def: "when(t,f,g) == split(t, \<lambda>b x. if b then f(x) else g(x))"
- split_def: "split(t,f) == case(t, bot, bot, f, \<lambda>u. bot)"
- fst_def: "fst(t) == split(t, \<lambda>x y. x)"
- snd_def: "snd(t) == split(t, \<lambda>x y. y)"
- thd_def: "thd(t) == split(t, \<lambda>x p. split(p, \<lambda>y z. z))"
- zero_def: "zero == inl(one)"
- succ_def: "succ(n) == inr(n)"
- ncase_def: "ncase(n,b,c) == when(n, \<lambda>x. b, \<lambda>y. c(y))"
- nrec_def: " nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
- nil_def: "[] == inl(one)"
- cons_def: "h$t == inr(<h,t>)"
- lcase_def: "lcase(l,b,c) == when(l, \<lambda>x. b, \<lambda>y. split(y,c))"
- lrec_def: "lrec(l,b,c) == letrec g x be lcase(x, b, \<lambda>h t. c(h,t,g(t))) in g(l)"
+definition cons :: "[i,i]\<Rightarrow>i" (infixr "$" 80)
+ where "h$t == inr(<h,t>)"
+
+definition lcase :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
+ where "lcase(l,b,c) == when(l, \<lambda>x. b, \<lambda>y. split(y,c))"
- let_def: "let x be t in f(x) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
- letrec_def:
- "letrec g x be h(x,g) in b(g) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)"
+definition lrec :: "[i,i,[i,i,i]\<Rightarrow>i]\<Rightarrow>i"
+ where "lrec(l,b,c) == letrec g x be lcase(x, b, \<lambda>h t. c(h,t,g(t))) in g(l)"
- letrec2_def: "letrec g x y be h(x,y,g) in f(g)==
- letrec g' p be split(p,\<lambda>x y. h(x,y,\<lambda>u v. g'(<u,v>)))
- in f(\<lambda>x y. g'(<x,y>))"
-
- letrec3_def: "letrec g x y z be h(x,y,z,g) in f(g) ==
- letrec g' p be split(p,\<lambda>x xs. split(xs,\<lambda>y z. h(x,y,z,\<lambda>u v w. g'(<u,<v,w>>))))
- in f(\<lambda>x y z. g'(<x,<y,z>>))"
-
- napply_def: "f ^n` a == nrec(n,a,\<lambda>x g. f(g))"
-
+definition napply :: "[i\<Rightarrow>i,i,i]\<Rightarrow>i" ("(_ ^ _ ` _)" [56,56,56] 56)
+ where "f ^n` a == nrec(n,a,\<lambda>x g. f(g))"
lemmas simp_can_defs = one_def inl_def inr_def
and simp_ncan_defs = if_def when_def split_def fst_def snd_def thd_def
--- a/src/CCL/Type.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/CCL/Type.thy Tue Jan 12 20:05:53 2016 +0100
@@ -9,42 +9,39 @@
imports Term
begin
-consts
-
- Subtype :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> 'a set"
- Bool :: "i set"
- Unit :: "i set"
- Plus :: "[i set, i set] \<Rightarrow> i set" (infixr "+" 55)
- Pi :: "[i set, i \<Rightarrow> i set] \<Rightarrow> i set"
- Sigma :: "[i set, i \<Rightarrow> i set] \<Rightarrow> i set"
- Nat :: "i set"
- List :: "i set \<Rightarrow> i set"
- Lists :: "i set \<Rightarrow> i set"
- ILists :: "i set \<Rightarrow> i set"
- TAll :: "(i set \<Rightarrow> i set) \<Rightarrow> i set" (binder "TALL " 55)
- TEx :: "(i set \<Rightarrow> i set) \<Rightarrow> i set" (binder "TEX " 55)
- Lift :: "i set \<Rightarrow> i set" ("(3[_])")
-
- SPLIT :: "[i, [i, i] \<Rightarrow> i set] \<Rightarrow> i set"
+definition Subtype :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> 'a set"
+ where "Subtype(A, P) == {x. x:A \<and> P(x)}"
syntax
- "_Pi" :: "[idt, i set, i set] \<Rightarrow> i set" ("(3PROD _:_./ _)"
- [0,0,60] 60)
+ "_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set" ("(1{_: _ ./ _})")
+translations
+ "{x: A. B}" == "CONST Subtype(A, \<lambda>x. B)"
- "_Sigma" :: "[idt, i set, i set] \<Rightarrow> i set" ("(3SUM _:_./ _)"
- [0,0,60] 60)
+definition Unit :: "i set"
+ where "Unit == {x. x=one}"
+
+definition Bool :: "i set"
+ where "Bool == {x. x=true | x=false}"
+
+definition Plus :: "[i set, i set] \<Rightarrow> i set" (infixr "+" 55)
+ where "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}"
- "_arrow" :: "[i set, i set] \<Rightarrow> i set" ("(_ ->/ _)" [54, 53] 53)
- "_star" :: "[i set, i set] \<Rightarrow> i set" ("(_ */ _)" [56, 55] 55)
- "_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set" ("(1{_: _ ./ _})")
+definition Pi :: "[i set, i \<Rightarrow> i set] \<Rightarrow> i set"
+ where "Pi(A,B) == {x. EX b. x=lam x. b(x) \<and> (ALL x:A. b(x):B(x))}"
+
+definition Sigma :: "[i set, i \<Rightarrow> i set] \<Rightarrow> i set"
+ where "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}"
+syntax
+ "_Pi" :: "[idt, i set, i set] \<Rightarrow> i set" ("(3PROD _:_./ _)" [0,0,60] 60)
+ "_Sigma" :: "[idt, i set, i set] \<Rightarrow> i set" ("(3SUM _:_./ _)" [0,0,60] 60)
+ "_arrow" :: "[i set, i set] \<Rightarrow> i set" ("(_ ->/ _)" [54, 53] 53)
+ "_star" :: "[i set, i set] \<Rightarrow> i set" ("(_ */ _)" [56, 55] 55)
translations
- "PROD x:A. B" => "CONST Pi(A, \<lambda>x. B)"
- "A -> B" => "CONST Pi(A, \<lambda>_. B)"
- "SUM x:A. B" => "CONST Sigma(A, \<lambda>x. B)"
- "A * B" => "CONST Sigma(A, \<lambda>_. B)"
- "{x: A. B}" == "CONST Subtype(A, \<lambda>x. B)"
-
+ "PROD x:A. B" \<rightharpoonup> "CONST Pi(A, \<lambda>x. B)"
+ "A -> B" \<rightharpoonup> "CONST Pi(A, \<lambda>_. B)"
+ "SUM x:A. B" \<rightharpoonup> "CONST Sigma(A, \<lambda>x. B)"
+ "A * B" \<rightharpoonup> "CONST Sigma(A, \<lambda>_. B)"
print_translation \<open>
[(@{const_syntax Pi},
fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
@@ -52,28 +49,34 @@
fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
\<close>
-defs
- Subtype_def: "{x:A. P(x)} == {x. x:A \<and> P(x)}"
- Unit_def: "Unit == {x. x=one}"
- Bool_def: "Bool == {x. x=true | x=false}"
- Plus_def: "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}"
- Pi_def: "Pi(A,B) == {x. EX b. x=lam x. b(x) \<and> (ALL x:A. b(x):B(x))}"
- Sigma_def: "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}"
- Nat_def: "Nat == lfp(\<lambda>X. Unit + X)"
- List_def: "List(A) == lfp(\<lambda>X. Unit + A*X)"
+definition Nat :: "i set"
+ where "Nat == lfp(\<lambda>X. Unit + X)"
+
+definition List :: "i set \<Rightarrow> i set"
+ where "List(A) == lfp(\<lambda>X. Unit + A*X)"
+
+definition Lists :: "i set \<Rightarrow> i set"
+ where "Lists(A) == gfp(\<lambda>X. Unit + A*X)"
+
+definition ILists :: "i set \<Rightarrow> i set"
+ where "ILists(A) == gfp(\<lambda>X.{} + A*X)"
- Lists_def: "Lists(A) == gfp(\<lambda>X. Unit + A*X)"
- ILists_def: "ILists(A) == gfp(\<lambda>X.{} + A*X)"
+
+definition TAll :: "(i set \<Rightarrow> i set) \<Rightarrow> i set" (binder "TALL " 55)
+ where "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})"
- Tall_def: "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})"
- Tex_def: "TEX X. B(X) == Union({X. EX Y. X=B(Y)})"
- Lift_def: "[A] == A Un {bot}"
+definition TEx :: "(i set \<Rightarrow> i set) \<Rightarrow> i set" (binder "TEX " 55)
+ where "TEX X. B(X) == Union({X. EX Y. X=B(Y)})"
- SPLIT_def: "SPLIT(p,B) == Union({A. EX x y. p=<x,y> \<and> A=B(x,y)})"
+definition Lift :: "i set \<Rightarrow> i set" ("(3[_])")
+ where "[A] == A Un {bot}"
+
+definition SPLIT :: "[i, [i, i] \<Rightarrow> i set] \<Rightarrow> i set"
+ where "SPLIT(p,B) == Union({A. EX x y. p=<x,y> \<and> A=B(x,y)})"
lemmas simp_type_defs =
- Subtype_def Unit_def Bool_def Plus_def Sigma_def Pi_def Lift_def Tall_def Tex_def
+ Subtype_def Unit_def Bool_def Plus_def Sigma_def Pi_def Lift_def TAll_def TEx_def
and ind_type_defs = Nat_def List_def
and simp_data_defs = one_def inl_def inr_def
and ind_data_defs = zero_def succ_def nil_def cons_def
--- a/src/Doc/JEdit/JEdit.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/Doc/JEdit/JEdit.thy Tue Jan 12 20:05:53 2016 +0100
@@ -948,6 +948,29 @@
\<close>
+section \<open>Proof state output \label{sec:state-output}\<close>
+
+text \<open>
+ FIXME
+ \figref{fig:output-and-state} versus \figref{fig:output-including-state}
+
+ \begin{figure}[htb]
+ \begin{center}
+ \includegraphics[scale=0.333]{output-and-state}
+ \end{center}
+ \caption{Separate proof state display (right) and other output (bottom).}
+ \label{fig:output-and-state}
+ \end{figure}
+
+ \begin{figure}[htb]
+ \begin{center}
+ \includegraphics[scale=0.333]{output-including-state}
+ \end{center}
+ \caption{Proof state display within the regular output panel}
+ \label{fig:output-including-state}
+ \end{figure}
+\<close>
+
section \<open>Query \label{sec:query}\<close>
text \<open>
@@ -967,7 +990,7 @@
\begin{center}
\includegraphics[scale=0.333]{query}
\end{center}
- \caption{An instance of the Query panel}
+ \caption{An instance of the Query panel: find theorems}
\label{fig:query}
\end{figure}
@@ -1655,6 +1678,22 @@
\<close>
+section \<open>Markdown structure\<close>
+
+text \<open>
+ FIXME
+ \figref{fig:markdown-document}
+
+ \begin{figure}[htb]
+ \begin{center}
+ \includegraphics[scale=0.333]{markdown-document}
+ \end{center}
+ \caption{Markdown structure within document text}
+ \label{fig:markdown-document}
+ \end{figure}
+\<close>
+
+
section \<open>Citations and Bib{\TeX} entries\<close>
text \<open>
@@ -1694,6 +1733,22 @@
\<close>
+chapter \<open>ML debugger\<close>
+
+text \<open>
+ FIXME
+ \figref{fig:ml-debugger}
+
+ \begin{figure}[htb]
+ \begin{center}
+ \includegraphics[scale=0.333]{ml-debugger}
+ \end{center}
+ \caption{ML debugger}
+ \label{fig:ml-debugger}
+ \end{figure}
+\<close>
+
+
chapter \<open>Miscellaneous tools\<close>
section \<open>Timing\<close>
Binary file src/Doc/JEdit/document/auto-tools.png has changed
Binary file src/Doc/JEdit/document/bibtex-mode.png has changed
Binary file src/Doc/JEdit/document/cite-completion.png has changed
Binary file src/Doc/JEdit/document/isabelle-jedit-hdpi.png has changed
Binary file src/Doc/JEdit/document/isabelle-jedit.png has changed
Binary file src/Doc/JEdit/document/markdown-document.png has changed
Binary file src/Doc/JEdit/document/ml-debugger.png has changed
Binary file src/Doc/JEdit/document/output-and-state.png has changed
Binary file src/Doc/JEdit/document/output-including-state.png has changed
Binary file src/Doc/JEdit/document/output.png has changed
Binary file src/Doc/JEdit/document/popup1.png has changed
Binary file src/Doc/JEdit/document/popup2.png has changed
Binary file src/Doc/JEdit/document/query.png has changed
Binary file src/Doc/JEdit/document/sidekick-document.png has changed
Binary file src/Doc/JEdit/document/sidekick.png has changed
Binary file src/Doc/JEdit/document/sledgehammer.png has changed
Binary file src/Doc/JEdit/document/theories.png has changed
--- a/src/Doc/ROOT Tue Jan 12 16:59:32 2016 +0100
+++ b/src/Doc/ROOT Tue Jan 12 20:05:53 2016 +0100
@@ -207,15 +207,19 @@
"bibtex-mode.png"
"build"
"cite-completion.png"
+ "isabelle-jedit-hdpi.png"
"isabelle-jedit.png"
- "isabelle-jedit-hdpi.png"
+ "markdown-document.png"
+ "ml-debugger.png"
+ "output-and-state.png"
+ "output-including-state.png"
"output.png"
- "query.png"
"popup1.png"
"popup2.png"
+ "query.png"
"root.tex"
+ "sidekick-document.png"
"sidekick.png"
- "sidekick-document.png"
"sledgehammer.png"
"theories.png"
--- a/src/FOLP/IFOLP.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/FOLP/IFOLP.thy Tue Jan 12 20:05:53 2016 +0100
@@ -28,15 +28,12 @@
eq :: "['a,'a] => o" (infixl "=" 50)
True :: "o"
False :: "o"
- Not :: "o => o" ("~ _" [40] 40)
conj :: "[o,o] => o" (infixr "&" 35)
disj :: "[o,o] => o" (infixr "|" 30)
imp :: "[o,o] => o" (infixr "-->" 25)
- iff :: "[o,o] => o" (infixr "<->" 25)
(*Quantifiers*)
All :: "('a => o) => o" (binder "ALL " 10)
Ex :: "('a => o) => o" (binder "EX " 10)
- Ex1 :: "('a => o) => o" (binder "EX! " 10)
(*Rewriting gadgets*)
NORM :: "o => o"
norm :: "'a => 'a"
@@ -157,12 +154,15 @@
(**** Definitions ****)
-defs
-not_def: "~P == P-->False"
-iff_def: "P<->Q == (P-->Q) & (Q-->P)"
+definition Not :: "o => o" ("~ _" [40] 40)
+ where not_def: "~P == P-->False"
+
+definition iff :: "[o,o] => o" (infixr "<->" 25)
+ where "P<->Q == (P-->Q) & (Q-->P)"
(*Unique existence*)
-ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
+definition Ex1 :: "('a => o) => o" (binder "EX! " 10)
+ where ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
(*Rewriting -- special constants to flag normalized terms and formulae*)
axiomatization where
--- a/src/HOL/Auth/All_Symmetric.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/Auth/All_Symmetric.thy Tue Jan 12 20:05:53 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 Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/Bali/Example.thy Tue Jan 12 20:05:53 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/HOL.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/HOL.thy Tue Jan 12 20:05:53 2016 +0100
@@ -69,25 +69,38 @@
typedecl bool
-judgment
- Trueprop :: "bool \<Rightarrow> prop" ("(_)" 5)
+judgment Trueprop :: "bool \<Rightarrow> prop" ("(_)" 5)
+
+axiomatization implies :: "[bool, bool] \<Rightarrow> bool" (infixr "\<longrightarrow>" 25)
+ and eq :: "['a, 'a] \<Rightarrow> bool" (infixl "=" 50)
+ and The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
+
-axiomatization
- implies :: "[bool, bool] \<Rightarrow> bool" (infixr "\<longrightarrow>" 25) and
- eq :: "['a, 'a] \<Rightarrow> bool" (infixl "=" 50) and
- The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
+subsubsection \<open>Defined connectives and quantifiers\<close>
+
+definition True :: bool
+ where "True \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))"
+
+definition All :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<forall>" 10)
+ where "All P \<equiv> (P = (\<lambda>x. True))"
-consts
- True :: bool
- False :: bool
- Not :: "bool \<Rightarrow> bool" ("\<not> _" [40] 40)
+definition Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<exists>" 10)
+ where "Ex P \<equiv> \<forall>Q. (\<forall>x. P x \<longrightarrow> Q) \<longrightarrow> Q"
+
+definition False :: bool
+ where "False \<equiv> (\<forall>P. P)"
+
+definition Not :: "bool \<Rightarrow> bool" ("\<not> _" [40] 40)
+ where not_def: "\<not> P \<equiv> P \<longrightarrow> False"
- conj :: "[bool, bool] \<Rightarrow> bool" (infixr "\<and>" 35)
- disj :: "[bool, bool] \<Rightarrow> bool" (infixr "\<or>" 30)
+definition conj :: "[bool, bool] \<Rightarrow> bool" (infixr "\<and>" 35)
+ where and_def: "P \<and> Q \<equiv> \<forall>R. (P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> R"
- All :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<forall>" 10)
- Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<exists>" 10)
- Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<exists>!" 10)
+definition disj :: "[bool, bool] \<Rightarrow> bool" (infixr "\<or>" 30)
+ where or_def: "P \<or> Q \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R"
+
+definition Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<exists>!" 10)
+ where "Ex1 P \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)"
subsubsection \<open>Additional concrete syntax\<close>
@@ -167,16 +180,6 @@
iff: "(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)" and
True_or_False: "(P = True) \<or> (P = False)"
-defs
- True_def: "True \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))"
- All_def: "All P \<equiv> (P = (\<lambda>x. True))"
- Ex_def: "Ex P \<equiv> \<forall>Q. (\<forall>x. P x \<longrightarrow> Q) \<longrightarrow> Q"
- False_def: "False \<equiv> (\<forall>P. P)"
- not_def: "\<not> P \<equiv> P \<longrightarrow> False"
- and_def: "P \<and> Q \<equiv> \<forall>R. (P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> R"
- or_def: "P \<or> Q \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R"
- Ex1_def: "Ex1 P \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)"
-
definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10)
where "If P x y \<equiv> (THE z::'a. (P = True \<longrightarrow> z = x) \<and> (P = False \<longrightarrow> z = y))"
--- a/src/HOL/IMPP/EvenOdd.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/IMPP/EvenOdd.thy Tue Jan 12 20:05:53 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 Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/IMPP/Misc.thy Tue Jan 12 20:05:53 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 Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/IOA/Asig.thy Tue Jan 12 20:05:53 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 Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/IOA/IOA.thy Tue Jan 12 20:05:53 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 Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/Library/Old_Datatype.thy Tue Jan 12 20:05:53 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 Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy Tue Jan 12 20:05:53 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 Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/MicroJava/J/Example.thy Tue Jan 12 20:05:53 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 Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy Tue Jan 12 20:05:53 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 Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy Tue Jan 12 20:05:53 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 Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Jan 12 20:05:53 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 Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/Nominal/Nominal.thy Tue Jan 12 20:05:53 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/Action.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Action.thy Tue Jan 12 20:05:53 2016 +0100
@@ -9,25 +9,19 @@
imports Stfun
begin
-
-(** abstract syntax **)
-
-type_synonym 'a trfun = "(state * state) \<Rightarrow> 'a"
-type_synonym action = "bool trfun"
+type_synonym 'a trfun = "state \<times> state \<Rightarrow> 'a"
+type_synonym action = "bool trfun"
instance prod :: (world, world) world ..
-consts
- (** abstract syntax **)
- before :: "'a stfun \<Rightarrow> 'a trfun"
- after :: "'a stfun \<Rightarrow> 'a trfun"
- unch :: "'a stfun \<Rightarrow> action"
+definition enabled :: "action \<Rightarrow> stpred"
+ where "enabled A s \<equiv> \<exists>u. (s,u) \<Turnstile> A"
+
- SqAct :: "[action, 'a stfun] \<Rightarrow> action"
- AnAct :: "[action, 'a stfun] \<Rightarrow> action"
- enabled :: "action \<Rightarrow> stpred"
-
-(** concrete syntax **)
+consts
+ before :: "'a stfun \<Rightarrow> 'a trfun"
+ after :: "'a stfun \<Rightarrow> 'a trfun"
+ unch :: "'a stfun \<Rightarrow> action"
syntax
(* Syntax for writing action expressions in arbitrary contexts *)
@@ -40,8 +34,6 @@
(*** Priming: same as "after" ***)
"_prime" :: "lift \<Rightarrow> lift" ("(_`)" [100] 99)
- "_SqAct" :: "[lift, lift] \<Rightarrow> lift" ("([_]'_(_))" [0,1000] 99)
- "_AnAct" :: "[lift, lift] \<Rightarrow> lift" ("(<_>'_(_))" [0,1000] 99)
"_Enabled" :: "lift \<Rightarrow> lift" ("(Enabled _)" [100] 100)
translations
@@ -50,25 +42,30 @@
"_after" == "CONST after"
"_prime" => "_after"
"_unchanged" == "CONST unch"
- "_SqAct" == "CONST SqAct"
- "_AnAct" == "CONST AnAct"
"_Enabled" == "CONST enabled"
- "w \<Turnstile> [A]_v" <= "_SqAct A v w"
- "w \<Turnstile> <A>_v" <= "_AnAct A v w"
"s \<Turnstile> Enabled A" <= "_Enabled A s"
"w \<Turnstile> unchanged f" <= "_unchanged f w"
axiomatization where
unl_before: "(ACT $v) (s,t) \<equiv> v s" and
unl_after: "(ACT v$) (s,t) \<equiv> v t" and
-
unchanged_def: "(s,t) \<Turnstile> unchanged v \<equiv> (v t = v s)"
-defs
- square_def: "ACT [A]_v \<equiv> ACT (A \<or> unchanged v)"
- angle_def: "ACT <A>_v \<equiv> ACT (A \<and> \<not> unchanged v)"
+
+definition SqAct :: "[action, 'a stfun] \<Rightarrow> action"
+ where square_def: "SqAct A v \<equiv> ACT (A \<or> unchanged v)"
+
+definition AnAct :: "[action, 'a stfun] \<Rightarrow> action"
+ where angle_def: "AnAct A v \<equiv> ACT (A \<and> \<not> unchanged v)"
- enabled_def: "s \<Turnstile> Enabled A \<equiv> \<exists>u. (s,u) \<Turnstile> A"
+syntax
+ "_SqAct" :: "[lift, lift] \<Rightarrow> lift" ("([_]'_(_))" [0, 1000] 99)
+ "_AnAct" :: "[lift, lift] \<Rightarrow> lift" ("(<_>'_(_))" [0, 1000] 99)
+translations
+ "_SqAct" == "CONST SqAct"
+ "_AnAct" == "CONST AnAct"
+ "w \<Turnstile> [A]_v" \<leftharpoondown> "_SqAct A v w"
+ "w \<Turnstile> <A>_v" \<leftharpoondown> "_AnAct A v w"
(* The following assertion specializes "intI" for any world type
--- a/src/HOL/TLA/Buffer/Buffer.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Buffer/Buffer.thy Tue Jan 12 20:05:53 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 Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Init.thy Tue Jan 12 20:05:53 2016 +0100
@@ -16,29 +16,33 @@
type_synonym temporal = "behavior form"
-
consts
- Initial :: "('w::world \<Rightarrow> bool) \<Rightarrow> temporal"
first_world :: "behavior \<Rightarrow> ('w::world)"
st1 :: "behavior \<Rightarrow> state"
st2 :: "behavior \<Rightarrow> state"
+definition Initial :: "('w::world \<Rightarrow> bool) \<Rightarrow> temporal"
+ where Init_def: "Initial F sigma = F (first_world sigma)"
+
syntax
"_TEMP" :: "lift \<Rightarrow> 'a" ("(TEMP _)")
"_Init" :: "lift \<Rightarrow> lift" ("(Init _)"[40] 50)
-
translations
"TEMP F" => "(F::behavior \<Rightarrow> _)"
"_Init" == "CONST Initial"
"sigma \<Turnstile> Init F" <= "_Init F sigma"
-defs
- Init_def: "sigma \<Turnstile> Init F == (first_world sigma) \<Turnstile> F"
+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
-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)"
+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/Intensional.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Intensional.thy Tue Jan 12 20:05:53 2016 +0100
@@ -17,17 +17,29 @@
type_synonym ('w,'a) expr = "'w \<Rightarrow> 'a" (* intention: 'w::world, 'a::type *)
type_synonym 'w form = "('w, bool) expr"
-consts
- Valid :: "('w::world) form \<Rightarrow> bool"
- const :: "'a \<Rightarrow> ('w::world, 'a) expr"
- lift :: "['a \<Rightarrow> 'b, ('w::world, 'a) expr] \<Rightarrow> ('w,'b) expr"
- lift2 :: "['a \<Rightarrow> 'b \<Rightarrow> 'c, ('w::world,'a) expr, ('w,'b) expr] \<Rightarrow> ('w,'c) expr"
- lift3 :: "['a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] \<Rightarrow> ('w,'d) expr"
+definition Valid :: "('w::world) form \<Rightarrow> bool"
+ where "Valid A \<equiv> \<forall>w. A w"
+
+definition const :: "'a \<Rightarrow> ('w::world, 'a) expr"
+ where unl_con: "const c w \<equiv> c"
+
+definition lift :: "['a \<Rightarrow> 'b, ('w::world, 'a) expr] \<Rightarrow> ('w,'b) expr"
+ where unl_lift: "lift f x w \<equiv> f (x w)"
+
+definition lift2 :: "['a \<Rightarrow> 'b \<Rightarrow> 'c, ('w::world,'a) expr, ('w,'b) expr] \<Rightarrow> ('w,'c) expr"
+ where unl_lift2: "lift2 f x y w \<equiv> f (x w) (y w)"
- (* "Rigid" quantification (logic level) *)
- RAll :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder "Rall " 10)
- REx :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder "Rex " 10)
- REx1 :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder "Rex! " 10)
+definition lift3 :: "['a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] \<Rightarrow> ('w,'d) expr"
+ where unl_lift3: "lift3 f x y z w \<equiv> f (x w) (y w) (z w)"
+
+(* "Rigid" quantification (logic level) *)
+definition RAll :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder "Rall " 10)
+ where unl_Rall: "(Rall x. A x) w \<equiv> \<forall>x. A x w"
+definition REx :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder "Rex " 10)
+ where unl_Rex: "(Rex x. A x) w \<equiv> \<exists>x. A x w"
+definition REx1 :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder "Rex! " 10)
+ where unl_Rex1: "(Rex! x. A x) w \<equiv> \<exists>!x. A x w"
+
(** concrete syntax **)
@@ -123,8 +135,6 @@
"_liftList (_liftargs x xs)" == "_liftCons x (_liftList xs)"
"_liftList x" == "_liftCons x (_const [])"
-
-
"w \<Turnstile> \<not>A" <= "_liftNot A w"
"w \<Turnstile> A \<and> B" <= "_liftAnd A B w"
"w \<Turnstile> A \<or> B" <= "_liftOr A B w"
@@ -134,18 +144,6 @@
"w \<Turnstile> \<exists>x. A" <= "_REx x A w"
"w \<Turnstile> \<exists>!x. A" <= "_REx1 x A w"
-defs
- Valid_def: "\<turnstile> A == \<forall>w. w \<Turnstile> A"
-
- unl_con: "LIFT #c w == c"
- unl_lift: "lift f x w == f (x w)"
- unl_lift2: "LIFT f<x, y> w == f (x w) (y w)"
- unl_lift3: "LIFT f<x, y, z> w == f (x w) (y w) (z w)"
-
- unl_Rall: "w \<Turnstile> \<forall>x. A x == \<forall>x. (w \<Turnstile> A x)"
- unl_Rex: "w \<Turnstile> \<exists>x. A x == \<exists>x. (w \<Turnstile> A x)"
- unl_Rex1: "w \<Turnstile> \<exists>!x. A x == \<exists>!x. (w \<Turnstile> A x)"
-
subsection \<open>Lemmas and tactics for "intensional" logics.\<close>
--- a/src/HOL/TLA/Memory/MemClerk.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Memory/MemClerk.thy Tue Jan 12 20:05:53 2016 +0100
@@ -74,10 +74,10 @@
unanswered call for that process.
*)
lemma MClkidle: "\<turnstile> \<not>$Calling send p \<and> $(cst!p) = #clkA \<longrightarrow> \<not>MClkNext send rcv cst p"
- by (auto simp: Return_def MC_action_defs)
+ by (auto simp: AReturn_def MC_action_defs)
lemma MClkbusy: "\<turnstile> $Calling rcv p \<longrightarrow> \<not>MClkNext send rcv cst p"
- by (auto simp: Call_def MC_action_defs)
+ by (auto simp: ACall_def MC_action_defs)
(* Enabledness of actions *)
@@ -86,7 +86,7 @@
\<turnstile> Calling send p \<and> \<not>Calling rcv p \<and> cst!p = #clkA
\<longrightarrow> Enabled (MClkFwd send rcv cst p)"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
- @{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
+ @{thm ACall_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
[@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
lemma MClkFwd_ch_enabled: "\<turnstile> Enabled (MClkFwd send rcv cst p) \<longrightarrow>
@@ -103,7 +103,7 @@
apply (tactic \<open>action_simp_tac @{context}
[@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1\<close>)
apply (tactic \<open>action_simp_tac (@{context} addsimps
- [@{thm MClkReply_def}, @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}])
+ [@{thm MClkReply_def}, @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}])
[exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
done
--- a/src/HOL/TLA/Memory/Memory.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Memory/Memory.thy Tue Jan 12 20:05:53 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
@@ -165,7 +178,7 @@
*)
lemma Memoryidle: "\<turnstile> \<not>$(Calling ch p) \<longrightarrow> \<not> RNext ch mm rs p"
- by (auto simp: Return_def RM_action_defs)
+ by (auto simp: AReturn_def RM_action_defs)
(* Enabledness conditions *)
@@ -178,7 +191,7 @@
apply (tactic
\<open>action_simp_tac @{context} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1\<close>)
apply (tactic
- \<open>action_simp_tac (@{context} addsimps [@{thm MemReturn_def}, @{thm Return_def},
+ \<open>action_simp_tac (@{context} addsimps [@{thm MemReturn_def}, @{thm AReturn_def},
@{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
done
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Tue Jan 12 20:05:53 2016 +0100
@@ -320,7 +320,7 @@
(* ==================== Lemmas about the environment ============================== *)
lemma Envbusy: "\<turnstile> $(Calling memCh p) \<longrightarrow> \<not>ENext p"
- by (auto simp: ENext_def Call_def)
+ by (auto simp: ENext_def ACall_def)
(* ==================== Lemmas about the implementation's states ==================== *)
@@ -333,7 +333,7 @@
lemma S1Env: "\<turnstile> ENext p \<and> $(S1 rmhist p) \<and> unchanged (c p, r p, m p, rmhist!p)
\<longrightarrow> (S2 rmhist p)$"
- by (force simp: ENext_def Call_def c_def r_def m_def
+ by (force simp: ENext_def ACall_def c_def r_def m_def
caller_def rtrner_def MVNROKBA_def S_def S1_def S2_def Calling_def)
lemma S1ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (c p)"
@@ -352,7 +352,7 @@
\<longrightarrow> unchanged (rmhist!p)"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def},
@{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
- @{thm Return_def}]) [] [temp_use @{context} @{thm squareE}] 1\<close>)
+ @{thm AReturn_def}]) [] [temp_use @{context} @{thm squareE}] 1\<close>)
(* ------------------------------ State S2 ---------------------------------------- *)
@@ -367,7 +367,7 @@
\<and> unchanged (e p, r p, m p, rmhist!p)
\<longrightarrow> (S3 rmhist p)$"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
- @{thm Call_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
+ @{thm ACall_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
@{thm rtrner_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1\<close>)
lemma S2RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (r p)"
@@ -380,7 +380,7 @@
\<longrightarrow> unchanged (rmhist!p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
- MClkReply_def Return_def S_def S2_def)
+ MClkReply_def AReturn_def S_def S2_def)
(* ------------------------------ State S3 ---------------------------------------- *)
@@ -405,7 +405,7 @@
\<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFwd_def},
@{thm HNext_def}, @{thm MemReturn_def}, @{thm RPCFail_def},
- @{thm MClkReply_def}, @{thm Return_def}, @{thm Call_def}, @{thm e_def},
+ @{thm MClkReply_def}, @{thm AReturn_def}, @{thm ACall_def}, @{thm e_def},
@{thm c_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
@{thm S3_def}, @{thm S4_def}, @{thm Calling_def}]) [] [] 1\<close>)
@@ -413,7 +413,7 @@
\<and> unchanged (e p, c p, m p)
\<longrightarrow> (S6 rmhist p)$"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
- @{thm RPCFail_def}, @{thm Return_def}, @{thm e_def}, @{thm c_def},
+ @{thm RPCFail_def}, @{thm AReturn_def}, @{thm e_def}, @{thm c_def},
@{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm MVOKBARF_def},
@{thm S_def}, @{thm S3_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
@@ -422,7 +422,7 @@
lemma S3Hist: "\<turnstile> HNext rmhist p \<and> $(S3 rmhist p) \<and> unchanged (r p) \<longrightarrow> unchanged (rmhist!p)"
by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
- Return_def r_def rtrner_def S_def S3_def Calling_def)
+ AReturn_def r_def rtrner_def S_def S3_def Calling_def)
(* ------------------------------ State S4 ---------------------------------------- *)
@@ -441,7 +441,7 @@
\<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ReadInner_def},
@{thm GoodRead_def}, @{thm BadRead_def}, @{thm HNext_def}, @{thm MemReturn_def},
- @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
+ @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm AReturn_def}, @{thm e_def},
@{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def},
@{thm MVNROKBA_def}, @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def},
@{thm Calling_def}, @{thm MemInv_def}]) [] [] 1\<close>)
@@ -455,7 +455,7 @@
\<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm WriteInner_def},
@{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm HNext_def}, @{thm MemReturn_def},
- @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
+ @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm AReturn_def}, @{thm e_def},
@{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, @{thm MVNROKBA_def},
@{thm S_def}, @{thm S4_def}, @{thm WrRequest_def}, @{thm Calling_def}]) [] [] 1\<close>)
@@ -471,12 +471,12 @@
lemma S4Return: "\<turnstile> MemReturn rmCh ires p \<and> $S4 rmhist p \<and> unchanged (e p, c p, r p)
\<and> HNext rmhist p
\<longrightarrow> (S5 rmhist p)$"
- by (auto simp: HNext_def MemReturn_def Return_def e_def c_def r_def
+ by (auto simp: HNext_def MemReturn_def AReturn_def e_def c_def r_def
rtrner_def caller_def MVNROKBA_def MVOKBA_def S_def S4_def S5_def Calling_def)
lemma S4Hist: "\<turnstile> HNext rmhist p \<and> $S4 rmhist p \<and> (m p)$ = $(m p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
- Return_def m_def rtrner_def S_def S4_def Calling_def)
+ AReturn_def m_def rtrner_def S_def S4_def Calling_def)
(* ------------------------------ State S5 ---------------------------------------- *)
@@ -493,14 +493,14 @@
lemma S5Reply: "\<turnstile> RPCReply crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
\<longrightarrow> (S6 rmhist p)$"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
- @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
+ @{thm AReturn_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
@{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
@{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
lemma S5Fail: "\<turnstile> RPCFail crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
\<longrightarrow> (S6 rmhist p)$"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
- @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
+ @{thm AReturn_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
@{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def},
@{thm S_def}, @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
@@ -511,7 +511,7 @@
\<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
- MClkReply_def Return_def S_def S5_def)
+ MClkReply_def AReturn_def S_def S5_def)
(* ------------------------------ State S6 ---------------------------------------- *)
@@ -526,7 +526,7 @@
\<and> unchanged (e p,r p,m p)
\<longrightarrow> (S3 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
- @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm Call_def}, @{thm Return_def},
+ @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm ACall_def}, @{thm AReturn_def},
@{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
@{thm S_def}, @{thm S6_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1\<close>)
@@ -534,7 +534,7 @@
\<and> unchanged (e p,r p,m p)
\<longrightarrow> (S1 rmhist p)$"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
- @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm Return_def}, @{thm MClkReply_def},
+ @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm AReturn_def}, @{thm MClkReply_def},
@{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
@{thm S_def}, @{thm S6_def}, @{thm S1_def}, @{thm Calling_def}]) [] [] 1\<close>)
@@ -545,7 +545,7 @@
by (auto simp: S_def S6_def dest!: Memoryidle [temp_use])
lemma S6Hist: "\<turnstile> HNext rmhist p \<and> $S6 rmhist p \<and> (c p)$ = $(c p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
- by (auto simp: HNext_def MClkReply_def Return_def c_def rtrner_def S_def S6_def Calling_def)
+ by (auto simp: HNext_def MClkReply_def AReturn_def c_def rtrner_def S_def S6_def Calling_def)
section "Correctness of predicate-action diagram"
@@ -676,7 +676,7 @@
apply (drule S6_excl [temp_use])
apply (auto simp: RPCFail_def MemFail_def e_def c_def m_def resbar_def)
apply (force simp: S3_def S_def)
- apply (auto simp: Return_def)
+ apply (auto simp: AReturn_def)
done
lemma Step1_4_4a1: "\<turnstile> $S4 rmhist p \<and> (S4 rmhist p)$ \<and> ReadInner rmCh mm ires p l
@@ -724,7 +724,7 @@
@{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1\<close>)
apply (drule S4_excl [temp_use] S5_excl [temp_use])+
using [[fast_solver]]
- apply (auto elim!: squareE [temp_use] simp: MemReturn_def Return_def)
+ apply (auto elim!: squareE [temp_use] simp: MemReturn_def AReturn_def)
done
lemma Step1_4_5a: "\<turnstile> RPCReply crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$
@@ -733,7 +733,7 @@
apply clarsimp
apply (drule S5_excl [temp_use] S6_excl [temp_use])+
apply (auto simp: e_def c_def m_def resbar_def)
- apply (auto simp: RPCReply_def Return_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
+ apply (auto simp: RPCReply_def AReturn_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
done
lemma Step1_4_5b: "\<turnstile> RPCFail crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$
@@ -741,7 +741,7 @@
\<longrightarrow> MemFail memCh (resbar rmhist) p"
apply clarsimp
apply (drule S6_excl [temp_use])
- apply (auto simp: e_def c_def m_def RPCFail_def Return_def MemFail_def resbar_def)
+ apply (auto simp: e_def c_def m_def RPCFail_def AReturn_def MemFail_def resbar_def)
apply (auto simp: S5_def S_def)
done
@@ -752,7 +752,7 @@
apply (drule S6_excl [temp_use])+
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm e_def},
@{thm r_def}, @{thm m_def}, @{thm MClkReply_def}, @{thm MemReturn_def},
- @{thm Return_def}, @{thm resbar_def}]) [] [] 1\<close>)
+ @{thm AReturn_def}, @{thm resbar_def}]) [] [] 1\<close>)
apply simp_all (* simplify if-then-else *)
apply (tactic \<open>ALLGOALS (action_simp_tac (@{context} addsimps
[@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}])\<close>)
@@ -909,7 +909,7 @@
lemma S1_Returndisabled: "\<turnstile> S1 rmhist p \<longrightarrow>
\<not>Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm angle_def}, @{thm MemReturn_def},
- @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1\<close>)
+ @{thm AReturn_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1\<close>)
lemma RNext_fair: "\<turnstile> \<box>\<diamond>S1 rmhist p
\<longrightarrow> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
@@ -1088,7 +1088,7 @@
lemma MClkReplyS6:
"\<turnstile> $ImpInv rmhist p \<and> <MClkReply memCh crCh cst p>_(c p) \<longrightarrow> $S6 rmhist p"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm angle_def},
- @{thm MClkReply_def}, @{thm Return_def}, @{thm ImpInv_def}, @{thm S_def},
+ @{thm MClkReply_def}, @{thm AReturn_def}, @{thm ImpInv_def}, @{thm S_def},
@{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1\<close>)
lemma S6MClkReply_enabled: "\<turnstile> S6 rmhist p \<longrightarrow> Enabled (<MClkReply memCh crCh cst p>_(c p))"
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy Tue Jan 12 20:05:53 2016 +0100
@@ -16,76 +16,90 @@
*)
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 *)
- slice :: "('a \<Rightarrow> 'b) stfun \<Rightarrow> 'a \<Rightarrow> 'b stfun"
+definition slice :: "('a \<Rightarrow> 'b) stfun \<Rightarrow> 'a \<Rightarrow> 'b stfun"
+ where "slice x i s \<equiv> x s i"
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)
-
+ "_slice" :: "[lift, 'a] \<Rightarrow> lift" ("(_!_)" [70,70] 70)
translations
- "_slice" == "CONST slice"
+ "_slice" \<rightleftharpoons> "CONST slice"
+
+
+(* state predicates *)
+
+definition Calling :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> stpred"
+ where "Calling ch p == PRED cbit< ch!p > \<noteq> rbit< ch!p >"
- "_Call" == "CONST ACall"
- "_Return" == "CONST AReturn"
+
+(* actions *)
-defs
- slice_def: "(PRED (x!i)) s == x s i"
+definition ACall :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
+ where "ACall ch p v \<equiv> ACT
+ \<not> $Calling ch p
+ \<and> (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
+ \<and> (arg<ch!p>$ = $v)"
- 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))"
+definition AReturn :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
+ where "AReturn ch p v == ACT
+ $Calling ch p
+ \<and> (rbit<ch!p>$ = $cbit<ch!p>)
+ \<and> (res<ch!p>$ = $v)"
+
+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" \<rightleftharpoons> "CONST ACall"
+ "_Return" \<rightleftharpoons> "CONST AReturn"
+
- Calling_def: "Calling ch p == PRED cbit< ch!p > \<noteq> rbit< ch!p >"
- 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]
-lemmas Procedure_defs = caller_def rtrner_def Calling_def Call_def Return_def
+lemmas Procedure_defs = caller_def rtrner_def Calling_def ACall_def AReturn_def
PLegalCaller_def LegalCaller_def PLegalReturner_def LegalReturner_def
(* Calls and returns change their subchannel *)
lemma Call_changed: "\<turnstile> Call ch p v \<longrightarrow> <Call ch p v>_((caller ch)!p)"
- by (auto simp: angle_def Call_def caller_def Calling_def)
+ by (auto simp: angle_def ACall_def caller_def Calling_def)
lemma Return_changed: "\<turnstile> Return ch p v \<longrightarrow> <Return ch p v>_((rtrner ch)!p)"
- by (auto simp: angle_def Return_def rtrner_def Calling_def)
+ by (auto simp: angle_def AReturn_def rtrner_def Calling_def)
end
--- a/src/HOL/TLA/Memory/RPC.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Memory/RPC.thy Tue Jan 12 20:05:53 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 =
@@ -82,7 +83,7 @@
*)
lemma RPCidle: "\<turnstile> \<not>$(Calling send p) \<longrightarrow> \<not>RPCNext send rcv rst p"
- by (auto simp: Return_def RPC_action_defs)
+ by (auto simp: AReturn_def RPC_action_defs)
lemma RPCbusy: "\<turnstile> $(Calling rcv p) \<and> $(rst!p) = #rpcB \<longrightarrow> \<not>RPCNext send rcv rst p"
by (auto simp: RPC_action_defs)
@@ -100,14 +101,14 @@
lemma RPCFail_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>
\<turnstile> \<not>Calling rcv p \<and> Calling send p \<longrightarrow> Enabled (RPCFail send rcv rst p)"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
- @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
+ @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
[@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
lemma RPCReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>
\<turnstile> \<not>Calling rcv p \<and> Calling send p \<and> rst!p = #rpcB
\<longrightarrow> Enabled (RPCReply send rcv rst p)"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
- @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
+ @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
[@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
end
--- a/src/HOL/TLA/Memory/RPCParameters.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Memory/RPCParameters.thy Tue Jan 12 20:05:53 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 Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/TLA/Stfun.thy Tue Jan 12 20:05:53 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/Refute_Examples.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/HOL/ex/Refute_Examples.thy Tue Jan 12 20:05:53 2016 +0100
@@ -894,10 +894,20 @@
consts inverse :: "'a \<Rightarrow> 'a"
-defs (overloaded)
- inverse_bool: "inverse (b::bool) == ~ b"
- inverse_set : "inverse (S::'a set) == -S"
- inverse_pair: "inverse p == (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"
refute [expect = genuine]
--- a/src/Pure/Thy/document_antiquotations.ML Tue Jan 12 16:59:32 2016 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Tue Jan 12 20:05:53 2016 +0100
@@ -7,6 +7,27 @@
structure Document_Antiquotations: sig end =
struct
+(* Markdown errors *)
+
+local
+
+fun markdown_error binding =
+ Thy_Output.antiquotation binding (Scan.succeed ())
+ (fn {source, ...} => fn _ =>
+ error ("Bad Markdown structure: illegal " ^ quote (Binding.name_of binding) ^
+ Position.here (Position.reset_range (#1 (Token.range_of source)))))
+
+in
+
+val _ =
+ Theory.setup
+ (markdown_error @{binding item} #>
+ markdown_error @{binding enum} #>
+ markdown_error @{binding descr});
+
+end;
+
+
(* control spacing *)
val _ =
--- a/src/Sequents/ILL.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/Sequents/ILL.thy Tue Jan 12 20:05:53 2016 +0100
@@ -12,14 +12,12 @@
tens :: "[o, o] \<Rightarrow> o" (infixr "><" 35)
limp :: "[o, o] \<Rightarrow> o" (infixr "-o" 45)
- liff :: "[o, o] \<Rightarrow> o" (infixr "o-o" 45)
FShriek :: "o \<Rightarrow> o" ("! _" [100] 1000)
lconj :: "[o, o] \<Rightarrow> o" (infixr "&&" 35)
ldisj :: "[o, o] \<Rightarrow> o" (infixr "++" 35)
zero :: "o" ("0")
top :: "o" ("1")
eye :: "o" ("I")
- aneg :: "o\<Rightarrow>o" ("~_")
(* context manipulation *)
@@ -47,11 +45,11 @@
(@{const_syntax PromAux}, K (three_seq_tr' @{syntax_const "_PromAux"}))]
\<close>
-defs
+definition liff :: "[o, o] \<Rightarrow> o" (infixr "o-o" 45)
+ where "P o-o Q == (P -o Q) >< (Q -o P)"
-liff_def: "P o-o Q == (P -o Q) >< (Q -o P)"
-
-aneg_def: "~A == A -o 0"
+definition aneg :: "o\<Rightarrow>o" ("~_")
+ where "~A == A -o 0"
axiomatization where
--- a/src/Sequents/Modal0.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/Sequents/Modal0.thy Tue Jan 12 20:05:53 2016 +0100
@@ -12,8 +12,6 @@
consts
box :: "o\<Rightarrow>o" ("[]_" [50] 50)
dia :: "o\<Rightarrow>o" ("<>_" [50] 50)
- strimp :: "[o,o]\<Rightarrow>o" (infixr "--<" 25)
- streqv :: "[o,o]\<Rightarrow>o" (infixr ">-<" 25)
Lstar :: "two_seqi"
Rstar :: "two_seqi"
@@ -36,9 +34,11 @@
(@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))]
\<close>
-defs
- strimp_def: "P --< Q == [](P \<longrightarrow> Q)"
- streqv_def: "P >-< Q == (P --< Q) \<and> (Q --< P)"
+definition strimp :: "[o,o]\<Rightarrow>o" (infixr "--<" 25)
+ where "P --< Q == [](P \<longrightarrow> Q)"
+
+definition streqv :: "[o,o]\<Rightarrow>o" (infixr ">-<" 25)
+ where "P >-< Q == (P --< Q) \<and> (Q --< P)"
lemmas rewrite_rls = strimp_def streqv_def
--- a/src/ZF/ZF.thy Tue Jan 12 16:59:32 2016 +0100
+++ b/src/ZF/ZF.thy Tue Jan 12 20:05:53 2016 +0100
@@ -3,147 +3,262 @@
Copyright 1993 University of Cambridge
*)
-section\<open>Zermelo-Fraenkel Set Theory\<close>
+section \<open>Zermelo-Fraenkel Set Theory\<close>
theory ZF
imports "~~/src/FOL/FOL"
begin
+subsection \<open>Signature\<close>
+
declare [[eta_contract = false]]
typedecl i
instance i :: "term" ..
-axiomatization
- zero :: "i" ("0") \<comment>\<open>the empty set\<close> and
- Pow :: "i => i" \<comment>\<open>power sets\<close> and
- Inf :: "i" \<comment>\<open>infinite set\<close>
+axiomatization mem :: "[i, i] \<Rightarrow> o" (infixl "\<in>" 50) \<comment> \<open>membership relation\<close>
+ and zero :: "i" ("0") \<comment> \<open>the empty set\<close>
+ and Pow :: "i \<Rightarrow> i" \<comment> \<open>power sets\<close>
+ and Inf :: "i" \<comment> \<open>infinite set\<close>
+ and Union :: "i \<Rightarrow> i" ("\<Union>_" [90] 90)
+ and PrimReplace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
+
+abbreviation not_mem :: "[i, i] \<Rightarrow> o" (infixl "\<notin>" 50) \<comment> \<open>negated membership relation\<close>
+ where "x \<notin> y \<equiv> \<not> (x \<in> y)"
+
+
+subsection \<open>Bounded Quantifiers\<close>
+
+definition Ball :: "[i, i \<Rightarrow> o] \<Rightarrow> o"
+ where "Ball(A, P) \<equiv> \<forall>x. x\<in>A \<longrightarrow> P(x)"
-text \<open>Bounded Quantifiers\<close>
-consts
- Ball :: "[i, i => o] => o"
- Bex :: "[i, i => o] => o"
+definition Bex :: "[i, i \<Rightarrow> o] \<Rightarrow> o"
+ where "Bex(A, P) \<equiv> \<exists>x. x\<in>A \<and> P(x)"
-text \<open>General Union and Intersection\<close>
-axiomatization Union :: "i => i" ("\<Union>_" [90] 90)
-consts Inter :: "i => i" ("\<Inter>_" [90] 90)
+syntax
+ "_Ball" :: "[pttrn, i, o] \<Rightarrow> o" ("(3\<forall>_\<in>_./ _)" 10)
+ "_Bex" :: "[pttrn, i, o] \<Rightarrow> o" ("(3\<exists>_\<in>_./ _)" 10)
+translations
+ "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball(A, \<lambda>x. P)"
+ "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex(A, \<lambda>x. P)"
+
+
+subsection \<open>Variations on Replacement\<close>
+
+(* Derived form of replacement, restricting P to its functional part.
+ The resulting set (for functional P) is the same as with
+ PrimReplace, but the rules are simpler. *)
+definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
+ where "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))"
-text \<open>Variations on Replacement\<close>
-axiomatization PrimReplace :: "[i, [i, i] => o] => i"
-consts
- Replace :: "[i, [i, i] => o] => i"
- RepFun :: "[i, i => i] => i"
- Collect :: "[i, i => o] => i"
+syntax
+ "_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
+translations
+ "{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"
+
+
+(* Functional form of replacement -- analgous to ML's map functional *)
+
+definition RepFun :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
+ where "RepFun(A,f) == {y . x\<in>A, y=f(x)}"
+
+syntax
+ "_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \<in> _})" [51,0,51])
+translations
+ "{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)"
+
-text\<open>Definite descriptions -- via Replace over the set "1"\<close>
-consts
- The :: "(i => o) => i" (binder "THE " 10)
- If :: "[o, i, i] => i" ("(if (_)/ then (_)/ else (_))" [10] 10)
+(* Separation and Pairing can be derived from the Replacement
+ and Powerset Axioms using the following definitions. *)
+definition Collect :: "[i, i \<Rightarrow> o] \<Rightarrow> i"
+ where "Collect(A,P) == {y . x\<in>A, x=y & P(x)}"
+
+syntax
+ "_Collect" :: "[pttrn, i, o] \<Rightarrow> i" ("(1{_ \<in> _ ./ _})")
+translations
+ "{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"
+
-abbreviation (input)
- old_if :: "[o, i, i] => i" ("if '(_,_,_')") where
- "if(P,a,b) == If(P,a,b)"
+subsection \<open>General union and intersection\<close>
+
+definition Inter :: "i => i" ("\<Inter>_" [90] 90)
+ where "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}"
+
+syntax
+ "_UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10)
+ "_INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10)
+translations
+ "\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})"
+ "\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})"
-text \<open>Finite Sets\<close>
-consts
- Upair :: "[i, i] => i"
- cons :: "[i, i] => i"
- succ :: "i => i"
+subsection \<open>Finite sets and binary operations\<close>
+
+(*Unordered pairs (Upair) express binary union/intersection and cons;
+ set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)
+
+definition Upair :: "[i, i] => i"
+ where "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
-text \<open>Ordered Pairing\<close>
-consts
- Pair :: "[i, i] => i"
- fst :: "i => i"
- snd :: "i => i"
- split :: "[[i, i] => 'a, i] => 'a::{}" \<comment>\<open>for pattern-matching\<close>
+definition Subset :: "[i, i] \<Rightarrow> o" (infixl "\<subseteq>" 50) \<comment> \<open>subset relation\<close>
+ where subset_def: "A \<subseteq> B \<equiv> \<forall>x\<in>A. x\<in>B"
+
+definition Diff :: "[i, i] \<Rightarrow> i" (infixl "-" 65) \<comment> \<open>set difference\<close>
+ where "A - B == { x\<in>A . ~(x\<in>B) }"
-text \<open>Sigma and Pi Operators\<close>
-consts
- Sigma :: "[i, i => i] => i"
- Pi :: "[i, i => i] => i"
+definition Un :: "[i, i] \<Rightarrow> i" (infixl "\<union>" 65) \<comment> \<open>binary union\<close>
+ where "A \<union> B == \<Union>(Upair(A,B))"
+
+definition Int :: "[i, i] \<Rightarrow> i" (infixl "\<inter>" 70) \<comment> \<open>binary intersection\<close>
+ where "A \<inter> B == \<Inter>(Upair(A,B))"
-text \<open>Relations and Functions\<close>
-consts
- "domain" :: "i => i"
- range :: "i => i"
- field :: "i => i"
- converse :: "i => i"
- relation :: "i => o" \<comment>\<open>recognizes sets of pairs\<close>
- "function" :: "i => o" \<comment>\<open>recognizes functions; can have non-pairs\<close>
- Lambda :: "[i, i => i] => i"
- restrict :: "[i, i] => i"
+definition cons :: "[i, i] => i"
+ where "cons(a,A) == Upair(a,a) \<union> A"
+
+definition succ :: "i => i"
+ where "succ(i) == cons(i, i)"
-text \<open>Infixes in order of decreasing precedence\<close>
-consts
- Image :: "[i, i] => i" (infixl "``" 90) \<comment>\<open>image\<close>
- vimage :: "[i, i] => i" (infixl "-``" 90) \<comment>\<open>inverse image\<close>
- "apply" :: "[i, i] => i" (infixl "`" 90) \<comment>\<open>function application\<close>
- "Int" :: "[i, i] => i" (infixl "\<inter>" 70) \<comment>\<open>binary intersection\<close>
- "Un" :: "[i, i] => i" (infixl "\<union>" 65) \<comment>\<open>binary union\<close>
- Diff :: "[i, i] => i" (infixl "-" 65) \<comment>\<open>set difference\<close>
- Subset :: "[i, i] => o" (infixl "\<subseteq>" 50) \<comment>\<open>subset relation\<close>
+nonterminal "is"
+syntax
+ "" :: "i \<Rightarrow> is" ("_")
+ "_Enum" :: "[i, is] \<Rightarrow> is" ("_,/ _")
+ "_Finset" :: "is \<Rightarrow> i" ("{(_)}")
+translations
+ "{x, xs}" == "CONST cons(x, {xs})"
+ "{x}" == "CONST cons(x, 0)"
+
+
+subsection \<open>Axioms\<close>
+
+(* ZF axioms -- see Suppes p.238
+ Axioms for Union, Pow and Replace state existence only,
+ uniqueness is derivable using extensionality. *)
axiomatization
- mem :: "[i, i] => o" (infixl "\<in>" 50) \<comment>\<open>membership relation\<close>
-
-abbreviation
- not_mem :: "[i, i] => o" (infixl "\<notin>" 50) \<comment>\<open>negated membership relation\<close>
- where "x \<notin> y \<equiv> \<not> (x \<in> y)"
+where
+ extension: "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" and
+ Union_iff: "A \<in> \<Union>(C) \<longleftrightarrow> (\<exists>B\<in>C. A\<in>B)" and
+ Pow_iff: "A \<in> Pow(B) \<longleftrightarrow> A \<subseteq> B" and
-abbreviation
- cart_prod :: "[i, i] => i" (infixr "\<times>" 80) \<comment>\<open>Cartesian product\<close>
- where "A \<times> B \<equiv> Sigma(A, \<lambda>_. B)"
+ (*We may name this set, though it is not uniquely defined.*)
+ infinity: "0 \<in> Inf \<and> (\<forall>y\<in>Inf. succ(y) \<in> Inf)" and
-abbreviation
- function_space :: "[i, i] => i" (infixr "->" 60) \<comment>\<open>function space\<close>
- where "A -> B \<equiv> Pi(A, \<lambda>_. B)"
+ (*This formulation facilitates case analysis on A.*)
+ foundation: "A = 0 \<or> (\<exists>x\<in>A. \<forall>y\<in>x. y\<notin>A)" and
+
+ (*Schema axiom since predicate P is a higher-order variable*)
+ replacement: "(\<forall>x\<in>A. \<forall>y z. P(x,y) \<and> P(x,z) \<longrightarrow> y = z) \<Longrightarrow>
+ b \<in> PrimReplace(A,P) \<longleftrightarrow> (\<exists>x\<in>A. P(x,b))"
-nonterminal "is" and patterns
+subsection \<open>Definite descriptions -- via Replace over the set "1"\<close>
+
+definition The :: "(i \<Rightarrow> o) \<Rightarrow> i" (binder "THE " 10)
+ where the_def: "The(P) == \<Union>({y . x \<in> {0}, P(y)})"
-syntax
- "" :: "i => is" ("_")
- "_Enum" :: "[i, is] => is" ("_,/ _")
+definition If :: "[o, i, i] \<Rightarrow> i" ("(if (_)/ then (_)/ else (_))" [10] 10)
+ where if_def: "if P then a else b == THE z. P & z=a | ~P & z=b"
+
+abbreviation (input)
+ old_if :: "[o, i, i] => i" ("if '(_,_,_')")
+ where "if(P,a,b) == If(P,a,b)"
+
+
+subsection \<open>Ordered Pairing\<close>
- "_Finset" :: "is => i" ("{(_)}")
- "_Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>")
- "_Collect" :: "[pttrn, i, o] => i" ("(1{_ \<in> _ ./ _})")
- "_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
- "_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \<in> _})" [51,0,51])
- "_UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10)
- "_INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10)
- "_PROD" :: "[pttrn, i, i] => i" ("(3\<Prod>_\<in>_./ _)" 10)
- "_SUM" :: "[pttrn, i, i] => i" ("(3\<Sum>_\<in>_./ _)" 10)
- "_lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10)
- "_Ball" :: "[pttrn, i, o] => o" ("(3\<forall>_\<in>_./ _)" 10)
- "_Bex" :: "[pttrn, i, o] => o" ("(3\<exists>_\<in>_./ _)" 10)
+(* this "symmetric" definition works better than {{a}, {a,b}} *)
+definition Pair :: "[i, i] => i"
+ where "Pair(a,b) == {{a,a}, {a,b}}"
+
+definition fst :: "i \<Rightarrow> i"
+ where "fst(p) == THE a. \<exists>b. p = Pair(a, b)"
- (** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
+definition snd :: "i \<Rightarrow> i"
+ where "snd(p) == THE b. \<exists>a. p = Pair(a, b)"
+definition split :: "[[i, i] \<Rightarrow> 'a, i] \<Rightarrow> 'a::{}" \<comment> \<open>for pattern-matching\<close>
+ where "split(c) == \<lambda>p. c(fst(p), snd(p))"
+
+(* Patterns -- extends pre-defined type "pttrn" used in abstractions *)
+nonterminal patterns
+syntax
"_pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>")
"" :: "pttrn => patterns" ("_")
"_patterns" :: "[pttrn, patterns] => patterns" ("_,/_")
-
+ "_Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>")
translations
- "{x, xs}" == "CONST cons(x, {xs})"
- "{x}" == "CONST cons(x, 0)"
- "{x\<in>A. P}" == "CONST Collect(A, \<lambda>x. P)"
- "{y. x\<in>A, Q}" == "CONST Replace(A, \<lambda>x y. Q)"
- "{b. x\<in>A}" == "CONST RepFun(A, \<lambda>x. b)"
- "\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})"
- "\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})"
- "\<Prod>x\<in>A. B" == "CONST Pi(A, \<lambda>x. B)"
- "\<Sum>x\<in>A. B" == "CONST Sigma(A, \<lambda>x. B)"
- "\<lambda>x\<in>A. f" == "CONST Lambda(A, \<lambda>x. f)"
- "\<forall>x\<in>A. P" == "CONST Ball(A, \<lambda>x. P)"
- "\<exists>x\<in>A. P" == "CONST Bex(A, \<lambda>x. P)"
-
"\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
"\<langle>x, y\<rangle>" == "CONST Pair(x, y)"
"\<lambda>\<langle>x,y,zs\<rangle>.b" == "CONST split(\<lambda>x \<langle>y,zs\<rangle>.b)"
"\<lambda>\<langle>x,y\<rangle>.b" == "CONST split(\<lambda>x y. b)"
+definition Sigma :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
+ where "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {\<langle>x,y\<rangle>}"
+
+abbreviation cart_prod :: "[i, i] => i" (infixr "\<times>" 80) \<comment> \<open>Cartesian product\<close>
+ where "A \<times> B \<equiv> Sigma(A, \<lambda>_. B)"
+
+
+subsection \<open>Relations and Functions\<close>
+
+(*converse of relation r, inverse of function*)
+definition converse :: "i \<Rightarrow> i"
+ where "converse(r) == {z. w\<in>r, \<exists>x y. w=\<langle>x,y\<rangle> \<and> z=\<langle>y,x\<rangle>}"
+
+definition domain :: "i \<Rightarrow> i"
+ where "domain(r) == {x. w\<in>r, \<exists>y. w=\<langle>x,y\<rangle>}"
+
+definition range :: "i \<Rightarrow> i"
+ where "range(r) == domain(converse(r))"
+
+definition field :: "i \<Rightarrow> i"
+ where "field(r) == domain(r) \<union> range(r)"
+
+definition relation :: "i \<Rightarrow> o" \<comment> \<open>recognizes sets of pairs\<close>
+ where "relation(r) == \<forall>z\<in>r. \<exists>x y. z = \<langle>x,y\<rangle>"
+
+definition function :: "i \<Rightarrow> o" \<comment> \<open>recognizes functions; can have non-pairs\<close>
+ where "function(r) == \<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> (\<forall>y'. \<langle>x,y'\<rangle> \<in> r \<longrightarrow> y = y')"
+
+definition Image :: "[i, i] \<Rightarrow> i" (infixl "``" 90) \<comment> \<open>image\<close>
+ where image_def: "r `` A == {y \<in> range(r). \<exists>x\<in>A. \<langle>x,y\<rangle> \<in> r}"
+
+definition vimage :: "[i, i] \<Rightarrow> i" (infixl "-``" 90) \<comment> \<open>inverse image\<close>
+ where vimage_def: "r -`` A == converse(r)``A"
+
+(* Restrict the relation r to the domain A *)
+definition restrict :: "[i, i] \<Rightarrow> i"
+ where "restrict(r,A) == {z \<in> r. \<exists>x\<in>A. \<exists>y. z = \<langle>x,y\<rangle>}"
+
+
+(* Abstraction, application and Cartesian product of a family of sets *)
+
+definition Lambda :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
+ where lam_def: "Lambda(A,b) == {\<langle>x,b(x)\<rangle>. x\<in>A}"
+
+definition "apply" :: "[i, i] \<Rightarrow> i" (infixl "`" 90) \<comment> \<open>function application\<close>
+ where "f`a == \<Union>(f``{a})"
+
+definition Pi :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
+ where "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A\<subseteq>domain(f) & function(f)}"
+
+abbreviation function_space :: "[i, i] \<Rightarrow> i" (infixr "->" 60) \<comment> \<open>function space\<close>
+ where "A -> B \<equiv> Pi(A, \<lambda>_. B)"
+
+
+(* binder syntax *)
+
+syntax
+ "_PROD" :: "[pttrn, i, i] => i" ("(3\<Prod>_\<in>_./ _)" 10)
+ "_SUM" :: "[pttrn, i, i] => i" ("(3\<Sum>_\<in>_./ _)" 10)
+ "_lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10)
+translations
+ "\<Prod>x\<in>A. B" == "CONST Pi(A, \<lambda>x. B)"
+ "\<Sum>x\<in>A. B" == "CONST Sigma(A, \<lambda>x. B)"
+ "\<lambda>x\<in>A. f" == "CONST Lambda(A, \<lambda>x. f)"
+
+
+subsection \<open>ASCII syntax\<close>
notation (ASCII)
cart_prod (infixr "*" 80) and
@@ -155,6 +270,8 @@
not_mem (infixl "~:" 50)
syntax (ASCII)
+ "_Ball" :: "[pttrn, i, o] => o" ("(3ALL _:_./ _)" 10)
+ "_Bex" :: "[pttrn, i, o] => o" ("(3EX _:_./ _)" 10)
"_Collect" :: "[pttrn, i, o] => i" ("(1{_: _ ./ _})")
"_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
"_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _: _})" [51,0,51])
@@ -163,104 +280,9 @@
"_PROD" :: "[pttrn, i, i] => i" ("(3PROD _:_./ _)" 10)
"_SUM" :: "[pttrn, i, i] => i" ("(3SUM _:_./ _)" 10)
"_lam" :: "[pttrn, i, i] => i" ("(3lam _:_./ _)" 10)
- "_Ball" :: "[pttrn, i, o] => o" ("(3ALL _:_./ _)" 10)
- "_Bex" :: "[pttrn, i, o] => o" ("(3EX _:_./ _)" 10)
"_Tuple" :: "[i, is] => i" ("<(_,/ _)>")
"_pattern" :: "patterns => pttrn" ("<_>")
-defs (* Bounded Quantifiers *)
- Ball_def: "Ball(A, P) == \<forall>x. x\<in>A \<longrightarrow> P(x)"
- Bex_def: "Bex(A, P) == \<exists>x. x\<in>A & P(x)"
-
- subset_def: "A \<subseteq> B == \<forall>x\<in>A. x\<in>B"
-
-
-axiomatization where
-
- (* ZF axioms -- see Suppes p.238
- Axioms for Union, Pow and Replace state existence only,
- uniqueness is derivable using extensionality. *)
-
- extension: "A = B <-> A \<subseteq> B & B \<subseteq> A" and
- Union_iff: "A \<in> \<Union>(C) <-> (\<exists>B\<in>C. A\<in>B)" and
- Pow_iff: "A \<in> Pow(B) <-> A \<subseteq> B" and
-
- (*We may name this set, though it is not uniquely defined.*)
- infinity: "0\<in>Inf & (\<forall>y\<in>Inf. succ(y): Inf)" and
-
- (*This formulation facilitates case analysis on A.*)
- foundation: "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y\<notin>A)" and
-
- (*Schema axiom since predicate P is a higher-order variable*)
- replacement: "(\<forall>x\<in>A. \<forall>y z. P(x,y) & P(x,z) \<longrightarrow> y=z) ==>
- b \<in> PrimReplace(A,P) <-> (\<exists>x\<in>A. P(x,b))"
-
-
-defs
-
- (* Derived form of replacement, restricting P to its functional part.
- The resulting set (for functional P) is the same as with
- PrimReplace, but the rules are simpler. *)
-
- Replace_def: "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))"
-
- (* Functional form of replacement -- analgous to ML's map functional *)
-
- RepFun_def: "RepFun(A,f) == {y . x\<in>A, y=f(x)}"
-
- (* Separation and Pairing can be derived from the Replacement
- and Powerset Axioms using the following definitions. *)
-
- Collect_def: "Collect(A,P) == {y . x\<in>A, x=y & P(x)}"
-
- (*Unordered pairs (Upair) express binary union/intersection and cons;
- set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)
-
- Upair_def: "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
- cons_def: "cons(a,A) == Upair(a,a) \<union> A"
- succ_def: "succ(i) == cons(i, i)"
-
- (* Difference, general intersection, binary union and small intersection *)
-
- Diff_def: "A - B == { x\<in>A . ~(x\<in>B) }"
- Inter_def: "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}"
- Un_def: "A \<union> B == \<Union>(Upair(A,B))"
- Int_def: "A \<inter> B == \<Inter>(Upair(A,B))"
-
- (* definite descriptions *)
- the_def: "The(P) == \<Union>({y . x \<in> {0}, P(y)})"
- if_def: "if(P,a,b) == THE z. P & z=a | ~P & z=b"
-
- (* this "symmetric" definition works better than {{a}, {a,b}} *)
- Pair_def: "<a,b> == {{a,a}, {a,b}}"
- fst_def: "fst(p) == THE a. \<exists>b. p=<a,b>"
- snd_def: "snd(p) == THE b. \<exists>a. p=<a,b>"
- split_def: "split(c) == %p. c(fst(p), snd(p))"
- Sigma_def: "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {<x,y>}"
-
- (* Operations on relations *)
-
- (*converse of relation r, inverse of function*)
- converse_def: "converse(r) == {z. w\<in>r, \<exists>x y. w=<x,y> & z=<y,x>}"
-
- domain_def: "domain(r) == {x. w\<in>r, \<exists>y. w=<x,y>}"
- range_def: "range(r) == domain(converse(r))"
- field_def: "field(r) == domain(r) \<union> range(r)"
- relation_def: "relation(r) == \<forall>z\<in>r. \<exists>x y. z = <x,y>"
- function_def: "function(r) ==
- \<forall>x y. <x,y>:r \<longrightarrow> (\<forall>y'. <x,y'>:r \<longrightarrow> y=y')"
- image_def: "r `` A == {y \<in> range(r) . \<exists>x\<in>A. <x,y> \<in> r}"
- vimage_def: "r -`` A == converse(r)``A"
-
- (* Abstraction, application and Cartesian product of a family of sets *)
-
- lam_def: "Lambda(A,b) == {<x,b(x)> . x\<in>A}"
- apply_def: "f`a == \<Union>(f``{a})"
- Pi_def: "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A<=domain(f) & function(f)}"
-
- (* Restrict the relation r to the domain A *)
- restrict_def: "restrict(r,A) == {z \<in> r. \<exists>x\<in>A. \<exists>y. z = <x,y>}"
-
subsection \<open>Substitution\<close>