--- a/NEWS Thu Feb 11 12:26:50 2010 -0800
+++ b/NEWS Thu Feb 11 23:50:38 2010 +0100
@@ -132,6 +132,9 @@
*** ML ***
+* Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw
+syntax constant (cf. 'syntax' command).
+
* Renamed old-style Drule.standard to Drule.export_without_context, to
emphasize that this is in no way a standard operation.
INCOMPATIBILITY.
--- a/doc-src/Classes/Thy/Setup.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/doc-src/Classes/Thy/Setup.thy Thu Feb 11 23:50:38 2010 +0100
@@ -18,17 +18,19 @@
fun alpha_ast_tr [] = Syntax.Variable "'a"
| alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
fun alpha_ofsort_ast_tr [ast] =
- Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast]
+ Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'a", ast]
| alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
fun beta_ast_tr [] = Syntax.Variable "'b"
| beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
fun beta_ofsort_ast_tr [ast] =
- Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast]
+ Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'b", ast]
| beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
- in [
- ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
- ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr)
- ] end
+ in
+ [(@{syntax_const "_alpha"}, alpha_ast_tr),
+ (@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr),
+ (@{syntax_const "_beta"}, beta_ast_tr),
+ (@{syntax_const "_beta_ofsort"}, beta_ofsort_ast_tr)]
+ end
*}
end
\ No newline at end of file
--- a/doc-src/TutorialI/Protocol/Message.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/doc-src/TutorialI/Protocol/Message.thy Thu Feb 11 23:50:38 2010 +0100
@@ -82,14 +82,14 @@
(*<*)
text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
syntax
- "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
+ "_MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
syntax (xsymbols)
- "@MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+ "_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
translations
"{|x, y, z|}" == "{|x, {|y, z|}|}"
- "{|x, y|}" == "MPair x y"
+ "{|x, y|}" == "CONST MPair x y"
constdefs
--- a/src/CCL/Set.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/CCL/Set.thy Thu Feb 11 23:50:38 2010 +0100
@@ -27,17 +27,17 @@
empty :: "'a set" ("{}")
syntax
- "@Coll" :: "[idt, o] => 'a set" ("(1{_./ _})") (*collection*)
+ "_Coll" :: "[idt, o] => 'a set" ("(1{_./ _})") (*collection*)
(* Big Intersection / Union *)
- "@INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(INT _:_./ _)" [0, 0, 0] 10)
- "@UNION" :: "[idt, 'a set, 'b set] => 'b set" ("(UN _:_./ _)" [0, 0, 0] 10)
+ "_INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(INT _:_./ _)" [0, 0, 0] 10)
+ "_UNION" :: "[idt, 'a set, 'b set] => 'b set" ("(UN _:_./ _)" [0, 0, 0] 10)
(* Bounded Quantifiers *)
- "@Ball" :: "[idt, 'a set, o] => o" ("(ALL _:_./ _)" [0, 0, 0] 10)
- "@Bex" :: "[idt, 'a set, o] => o" ("(EX _:_./ _)" [0, 0, 0] 10)
+ "_Ball" :: "[idt, 'a set, o] => o" ("(ALL _:_./ _)" [0, 0, 0] 10)
+ "_Bex" :: "[idt, 'a set, o] => o" ("(EX _:_./ _)" [0, 0, 0] 10)
translations
"{x. P}" == "CONST Collect(%x. P)"
--- a/src/CCL/Term.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/CCL/Term.thy Thu Feb 11 23:50:38 2010 +0100
@@ -40,16 +40,16 @@
letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"
syntax
- "@let" :: "[idt,i,i]=>i" ("(3let _ be _/ in _)"
+ "_let" :: "[idt,i,i]=>i" ("(3let _ be _/ in _)"
[0,0,60] 60)
- "@letrec" :: "[idt,idt,i,i]=>i" ("(3letrec _ _ be _/ in _)"
+ "_letrec" :: "[idt,idt,i,i]=>i" ("(3letrec _ _ be _/ in _)"
[0,0,0,60] 60)
- "@letrec2" :: "[idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ be _/ in _)"
+ "_letrec2" :: "[idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ be _/ in _)"
[0,0,0,0,60] 60)
- "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
+ "_letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
[0,0,0,0,0,60] 60)
ML {*
@@ -58,29 +58,30 @@
(* FIXME does not handle "_idtdummy" *)
(* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *)
-fun let_tr [Free(id,T),a,b] = Const("let",dummyT) $ a $ absfree(id,T,b);
+fun let_tr [Free(id,T),a,b] = Const(@{const_syntax let},dummyT) $ a $ absfree(id,T,b);
fun let_tr' [a,Abs(id,T,b)] =
let val (id',b') = variant_abs(id,T,b)
- in Const("@let",dummyT) $ Free(id',T) $ a $ b' end;
+ in Const(@{syntax_const "_let"},dummyT) $ Free(id',T) $ a $ b' end;
fun letrec_tr [Free(f,S),Free(x,T),a,b] =
- Const("letrec",dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b);
+ Const(@{const_syntax letrec},dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b);
fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] =
- Const("letrec2",dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b);
+ Const(@{const_syntax letrec2},dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b);
fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] =
- Const("letrec3",dummyT) $ absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
+ Const(@{const_syntax letrec3},dummyT) $
+ absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
let val (f',b') = variant_abs(ff,SS,b)
val (_,a'') = variant_abs(f,S,a)
val (x',a') = variant_abs(x,T,a'')
- in Const("@letrec",dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
+ in Const(@{syntax_const "_letrec"},dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
let val (f',b') = variant_abs(ff,SS,b)
val ( _,a1) = variant_abs(f,S,a)
val (y',a2) = variant_abs(y,U,a1)
val (x',a') = variant_abs(x,T,a2)
- in Const("@letrec2",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
+ in Const(@{syntax_const "_letrec2"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
end;
fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
let val (f',b') = variant_abs(ff,SS,b)
@@ -88,22 +89,24 @@
val (z',a2) = variant_abs(z,V,a1)
val (y',a3) = variant_abs(y,U,a2)
val (x',a') = variant_abs(x,T,a3)
- in Const("@letrec3",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
+ in Const(@{syntax_const "_letrec3"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
end;
*}
parse_translation {*
- [("@let", let_tr),
- ("@letrec", letrec_tr),
- ("@letrec2", letrec2_tr),
- ("@letrec3", letrec3_tr)] *}
+ [(@{syntax_const "_let"}, let_tr),
+ (@{syntax_const "_letrec"}, letrec_tr),
+ (@{syntax_const "_letrec2"}, letrec2_tr),
+ (@{syntax_const "_letrec3"}, letrec3_tr)]
+*}
print_translation {*
- [("let", let_tr'),
- ("letrec", letrec_tr'),
- ("letrec2", letrec2_tr'),
- ("letrec3", letrec3_tr')] *}
+ [(@{const_syntax let}, let_tr'),
+ (@{const_syntax letrec}, letrec_tr'),
+ (@{const_syntax letrec2}, letrec2_tr'),
+ (@{const_syntax letrec3}, letrec3_tr')]
+*}
consts
napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56)
--- a/src/CCL/Type.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/CCL/Type.thy Thu Feb 11 23:50:38 2010 +0100
@@ -28,15 +28,15 @@
SPLIT :: "[i, [i, i] => i set] => i set"
syntax
- "@Pi" :: "[idt, i set, i set] => i set" ("(3PROD _:_./ _)"
+ "_Pi" :: "[idt, i set, i set] => i set" ("(3PROD _:_./ _)"
[0,0,60] 60)
- "@Sigma" :: "[idt, i set, i set] => i set" ("(3SUM _:_./ _)"
+ "_Sigma" :: "[idt, i set, i set] => i set" ("(3SUM _:_./ _)"
[0,0,60] 60)
- "@->" :: "[i set, i set] => i set" ("(_ ->/ _)" [54, 53] 53)
- "@*" :: "[i set, i set] => i set" ("(_ */ _)" [56, 55] 55)
- "@Subtype" :: "[idt, 'a set, o] => 'a set" ("(1{_: _ ./ _})")
+ "_arrow" :: "[i set, i set] => i set" ("(_ ->/ _)" [54, 53] 53)
+ "_star" :: "[i set, i set] => i set" ("(_ */ _)" [56, 55] 55)
+ "_Subtype" :: "[idt, 'a set, o] => 'a set" ("(1{_: _ ./ _})")
translations
"PROD x:A. B" => "CONST Pi(A, %x. B)"
@@ -46,8 +46,9 @@
"{x: A. B}" == "CONST Subtype(A, %x. B)"
print_translation {*
- [(@{const_syntax Pi}, dependent_tr' ("@Pi", "@->")),
- (@{const_syntax Sigma}, dependent_tr' ("@Sigma", "@*"))] *}
+ [(@{const_syntax Pi}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
+ (@{const_syntax Sigma}, dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
+*}
axioms
Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}"
--- a/src/Cube/Cube.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Cube/Cube.thy Thu Feb 11 23:50:38 2010 +0100
@@ -1,5 +1,4 @@
(* Title: Cube/Cube.thy
- ID: $Id$
Author: Tobias Nipkow
*)
@@ -54,7 +53,9 @@
Pi :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10)
arrow :: "[term, term] => term" (infixr "\<rightarrow>" 10)
-print_translation {* [(@{const_syntax Prod}, dependent_tr' ("Pi", "arrow"))] *}
+print_translation {*
+ [(@{const_syntax Prod}, dependent_tr' (@{syntax_const Pi}, @{syntax_const arrow}))]
+*}
axioms
s_b: "*: []"
--- a/src/FOLP/IFOLP.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/FOLP/IFOLP.thy Thu Feb 11 23:50:38 2010 +0100
@@ -22,7 +22,6 @@
consts
(*** Judgements ***)
- "@Proof" :: "[p,o]=>prop" ("(_ /: _)" [51,10] 5)
Proof :: "[o,p]=>prop"
EqProof :: "[p,p,o]=>prop" ("(3_ /= _ :/ _)" [10,10,10] 5)
@@ -66,6 +65,8 @@
local
+syntax "_Proof" :: "[p,o]=>prop" ("(_ /: _)" [51, 10] 5)
+
ML {*
(*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
@@ -74,12 +75,12 @@
fun proof_tr [p,P] = Const (@{const_name Proof}, dummyT) $ P $ p;
fun proof_tr' [P,p] =
- if !show_proofs then Const("@Proof",dummyT) $ p $ P
- else P (*this case discards the proof term*);
+ if ! show_proofs then Const (@{syntax_const "_Proof"}, dummyT) $ p $ P
+ else P (*this case discards the proof term*);
*}
-parse_translation {* [("@Proof", proof_tr)] *}
-print_translation {* [("Proof", proof_tr')] *}
+parse_translation {* [(@{syntax_const "_Proof"}, proof_tr)] *}
+print_translation {* [(@{const_syntax Proof}, proof_tr')] *}
axioms
--- a/src/HOL/Auth/Message.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Auth/Message.thy Thu Feb 11 23:50:38 2010 +0100
@@ -51,10 +51,10 @@
text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
syntax
- "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
+ "_MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
syntax (xsymbols)
- "@MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+ "_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
translations
"{|x, y, z|}" == "{|x, {|y, z|}|}"
--- a/src/HOL/Complete_Lattice.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Complete_Lattice.thy Thu Feb 11 23:50:38 2010 +0100
@@ -106,10 +106,10 @@
"INF x. B" == "INF x:CONST UNIV. B"
"INF x:A. B" == "CONST INFI A (%x. B)"
-print_translation {* [
-Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} "_SUP",
-Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} "_INF"
-] *} -- {* to avoid eta-contraction of body *}
+print_translation {*
+ [Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"},
+ Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"}]
+*} -- {* to avoid eta-contraction of body *}
context complete_lattice
begin
@@ -282,16 +282,16 @@
"UNION \<equiv> SUPR"
syntax
- "@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10)
- "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" [0, 10] 10)
+ "_UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10)
+ "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" [0, 10] 10)
syntax (xsymbols)
- "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" [0, 10] 10)
- "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
+ "_UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" [0, 10] 10)
+ "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
syntax (latex output)
- "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
- "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
+ "_UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
+ "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
translations
"UN x y. B" == "UN x. UN y. B"
@@ -308,9 +308,9 @@
subscripts in Proof General.
*}
-print_translation {* [
-Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} "@UNION"
-] *} -- {* to avoid eta-contraction of body *}
+print_translation {*
+ [Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
+*} -- {* to avoid eta-contraction of body *}
lemma UNION_eq_Union_image:
"(\<Union>x\<in>A. B x) = \<Union>(B`A)"
@@ -518,16 +518,16 @@
"INTER \<equiv> INFI"
syntax
- "@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10)
- "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" [0, 10] 10)
+ "_INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10)
+ "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" [0, 10] 10)
syntax (xsymbols)
- "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" [0, 10] 10)
- "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
+ "_INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" [0, 10] 10)
+ "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
syntax (latex output)
- "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
- "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
+ "_INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
+ "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
translations
"INT x y. B" == "INT x. INT y. B"
@@ -535,9 +535,9 @@
"INT x. B" == "INT x:CONST UNIV. B"
"INT x:A. B" == "CONST INTER A (%x. B)"
-print_translation {* [
-Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} "@INTER"
-] *} -- {* to avoid eta-contraction of body *}
+print_translation {*
+ [Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
+*} -- {* to avoid eta-contraction of body *}
lemma INTER_eq_Inter_image:
"(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
--- a/src/HOL/Finite_Set.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Finite_Set.thy Thu Feb 11 23:50:38 2010 +0100
@@ -1095,13 +1095,16 @@
print_translation {*
let
- fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] =
- if x<>y then raise Match
- else let val x' = Syntax.mark_bound x
- val t' = subst_bound(x',t)
- val P' = subst_bound(x',P)
- in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end
-in [("setsum", setsum_tr')] end
+ fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
+ if x <> y then raise Match
+ else
+ let
+ val x' = Syntax.mark_bound x;
+ val t' = subst_bound (x', t);
+ val P' = subst_bound (x', P);
+ in Syntax.const @{syntax_const "_qsetsum"} $ Syntax.mark_bound x $ P' $ t' end
+ | setsum_tr' _ = raise Match;
+in [(@{const_syntax setsum}, setsum_tr')] end
*}
--- a/src/HOL/Fun.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Fun.thy Thu Feb 11 23:50:38 2010 +0100
@@ -387,18 +387,16 @@
"_updbind" :: "['a, 'a] => updbind" ("(2_ :=/ _)")
"" :: "updbind => updbinds" ("_")
"_updbinds":: "[updbind, updbinds] => updbinds" ("_,/ _")
- "_Update" :: "['a, updbinds] => 'a" ("_/'((_)')" [1000,0] 900)
+ "_Update" :: "['a, updbinds] => 'a" ("_/'((_)')" [1000, 0] 900)
translations
- "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs"
- "f(x:=y)" == "fun_upd f x y"
+ "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs"
+ "f(x:=y)" == "CONST fun_upd f x y"
(* Hint: to define the sum of two functions (or maps), use sum_case.
A nice infix syntax could be defined (in Datatype.thy or below) by
-consts
- fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
-translations
- "fun_sum" == sum_case
+notation
+ sum_case (infixr "'(+')"80)
*)
lemma fun_upd_idem_iff: "(f(x:=y) = f) = (f x = y)"
--- a/src/HOL/HOL.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/HOL.thy Thu Feb 11 23:50:38 2010 +0100
@@ -129,16 +129,15 @@
"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _")
translations
- "THE x. P" == "The (%x. P)"
+ "THE x. P" == "CONST The (%x. P)"
"_Let (_binds b bs) e" == "_Let b (_Let bs e)"
- "let x = a in e" == "Let a (%x. e)"
+ "let x = a in e" == "CONST Let a (%x. e)"
print_translation {*
-(* To avoid eta-contraction of body: *)
-[("The", fn [Abs abs] =>
- let val (x,t) = atomic_abs_tr' abs
- in Syntax.const "_The" $ x $ t end)]
-*}
+ [(@{const_syntax The}, fn [Abs abs] =>
+ let val (x, t) = atomic_abs_tr' abs
+ in Syntax.const @{syntax_const "_The"} $ x $ t end)]
+*} -- {* To avoid eta-contraction of body *}
syntax (xsymbols)
"_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10)
--- a/src/HOL/Hilbert_Choice.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hilbert_Choice.thy Thu Feb 11 23:50:38 2010 +0100
@@ -25,11 +25,10 @@
"SOME x. P" == "CONST Eps (%x. P)"
print_translation {*
-(* to avoid eta-contraction of body *)
-[(@{const_syntax Eps}, fn [Abs abs] =>
- let val (x,t) = atomic_abs_tr' abs
- in Syntax.const "_Eps" $ x $ t end)]
-*}
+ [(@{const_syntax Eps}, fn [Abs abs] =>
+ let val (x, t) = atomic_abs_tr' abs
+ in Syntax.const @{syntax_const "_Eps"} $ x $ t end)]
+*} -- {* to avoid eta-contraction of body *}
definition inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
"inv_into A f == %x. SOME y. y : A & f y = x"
@@ -315,7 +314,7 @@
syntax
"_LeastM" :: "[pttrn, 'a => 'b::ord, bool] => 'a" ("LEAST _ WRT _. _" [0, 4, 10] 10)
translations
- "LEAST x WRT m. P" == "LeastM m (%x. P)"
+ "LEAST x WRT m. P" == "CONST LeastM m (%x. P)"
lemma LeastMI2:
"P x ==> (!!y. P y ==> m x <= m y)
@@ -369,11 +368,10 @@
"Greatest == GreatestM (%x. x)"
syntax
- "_GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a"
+ "_GreatestM" :: "[pttrn, 'a => 'b::ord, bool] => 'a"
("GREATEST _ WRT _. _" [0, 4, 10] 10)
-
translations
- "GREATEST x WRT m. P" == "GreatestM m (%x. P)"
+ "GREATEST x WRT m. P" == "CONST GreatestM m (%x. P)"
lemma GreatestMI2:
"P x ==> (!!y. P y ==> m y <= m x)
--- a/src/HOL/Hoare/HeapSyntax.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hoare/HeapSyntax.thy Thu Feb 11 23:50:38 2010 +0100
@@ -15,9 +15,9 @@
"_faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
("_^._" [65,1000] 65)
translations
- "f(r \<rightarrow> v)" == "f(CONST addr r := v)"
- "p^.f := e" => "f := f(p \<rightarrow> e)"
- "p^.f" => "f(CONST addr p)"
+ "f(r \<rightarrow> v)" == "f(CONST addr r := v)"
+ "p^.f := e" => "f := f(p \<rightarrow> e)"
+ "p^.f" => "f(CONST addr p)"
declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
--- a/src/HOL/Hoare/HeapSyntaxAbort.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hoare/HeapSyntaxAbort.thy Thu Feb 11 23:50:38 2010 +0100
@@ -23,9 +23,9 @@
"_faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
("_^._" [65,1000] 65)
translations
- "_refupdate f r v" == "f(CONST addr r := v)"
- "p^.f := e" => "(p \<noteq> CONST Null) \<rightarrow> (f := _refupdate f p e)"
- "p^.f" => "f(CONST addr p)"
+ "_refupdate f r v" == "f(CONST addr r := v)"
+ "p^.f := e" => "(p \<noteq> CONST Null) \<rightarrow> (f := _refupdate f p e)"
+ "p^.f" => "f(CONST addr p)"
declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]
--- a/src/HOL/Hoare/Hoare.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hoare/Hoare.thy Thu Feb 11 23:50:38 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Hoare/Hoare.thy
- ID: $Id$
Author: Leonor Prensa Nieto & Tobias Nipkow
Copyright 1998 TUM
@@ -19,11 +18,11 @@
'a assn = "'a set"
datatype
- 'a com = Basic "'a \<Rightarrow> 'a"
+ 'a com = Basic "'a \<Rightarrow> 'a"
| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60)
| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
| While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
-
+
abbreviation annskip ("SKIP") where "SKIP == Basic id"
types 'a sem = "'a => 'a => bool"
@@ -68,11 +67,11 @@
fun mk_abstuple [x] body = abs (x, body)
| mk_abstuple (x::xs) body =
- Syntax.const "split" $ abs (x, mk_abstuple xs body);
+ Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body);
fun mk_fbody a e [x as (b,_)] = if a=b then e else Syntax.free b
| mk_fbody a e ((b,_)::xs) =
- Syntax.const "Pair" $ (if a=b then e else Syntax.free b) $ mk_fbody a e xs;
+ Syntax.const @{const_syntax Pair} $ (if a=b then e else Syntax.free b) $ mk_fbody a e xs;
fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs)
end
@@ -82,22 +81,22 @@
(*all meta-variables for bexp except for TRUE are translated as if they
were boolean expressions*)
ML{*
-fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"
- | bexp_tr b xs = Syntax.const "Collect" $ mk_abstuple xs b;
-
-fun assn_tr r xs = Syntax.const "Collect" $ mk_abstuple xs r;
+fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" (* FIXME !? *)
+ | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
+
+fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
*}
(* com_tr *)
ML{*
-fun com_tr (Const("_assign",_) $ Free (a,_) $ e) xs =
- Syntax.const "Basic" $ mk_fexp a e xs
- | com_tr (Const ("Basic",_) $ f) xs = Syntax.const "Basic" $ f
- | com_tr (Const ("Seq",_) $ c1 $ c2) xs =
- Syntax.const "Seq" $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const ("Cond",_) $ b $ c1 $ c2) xs =
- Syntax.const "Cond" $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const ("While",_) $ b $ I $ c) xs =
- Syntax.const "While" $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
+fun com_tr (Const(@{syntax_const "_assign"},_) $ Free (a,_) $ e) xs =
+ Syntax.const @{const_syntax Basic} $ mk_fexp a e xs
+ | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
+ | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
+ Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
+ | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
+ Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
+ | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
+ Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
| com_tr t _ = t (* if t is just a Free/Var *)
*}
@@ -106,65 +105,66 @@
local
fun var_tr(Free(a,_)) = (a,Bound 0) (* Bound 0 = dummy term *)
- | var_tr(Const ("_constrain", _) $ (Free (a,_)) $ T) = (a,T);
+ | var_tr(Const (@{syntax_const "_constrain"}, _) $ (Free (a,_)) $ T) = (a,T);
-fun vars_tr (Const ("_idts", _) $ idt $ vars) = var_tr idt :: vars_tr vars
+fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = var_tr idt :: vars_tr vars
| vars_tr t = [var_tr t]
in
fun hoare_vars_tr [vars, pre, prg, post] =
let val xs = vars_tr vars
- in Syntax.const "Valid" $
+ in Syntax.const @{const_syntax Valid} $
assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
end
| hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
end
*}
-parse_translation {* [("_hoare_vars", hoare_vars_tr)] *}
+parse_translation {* [(@{syntax_const "_hoare_vars"}, hoare_vars_tr)] *}
(*****************************************************************************)
(*** print translations ***)
ML{*
-fun dest_abstuple (Const ("split",_) $ (Abs(v,_, body))) =
+fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) =
subst_bound (Syntax.free v, dest_abstuple body)
| dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
| dest_abstuple trm = trm;
-fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
+fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
| abs2list (Abs(x,T,t)) = [Free (x, T)]
| abs2list _ = [];
-fun mk_ts (Const ("split",_) $ (Abs(x,_,t))) = mk_ts t
+fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t
| mk_ts (Abs(x,_,t)) = mk_ts t
- | mk_ts (Const ("Pair",_) $ a $ b) = a::(mk_ts b)
+ | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
| mk_ts t = [t];
-fun mk_vts (Const ("split",_) $ (Abs(x,_,t))) =
+fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) =
((Syntax.free x)::(abs2list t), mk_ts t)
| mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
| mk_vts t = raise Match;
-
-fun find_ch [] i xs = (false, (Syntax.free "not_ch",Syntax.free "not_ch" ))
- | find_ch ((v,t)::vts) i xs = if t=(Bound i) then find_ch vts (i-1) xs
- else (true, (v, subst_bounds (xs,t)));
-
-fun is_f (Const ("split",_) $ (Abs(x,_,t))) = true
+
+fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))
+ | find_ch ((v,t)::vts) i xs =
+ if t = Bound i then find_ch vts (i-1) xs
+ else (true, (v, subst_bounds (xs, t)));
+
+fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true
| is_f (Abs(x,_,t)) = true
| is_f t = false;
*}
(* assn_tr' & bexp_tr'*)
-ML{*
-fun assn_tr' (Const ("Collect",_) $ T) = dest_abstuple T
- | assn_tr' (Const (@{const_name inter}, _) $ (Const ("Collect",_) $ T1) $
- (Const ("Collect",_) $ T2)) =
- Syntax.const "Set.Int" $ dest_abstuple T1 $ dest_abstuple T2
+ML{*
+fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
+ | assn_tr' (Const (@{const_syntax inter}, _) $
+ (Const (@{const_syntax Collect},_) $ T1) $ (Const (@{const_syntax Collect},_) $ T2)) =
+ Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
| assn_tr' t = t;
-fun bexp_tr' (Const ("Collect",_) $ T) = dest_abstuple T
+fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
| bexp_tr' t = t;
*}
@@ -173,22 +173,24 @@
fun mk_assign f =
let val (vs, ts) = mk_vts f;
val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
- in if ch then Syntax.const "_assign" $ fst(which) $ snd(which)
- else Syntax.const @{const_syntax annskip} end;
+ in
+ if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
+ else Syntax.const @{const_syntax annskip}
+ end;
-fun com_tr' (Const ("Basic",_) $ f) = if is_f f then mk_assign f
- else Syntax.const "Basic" $ f
- | com_tr' (Const ("Seq",_) $ c1 $ c2) = Syntax.const "Seq" $
- com_tr' c1 $ com_tr' c2
- | com_tr' (Const ("Cond",_) $ b $ c1 $ c2) = Syntax.const "Cond" $
- bexp_tr' b $ com_tr' c1 $ com_tr' c2
- | com_tr' (Const ("While",_) $ b $ I $ c) = Syntax.const "While" $
- bexp_tr' b $ assn_tr' I $ com_tr' c
+fun com_tr' (Const (@{const_syntax Basic},_) $ f) =
+ if is_f f then mk_assign f
+ else Syntax.const @{const_syntax Basic} $ f
+ | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
+ Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
+ | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) =
+ Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
+ | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) =
+ Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
| com_tr' t = t;
-
fun spec_tr' [p, c, q] =
- Syntax.const "_hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
+ Syntax.const @{syntax_const "_hoare"} $ assn_tr' p $ com_tr' c $ assn_tr' q
*}
print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
--- a/src/HOL/Hoare/HoareAbort.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hoare/HoareAbort.thy Thu Feb 11 23:50:38 2010 +0100
@@ -20,7 +20,7 @@
| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60)
| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
| While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
-
+
abbreviation annskip ("SKIP") where "SKIP == Basic id"
types 'a sem = "'a option => 'a option => bool"
@@ -69,11 +69,11 @@
fun mk_abstuple [x] body = abs (x, body)
| mk_abstuple (x::xs) body =
- Syntax.const "split" $ abs (x, mk_abstuple xs body);
+ Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body);
fun mk_fbody a e [x as (b,_)] = if a=b then e else free b
| mk_fbody a e ((b,_)::xs) =
- Syntax.const "Pair" $ (if a=b then e else free b) $ mk_fbody a e xs;
+ Syntax.const @{const_syntax Pair} $ (if a=b then e else free b) $ mk_fbody a e xs;
fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs)
end
@@ -83,22 +83,22 @@
(*all meta-variables for bexp except for TRUE are translated as if they
were boolean expressions*)
ML{*
-fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"
- | bexp_tr b xs = Syntax.const "Collect" $ mk_abstuple xs b;
-
-fun assn_tr r xs = Syntax.const "Collect" $ mk_abstuple xs r;
+fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" (* FIXME !? *)
+ | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
+
+fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
*}
(* com_tr *)
ML{*
-fun com_tr (Const("_assign",_) $ Free (a,_) $ e) xs =
- Syntax.const "Basic" $ mk_fexp a e xs
- | com_tr (Const ("Basic",_) $ f) xs = Syntax.const "Basic" $ f
- | com_tr (Const ("Seq",_) $ c1 $ c2) xs =
- Syntax.const "Seq" $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const ("Cond",_) $ b $ c1 $ c2) xs =
- Syntax.const "Cond" $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const ("While",_) $ b $ I $ c) xs =
- Syntax.const "While" $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
+fun com_tr (Const (@{syntax_const "_assign"},_) $ Free (a,_) $ e) xs =
+ Syntax.const @{const_syntax Basic} $ mk_fexp a e xs
+ | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
+ | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
+ Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
+ | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
+ Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
+ | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
+ Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
| com_tr t _ = t (* if t is just a Free/Var *)
*}
@@ -106,66 +106,67 @@
ML{*
local
-fun var_tr(Free(a,_)) = (a,Bound 0) (* Bound 0 = dummy term *)
- | var_tr(Const ("_constrain", _) $ (Free (a,_)) $ T) = (a,T);
+fun var_tr (Free (a, _)) = (a, Bound 0) (* Bound 0 = dummy term *)
+ | var_tr (Const (@{syntax_const "_constrain"}, _) $ Free (a, _) $ T) = (a, T);
-fun vars_tr (Const ("_idts", _) $ idt $ vars) = var_tr idt :: vars_tr vars
+fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = var_tr idt :: vars_tr vars
| vars_tr t = [var_tr t]
in
fun hoare_vars_tr [vars, pre, prg, post] =
let val xs = vars_tr vars
- in Syntax.const "Valid" $
+ in Syntax.const @{const_syntax Valid} $
assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
end
| hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
end
*}
-parse_translation {* [("_hoare_vars", hoare_vars_tr)] *}
+parse_translation {* [(@{syntax_const "_hoare_vars"}, hoare_vars_tr)] *}
(*****************************************************************************)
(*** print translations ***)
ML{*
-fun dest_abstuple (Const ("split",_) $ (Abs(v,_, body))) =
- subst_bound (Syntax.free v, dest_abstuple body)
+fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) =
+ subst_bound (Syntax.free v, dest_abstuple body)
| dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
| dest_abstuple trm = trm;
-fun abs2list (Const ("split",_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
+fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
| abs2list (Abs(x,T,t)) = [Free (x, T)]
| abs2list _ = [];
-fun mk_ts (Const ("split",_) $ (Abs(x,_,t))) = mk_ts t
+fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t
| mk_ts (Abs(x,_,t)) = mk_ts t
- | mk_ts (Const ("Pair",_) $ a $ b) = a::(mk_ts b)
+ | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
| mk_ts t = [t];
-fun mk_vts (Const ("split",_) $ (Abs(x,_,t))) =
+fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) =
((Syntax.free x)::(abs2list t), mk_ts t)
| mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
| mk_vts t = raise Match;
-
-fun find_ch [] i xs = (false, (Syntax.free "not_ch",Syntax.free "not_ch" ))
- | find_ch ((v,t)::vts) i xs = if t=(Bound i) then find_ch vts (i-1) xs
- else (true, (v, subst_bounds (xs,t)));
-
-fun is_f (Const ("split",_) $ (Abs(x,_,t))) = true
+
+fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))
+ | find_ch ((v,t)::vts) i xs =
+ if t = Bound i then find_ch vts (i-1) xs
+ else (true, (v, subst_bounds (xs,t)));
+
+fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true
| is_f (Abs(x,_,t)) = true
| is_f t = false;
*}
(* assn_tr' & bexp_tr'*)
-ML{*
-fun assn_tr' (Const ("Collect",_) $ T) = dest_abstuple T
- | assn_tr' (Const (@{const_name inter},_) $ (Const ("Collect",_) $ T1) $
- (Const ("Collect",_) $ T2)) =
- Syntax.const "Set.Int" $ dest_abstuple T1 $ dest_abstuple T2
+ML{*
+fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
+ | assn_tr' (Const (@{const_syntax inter},_) $ (Const (@{const_syntax Collect},_) $ T1) $
+ (Const (@{const_syntax Collect},_) $ T2)) =
+ Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
| assn_tr' t = t;
-fun bexp_tr' (Const ("Collect",_) $ T) = dest_abstuple T
+fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
| bexp_tr' t = t;
*}
@@ -174,22 +175,23 @@
fun mk_assign f =
let val (vs, ts) = mk_vts f;
val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
- in if ch then Syntax.const "_assign" $ fst(which) $ snd(which)
- else Syntax.const @{const_syntax annskip} end;
+ in
+ if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
+ else Syntax.const @{const_syntax annskip}
+ end;
-fun com_tr' (Const ("Basic",_) $ f) = if is_f f then mk_assign f
- else Syntax.const "Basic" $ f
- | com_tr' (Const ("Seq",_) $ c1 $ c2) = Syntax.const "Seq" $
- com_tr' c1 $ com_tr' c2
- | com_tr' (Const ("Cond",_) $ b $ c1 $ c2) = Syntax.const "Cond" $
- bexp_tr' b $ com_tr' c1 $ com_tr' c2
- | com_tr' (Const ("While",_) $ b $ I $ c) = Syntax.const "While" $
- bexp_tr' b $ assn_tr' I $ com_tr' c
+fun com_tr' (Const (@{const_syntax Basic},_) $ f) =
+ if is_f f then mk_assign f else Syntax.const @{const_syntax Basic} $ f
+ | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
+ Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
+ | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) =
+ Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
+ | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) =
+ Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
| com_tr' t = t;
-
fun spec_tr' [p, c, q] =
- Syntax.const "_hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
+ Syntax.const @{syntax_const "_hoare"} $ assn_tr' p $ com_tr' c $ assn_tr' q
*}
print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
--- a/src/HOL/Hoare/Separation.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hoare/Separation.thy Thu Feb 11 23:50:38 2010 +0100
@@ -64,22 +64,25 @@
*)
| free_tr t = t
-fun emp_tr [] = Syntax.const "is_empty" $ Syntax.free "H"
+fun emp_tr [] = Syntax.const @{const_syntax is_empty} $ Syntax.free "H"
| emp_tr ts = raise TERM ("emp_tr", ts);
-fun singl_tr [p,q] = Syntax.const "singl" $ Syntax.free "H" $ p $ q
+fun singl_tr [p, q] = Syntax.const @{const_syntax singl} $ Syntax.free "H" $ p $ q
| singl_tr ts = raise TERM ("singl_tr", ts);
-fun star_tr [P,Q] = Syntax.const "star" $
- absfree("H",dummyT,free_tr P) $ absfree("H",dummyT,free_tr Q) $
+fun star_tr [P,Q] = Syntax.const @{const_syntax star} $
+ absfree ("H", dummyT, free_tr P) $ absfree ("H", dummyT, free_tr Q) $
Syntax.free "H"
| star_tr ts = raise TERM ("star_tr", ts);
-fun wand_tr [P,Q] = Syntax.const "wand" $
- absfree("H",dummyT,P) $ absfree("H",dummyT,Q) $ Syntax.free "H"
+fun wand_tr [P, Q] = Syntax.const @{const_syntax wand} $
+ absfree ("H", dummyT, P) $ absfree ("H", dummyT, Q) $ Syntax.free "H"
| wand_tr ts = raise TERM ("wand_tr", ts);
*}
-parse_translation
- {* [("_emp", emp_tr), ("_singl", singl_tr),
- ("_star", star_tr), ("_wand", wand_tr)] *}
+parse_translation {*
+ [(@{syntax_const "_emp"}, emp_tr),
+ (@{syntax_const "_singl"}, singl_tr),
+ (@{syntax_const "_star"}, star_tr),
+ (@{syntax_const "_wand"}, wand_tr)]
+*}
text{* Now it looks much better: *}
@@ -102,17 +105,9 @@
text{* But the output is still unreadable. Thus we also strip the heap
parameters upon output: *}
-(* debugging code:
-fun sot(Free(s,_)) = s
- | sot(Var((s,i),_)) = "?" ^ s ^ string_of_int i
- | sot(Const(s,_)) = s
- | sot(Bound i) = "B." ^ string_of_int i
- | sot(s $ t) = "(" ^ sot s ^ " " ^ sot t ^ ")"
- | sot(Abs(_,_,t)) = "(% " ^ sot t ^ ")";
-*)
+ML {*
+local
-ML{*
-local
fun strip (Abs(_,_,(t as Const("_free",_) $ Free _) $ Bound 0)) = t
| strip (Abs(_,_,(t as Free _) $ Bound 0)) = t
(*
@@ -120,19 +115,25 @@
*)
| strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t
| strip (Abs(_,_,P)) = P
- | strip (Const("is_empty",_)) = Syntax.const "_emp"
+ | strip (Const(@{const_syntax is_empty},_)) = Syntax.const @{syntax_const "_emp"}
| strip t = t;
+
in
-fun is_empty_tr' [_] = Syntax.const "_emp"
-fun singl_tr' [_,p,q] = Syntax.const "_singl" $ p $ q
-fun star_tr' [P,Q,_] = Syntax.const "_star" $ strip P $ strip Q
-fun wand_tr' [P,Q,_] = Syntax.const "_wand" $ strip P $ strip Q
+
+fun is_empty_tr' [_] = Syntax.const @{syntax_const "_emp"}
+fun singl_tr' [_,p,q] = Syntax.const @{syntax_const "_singl"} $ p $ q
+fun star_tr' [P,Q,_] = Syntax.const @{syntax_const "_star"} $ strip P $ strip Q
+fun wand_tr' [P,Q,_] = Syntax.const @{syntax_const "_wand"} $ strip P $ strip Q
+
end
*}
-print_translation
- {* [("is_empty", is_empty_tr'),("singl", singl_tr'),
- ("star", star_tr'),("wand", wand_tr')] *}
+print_translation {*
+ [(@{const_syntax is_empty}, is_empty_tr'),
+ (@{const_syntax singl}, singl_tr'),
+ (@{const_syntax star}, star_tr'),
+ (@{const_syntax wand}, wand_tr')]
+*}
text{* Now the intermediate proof states are also readable: *}
--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Thu Feb 11 23:50:38 2010 +0100
@@ -5,18 +5,25 @@
text{* Syntax for commands and for assertions and boolean expressions in
commands @{text com} and annotated commands @{text ann_com}. *}
+abbreviation Skip :: "'a com" ("SKIP" 63)
+ where "SKIP \<equiv> Basic id"
+
+abbreviation AnnSkip :: "'a assn \<Rightarrow> 'a ann_com" ("_//SKIP" [90] 63)
+ where "r SKIP \<equiv> AnnBasic r id"
+
+notation
+ Seq ("_,,/ _" [55, 56] 55) and
+ AnnSeq ("_;;/ _" [60,61] 60)
+
syntax
"_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61)
"_AnnAssign" :: "'a assn \<Rightarrow> idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(_ \<acute>_ :=/ _)" [90,70,65] 61)
translations
- "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (\<lambda>_. a))\<guillemotright>"
- "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x (\<lambda>_. a))\<guillemotright>"
+ "\<acute>x := a" \<rightharpoonup> "CONST Basic \<guillemotleft>\<acute>(_update_name x (\<lambda>_. a))\<guillemotright>"
+ "r \<acute>x := a" \<rightharpoonup> "CONST AnnBasic r \<guillemotleft>\<acute>(_update_name x (\<lambda>_. a))\<guillemotright>"
syntax
- "_AnnSkip" :: "'a assn \<Rightarrow> 'a ann_com" ("_//SKIP" [90] 63)
- "_AnnSeq" :: "'a ann_com \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com" ("_;;/ _" [60,61] 60)
-
"_AnnCond1" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com"
("_ //IF _ /THEN _ /ELSE _ /FI" [90,0,0,0] 61)
"_AnnCond2" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com"
@@ -28,8 +35,6 @@
"_AnnAtom" :: "'a assn \<Rightarrow> 'a com \<Rightarrow> 'a ann_com" ("_//\<langle>_\<rangle>" [90,0] 61)
"_AnnWait" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a ann_com" ("_//WAIT _ END" [90,0] 61)
- "_Skip" :: "'a com" ("SKIP" 63)
- "_Seq" :: "'a com \<Rightarrow> 'a com \<Rightarrow> 'a com" ("_,,/ _" [55, 56] 55)
"_Cond" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"
("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
"_Cond2" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" ("IF _ THEN _ FI" [0,0] 56)
@@ -39,21 +44,16 @@
("(0WHILE _ //DO _ /OD)" [0, 0] 61)
translations
- "SKIP" \<rightleftharpoons> "Basic id"
- "c_1,, c_2" \<rightleftharpoons> "Seq c_1 c_2"
-
- "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2"
+ "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond .{b}. c1 c2"
"IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI"
- "WHILE b INV i DO c OD" \<rightharpoonup> "While .{b}. i c"
+ "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While .{b}. i c"
"WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
- "r SKIP" \<rightleftharpoons> "AnnBasic r id"
- "c_1;; c_2" \<rightleftharpoons> "AnnSeq c_1 c_2"
- "r IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "AnnCond1 r .{b}. c1 c2"
- "r IF b THEN c FI" \<rightharpoonup> "AnnCond2 r .{b}. c"
- "r WHILE b INV i DO c OD" \<rightharpoonup> "AnnWhile r .{b}. i c"
- "r AWAIT b THEN c END" \<rightharpoonup> "AnnAwait r .{b}. c"
- "r \<langle>c\<rangle>" \<rightleftharpoons> "r AWAIT True THEN c END"
+ "r IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST AnnCond1 r .{b}. c1 c2"
+ "r IF b THEN c FI" \<rightharpoonup> "CONST AnnCond2 r .{b}. c"
+ "r WHILE b INV i DO c OD" \<rightharpoonup> "CONST AnnWhile r .{b}. i c"
+ "r AWAIT b THEN c END" \<rightharpoonup> "CONST AnnAwait r .{b}. c"
+ "r \<langle>c\<rangle>" \<rightleftharpoons> "r AWAIT CONST True THEN c END"
"r WAIT b END" \<rightleftharpoons> "r AWAIT b THEN SKIP END"
nonterminals
@@ -68,29 +68,29 @@
("SCHEME [_ \<le> _ < _] _// _" [0,0,0,60, 90] 57)
translations
- "_prg c q" \<rightleftharpoons> "[(Some c, q)]"
- "_prgs c q ps" \<rightleftharpoons> "(Some c, q) # ps"
- "_PAR ps" \<rightleftharpoons> "Parallel ps"
+ "_prg c q" \<rightleftharpoons> "[(CONST Some c, q)]"
+ "_prgs c q ps" \<rightleftharpoons> "(CONST Some c, q) # ps"
+ "_PAR ps" \<rightleftharpoons> "CONST Parallel ps"
- "_prg_scheme j i k c q" \<rightleftharpoons> "CONST map (\<lambda>i. (Some c, q)) [j..<k]"
+ "_prg_scheme j i k c q" \<rightleftharpoons> "CONST map (\<lambda>i. (CONST Some c, q)) [j..<k]"
print_translation {*
let
fun quote_tr' f (t :: ts) =
- Term.list_comb (f $ Syntax.quote_tr' "_antiquote" t, ts)
+ Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
| quote_tr' _ _ = raise Match;
fun annquote_tr' f (r :: t :: ts) =
- Term.list_comb (f $ r $ Syntax.quote_tr' "_antiquote" t, ts)
+ Term.list_comb (f $ r $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
| annquote_tr' _ _ = raise Match;
- val assert_tr' = quote_tr' (Syntax.const "_Assert");
+ val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
- fun bexp_tr' name ((Const ("Collect", _) $ t) :: ts) =
+ fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) =
quote_tr' (Syntax.const name) (t :: ts)
| bexp_tr' _ _ = raise Match;
- fun annbexp_tr' name (r :: (Const ("Collect", _) $ t) :: ts) =
+ fun annbexp_tr' name (r :: (Const (@{const_syntax Collect}, _) $ t) :: ts) =
annquote_tr' (Syntax.const name) (r :: t :: ts)
| annbexp_tr' _ _ = raise Match;
@@ -100,41 +100,47 @@
| NONE => raise Match);
fun update_name_tr' (Free x) = Free (upd_tr' x)
- | update_name_tr' ((c as Const ("_free", _)) $ Free x) =
+ | update_name_tr' ((c as Const (@{syntax_const "_free"}, _)) $ Free x) =
c $ Free (upd_tr' x)
| update_name_tr' (Const x) = Const (upd_tr' x)
| update_name_tr' _ = raise Match;
- fun K_tr' (Abs (_,_,t)) = if null (loose_bnos t) then t else raise Match
- | K_tr' (Abs (_,_,Abs (_,_,t)$Bound 0)) = if null (loose_bnos t) then t else raise Match
+ fun K_tr' (Abs (_, _, t)) =
+ if null (loose_bnos t) then t else raise Match
+ | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
+ if null (loose_bnos t) then t else raise Match
| K_tr' _ = raise Match;
fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
- quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
+ quote_tr' (Syntax.const @{syntax_const "_Assign"} $ update_name_tr' f)
(Abs (x, dummyT, K_tr' k) :: ts)
| assign_tr' _ = raise Match;
fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) =
- quote_tr' (Syntax.const "_AnnAssign" $ r $ update_name_tr' f)
+ quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ update_name_tr' f)
(Abs (x, dummyT, K_tr' k) :: ts)
| annassign_tr' _ = raise Match;
- fun Parallel_PAR [(Const ("Cons",_) $ (Const ("Pair",_) $ (Const ("Some",_) $ t1 ) $ t2) $ Const ("Nil",_))] =
- (Syntax.const "_prg" $ t1 $ t2)
- | Parallel_PAR [(Const ("Cons",_) $ (Const ("Pair",_) $ (Const ("Some",_) $ t1) $ t2) $ ts)] =
- (Syntax.const "_prgs" $ t1 $ t2 $ Parallel_PAR [ts])
+ fun Parallel_PAR [(Const (@{const_syntax Cons}, _) $
+ (Const (@{const_syntax Pair}, _) $ (Const (@{const_syntax Some},_) $ t1 ) $ t2) $
+ Const (@{const_syntax Nil}, _))] = Syntax.const @{syntax_const "_prg"} $ t1 $ t2
+ | Parallel_PAR [(Const (@{const_syntax Cons}, _) $
+ (Const (@{const_syntax Pair}, _) $ (Const (@{const_syntax Some}, _) $ t1) $ t2) $ ts)] =
+ Syntax.const @{syntax_const "_prgs"} $ t1 $ t2 $ Parallel_PAR [ts]
| Parallel_PAR _ = raise Match;
-fun Parallel_tr' ts = Syntax.const "_PAR" $ Parallel_PAR ts;
+ fun Parallel_tr' ts = Syntax.const @{syntax_const "_PAR"} $ Parallel_PAR ts;
in
- [("Collect", assert_tr'), ("Basic", assign_tr'),
- ("Cond", bexp_tr' "_Cond"), ("While", bexp_tr' "_While_inv"),
- ("AnnBasic", annassign_tr'),
- ("AnnWhile", annbexp_tr' "_AnnWhile"), ("AnnAwait", annbexp_tr' "_AnnAwait"),
- ("AnnCond1", annbexp_tr' "_AnnCond1"), ("AnnCond2", annbexp_tr' "_AnnCond2")]
-
- end
-
+ [(@{const_syntax Collect}, assert_tr'),
+ (@{const_syntax Basic}, assign_tr'),
+ (@{const_syntax Cond}, bexp_tr' "_Cond"),
+ (@{const_syntax While}, bexp_tr' "_While_inv"),
+ (@{const_syntax AnnBasic}, annassign_tr'),
+ (@{const_syntax AnnWhile}, annbexp_tr' "_AnnWhile"),
+ (@{const_syntax AnnAwait}, annbexp_tr' "_AnnAwait"),
+ (@{const_syntax AnnCond1}, annbexp_tr' "_AnnCond1"),
+ (@{const_syntax AnnCond2}, annbexp_tr' "_AnnCond2")]
+ end;
*}
end
\ No newline at end of file
--- a/src/HOL/Hoare_Parallel/OG_Tran.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hoare_Parallel/OG_Tran.thy Thu Feb 11 23:50:38 2010 +0100
@@ -69,7 +69,7 @@
monos "rtrancl_mono"
-text {* The corresponding syntax translations are: *}
+text {* The corresponding abbreviations are: *}
abbreviation
ann_transition_n :: "('a ann_com_op \<times> 'a) \<Rightarrow> nat \<Rightarrow> ('a ann_com_op \<times> 'a)
@@ -101,8 +101,8 @@
SEM :: "'a com \<Rightarrow> 'a set \<Rightarrow> 'a set"
"SEM c S \<equiv> \<Union>sem c ` S "
-syntax "_Omega" :: "'a com" ("\<Omega>" 63)
-translations "\<Omega>" \<rightleftharpoons> "While CONST UNIV CONST UNIV (Basic id)"
+abbreviation Omega :: "'a com" ("\<Omega>" 63)
+ where "\<Omega> \<equiv> While UNIV UNIV (Basic id)"
consts fwhile :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> nat \<Rightarrow> 'a com"
primrec
--- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Thu Feb 11 23:50:38 2010 +0100
@@ -12,13 +12,13 @@
"_Assert" :: "'a \<Rightarrow> 'a set" ("(\<lbrace>_\<rbrace>)" [0] 1000)
translations
- ".{b}." \<rightharpoonup> "Collect \<guillemotleft>b\<guillemotright>"
+ ".{b}." \<rightharpoonup> "CONST Collect \<guillemotleft>b\<guillemotright>"
parse_translation {*
let
- fun quote_tr [t] = Syntax.quote_tr "_antiquote" t
+ fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t
| quote_tr ts = raise TERM ("quote_tr", ts);
- in [("_quote", quote_tr)] end
+ in [(@{syntax_const "_quote"}, quote_tr)] end
*}
end
\ No newline at end of file
--- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Thu Feb 11 23:50:38 2010 +0100
@@ -4,10 +4,13 @@
imports RG_Hoare Quote_Antiquote
begin
+abbreviation Skip :: "'a com" ("SKIP")
+ where "SKIP \<equiv> Basic id"
+
+notation Seq ("(_;;/ _)" [60,61] 60)
+
syntax
"_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61)
- "_skip" :: "'a com" ("SKIP")
- "_Seq" :: "'a com \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(_;;/ _)" [60,61] 60)
"_Cond" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(0IF _/ THEN _/ ELSE _/FI)" [0, 0, 0] 61)
"_Cond2" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(0IF _ THEN _ FI)" [0,0] 56)
"_While" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(0WHILE _ /DO _ /OD)" [0, 0] 61)
@@ -16,14 +19,12 @@
"_Wait" :: "'a bexp \<Rightarrow> 'a com" ("(0WAIT _ END)" 61)
translations
- "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (\<lambda>_. a))\<guillemotright>"
- "SKIP" \<rightleftharpoons> "Basic id"
- "c1;; c2" \<rightleftharpoons> "Seq c1 c2"
- "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2"
+ "\<acute>x := a" \<rightharpoonup> "CONST Basic \<guillemotleft>\<acute>(_update_name x (\<lambda>_. a))\<guillemotright>"
+ "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond .{b}. c1 c2"
"IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI"
- "WHILE b DO c OD" \<rightharpoonup> "While .{b}. c"
- "AWAIT b THEN c END" \<rightleftharpoons> "Await .{b}. c"
- "\<langle>c\<rangle>" \<rightleftharpoons> "AWAIT True THEN c END"
+ "WHILE b DO c OD" \<rightharpoonup> "CONST While .{b}. c"
+ "AWAIT b THEN c END" \<rightleftharpoons> "CONST Await .{b}. c"
+ "\<langle>c\<rangle>" \<rightleftharpoons> "AWAIT CONST True THEN c END"
"WAIT b END" \<rightleftharpoons> "AWAIT b THEN SKIP END"
nonterminals
@@ -52,18 +53,18 @@
"_after" :: "id \<Rightarrow> 'a" ("\<ordfeminine>_")
translations
- "\<ordmasculine>x" \<rightleftharpoons> "x \<acute>fst"
- "\<ordfeminine>x" \<rightleftharpoons> "x \<acute>snd"
+ "\<ordmasculine>x" \<rightleftharpoons> "x \<acute>CONST fst"
+ "\<ordfeminine>x" \<rightleftharpoons> "x \<acute>CONST snd"
print_translation {*
let
fun quote_tr' f (t :: ts) =
- Term.list_comb (f $ Syntax.quote_tr' "_antiquote" t, ts)
+ Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
| quote_tr' _ _ = raise Match;
- val assert_tr' = quote_tr' (Syntax.const "_Assert");
+ val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
- fun bexp_tr' name ((Const ("Collect", _) $ t) :: ts) =
+ fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) =
quote_tr' (Syntax.const name) (t :: ts)
| bexp_tr' _ _ = raise Match;
@@ -73,22 +74,26 @@
| NONE => raise Match);
fun update_name_tr' (Free x) = Free (upd_tr' x)
- | update_name_tr' ((c as Const ("_free", _)) $ Free x) =
+ | update_name_tr' ((c as Const (@{syntax_const "_free"}, _)) $ Free x) =
c $ Free (upd_tr' x)
| update_name_tr' (Const x) = Const (upd_tr' x)
| update_name_tr' _ = raise Match;
- fun K_tr' (Abs (_,_,t)) = if null (loose_bnos t) then t else raise Match
- | K_tr' (Abs (_,_,Abs (_,_,t)$Bound 0)) = if null (loose_bnos t) then t else raise Match
+ fun K_tr' (Abs (_, _, t)) =
+ if null (loose_bnos t) then t else raise Match
+ | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
+ if null (loose_bnos t) then t else raise Match
| K_tr' _ = raise Match;
fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
- quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
+ quote_tr' (Syntax.const @{syntax_const "_Assign"} $ update_name_tr' f)
(Abs (x, dummyT, K_tr' k) :: ts)
| assign_tr' _ = raise Match;
in
- [("Collect", assert_tr'), ("Basic", assign_tr'),
- ("Cond", bexp_tr' "_Cond"), ("While", bexp_tr' "_While_inv")]
+ [(@{const_syntax Collect}, assert_tr'),
+ (@{const_syntax Basic}, assign_tr'),
+ (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
+ (@{const_syntax While}, bexp_tr' @{syntax_const "_While"})]
end
*}
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Feb 11 23:50:38 2010 +0100
@@ -147,16 +147,16 @@
val v_used = fold_aterms
(fn Free (w, _) => (fn s => s orelse member (op =) vs w) | _ => I) g' false;
in if v_used then
- Const ("_bindM", dummyT) $ v $ f $ unfold_monad g'
+ Const (@{syntax_const "_bindM"}, dummyT) $ v $ f $ unfold_monad g'
else
- Const ("_chainM", dummyT) $ f $ unfold_monad g'
+ Const (@{syntax_const "_chainM"}, dummyT) $ f $ unfold_monad g'
end
| unfold_monad (Const (@{const_syntax chainM}, _) $ f $ g) =
- Const ("_chainM", dummyT) $ f $ unfold_monad g
+ Const (@{syntax_const "_chainM"}, dummyT) $ f $ unfold_monad g
| unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
let
val (v, g') = dest_abs_eta g;
- in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end
+ in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end
| unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
Const (@{const_syntax return}, dummyT) $ f
| unfold_monad f = f;
@@ -164,14 +164,17 @@
| contains_bindM (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
contains_bindM t;
fun bindM_monad_tr' (f::g::ts) = list_comb
- (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts);
- fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_bindM g' then list_comb
- (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
+ (Const (@{syntax_const "_do"}, dummyT) $
+ unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts);
+ fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
+ if contains_bindM g' then list_comb
+ (Const (@{syntax_const "_do"}, dummyT) $
+ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
else raise Match;
-in [
- (@{const_syntax bindM}, bindM_monad_tr'),
- (@{const_syntax Let}, Let_monad_tr')
-] end;
+in
+ [(@{const_syntax bindM}, bindM_monad_tr'),
+ (@{const_syntax Let}, Let_monad_tr')]
+end;
*}
--- a/src/HOL/Inductive.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Inductive.thy Thu Feb 11 23:50:38 2010 +0100
@@ -301,10 +301,9 @@
fun fun_tr ctxt [cs] =
let
val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
- val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr
- ctxt [x, cs]
+ val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs];
in lambda x ft end
-in [("_lam_pats_syntax", fun_tr)] end
+in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
*}
end
--- a/src/HOL/Isar_Examples/Hoare.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Isar_Examples/Hoare.thy Thu Feb 11 23:50:38 2010 +0100
@@ -237,9 +237,9 @@
parse_translation {*
let
- fun quote_tr [t] = Syntax.quote_tr "_antiquote" t
+ fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t
| quote_tr ts = raise TERM ("quote_tr", ts);
- in [("_quote", quote_tr)] end
+ in [(@{syntax_const "_quote"}, quote_tr)] end
*}
text {*
@@ -251,12 +251,12 @@
print_translation {*
let
fun quote_tr' f (t :: ts) =
- Term.list_comb (f $ Syntax.quote_tr' "_antiquote" t, ts)
+ Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
| quote_tr' _ _ = raise Match;
- val assert_tr' = quote_tr' (Syntax.const "_Assert");
+ val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
- fun bexp_tr' name ((Const ("Collect", _) $ t) :: ts) =
+ fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) =
quote_tr' (Syntax.const name) (t :: ts)
| bexp_tr' _ _ = raise Match;
@@ -266,7 +266,7 @@
| NONE => raise Match);
fun update_name_tr' (Free x) = Free (upd_tr' x)
- | update_name_tr' ((c as Const ("_free", _)) $ Free x) =
+ | update_name_tr' ((c as Const (@{syntax_const "_free"}, _)) $ Free x) =
c $ Free (upd_tr' x)
| update_name_tr' (Const x) = Const (upd_tr' x)
| update_name_tr' _ = raise Match;
@@ -276,12 +276,14 @@
| K_tr' _ = raise Match;
fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
- quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
+ quote_tr' (Syntax.const @{syntax_const "_Assign"} $ update_name_tr' f)
(Abs (x, dummyT, K_tr' k) :: ts)
| assign_tr' _ = raise Match;
in
- [("Collect", assert_tr'), ("Basic", assign_tr'),
- ("Cond", bexp_tr' "_Cond"), ("While", bexp_tr' "_While_inv")]
+ [(@{const_syntax Collect}, assert_tr'),
+ (@{const_syntax Basic}, assign_tr'),
+ (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
+ (@{const_syntax While}, bexp_tr' @{syntax_const "_While_inv"})]
end
*}
--- a/src/HOL/Library/Coinductive_List.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Library/Coinductive_List.thy Thu Feb 11 23:50:38 2010 +0100
@@ -204,7 +204,7 @@
LNil :: logic
LCons :: logic
translations
- "case p of LNil \<Rightarrow> a | LCons x l \<Rightarrow> b" \<rightleftharpoons> "CONST llist_case a (\<lambda>x l. b) p"
+ "case p of XCONST LNil \<Rightarrow> a | XCONST LCons x l \<Rightarrow> b" \<rightleftharpoons> "CONST llist_case a (\<lambda>x l. b) p"
lemma llist_case_LNil [simp, code]: "llist_case c d LNil = c"
by (simp add: llist_case_def LNil_def
--- a/src/HOL/Library/Numeral_Type.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Library/Numeral_Type.thy Thu Feb 11 23:50:38 2010 +0100
@@ -36,8 +36,8 @@
typed_print_translation {*
let
- fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_,[T,_]))] =
- Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T;
+ fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] =
+ Syntax.const @{syntax_const "_type_card"} $ Syntax.term_of_typ show_sorts T;
in [(@{const_syntax card}, card_univ_tr')]
end
*}
@@ -389,7 +389,7 @@
parse_translation {*
let
-
+(* FIXME @{type_syntax} *)
val num1_const = Syntax.const "Numeral_Type.num1";
val num0_const = Syntax.const "Numeral_Type.num0";
val B0_const = Syntax.const "Numeral_Type.bit0";
@@ -411,7 +411,7 @@
mk_bintype (the (Int.fromString str))
| numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
-in [("_NumeralType", numeral_tr)] end;
+in [(@{syntax_const "_NumeralType"}, numeral_tr)] end;
*}
print_translation {*
@@ -419,6 +419,7 @@
fun int_of [] = 0
| int_of (b :: bs) = b + 2 * int_of bs;
+(* FIXME @{type_syntax} *)
fun bin_of (Const ("num0", _)) = []
| bin_of (Const ("num1", _)) = [1]
| bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs
@@ -435,6 +436,7 @@
end
| bit_tr' b _ = raise Match;
+(* FIXME @{type_syntax} *)
in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end;
*}
--- a/src/HOL/Library/OptionalSugar.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Library/OptionalSugar.thy Thu Feb 11 23:50:38 2010 +0100
@@ -15,7 +15,7 @@
translations
"n" <= "CONST of_nat n"
"n" <= "CONST int n"
- "n" <= "real n"
+ "n" <= "CONST real n"
"n" <= "CONST real_of_nat n"
"n" <= "CONST real_of_int n"
"n" <= "CONST of_real n"
@@ -23,10 +23,10 @@
(* append *)
syntax (latex output)
- "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
+ "_appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
translations
- "appendL xs ys" <= "xs @ ys"
- "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
+ "_appendL xs ys" <= "xs @ ys"
+ "_appendL (_appendL xs ys) zs" <= "_appendL xs (_appendL ys zs)"
(* deprecated, use thm with style instead, will be removed *)
--- a/src/HOL/Library/State_Monad.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Library/State_Monad.thy Thu Feb 11 23:50:38 2010 +0100
@@ -159,15 +159,15 @@
fun unfold_monad (Const (@{const_syntax scomp}, _) $ f $ g) =
let
val (v, g') = dest_abs_eta g;
- in Const ("_scomp", dummyT) $ v $ f $ unfold_monad g' end
+ in Const (@{syntax_const "_scomp"}, dummyT) $ v $ f $ unfold_monad g' end
| unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
- Const ("_fcomp", dummyT) $ f $ unfold_monad g
+ Const (@{syntax_const "_fcomp"}, dummyT) $ f $ unfold_monad g
| unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
let
val (v, g') = dest_abs_eta g;
- in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end
+ in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end
| unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
- Const ("return", dummyT) $ f
+ Const (@{const_syntax "return"}, dummyT) $ f
| unfold_monad f = f;
fun contains_scomp (Const (@{const_syntax scomp}, _) $ _ $ _) = true
| contains_scomp (Const (@{const_syntax fcomp}, _) $ _ $ t) =
@@ -175,18 +175,23 @@
| contains_scomp (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
contains_scomp t;
fun scomp_monad_tr' (f::g::ts) = list_comb
- (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax scomp}, dummyT) $ f $ g), ts);
- fun fcomp_monad_tr' (f::g::ts) = if contains_scomp g then list_comb
- (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax fcomp}, dummyT) $ f $ g), ts)
+ (Const (@{syntax_const "_do"}, dummyT) $
+ unfold_monad (Const (@{const_syntax scomp}, dummyT) $ f $ g), ts);
+ fun fcomp_monad_tr' (f::g::ts) =
+ if contains_scomp g then list_comb
+ (Const (@{syntax_const "_do"}, dummyT) $
+ unfold_monad (Const (@{const_syntax fcomp}, dummyT) $ f $ g), ts)
else raise Match;
- fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_scomp g' then list_comb
- (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
+ fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
+ if contains_scomp g' then list_comb
+ (Const (@{syntax_const "_do"}, dummyT) $
+ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
else raise Match;
-in [
- (@{const_syntax scomp}, scomp_monad_tr'),
+in
+ [(@{const_syntax scomp}, scomp_monad_tr'),
(@{const_syntax fcomp}, fcomp_monad_tr'),
- (@{const_syntax Let}, Let_monad_tr')
-] end;
+ (@{const_syntax Let}, Let_monad_tr')]
+end;
*}
text {*
--- a/src/HOL/List.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/List.thy Thu Feb 11 23:50:38 2010 +0100
@@ -15,13 +15,14 @@
syntax
-- {* list Enumeration *}
- "@list" :: "args => 'a list" ("[(_)]")
+ "_list" :: "args => 'a list" ("[(_)]")
translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
-subsection{*Basic list processing functions*}
+
+subsection {* Basic list processing functions *}
primrec
hd :: "'a list \<Rightarrow> 'a" where
@@ -68,15 +69,15 @@
syntax
-- {* Special syntax for filter *}
- "@filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])")
+ "_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])")
translations
"[x<-xs . P]"== "CONST filter (%x. P) xs"
syntax (xsymbols)
- "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
+ "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
syntax (HTML output)
- "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
+ "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
primrec
foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where
@@ -132,7 +133,7 @@
"_LUpdate" :: "['a, lupdbinds] => 'a" ("_/[(_)]" [900,0] 900)
translations
- "_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs"
+ "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
"xs[i:=x]" == "CONST list_update xs i x"
primrec
@@ -363,45 +364,52 @@
val mapC = Syntax.const @{const_name map};
val concatC = Syntax.const @{const_name concat};
val IfC = Syntax.const @{const_name If};
+
fun singl x = ConsC $ x $ NilC;
- fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
+ fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
let
val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
val e = if opti then singl e else e;
- val case1 = Syntax.const "_case1" $ p $ e;
- val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
- $ NilC;
- val cs = Syntax.const "_case2" $ case1 $ case2
- val ft = Datatype_Case.case_tr false Datatype.info_of_constr
- ctxt [x, cs]
+ val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
+ val case2 = Syntax.const @{syntax_const "_case1"} $ Syntax.const Term.dummy_patternN $ NilC;
+ val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
+ val ft = Datatype_Case.case_tr false Datatype.info_of_constr ctxt [x, cs];
in lambda x ft end;
fun abs_tr ctxt (p as Free(s,T)) e opti =
- let val thy = ProofContext.theory_of ctxt;
- val s' = Sign.intern_const thy s
- in if Sign.declared_const thy s'
- then (pat_tr ctxt p e opti, false)
- else (lambda p e, true)
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val s' = Sign.intern_const thy s;
+ in
+ if Sign.declared_const thy s'
+ then (pat_tr ctxt p e opti, false)
+ else (lambda p e, true)
end
| abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);
- fun lc_tr ctxt [e, Const("_lc_test",_)$b, qs] =
- let val res = case qs of Const("_lc_end",_) => singl e
- | Const("_lc_quals",_)$q$qs => lc_tr ctxt [e,q,qs];
+ fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] =
+ let
+ val res =
+ (case qs of
+ Const (@{syntax_const "_lc_end"}, _) => singl e
+ | Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]);
in IfC $ b $ res $ NilC end
- | lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_end",_)] =
+ | lc_tr ctxt
+ [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
+ Const(@{syntax_const "_lc_end"}, _)] =
(case abs_tr ctxt p e true of
- (f,true) => mapC $ f $ es
- | (f, false) => concatC $ (mapC $ f $ es))
- | lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_quals",_)$q$qs] =
- let val e' = lc_tr ctxt [e,q,qs];
- in concatC $ (mapC $ (fst(abs_tr ctxt p e' false)) $ es) end
-
-in [("_listcompr", lc_tr)] end
+ (f, true) => mapC $ f $ es
+ | (f, false) => concatC $ (mapC $ f $ es))
+ | lc_tr ctxt
+ [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
+ Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] =
+ let val e' = lc_tr ctxt [e, q, qs];
+ in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end;
+
+in [(@{syntax_const "_listcompr"}, lc_tr)] end
*}
-(*
term "[(x,y,z). b]"
term "[(x,y,z). x\<leftarrow>xs]"
term "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]"
@@ -418,9 +426,11 @@
term "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"
term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"
term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"
+(*
term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"
*)
+
subsubsection {* @{const Nil} and @{const Cons} *}
lemma not_Cons_self [simp]:
@@ -1019,6 +1029,7 @@
"set xs - {y} = set (filter (\<lambda>x. \<not> (x = y)) xs)"
by (induct xs) auto
+
subsubsection {* @{text filter} *}
lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
@@ -1200,6 +1211,7 @@
declare partition.simps[simp del]
+
subsubsection {* @{text concat} *}
lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
@@ -2074,6 +2086,7 @@
qed simp
qed simp
+
subsubsection {* @{text list_all2} *}
lemma list_all2_lengthD [intro?]:
@@ -2413,6 +2426,7 @@
unfolding SUPR_def set_map [symmetric] Sup_set_fold foldl_map
by (simp add: sup_commute)
+
subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
@@ -2835,6 +2849,7 @@
from length_remdups_concat[of "[xs]"] show ?thesis unfolding xs by simp
qed
+
subsubsection {* @{const insert} *}
lemma in_set_insert [simp]:
@@ -3254,7 +3269,8 @@
apply auto
done
-subsubsection{*Transpose*}
+
+subsubsection {* Transpose *}
function transpose where
"transpose [] = []" |
@@ -3366,6 +3382,7 @@
by (simp add: nth_transpose filter_map comp_def)
qed
+
subsubsection {* (In)finiteness *}
lemma finite_maxlen:
@@ -3407,7 +3424,7 @@
done
-subsection {*Sorting*}
+subsection {* Sorting *}
text{* Currently it is not shown that @{const sort} returns a
permutation of its input because the nicest proof is via multisets,
@@ -3626,7 +3643,8 @@
apply(simp add:sorted_Cons)
done
-subsubsection {*@{const transpose} on sorted lists*}
+
+subsubsection {* @{const transpose} on sorted lists *}
lemma sorted_transpose[simp]:
shows "sorted (rev (map length (transpose xs)))"
@@ -3774,6 +3792,7 @@
by (auto simp: nth_transpose intro: nth_equalityI)
qed
+
subsubsection {* @{text sorted_list_of_set} *}
text{* This function maps (finite) linearly ordered sets to sorted
@@ -3805,6 +3824,7 @@
end
+
subsubsection {* @{text lists}: the list-forming operator over sets *}
inductive_set
@@ -3864,8 +3884,7 @@
by auto
-
-subsubsection{* Inductive definition for membership *}
+subsubsection {* Inductive definition for membership *}
inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
where
@@ -3881,8 +3900,7 @@
done
-
-subsubsection{*Lists as Cartesian products*}
+subsubsection {* Lists as Cartesian products *}
text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
@{term A} and tail drawn from @{term Xs}.*}
@@ -3903,7 +3921,7 @@
| "listset (A # As) = set_Cons A (listset As)"
-subsection{*Relations on Lists*}
+subsection {* Relations on Lists *}
subsubsection {* Length Lexicographic Ordering *}
@@ -4108,7 +4126,7 @@
by auto
-subsubsection{*Lifting a Relation on List Elements to the Lists*}
+subsubsection {* Lifting a Relation on List Elements to the Lists *}
inductive_set
listrel :: "('a * 'a)set => ('a list * 'a list)set"
--- a/src/HOL/Map.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Map.thy Thu Feb 11 23:50:38 2010 +0100
@@ -68,7 +68,7 @@
translations
"_MapUpd m (_Maplets xy ms)" == "_MapUpd (_MapUpd m xy) ms"
- "_MapUpd m (_maplet x y)" == "m(x:=Some y)"
+ "_MapUpd m (_maplet x y)" == "m(x := CONST Some y)"
"_Map ms" == "_MapUpd (CONST empty) ms"
"_Map (_Maplets ms1 ms2)" <= "_MapUpd (_Map ms1) ms2"
"_Maplets ms1 (_Maplets ms2 ms3)" <= "_Maplets (_Maplets ms1 ms2) ms3"
--- a/src/HOL/Metis_Examples/Message.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Metis_Examples/Message.thy Thu Feb 11 23:50:38 2010 +0100
@@ -45,10 +45,10 @@
text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
syntax
- "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
+ "_MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
syntax (xsymbols)
- "@MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+ "_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
translations
"{|x, y, z|}" == "{|x, {|y, z|}|}"
--- a/src/HOL/MicroJava/DFA/Product.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/MicroJava/DFA/Product.thy Thu Feb 11 23:50:38 2010 +0100
@@ -19,9 +19,10 @@
esl :: "'a esl \<Rightarrow> 'b esl \<Rightarrow> ('a * 'b ) esl"
"esl == %(A,rA,fA) (B,rB,fB). (A <*> B, le rA rB, sup fA fB)"
-syntax "@lesubprod" :: "'a*'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'b \<Rightarrow> bool"
+abbreviation
+ lesubprod_sntax :: "'a * 'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'a * 'b \<Rightarrow> bool"
("(_ /<='(_,_') _)" [50, 0, 0, 51] 50)
-translations "p <=(rA,rB) q" == "p <=_(Product.le rA rB) q"
+ where "p <=(rA,rB) q == p <=_(le rA rB) q"
lemma unfold_lesub_prod:
"p <=(rA,rB) q == le rA rB p q"
--- a/src/HOL/MicroJava/DFA/Semilat.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/MicroJava/DFA/Semilat.thy Thu Feb 11 23:50:38 2010 +0100
@@ -33,9 +33,9 @@
"plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
(*<*)
(* allow \<sub> instead of \<bsub>..\<esub> *)
- "@lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
- "@lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
- "@plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
+ "_lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
+ "_lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
+ "_plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
translations
"x \<sqsubseteq>\<^sub>r y" => "x \<sqsubseteq>\<^bsub>r\<^esub> y"
--- a/src/HOL/MicroJava/DFA/SemilatAlg.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/MicroJava/DFA/SemilatAlg.thy Thu Feb 11 23:50:38 2010 +0100
@@ -15,7 +15,7 @@
"x <=|r| y \<equiv> \<forall>(p,s) \<in> set x. \<exists>s'. (p,s') \<in> set y \<and> s <=_r s'"
consts
- "@plusplussub" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
+ plusplussub :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
primrec
"[] ++_f y = y"
"(x#xs) ++_f y = xs ++_f (x +_f y)"
--- a/src/HOL/Modelcheck/MuckeSyn.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Modelcheck/MuckeSyn.thy Thu Feb 11 23:50:38 2010 +0100
@@ -38,7 +38,7 @@
"_idts" :: "[idt, idts] => idts" ("_,/ _" [1, 0] 0)
"_tuple" :: "'a => tuple_args => 'a * 'b" ("(1_,/ _)")
-(* "@pttrn" :: "[pttrn, pttrns] => pttrn" ("_,/ _" [1, 0] 0)
+(* "_pttrn" :: "[pttrn, pttrns] => pttrn" ("_,/ _" [1, 0] 0)
"_pattern" :: "[pttrn, patterns] => pttrn" ("_,/ _" [1, 0] 0) *)
"_decl" :: "[mutype,pttrn] => decl" ("_ _")
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Feb 11 23:50:38 2010 +0100
@@ -27,14 +27,14 @@
parse_translation {*
let
- fun cart t u = Syntax.const @{type_name cart} $ t $ u
+ fun cart t u = Syntax.const @{type_name cart} $ t $ u; (* FIXME @{type_syntax} *)
fun finite_cart_tr [t, u as Free (x, _)] =
- if Syntax.is_tid x
- then cart t (Syntax.const "_ofsort" $ u $ Syntax.const (hd @{sort finite}))
+ if Syntax.is_tid x then
+ cart t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const (hd @{sort finite}))
else cart t u
| finite_cart_tr [t, u] = cart t u
in
- [("_finite_cart", finite_cart_tr)]
+ [(@{syntax_const "_finite_cart"}, finite_cart_tr)]
end
*}
--- a/src/HOL/Orderings.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Orderings.thy Thu Feb 11 23:50:38 2010 +0100
@@ -646,25 +646,30 @@
val less_eq = @{const_syntax less_eq};
val trans =
- [((All_binder, impl, less), ("_All_less", "_All_greater")),
- ((All_binder, impl, less_eq), ("_All_less_eq", "_All_greater_eq")),
- ((Ex_binder, conj, less), ("_Ex_less", "_Ex_greater")),
- ((Ex_binder, conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))];
+ [((All_binder, impl, less),
+ (@{syntax_const "_All_less"}, @{syntax_const "_All_greater"})),
+ ((All_binder, impl, less_eq),
+ (@{syntax_const "_All_less_eq"}, @{syntax_const "_All_greater_eq"})),
+ ((Ex_binder, conj, less),
+ (@{syntax_const "_Ex_less"}, @{syntax_const "_Ex_greater"})),
+ ((Ex_binder, conj, less_eq),
+ (@{syntax_const "_Ex_less_eq"}, @{syntax_const "_Ex_greater_eq"}))];
- fun matches_bound v t =
- case t of (Const ("_bound", _) $ Free (v', _)) => (v = v')
- | _ => false
- fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false)
- fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P
+ fun matches_bound v t =
+ (case t of
+ Const ("_bound", _) $ Free (v', _) => v = v'
+ | _ => false);
+ fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
+ fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P;
fun tr' q = (q,
fn [Const ("_bound", _) $ Free (v, _), Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
- (case AList.lookup (op =) trans (q, c, d) of
- NONE => raise Match
- | SOME (l, g) =>
- if matches_bound v t andalso not (contains_var v u) then mk v l u P
- else if matches_bound v u andalso not (contains_var v t) then mk v g t P
- else raise Match)
+ (case AList.lookup (op =) trans (q, c, d) of
+ NONE => raise Match
+ | SOME (l, g) =>
+ if matches_bound v t andalso not (contains_var v u) then mk v l u P
+ else if matches_bound v u andalso not (contains_var v t) then mk v g t P
+ else raise Match)
| _ => raise Match);
in [tr' All_binder, tr' Ex_binder] end
*}
--- a/src/HOL/Product_Type.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Product_Type.thy Thu Feb 11 23:50:38 2010 +0100
@@ -180,65 +180,81 @@
"_patterns" :: "[pttrn, patterns] => patterns" ("_,/ _")
translations
- "(x, y)" == "Pair x y"
+ "(x, y)" == "CONST Pair x y"
"_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))"
- "%(x,y,zs).b" == "split(%x (y,zs).b)"
- "%(x,y).b" == "split(%x y. b)"
- "_abs (Pair x y) t" => "%(x,y).t"
+ "%(x, y, zs). b" == "CONST split (%x (y, zs). b)"
+ "%(x, y). b" == "CONST split (%x y. b)"
+ "_abs (CONST Pair x y) t" => "%(x, y). t"
(* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
-(* reconstructs pattern from (nested) splits, avoiding eta-contraction of body*)
-(* works best with enclosing "let", if "let" does not avoid eta-contraction *)
+(*reconstruct pattern from (nested) splits, avoiding eta-contraction of body;
+ works best with enclosing "let", if "let" does not avoid eta-contraction*)
print_translation {*
-let fun split_tr' [Abs (x,T,t as (Abs abs))] =
- (* split (%x y. t) => %(x,y) t *)
- let val (y,t') = atomic_abs_tr' abs;
- val (x',t'') = atomic_abs_tr' (x,T,t');
-
- in Syntax.const "_abs" $ (Syntax.const "_pattern" $x'$y) $ t'' end
- | split_tr' [Abs (x,T,(s as Const ("split",_)$t))] =
- (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
- let val (Const ("_abs",_)$(Const ("_pattern",_)$y$z)$t') = split_tr' [t];
- val (x',t'') = atomic_abs_tr' (x,T,t');
- in Syntax.const "_abs"$
- (Syntax.const "_pattern"$x'$(Syntax.const "_patterns"$y$z))$t'' end
- | split_tr' [Const ("split",_)$t] =
- (* split (split (%x y z. t)) => %((x,y),z). t *)
- split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
- | split_tr' [Const ("_abs",_)$x_y$(Abs abs)] =
- (* split (%pttrn z. t) => %(pttrn,z). t *)
- let val (z,t) = atomic_abs_tr' abs;
- in Syntax.const "_abs" $ (Syntax.const "_pattern" $x_y$z) $ t end
- | split_tr' _ = raise Match;
-in [("split", split_tr')]
-end
+let
+ fun split_tr' [Abs (x, T, t as (Abs abs))] =
+ (* split (%x y. t) => %(x,y) t *)
+ let
+ val (y, t') = atomic_abs_tr' abs;
+ val (x', t'') = atomic_abs_tr' (x, T, t');
+ in
+ Syntax.const @{syntax_const "_abs"} $
+ (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
+ end
+ | split_tr' [Abs (x, T, (s as Const (@{const_syntax split}, _) $ t))] =
+ (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
+ let
+ val Const (@{syntax_const "_abs"}, _) $
+ (Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' = split_tr' [t];
+ val (x', t'') = atomic_abs_tr' (x, T, t');
+ in
+ Syntax.const @{syntax_const "_abs"} $
+ (Syntax.const @{syntax_const "_pattern"} $ x' $
+ (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t''
+ end
+ | split_tr' [Const (@{const_syntax split}, _) $ t] =
+ (* split (split (%x y z. t)) => %((x, y), z). t *)
+ split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
+ | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
+ (* split (%pttrn z. t) => %(pttrn,z). t *)
+ let val (z, t) = atomic_abs_tr' abs in
+ Syntax.const @{syntax_const "_abs"} $
+ (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
+ end
+ | split_tr' _ = raise Match;
+in [(@{const_syntax split}, split_tr')] end
*}
(* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *)
typed_print_translation {*
let
- fun split_guess_names_tr' _ T [Abs (x,_,Abs _)] = raise Match
- | split_guess_names_tr' _ T [Abs (x,xT,t)] =
+ fun split_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match
+ | split_guess_names_tr' _ T [Abs (x, xT, t)] =
(case (head_of t) of
- Const ("split",_) => raise Match
- | _ => let
- val (_::yT::_) = binder_types (domain_type T) handle Bind => raise Match;
- val (y,t') = atomic_abs_tr' ("y",yT,(incr_boundvars 1 t)$Bound 0);
- val (x',t'') = atomic_abs_tr' (x,xT,t');
- in Syntax.const "_abs" $ (Syntax.const "_pattern" $x'$y) $ t'' end)
+ Const (@{const_syntax split}, _) => raise Match
+ | _ =>
+ let
+ val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
+ val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
+ val (x', t'') = atomic_abs_tr' (x, xT, t');
+ in
+ Syntax.const @{syntax_const "_abs"} $
+ (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
+ end)
| split_guess_names_tr' _ T [t] =
- (case (head_of t) of
- Const ("split",_) => raise Match
- | _ => let
- val (xT::yT::_) = binder_types (domain_type T) handle Bind => raise Match;
- val (y,t') =
- atomic_abs_tr' ("y",yT,(incr_boundvars 2 t)$Bound 1$Bound 0);
- val (x',t'') = atomic_abs_tr' ("x",xT,t');
- in Syntax.const "_abs" $ (Syntax.const "_pattern" $x'$y) $ t'' end)
+ (case head_of t of
+ Const (@{const_syntax split}, _) => raise Match
+ | _ =>
+ let
+ val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
+ val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
+ val (x', t'') = atomic_abs_tr' ("x", xT, t');
+ in
+ Syntax.const @{syntax_const "_abs"} $
+ (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
+ end)
| split_guess_names_tr' _ _ _ = raise Match;
-in [("split", split_guess_names_tr')]
-end
+in [(@{const_syntax split}, split_guess_names_tr')] end
*}
@@ -855,10 +871,9 @@
Times (infixr "\<times>" 80)
syntax
- "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
-
+ "_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
translations
- "SIGMA x:A. B" == "Product_Type.Sigma A (%x. B)"
+ "SIGMA x:A. B" == "CONST Sigma A (%x. B)"
lemma SigmaI [intro!]: "[| a:A; b:B(a) |] ==> (a,b) : Sigma A B"
by (unfold Sigma_def) blast
--- a/src/HOL/Prolog/Test.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Prolog/Test.thy Thu Feb 11 23:50:38 2010 +0100
@@ -18,7 +18,7 @@
syntax
(* list Enumeration *)
- "@list" :: "args => 'a list" ("[(_)]")
+ "_list" :: "args => 'a list" ("[(_)]")
translations
"[x, xs]" == "x#[xs]"
--- a/src/HOL/Set.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Set.thy Thu Feb 11 23:50:38 2010 +0100
@@ -48,20 +48,16 @@
text {* Set comprehensions *}
syntax
- "@Coll" :: "pttrn => bool => 'a set" ("(1{_./ _})")
-
+ "_Coll" :: "pttrn => bool => 'a set" ("(1{_./ _})")
translations
- "{x. P}" == "Collect (%x. P)"
+ "{x. P}" == "CONST Collect (%x. P)"
syntax
- "@SetCompr" :: "'a => idts => bool => 'a set" ("(1{_ |/_./ _})")
- "@Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ :/ _./ _})")
-
+ "_Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ :/ _./ _})")
syntax (xsymbols)
- "@Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ \<in>/ _./ _})")
-
+ "_Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ \<in>/ _./ _})")
translations
- "{x:A. P}" => "{x. x:A & P}"
+ "{x:A. P}" => "{x. x:A & P}"
lemma mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)"
by (simp add: Collect_def mem_def)
@@ -107,11 +103,10 @@
insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
syntax
- "@Finset" :: "args => 'a set" ("{(_)}")
-
+ "_Finset" :: "args => 'a set" ("{(_)}")
translations
- "{x, xs}" == "CONST insert x {xs}"
- "{x}" == "CONST insert x {}"
+ "{x, xs}" == "CONST insert x {xs}"
+ "{x}" == "CONST insert x {}"
subsection {* Subsets and bounded quantifiers *}
@@ -191,9 +186,9 @@
"_Bex1" :: "pttrn => 'a set => bool => bool" ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
translations
- "ALL x:A. P" == "Ball A (%x. P)"
- "EX x:A. P" == "Bex A (%x. P)"
- "EX! x:A. P" => "EX! x. x:A & P"
+ "ALL x:A. P" == "CONST Ball A (%x. P)"
+ "EX x:A. P" == "CONST Bex A (%x. P)"
+ "EX! x:A. P" => "EX! x. x:A & P"
"LEAST x:A. P" => "LEAST x. x:A & P"
syntax (output)
@@ -233,31 +228,34 @@
print_translation {*
let
- val Type (set_type, _) = @{typ "'a set"};
- val All_binder = Syntax.binder_name @{const_syntax "All"};
- val Ex_binder = Syntax.binder_name @{const_syntax "Ex"};
+ val Type (set_type, _) = @{typ "'a set"}; (* FIXME 'a => bool (!?!) *)
+ val All_binder = Syntax.binder_name @{const_syntax All};
+ val Ex_binder = Syntax.binder_name @{const_syntax Ex};
val impl = @{const_syntax "op -->"};
val conj = @{const_syntax "op &"};
- val sbset = @{const_syntax "subset"};
- val sbset_eq = @{const_syntax "subset_eq"};
+ val sbset = @{const_syntax subset};
+ val sbset_eq = @{const_syntax subset_eq};
val trans =
- [((All_binder, impl, sbset), "_setlessAll"),
- ((All_binder, impl, sbset_eq), "_setleAll"),
- ((Ex_binder, conj, sbset), "_setlessEx"),
- ((Ex_binder, conj, sbset_eq), "_setleEx")];
+ [((All_binder, impl, sbset), @{syntax_const "_setlessAll"}),
+ ((All_binder, impl, sbset_eq), @{syntax_const "_setleAll"}),
+ ((Ex_binder, conj, sbset), @{syntax_const "_setlessEx"}),
+ ((Ex_binder, conj, sbset_eq), @{syntax_const "_setleEx"})];
fun mk v v' c n P =
if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
then Syntax.const c $ Syntax.mark_bound v' $ n $ P else raise Match;
fun tr' q = (q,
- fn [Const ("_bound", _) $ Free (v, Type (T, _)), Const (c, _) $ (Const (d, _) $ (Const ("_bound", _) $ Free (v', _)) $ n) $ P] =>
- if T = (set_type) then case AList.lookup (op =) trans (q, c, d)
- of NONE => raise Match
- | SOME l => mk v v' l n P
- else raise Match
- | _ => raise Match);
+ fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (T, _)),
+ Const (c, _) $
+ (Const (d, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (v', _)) $ n) $ P] =>
+ if T = set_type then
+ (case AList.lookup (op =) trans (q, c, d) of
+ NONE => raise Match
+ | SOME l => mk v v' l n P)
+ else raise Match
+ | _ => raise Match);
in
[tr' All_binder, tr' Ex_binder]
end
@@ -270,55 +268,63 @@
only translated if @{text "[0..n] subset bvs(e)"}.
*}
+syntax
+ "_Setcompr" :: "'a => idts => bool => 'a set" ("(1{_ |/_./ _})")
+
parse_translation {*
let
- val ex_tr = snd (mk_binder_tr ("EX ", "Ex"));
+ val ex_tr = snd (mk_binder_tr ("EX ", @{const_syntax Ex}));
- fun nvars (Const ("_idts", _) $ _ $ idts) = nvars idts + 1
+ fun nvars (Const (@{syntax_const "_idts"}, _) $ _ $ idts) = nvars idts + 1
| nvars _ = 1;
fun setcompr_tr [e, idts, b] =
let
- val eq = Syntax.const "op =" $ Bound (nvars idts) $ e;
- val P = Syntax.const "op &" $ eq $ b;
+ val eq = Syntax.const @{const_syntax "op ="} $ Bound (nvars idts) $ e;
+ val P = Syntax.const @{const_syntax "op &"} $ eq $ b;
val exP = ex_tr [idts, P];
- in Syntax.const "Collect" $ Term.absdummy (dummyT, exP) end;
+ in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
- in [("@SetCompr", setcompr_tr)] end;
+ in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end;
*}
-print_translation {* [
-Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} "_Ball",
-Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} "_Bex"
-] *} -- {* to avoid eta-contraction of body *}
+print_translation {*
+ [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
+ Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}]
+*} -- {* to avoid eta-contraction of body *}
print_translation {*
let
- val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY"));
+ val ex_tr' = snd (mk_binder_tr' (@{const_syntax Ex}, "DUMMY"));
fun setcompr_tr' [Abs (abs as (_, _, P))] =
let
- fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1)
- | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
+ fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
+ | check (Const (@{const_syntax "op &"}, _) $
+ (Const (@{const_syntax "op ="}, _) $ Bound m $ e) $ P, n) =
n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
- | check _ = false
+ | check _ = false;
fun tr' (_ $ abs) =
let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs]
- in Syntax.const "@SetCompr" $ e $ idts $ Q end;
- in if check (P, 0) then tr' P
- else let val (x as _ $ Free(xN,_), t) = atomic_abs_tr' abs
- val M = Syntax.const "@Coll" $ x $ t
- in case t of
- Const("op &",_)
- $ (Const("op :",_) $ (Const("_bound",_) $ Free(yN,_)) $ A)
- $ P =>
- if xN=yN then Syntax.const "@Collect" $ x $ A $ P else M
- | _ => M
- end
+ in Syntax.const @{syntax_const "_Setcompr"} $ e $ idts $ Q end;
+ in
+ if check (P, 0) then tr' P
+ else
+ let
+ val (x as _ $ Free(xN, _), t) = atomic_abs_tr' abs;
+ val M = Syntax.const @{syntax_const "_Coll"} $ x $ t;
+ in
+ case t of
+ Const (@{const_syntax "op &"}, _) $
+ (Const (@{const_syntax "op :"}, _) $
+ (Const (@{syntax_const "_bound"}, _) $ Free (yN, _)) $ A) $ P =>
+ if xN = yN then Syntax.const @{syntax_const "_Collect"} $ x $ A $ P else M
+ | _ => M
+ end
end;
- in [("Collect", setcompr_tr')] end;
+ in [(@{const_syntax Collect}, setcompr_tr')] end;
*}
setup {*
--- a/src/HOL/SetInterval.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/SetInterval.thy Thu Feb 11 23:50:38 2010 +0100
@@ -54,22 +54,22 @@
@{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well. *}
syntax
- "@UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3UN _<=_./ _)" 10)
- "@UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" 10)
- "@INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" 10)
- "@INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" 10)
+ "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3UN _<=_./ _)" 10)
+ "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" 10)
+ "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" 10)
+ "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" 10)
syntax (xsymbols)
- "@UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Union> _\<le>_./ _)" 10)
- "@UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Union> _<_./ _)" 10)
- "@INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter> _\<le>_./ _)" 10)
- "@INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter> _<_./ _)" 10)
+ "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Union> _\<le>_./ _)" 10)
+ "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Union> _<_./ _)" 10)
+ "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter> _\<le>_./ _)" 10)
+ "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter> _<_./ _)" 10)
syntax (latex output)
- "@UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ \<le> _)/ _)" 10)
- "@UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ < _)/ _)" 10)
- "@INTER_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ \<le> _)/ _)" 10)
- "@INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ < _)/ _)" 10)
+ "_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ \<le> _)/ _)" 10)
+ "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ < _)/ _)" 10)
+ "_INTER_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ \<le> _)/ _)" 10)
+ "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ < _)/ _)" 10)
translations
"UN i<=n. A" == "UN i:{..n}. A"
--- a/src/HOL/Statespace/StateFun.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Statespace/StateFun.thy Thu Feb 11 23:50:38 2010 +0100
@@ -1,5 +1,4 @@
(* Title: StateFun.thy
- ID: $Id$
Author: Norbert Schirmer, TU Muenchen
*)
@@ -34,12 +33,12 @@
lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
by (rule refl)
-constdefs lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
-"lookup destr n s \<equiv> destr (s n)"
+definition lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
+ where "lookup destr n s = destr (s n)"
-constdefs update::
+definition update::
"('v \<Rightarrow> 'a1) \<Rightarrow> ('a2 \<Rightarrow> 'v) \<Rightarrow> 'n \<Rightarrow> ('a1 \<Rightarrow> 'a2) \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> ('n \<Rightarrow> 'v)"
-"update destr constr n f s \<equiv> s(n := constr (f (destr (s n))))"
+ where "update destr constr n f s = s(n := constr (f (destr (s n))))"
lemma lookup_update_same:
"(\<And>v. destr (constr v) = v) \<Longrightarrow> lookup destr n (update destr constr n f s) =
--- a/src/HOL/Statespace/StateSpaceSyntax.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Statespace/StateSpaceSyntax.thy Thu Feb 11 23:50:38 2010 +0100
@@ -1,5 +1,4 @@
(* Title: StateSpaceSyntax.thy
- ID: $Id$
Author: Norbert Schirmer, TU Muenchen
*)
@@ -13,30 +12,27 @@
can choose if you want to use it or not. *}
syntax
- "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" ("_\<cdot>_" [60,60] 60)
- "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)"
- "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_<_>" [900,0] 900)
+ "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" ("_\<cdot>_" [60, 60] 60)
+ "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)"
+ "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_<_>" [900, 0] 900)
translations
- "_statespace_updates f (_updbinds b bs)" ==
- "_statespace_updates (_statespace_updates f b) bs"
- "s<x:=y>" == "_statespace_update s x y"
+ "_statespace_updates f (_updbinds b bs)" ==
+ "_statespace_updates (_statespace_updates f b) bs"
+ "s<x:=y>" == "_statespace_update s x y"
parse_translation (advanced)
{*
-[("_statespace_lookup",StateSpace.lookup_tr),
- ("_get",StateSpace.lookup_tr),
- ("_statespace_update",StateSpace.update_tr)]
+ [(@{syntax_const "_statespace_lookup"}, StateSpace.lookup_tr),
+ (@{syntax_const "_statespace_update"}, StateSpace.update_tr)]
*}
print_translation (advanced)
{*
-[("lookup",StateSpace.lookup_tr'),
- ("StateFun.lookup",StateSpace.lookup_tr'),
- ("update",StateSpace.update_tr'),
- ("StateFun.update",StateSpace.update_tr')]
+ [(@{const_syntax lookup}, StateSpace.lookup_tr'),
+ (@{const_syntax update}, StateSpace.update_tr')]
*}
-end
\ No newline at end of file
+end
--- a/src/HOL/String.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/String.thy Thu Feb 11 23:50:38 2010 +0100
@@ -5,7 +5,7 @@
theory String
imports List
uses
- "Tools/string_syntax.ML"
+ ("Tools/string_syntax.ML")
("Tools/string_code.ML")
begin
@@ -78,6 +78,7 @@
syntax
"_String" :: "xstr => string" ("_")
+use "Tools/string_syntax.ML"
setup StringSyntax.setup
definition chars :: string where
--- a/src/HOL/TLA/Action.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/TLA/Action.thy Thu Feb 11 23:50:38 2010 +0100
@@ -1,8 +1,6 @@
-(*
- File: TLA/Action.thy
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1998 University of Munich
+(* Title: HOL/TLA/Action.thy
+ Author: Stephan Merz
+ Copyright: 1998 University of Munich
*)
header {* The action level of TLA as an Isabelle theory *}
@@ -50,13 +48,13 @@
translations
"ACT A" => "(A::state*state => _)"
- "_before" == "before"
- "_after" == "after"
+ "_before" == "CONST before"
+ "_after" == "CONST after"
"_prime" => "_after"
- "_unchanged" == "unch"
- "_SqAct" == "SqAct"
- "_AnAct" == "AnAct"
- "_Enabled" == "enabled"
+ "_unchanged" == "CONST unch"
+ "_SqAct" == "CONST SqAct"
+ "_AnAct" == "CONST AnAct"
+ "_Enabled" == "CONST enabled"
"w |= [A]_v" <= "_SqAct A v w"
"w |= <A>_v" <= "_AnAct A v w"
"s |= Enabled A" <= "_Enabled A s"
--- a/src/HOL/TLA/Init.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/TLA/Init.thy Thu Feb 11 23:50:38 2010 +0100
@@ -1,11 +1,10 @@
-(*
- File: TLA/Init.thy
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1998 University of Munich
+(* Title: HOL/TLA/Init.thy
+ Author: Stephan Merz
+ Copyright: 1998 University of Munich
-Introduces type of temporal formulas. Defines interface between
-temporal formulas and its "subformulas" (state predicates and actions).
+Introduces type of temporal formulas. Defines interface between
+temporal formulas and its "subformulas" (state predicates and
+actions).
*)
theory Init
@@ -26,12 +25,12 @@
st2 :: "behavior => state"
syntax
- TEMP :: "lift => 'a" ("(TEMP _)")
+ "_TEMP" :: "lift => 'a" ("(TEMP _)")
"_Init" :: "lift => lift" ("(Init _)"[40] 50)
translations
"TEMP F" => "(F::behavior => _)"
- "_Init" == "Initial"
+ "_Init" == "CONST Initial"
"sigma |= Init F" <= "_Init F sigma"
defs
--- a/src/HOL/TLA/Intensional.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/TLA/Intensional.thy Thu Feb 11 23:50:38 2010 +0100
@@ -1,8 +1,6 @@
-(*
- File: TLA/Intensional.thy
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1998 University of Munich
+(* Title: HOL/TLA/Intensional.thy
+ Author: Stephan Merz
+ Copyright: 1998 University of Munich
*)
header {* A framework for "intensional" (possible-world based) logics
@@ -95,11 +93,11 @@
"_REx1" :: "[idts, lift] => lift" ("(3EX! _./ _)" [0, 10] 10)
translations
- "_const" == "const"
- "_lift" == "lift"
- "_lift2" == "lift2"
- "_lift3" == "lift3"
- "_Valid" == "Valid"
+ "_const" == "CONST const"
+ "_lift" == "CONST lift"
+ "_lift2" == "CONST lift2"
+ "_lift3" == "CONST lift3"
+ "_Valid" == "CONST Valid"
"_RAll x A" == "Rall x. A"
"_REx x A" == "Rex x. A"
"_REx1 x A" == "Rex! x. A"
@@ -112,11 +110,11 @@
"_liftEqu" == "_lift2 (op =)"
"_liftNeq u v" == "_liftNot (_liftEqu u v)"
- "_liftNot" == "_lift Not"
+ "_liftNot" == "_lift (CONST Not)"
"_liftAnd" == "_lift2 (op &)"
"_liftOr" == "_lift2 (op | )"
"_liftImp" == "_lift2 (op -->)"
- "_liftIf" == "_lift3 If"
+ "_liftIf" == "_lift3 (CONST If)"
"_liftPlus" == "_lift2 (op +)"
"_liftMinus" == "_lift2 (op -)"
"_liftTimes" == "_lift2 (op *)"
@@ -126,12 +124,12 @@
"_liftLeq" == "_lift2 (op <=)"
"_liftMem" == "_lift2 (op :)"
"_liftNotMem x xs" == "_liftNot (_liftMem x xs)"
- "_liftFinset (_liftargs x xs)" == "_lift2 CONST insert x (_liftFinset xs)"
- "_liftFinset x" == "_lift2 CONST insert x (_const {})"
+ "_liftFinset (_liftargs x xs)" == "_lift2 (CONST insert) x (_liftFinset xs)"
+ "_liftFinset x" == "_lift2 (CONST insert) x (_const {})"
"_liftPair x (_liftargs y z)" == "_liftPair x (_liftPair y z)"
- "_liftPair" == "_lift2 Pair"
- "_liftCons" == "lift2 Cons"
- "_liftApp" == "lift2 (op @)"
+ "_liftPair" == "_lift2 (CONST Pair)"
+ "_liftCons" == "CONST lift2 (CONST Cons)"
+ "_liftApp" == "CONST lift2 (op @)"
"_liftList (_liftargs x xs)" == "_liftCons x (_liftList xs)"
"_liftList x" == "_liftCons x (_const [])"
--- a/src/HOL/TLA/ROOT.ML Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/TLA/ROOT.ML Thu Feb 11 23:50:38 2010 +0100
@@ -1,7 +1,3 @@
-(* Title: HOL/TLA/ROOT.ML
-
-Adds the Temporal Logic of Actions to a database containing Isabelle/HOL.
-*)
+(* The Temporal Logic of Actions *)
use_thys ["TLA"];
-
--- a/src/HOL/TLA/Stfun.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/TLA/Stfun.thy Thu Feb 11 23:50:38 2010 +0100
@@ -1,8 +1,6 @@
-(*
- File: TLA/Stfun.thy
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1998 University of Munich
+(* Title: HOL/TLA/Stfun.thy
+ Author: Stephan Merz
+ Copyright: 1998 University of Munich
*)
header {* States and state functions for TLA as an "intensional" logic *}
@@ -42,7 +40,7 @@
translations
"PRED P" => "(P::state => _)"
- "_stvars" == "stvars"
+ "_stvars" == "CONST stvars"
defs
(* Base variables may be assigned arbitrary (type-correct) values.
--- a/src/HOL/TLA/TLA.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/TLA/TLA.thy Thu Feb 11 23:50:38 2010 +0100
@@ -1,8 +1,6 @@
-(*
- File: TLA/TLA.thy
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1998 University of Munich
+(* Title: HOL/TLA/TLA.thy
+ Author: Stephan Merz
+ Copyright: 1998 University of Munich
*)
header {* The temporal level of TLA *}
@@ -1168,4 +1166,3 @@
done
end
-
--- a/src/HOL/Tools/float_syntax.ML Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Tools/float_syntax.ML Thu Feb 11 23:50:38 2010 +0100
@@ -1,7 +1,6 @@
-(* ID: $Id$
- Authors: Tobias Nipkow, TU Muenchen
+(* Author: Tobias Nipkow, TU Muenchen
-Concrete syntax for floats
+Concrete syntax for floats.
*)
signature FLOAT_SYNTAX =
@@ -18,19 +17,21 @@
fun mk_number i =
let
- fun mk 0 = Syntax.const @{const_name Int.Pls}
- | mk ~1 = Syntax.const @{const_name Int.Min}
- | mk i = let val (q, r) = Integer.div_mod i 2
- in HOLogic.mk_bit r $ (mk q) end;
- in Syntax.const @{const_name Int.number_of} $ mk i end;
+ fun mk 0 = Syntax.const @{const_syntax Int.Pls}
+ | mk ~1 = Syntax.const @{const_syntax Int.Min}
+ | mk i =
+ let val (q, r) = Integer.div_mod i 2
+ in HOLogic.mk_bit r $ (mk q) end;
+ in Syntax.const @{const_syntax Int.number_of} $ mk i end;
fun mk_frac str =
let
- val {mant=i, exp = n} = Syntax.read_float str;
- val exp = Syntax.const @{const_name Power.power};
+ val {mant = i, exp = n} = Syntax.read_float str;
+ val exp = Syntax.const @{const_syntax Power.power};
val ten = mk_number 10;
- val exp10 = if n=1 then ten else exp $ ten $ (mk_number n);
- in (Syntax.const @{const_name divide}) $ (mk_number i) $ exp10 end
+ val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
+ in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end;
+
in
fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
@@ -42,6 +43,6 @@
(* theory setup *)
val setup =
- Sign.add_trfuns ([], [("_Float", float_tr)], [], []);
+ Sign.add_trfuns ([], [(@{syntax_const "_Float"}, float_tr)], [], []);
end;
--- a/src/HOL/Tools/numeral_syntax.ML Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Tools/numeral_syntax.ML Thu Feb 11 23:50:38 2010 +0100
@@ -27,7 +27,7 @@
in
fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] =
- Syntax.const @{const_name Int.number_of} $ mk_bin num
+ Syntax.const @{const_syntax Int.number_of} $ mk_bin num
| numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
end;
@@ -37,10 +37,10 @@
local
-fun dest_bin (Const (@{const_syntax "Int.Pls"}, _)) = []
- | dest_bin (Const (@{const_syntax "Int.Min"}, _)) = [~1]
- | dest_bin (Const (@{const_syntax "Int.Bit0"}, _) $ bs) = 0 :: dest_bin bs
- | dest_bin (Const (@{const_syntax "Int.Bit1"}, _) $ bs) = 1 :: dest_bin bs
+fun dest_bin (Const (@{const_syntax Int.Pls}, _)) = []
+ | dest_bin (Const (@{const_syntax Int.Min}, _)) = [~1]
+ | dest_bin (Const (@{const_syntax Int.Bit0}, _) $ bs) = 0 :: dest_bin bs
+ | dest_bin (Const (@{const_syntax Int.Bit1}, _) $ bs) = 1 :: dest_bin bs
| dest_bin _ = raise Match;
fun leading _ [] = 0
@@ -64,11 +64,12 @@
end;
fun syntax_numeral t =
- Syntax.const "_Numeral" $ (Syntax.const "_numeral" $ Syntax.free (dest_bin_str t));
+ Syntax.const @{syntax_const "_Numeral"} $
+ (Syntax.const @{syntax_const "_numeral"} $ Syntax.free (dest_bin_str t));
in
-fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
+fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) = (* FIXME @{type_syntax} *)
let val t' =
if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
@@ -84,7 +85,7 @@
(* theory setup *)
val setup =
- Sign.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
+ Sign.add_trfuns ([], [(@{syntax_const "_Numeral"}, numeral_tr)], [], []) #>
Sign.add_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
end;
--- a/src/HOL/Tools/string_syntax.ML Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Tools/string_syntax.ML Thu Feb 11 23:50:38 2010 +0100
@@ -30,7 +30,7 @@
fun mk_char s =
if Symbol.is_ascii s then
- Syntax.Appl [Syntax.Constant "Char", mk_nib (ord s div 16), mk_nib (ord s mod 16)]
+ Syntax.Appl [Syntax.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)]
else error ("Non-ASCII symbol: " ^ quote s);
val specials = explode "\\\"`'";
@@ -41,11 +41,13 @@
then c else raise Match
end;
-fun dest_char (Syntax.Appl [Syntax.Constant "Char", c1, c2]) = dest_chr c1 c2
+fun dest_char (Syntax.Appl [Syntax.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
| dest_char _ = raise Match;
fun syntax_string cs =
- Syntax.Appl [Syntax.Constant "_inner_string", Syntax.Variable (Syntax.implode_xstr cs)];
+ Syntax.Appl
+ [Syntax.Constant @{syntax_const "_inner_string"},
+ Syntax.Variable (Syntax.implode_xstr cs)];
fun char_ast_tr [Syntax.Variable xstr] =
@@ -54,24 +56,29 @@
| _ => error ("Single character expected: " ^ xstr))
| char_ast_tr asts = raise AST ("char_ast_tr", asts);
-fun char_ast_tr' [c1, c2] = Syntax.Appl [Syntax.Constant "_Char", syntax_string [dest_chr c1 c2]]
+fun char_ast_tr' [c1, c2] =
+ Syntax.Appl [Syntax.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]]
| char_ast_tr' _ = raise Match;
(* string *)
-fun mk_string [] = Syntax.Constant "Nil"
- | mk_string (c :: cs) = Syntax.Appl [Syntax.Constant "Cons", mk_char c, mk_string cs];
+fun mk_string [] = Syntax.Constant @{const_syntax Nil}
+ | mk_string (c :: cs) =
+ Syntax.Appl [Syntax.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
fun string_ast_tr [Syntax.Variable xstr] =
(case Syntax.explode_xstr xstr of
- [] => Syntax.Appl
- [Syntax.Constant Syntax.constrainC, Syntax.Constant "Nil", Syntax.Constant "string"]
+ [] =>
+ Syntax.Appl
+ [Syntax.Constant Syntax.constrainC,
+ Syntax.Constant @{const_syntax Nil}, Syntax.Constant "string"] (* FIXME @{type_syntax} *)
| cs => mk_string cs)
| string_ast_tr asts = raise AST ("string_tr", asts);
-fun list_ast_tr' [args] = Syntax.Appl [Syntax.Constant "_String",
- syntax_string (map dest_char (Syntax.unfold_ast "_args" args))]
+fun list_ast_tr' [args] =
+ Syntax.Appl [Syntax.Constant @{syntax_const "_String"},
+ syntax_string (map dest_char (Syntax.unfold_ast @{syntax_const "_args"} args))]
| list_ast_tr' ts = raise Match;
@@ -79,7 +86,7 @@
val setup =
Sign.add_trfuns
- ([("_Char", char_ast_tr), ("_String", string_ast_tr)], [], [],
- [("Char", char_ast_tr'), ("@list", list_ast_tr')]);
+ ([(@{syntax_const "_Char"}, char_ast_tr), (@{syntax_const "_String"}, string_ast_tr)], [], [],
+ [(@{const_syntax Char}, char_ast_tr'), (@{syntax_const "_list"}, list_ast_tr')]);
end;
--- a/src/HOL/Typerep.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/Typerep.thy Thu Feb 11 23:50:38 2010 +0100
@@ -17,22 +17,27 @@
end
-setup {*
+syntax
+ "_TYPEREP" :: "type => logic" ("(1TYPEREP/(1'(_')))")
+
+parse_translation {*
let
fun typerep_tr (*"_TYPEREP"*) [ty] =
- Lexicon.const @{const_syntax typerep} $ (Lexicon.const "_constrain" $ Lexicon.const "TYPE" $
- (Lexicon.const "itself" $ ty))
+ Syntax.const @{const_syntax typerep} $
+ (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
+ (Syntax.const "itself" $ ty)) (* FIXME @{type_syntax} *)
| typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
- fun typerep_tr' show_sorts (*"typerep"*)
+in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end
+*}
+
+typed_print_translation {*
+let
+ fun typerep_tr' show_sorts (*"typerep"*) (* FIXME @{type_syntax} *)
(Type ("fun", [Type ("itself", [T]), _])) (Const (@{const_syntax TYPE}, _) :: ts) =
- Term.list_comb (Lexicon.const "_TYPEREP" $ Syntax.term_of_typ show_sorts T, ts)
+ Term.list_comb
+ (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
| typerep_tr' _ T ts = raise Match;
-in
- Sign.add_syntax_i
- [("_TYPEREP", Simple_Syntax.read_typ "type => logic", Delimfix "(1TYPEREP/(1'(_')))")]
- #> Sign.add_trfuns ([], [("_TYPEREP", typerep_tr)], [], [])
- #> Sign.add_trfunsT [(@{const_syntax typerep}, typerep_tr')]
-end
+in [(@{const_syntax typerep}, typerep_tr')] end
*}
setup {*
--- a/src/HOL/ex/Antiquote.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/ex/Antiquote.thy Thu Feb 11 23:50:38 2010 +0100
@@ -1,11 +1,12 @@
(* Title: HOL/ex/Antiquote.thy
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
*)
header {* Antiquotations *}
-theory Antiquote imports Main begin
+theory Antiquote
+imports Main
+begin
text {*
A simple example on quote / antiquote in higher-order abstract
@@ -13,17 +14,23 @@
*}
syntax
- "_Expr" :: "'a => 'a" ("EXPR _" [1000] 999)
+ "_Expr" :: "'a => 'a" ("EXPR _" [1000] 999)
-constdefs
- var :: "'a => ('a => nat) => nat" ("VAR _" [1000] 999)
- "var x env == env x"
+definition
+ var :: "'a => ('a => nat) => nat" ("VAR _" [1000] 999)
+ where "var x env = env x"
+definition
Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
- "Expr exp env == exp env"
+ where "Expr exp env = exp env"
-parse_translation {* [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"] *}
-print_translation {* [Syntax.quote_antiquote_tr' "_Expr" "var" "Expr"] *}
+parse_translation {*
+ [Syntax.quote_antiquote_tr @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
+*}
+
+print_translation {*
+ [Syntax.quote_antiquote_tr' @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
+*}
term "EXPR (a + b + c)"
term "EXPR (a + b + c + VAR x + VAR y + 1)"
--- a/src/HOL/ex/Binary.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/ex/Binary.thy Thu Feb 11 23:50:38 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/ex/Binary.thy
- ID: $Id$
Author: Makarius
*)
@@ -21,8 +20,6 @@
unfolding bit_def by simp_all
ML {*
-structure Binary =
-struct
fun dest_bit (Const (@{const_name False}, _)) = 0
| dest_bit (Const (@{const_name True}, _)) = 1
| dest_bit t = raise TERM ("dest_bit", [t]);
@@ -43,7 +40,6 @@
else
let val (q, r) = Integer.div_mod n 2
in @{term bit} $ mk_binary q $ mk_bit r end;
-end
*}
@@ -126,7 +122,7 @@
fun binary_proc proc ss ct =
(case Thm.term_of ct of
_ $ t $ u =>
- (case try (pairself (`Binary.dest_binary)) (t, u) of
+ (case try (pairself (`dest_binary)) (t, u) of
SOME args => proc (Simplifier.the_context ss) args
| NONE => NONE)
| _ => NONE);
@@ -135,34 +131,34 @@
val less_eq_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
let val k = n - m in
if k >= 0 then
- SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (Binary.mk_binary k))])
+ SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (mk_binary k))])
else
SOME (@{thm binary_less_eq(2)} OF
- [prove ctxt (t == plus (plus u (Binary.mk_binary (~ k - 1))) (Binary.mk_binary 1))])
+ [prove ctxt (t == plus (plus u (mk_binary (~ k - 1))) (mk_binary 1))])
end);
val less_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
let val k = m - n in
if k >= 0 then
- SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (Binary.mk_binary k))])
+ SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (mk_binary k))])
else
SOME (@{thm binary_less(2)} OF
- [prove ctxt (u == plus (plus t (Binary.mk_binary (~ k - 1))) (Binary.mk_binary 1))])
+ [prove ctxt (u == plus (plus t (mk_binary (~ k - 1))) (mk_binary 1))])
end);
val diff_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
let val k = m - n in
if k >= 0 then
- SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (Binary.mk_binary k))])
+ SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (mk_binary k))])
else
- SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (Binary.mk_binary (~ k)))])
+ SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (mk_binary (~ k)))])
end);
fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
if n = 0 then NONE
else
let val (k, l) = Integer.div_mod m n
- in SOME (rule OF [prove ctxt (t == plus (mult u (Binary.mk_binary k)) (Binary.mk_binary l))]) end);
+ in SOME (rule OF [prove ctxt (t == plus (mult u (mk_binary k)) (mk_binary l))]) end);
end;
*}
@@ -194,17 +190,17 @@
parse_translation {*
let
-
-val syntax_consts = map_aterms (fn Const (c, T) => Const (Syntax.constN ^ c, T) | a => a);
+ val syntax_consts =
+ map_aterms (fn Const (c, T) => Const (Syntax.constN ^ c, T) | a => a);
-fun binary_tr [Const (num, _)] =
- let
- val {leading_zeros = z, value = n, ...} = Syntax.read_xnum num;
- val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
- in syntax_consts (Binary.mk_binary n) end
- | binary_tr ts = raise TERM ("binary_tr", ts);
+ fun binary_tr [Const (num, _)] =
+ let
+ val {leading_zeros = z, value = n, ...} = Syntax.read_xnum num;
+ val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
+ in syntax_consts (mk_binary n) end
+ | binary_tr ts = raise TERM ("binary_tr", ts);
-in [("_Binary", binary_tr)] end
+in [(@{syntax_const "_Binary"}, binary_tr)] end
*}
--- a/src/HOL/ex/Multiquote.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/ex/Multiquote.thy Thu Feb 11 23:50:38 2010 +0100
@@ -1,11 +1,12 @@
(* Title: HOL/ex/Multiquote.thy
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
*)
header {* Multiple nested quotations and anti-quotations *}
-theory Multiquote imports Main begin
+theory Multiquote
+imports Main
+begin
text {*
Multiple nested quotations and anti-quotations -- basically a
@@ -13,25 +14,25 @@
*}
syntax
- "_quote" :: "'b => ('a => 'b)" ("\<guillemotleft>_\<guillemotright>" [0] 1000)
- "_antiquote" :: "('a => 'b) => 'b" ("\<acute>_" [1000] 1000)
+ "_quote" :: "'b => ('a => 'b)" ("\<guillemotleft>_\<guillemotright>" [0] 1000)
+ "_antiquote" :: "('a => 'b) => 'b" ("\<acute>_" [1000] 1000)
parse_translation {*
let
- fun antiquote_tr i (Const ("_antiquote", _) $ (t as Const ("_antiquote", _) $ _)) =
- skip_antiquote_tr i t
- | antiquote_tr i (Const ("_antiquote", _) $ t) =
+ fun antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $
+ (t as Const (@{syntax_const "_antiquote"}, _) $ _)) = skip_antiquote_tr i t
+ | antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $ t) =
antiquote_tr i t $ Bound i
| antiquote_tr i (t $ u) = antiquote_tr i t $ antiquote_tr i u
| antiquote_tr i (Abs (x, T, t)) = Abs (x, T, antiquote_tr (i + 1) t)
| antiquote_tr _ a = a
- and skip_antiquote_tr i ((c as Const ("_antiquote", _)) $ t) =
+ and skip_antiquote_tr i ((c as Const (@{syntax_const "_antiquote"}, _)) $ t) =
c $ skip_antiquote_tr i t
| skip_antiquote_tr i t = antiquote_tr i t;
fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
| quote_tr ts = raise TERM ("quote_tr", ts);
- in [("_quote", quote_tr)] end
+ in [(@{syntax_const "_quote"}, quote_tr)] end
*}
text {* basic examples *}
--- a/src/HOL/ex/Numeral.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOL/ex/Numeral.thy Thu Feb 11 23:50:38 2010 +0100
@@ -311,7 +311,7 @@
orelse error ("Bad numeral: " ^ num);
in Const (@{const_name of_num}, @{typ num} --> dummyT) $ num_of_int value end
| numeral_tr ts = raise TERM ("numeral_tr", ts);
-in [("_Numerals", numeral_tr)] end
+in [(@{syntax_const "_Numerals"}, numeral_tr)] end
*}
typed_print_translation {*
@@ -325,9 +325,9 @@
fun num_tr' show_sorts T [n] =
let
val k = int_of_num' n;
- val t' = Syntax.const "_Numerals" $ Syntax.free ("#" ^ string_of_int k);
+ val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
in case T
- of Type ("fun", [_, T']) =>
+ of Type ("fun", [_, T']) => (* FIXME @{type_syntax} *)
if not (! show_types) andalso can Term.dest_Type T' then t'
else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
| T' => if T' = dummyT then t' else raise Match
--- a/src/HOLCF/Cfun.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOLCF/Cfun.thy Thu Feb 11 23:50:38 2010 +0100
@@ -40,8 +40,8 @@
syntax "_cabs" :: "'a"
parse_translation {*
-(* rewrites (_cabs x t) => (Abs_CFun (%x. t)) *)
- [mk_binder_tr ("_cabs", @{const_syntax Abs_CFun})];
+(* rewrite (_cabs x t) => (Abs_CFun (%x. t)) *)
+ [mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_CFun})];
*}
text {* To avoid eta-contraction of body: *}
@@ -49,13 +49,13 @@
let
fun cabs_tr' _ _ [Abs abs] = let
val (x,t) = atomic_abs_tr' abs
- in Syntax.const "_cabs" $ x $ t end
+ in Syntax.const @{syntax_const "_cabs"} $ x $ t end
| cabs_tr' _ T [t] = let
val xT = domain_type (domain_type T);
val abs' = ("x",xT,(incr_boundvars 1 t)$Bound 0);
val (x,t') = atomic_abs_tr' abs';
- in Syntax.const "_cabs" $ x $ t' end;
+ in Syntax.const @{syntax_const "_cabs"} $ x $ t' end;
in [(@{const_syntax Abs_CFun}, cabs_tr')] end;
*}
@@ -69,26 +69,28 @@
"_Lambda" :: "[cargs, 'a] \<Rightarrow> logic" ("(3\<Lambda> _./ _)" [1000, 10] 10)
parse_ast_translation {*
-(* rewrites (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *)
-(* cf. Syntax.lambda_ast_tr from Syntax/syn_trans.ML *)
+(* rewrite (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *)
+(* cf. Syntax.lambda_ast_tr from src/Pure/Syntax/syn_trans.ML *)
let
fun Lambda_ast_tr [pats, body] =
- Syntax.fold_ast_p "_cabs" (Syntax.unfold_ast "_cargs" pats, body)
+ Syntax.fold_ast_p @{syntax_const "_cabs"}
+ (Syntax.unfold_ast @{syntax_const "_cargs"} pats, body)
| Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts);
- in [("_Lambda", Lambda_ast_tr)] end;
+ in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
*}
print_ast_translation {*
-(* rewrites (_cabs x (_cabs y (_cabs z t))) => (LAM x y z. t) *)
-(* cf. Syntax.abs_ast_tr' from Syntax/syn_trans.ML *)
+(* rewrite (_cabs x (_cabs y (_cabs z t))) => (LAM x y z. t) *)
+(* cf. Syntax.abs_ast_tr' from src/Pure/Syntax/syn_trans.ML *)
let
fun cabs_ast_tr' asts =
- (case Syntax.unfold_ast_p "_cabs"
- (Syntax.Appl (Syntax.Constant "_cabs" :: asts)) of
+ (case Syntax.unfold_ast_p @{syntax_const "_cabs"}
+ (Syntax.Appl (Syntax.Constant @{syntax_const "_cabs"} :: asts)) of
([], _) => raise Syntax.AST ("cabs_ast_tr'", asts)
| (xs, body) => Syntax.Appl
- [Syntax.Constant "_Lambda", Syntax.fold_ast "_cargs" xs, body]);
- in [("_cabs", cabs_ast_tr')] end;
+ [Syntax.Constant @{syntax_const "_Lambda"},
+ Syntax.fold_ast @{syntax_const "_cargs"} xs, body]);
+ in [(@{syntax_const "_cabs"}, cabs_ast_tr')] end
*}
text {* Dummy patterns for continuous abstraction *}
--- a/src/HOLCF/Fixrec.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOLCF/Fixrec.thy Thu Feb 11 23:50:38 2010 +0100
@@ -226,10 +226,10 @@
"_variable _noargs r" => "CONST unit_when\<cdot>r"
parse_translation {*
-(* rewrites (_pat x) => (return) *)
-(* rewrites (_variable x t) => (Abs_CFun (%x. t)) *)
- [("_pat", K (Syntax.const "Fixrec.return")),
- mk_binder_tr ("_variable", "Abs_CFun")];
+(* rewrite (_pat x) => (return) *)
+(* rewrite (_variable x t) => (Abs_CFun (%x. t)) *)
+ [(@{syntax_const "_pat"}, fn _ => Syntax.const @{const_syntax Fixrec.return}),
+ mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_CFun})];
*}
text {* Printing Case expressions *}
@@ -240,23 +240,26 @@
print_translation {*
let
fun dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax unit_when},_) $ t) =
- (Syntax.const "_noargs", t)
+ (Syntax.const @{syntax_const "_noargs"}, t)
| dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax csplit},_) $ t) =
let
val (v1, t1) = dest_LAM t;
val (v2, t2) = dest_LAM t1;
- in (Syntax.const "_args" $ v1 $ v2, t2) end
+ in (Syntax.const @{syntax_const "_args"} $ v1 $ v2, t2) end
| dest_LAM (Const (@{const_syntax Abs_CFun},_) $ t) =
let
- val abs = case t of Abs abs => abs
+ val abs =
+ case t of Abs abs => abs
| _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
val (x, t') = atomic_abs_tr' abs;
- in (Syntax.const "_variable" $ x, t') end
+ in (Syntax.const @{syntax_const "_variable"} $ x, t') end
| dest_LAM _ = raise Match; (* too few vars: abort translation *)
fun Case1_tr' [Const(@{const_syntax branch},_) $ p, r] =
- let val (v, t) = dest_LAM r;
- in Syntax.const "_Case1" $ (Syntax.const "_match" $ p $ v) $ t end;
+ let val (v, t) = dest_LAM r in
+ Syntax.const @{syntax_const "_Case1"} $
+ (Syntax.const @{syntax_const "_match"} $ p $ v) $ t
+ end;
in [(@{const_syntax Rep_CFun}, Case1_tr')] end;
*}
--- a/src/HOLCF/Sprod.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/HOLCF/Sprod.thy Thu Feb 11 23:50:38 2010 +0100
@@ -51,7 +51,7 @@
"ssplit = (\<Lambda> f. strictify\<cdot>(\<Lambda> p. f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
syntax
- "@stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))")
+ "_stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))")
translations
"(:x, y, z:)" == "(:x, (:y, z:):)"
"(:x, y:)" == "CONST spair\<cdot>x\<cdot>y"
--- a/src/Pure/Isar/proof_context.ML Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Pure/Isar/proof_context.ML Thu Feb 11 23:50:38 2010 +0100
@@ -26,6 +26,7 @@
val naming_of: Proof.context -> Name_Space.naming
val restore_naming: Proof.context -> Proof.context -> Proof.context
val full_name: Proof.context -> binding -> string
+ val syn_of: Proof.context -> Syntax.syntax
val consts_of: Proof.context -> Consts.T
val const_syntax_name: Proof.context -> string -> string
val the_const_constraint: Proof.context -> string -> typ
--- a/src/Pure/ML/ml_antiquote.ML Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Pure/ML/ml_antiquote.ML Thu Feb 11 23:50:38 2010 +0100
@@ -127,5 +127,10 @@
let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));
+val _ = inline "syntax_const"
+ (Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
+ if Syntax.is_const (ProofContext.syn_of ctxt) c then ML_Syntax.print_string c
+ else error ("Unknown syntax const: " ^ quote c)));
+
end;
--- a/src/Pure/Syntax/syn_ext.ML Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Pure/Syntax/syn_ext.ML Thu Feb 11 23:50:38 2010 +0100
@@ -401,7 +401,7 @@
Mfix ("'(_')", spropT --> spropT, "", [0], max_pri),
Mfix ("_::_", [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3),
Mfix ("_::_", [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)]
- []
+ standard_token_markers
([], [], [], [])
[]
([], []);
--- a/src/Pure/Syntax/syntax.ML Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Pure/Syntax/syntax.ML Thu Feb 11 23:50:38 2010 +0100
@@ -54,6 +54,7 @@
PrintRule of 'a * 'a |
ParsePrintRule of 'a * 'a
val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
+ val is_const: syntax -> string -> bool
val standard_unparse_term: (string -> xstring) ->
Proof.context -> syntax -> bool -> term -> Pretty.T
val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
@@ -592,6 +593,8 @@
| print_rule (ParsePrintRule pats) = SOME (swap pats);
+fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c;
+
local
fun check_rule (rule as (lhs, rhs)) =
@@ -603,11 +606,9 @@
fun read_pattern ctxt is_logtype syn (root, str) =
let
- val Syntax ({consts, ...}, _) = syn;
-
fun constify (ast as Ast.Constant _) = ast
| constify (ast as Ast.Variable x) =
- if member (op =) consts x orelse Long_Name.is_qualified x then Ast.Constant x
+ if is_const syn x orelse Long_Name.is_qualified x then Ast.Constant x
else ast
| constify (Ast.Appl asts) = Ast.Appl (map constify asts);
--- a/src/Sequents/ILL.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Sequents/ILL.thy Thu Feb 11 23:50:38 2010 +0100
@@ -1,5 +1,4 @@
(* Title: Sequents/ILL.thy
- ID: $Id$
Author: Sara Kalvala and Valeria de Paiva
Copyright 1995 University of Cambridge
*)
@@ -32,19 +31,21 @@
PromAux :: "three_seqi"
syntax
- "@Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
- "@Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5)
- "@PromAux" :: "three_seqe" ("promaux {_||_||_}")
+ "_Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
+ "_Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5)
+ "_PromAux" :: "three_seqe" ("promaux {_||_||_}")
parse_translation {*
- [("@Trueprop", single_tr "Trueprop"),
- ("@Context", two_seq_tr "Context"),
- ("@PromAux", three_seq_tr "PromAux")] *}
+ [(@{syntax_const "_Trueprop"}, single_tr @{const_syntax Trueprop}),
+ (@{syntax_const "_Context"}, two_seq_tr @{const_syntax Context}),
+ (@{syntax_const "_PromAux"}, three_seq_tr @{const_syntax PromAux})]
+*}
print_translation {*
- [("Trueprop", single_tr' "@Trueprop"),
- ("Context", two_seq_tr'"@Context"),
- ("PromAux", three_seq_tr'"@PromAux")] *}
+ [(@{const_syntax Trueprop}, single_tr' @{syntax_const "_Trueprop"}),
+ (@{const_syntax Context}, two_seq_tr' @{syntax_const "_Context"}),
+ (@{const_syntax PromAux}, three_seq_tr' @{syntax_const "_PromAux"})]
+*}
defs
--- a/src/Sequents/LK0.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Sequents/LK0.thy Thu Feb 11 23:50:38 2010 +0100
@@ -1,10 +1,9 @@
(* Title: LK/LK0.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
There may be printing problems if a seqent is in expanded normal form
- (eta-expanded, beta-contracted)
+(eta-expanded, beta-contracted).
*)
header {* Classical First-Order Sequent Calculus *}
@@ -35,10 +34,10 @@
Ex :: "('a => o) => o" (binder "EX " 10)
syntax
- "@Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
+ "_Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
-parse_translation {* [("@Trueprop", two_seq_tr "Trueprop")] *}
-print_translation {* [("Trueprop", two_seq_tr' "@Trueprop")] *}
+parse_translation {* [(@{syntax_const "_Trueprop"}, two_seq_tr @{const_syntax Trueprop})] *}
+print_translation {* [(@{const_syntax Trueprop}, two_seq_tr' @{syntax_const "_Trueprop"})] *}
abbreviation
not_equal (infixl "~=" 50) where
--- a/src/Sequents/Modal0.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Sequents/Modal0.thy Thu Feb 11 23:50:38 2010 +0100
@@ -1,5 +1,4 @@
(* Title: Sequents/Modal0.thy
- ID: $Id$
Author: Martin Coen
Copyright 1991 University of Cambridge
*)
@@ -18,21 +17,23 @@
Rstar :: "two_seqi"
syntax
- "@Lstar" :: "two_seqe" ("(_)|L>(_)" [6,6] 5)
- "@Rstar" :: "two_seqe" ("(_)|R>(_)" [6,6] 5)
+ "_Lstar" :: "two_seqe" ("(_)|L>(_)" [6,6] 5)
+ "_Rstar" :: "two_seqe" ("(_)|R>(_)" [6,6] 5)
ML {*
- val Lstar = "Lstar";
- val Rstar = "Rstar";
- val SLstar = "@Lstar";
- val SRstar = "@Rstar";
-
- fun star_tr c [s1,s2] = Const(c,dummyT)$ seq_tr s1$ seq_tr s2;
- fun star_tr' c [s1,s2] = Const(c,dummyT) $ seq_tr' s1 $ seq_tr' s2;
+ fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2;
+ fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
*}
-parse_translation {* [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)] *}
-print_translation {* [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)] *}
+parse_translation {*
+ [(@{syntax_const "_Lstar"}, star_tr @{const_syntax Lstar}),
+ (@{syntax_const "_Rstar"}, star_tr @{const_syntax Rstar})]
+*}
+
+print_translation {*
+ [(@{const_syntax Lstar}, star_tr' @{syntax_const "_Lstar"}),
+ (@{const_syntax Rstar}, star_tr' @{syntax_const "_Rstar"})]
+*}
defs
strimp_def: "P --< Q == [](P --> Q)"
--- a/src/Sequents/S43.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Sequents/S43.thy Thu Feb 11 23:50:38 2010 +0100
@@ -1,5 +1,4 @@
(* Title: Modal/S43.thy
- ID: $Id$
Author: Martin Coen
Copyright 1991 University of Cambridge
@@ -14,25 +13,24 @@
S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq',
seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
syntax
- "@S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
+ "_S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
-ML {*
- val S43pi = "S43pi";
- val SS43pi = "@S43pi";
-
- val tr = seq_tr;
- val tr' = seq_tr';
-
- fun s43pi_tr[s1,s2,s3,s4,s5,s6]=
- Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
- fun s43pi_tr'[s1,s2,s3,s4,s5,s6] =
- Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6;
-
+parse_translation {*
+ let
+ val tr = seq_tr;
+ fun s43pi_tr [s1, s2, s3, s4, s5, s6] =
+ Const (@{const_syntax S43pi}, dummyT) $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6;
+ in [(@{syntax_const "_S43pi"}, s43pi_tr)] end
*}
-parse_translation {* [(SS43pi,s43pi_tr)] *}
-print_translation {* [(S43pi,s43pi_tr')] *}
+print_translation {*
+let
+ val tr' = seq_tr';
+ fun s43pi_tr' [s1, s2, s3, s4, s5, s6] =
+ Const(@{syntax_const "_S43pi"}, dummyT) $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6;
+in [(@{const_syntax S43pi}, s43pi_tr')] end
+*}
axioms
(* Definition of the star operation using a set of Horn clauses *)
--- a/src/Sequents/Sequents.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/Sequents/Sequents.thy Thu Feb 11 23:50:38 2010 +0100
@@ -1,5 +1,4 @@
(* Title: Sequents/Sequents.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
*)
@@ -36,14 +35,14 @@
syntax
- SeqEmp :: seq ("")
- SeqApp :: "[seqobj,seqcont] => seq" ("__")
+ "_SeqEmp" :: seq ("")
+ "_SeqApp" :: "[seqobj,seqcont] => seq" ("__")
- SeqContEmp :: seqcont ("")
- SeqContApp :: "[seqobj,seqcont] => seqcont" (",/ __")
+ "_SeqContEmp" :: seqcont ("")
+ "_SeqContApp" :: "[seqobj,seqcont] => seqcont" (",/ __")
- SeqO :: "o => seqobj" ("_")
- SeqId :: "'a => seqobj" ("$_")
+ "_SeqO" :: "o => seqobj" ("_")
+ "_SeqId" :: "'a => seqobj" ("$_")
types
single_seqe = "[seq,seqobj] => prop"
@@ -60,86 +59,76 @@
syntax
(*Constant to allow definitions of SEQUENCES of formulas*)
- "@Side" :: "seq=>(seq'=>seq')" ("<<(_)>>")
+ "_Side" :: "seq=>(seq'=>seq')" ("<<(_)>>")
ML {*
(* parse translation for sequences *)
-fun abs_seq' t = Abs("s", Type("seq'",[]), t);
+fun abs_seq' t = Abs ("s", Type ("seq'", []), t); (* FIXME @{type_syntax} *)
-fun seqobj_tr(Const("SeqO",_) $ f) = Const("SeqO'",dummyT) $ f |
- seqobj_tr(_ $ i) = i;
-
-fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
- seqcont_tr(Const("SeqContApp",_) $ so $ sc) =
- (seqobj_tr so) $ (seqcont_tr sc);
+fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) =
+ Const (@{const_syntax SeqO'}, dummyT) $ f
+ | seqobj_tr (_ $ i) = i;
-fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
- seq_tr(Const("SeqApp",_) $ so $ sc) =
- abs_seq'(seqobj_tr(so) $ seqcont_tr(sc));
+fun seqcont_tr (Const (@{syntax_const "_SeqContEmp"}, _)) = Bound 0
+ | seqcont_tr (Const (@{syntax_const "_SeqContApp"}, _) $ so $ sc) =
+ seqobj_tr so $ seqcont_tr sc;
+fun seq_tr (Const (@{syntax_const "_SeqEmp"}, _)) = abs_seq' (Bound 0)
+ | seq_tr (Const (@{syntax_const "_SeqApp"}, _) $ so $ sc) =
+ abs_seq'(seqobj_tr so $ seqcont_tr sc);
-fun singlobj_tr(Const("SeqO",_) $ f) =
- abs_seq' ((Const("SeqO'",dummyT) $ f) $ Bound 0);
-
+fun singlobj_tr (Const (@{syntax_const "_SeqO"},_) $ f) =
+ abs_seq' ((Const (@{const_syntax SeqO'}, dummyT) $ f) $ Bound 0);
(* print translation for sequences *)
fun seqcont_tr' (Bound 0) =
- Const("SeqContEmp",dummyT) |
- seqcont_tr' (Const("SeqO'",_) $ f $ s) =
- Const("SeqContApp",dummyT) $
- (Const("SeqO",dummyT) $ f) $
- (seqcont_tr' s) |
-(* seqcont_tr' ((a as Abs(_,_,_)) $ s)=
- seqcont_tr'(Term.betapply(a,s)) | *)
- seqcont_tr' (i $ s) =
- Const("SeqContApp",dummyT) $
- (Const("SeqId",dummyT) $ i) $
- (seqcont_tr' s);
+ Const (@{syntax_const "_SeqContEmp"}, dummyT)
+ | seqcont_tr' (Const (@{const_syntax SeqO'}, _) $ f $ s) =
+ Const (@{syntax_const "_SeqContApp"}, dummyT) $
+ (Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s
+ | seqcont_tr' (i $ s) =
+ Const (@{syntax_const "_SeqContApp"}, dummyT) $
+ (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s;
fun seq_tr' s =
- let fun seq_itr' (Bound 0) =
- Const("SeqEmp",dummyT) |
- seq_itr' (Const("SeqO'",_) $ f $ s) =
- Const("SeqApp",dummyT) $
- (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) |
-(* seq_itr' ((a as Abs(_,_,_)) $ s) =
- seq_itr'(Term.betapply(a,s)) | *)
- seq_itr' (i $ s) =
- Const("SeqApp",dummyT) $
- (Const("SeqId",dummyT) $ i) $
- (seqcont_tr' s)
- in case s of
- Abs(_,_,t) => seq_itr' t |
- _ => s $ (Bound 0)
- end;
+ let
+ fun seq_itr' (Bound 0) = Const (@{syntax_const "_SeqEmp"}, dummyT)
+ | seq_itr' (Const (@{const_syntax SeqO'}, _) $ f $ s) =
+ Const (@{syntax_const "_SeqApp"}, dummyT) $
+ (Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s
+ | seq_itr' (i $ s) =
+ Const (@{syntax_const "_SeqApp"}, dummyT) $
+ (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s
+ in
+ case s of
+ Abs (_, _, t) => seq_itr' t
+ | _ => s $ Bound 0
+ end;
+fun single_tr c [s1, s2] =
+ Const (c, dummyT) $ seq_tr s1 $ singlobj_tr s2;
+
+fun two_seq_tr c [s1, s2] =
+ Const (c, dummyT) $ seq_tr s1 $ seq_tr s2;
+
+fun three_seq_tr c [s1, s2, s3] =
+ Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
+
+fun four_seq_tr c [s1, s2, s3, s4] =
+ Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
-fun single_tr c [s1,s2] =
- Const(c,dummyT) $ seq_tr s1 $ singlobj_tr s2;
-
-fun two_seq_tr c [s1,s2] =
- Const(c,dummyT) $ seq_tr s1 $ seq_tr s2;
-
-fun three_seq_tr c [s1,s2,s3] =
- Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
-
-fun four_seq_tr c [s1,s2,s3,s4] =
- Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
-
-
-fun singlobj_tr'(Const("SeqO'",_) $ fm) = fm |
- singlobj_tr'(id) = Const("@SeqId",dummyT) $ id;
+fun singlobj_tr' (Const (@{const_syntax SeqO'},_) $ fm) = fm
+ | singlobj_tr' id = Const (@{syntax_const "_SeqId"}, dummyT) $ id;
fun single_tr' c [s1, s2] =
-(Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 );
-
+ Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
fun two_seq_tr' c [s1, s2] =
Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
@@ -157,7 +146,7 @@
fun side_tr [s1] = seq_tr s1;
*}
-parse_translation {* [("@Side", side_tr)] *}
+parse_translation {* [(@{syntax_const "_Side"}, side_tr)] *}
use "prover.ML"
--- a/src/ZF/Bin.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/ZF/Bin.thy Thu Feb 11 23:50:38 2010 +0100
@@ -26,11 +26,6 @@
| Min
| Bit ("w: bin", "b: bool") (infixl "BIT" 90)
-use "Tools/numeral_syntax.ML"
-
-syntax
- "_Int" :: "xnum => i" ("_")
-
consts
integ_of :: "i=>i"
NCons :: "[i,i]=>i"
@@ -106,6 +101,10 @@
"bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
NCons(bin_mult(v,w),0))"
+syntax
+ "_Int" :: "xnum => i" ("_")
+
+use "Tools/numeral_syntax.ML"
setup NumeralSyntax.setup
--- a/src/ZF/Induct/Multiset.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/ZF/Induct/Multiset.thy Thu Feb 11 23:50:38 2010 +0100
@@ -74,9 +74,9 @@
"a :# M == a \<in> mset_of(M)"
syntax
- "@MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})")
+ "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})")
syntax (xsymbols)
- "@MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
+ "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
translations
"{#x \<in> M. P#}" == "CONST MCollect(M, %x. P)"
--- a/src/ZF/List_ZF.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/ZF/List_ZF.thy Thu Feb 11 23:50:38 2010 +0100
@@ -16,7 +16,7 @@
syntax
"[]" :: i ("[]")
- "@List" :: "is => i" ("[(_)]")
+ "_List" :: "is => i" ("[(_)]")
translations
"[x, xs]" == "CONST Cons(x, [xs])"
--- a/src/ZF/OrdQuant.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/ZF/OrdQuant.thy Thu Feb 11 23:50:38 2010 +0100
@@ -23,9 +23,9 @@
"OUnion(i,B) == {z: \<Union>x\<in>i. B(x). Ord(i)}"
syntax
- "@oall" :: "[idt, i, o] => o" ("(3ALL _<_./ _)" 10)
- "@oex" :: "[idt, i, o] => o" ("(3EX _<_./ _)" 10)
- "@OUNION" :: "[idt, i, i] => i" ("(3UN _<_./ _)" 10)
+ "_oall" :: "[idt, i, o] => o" ("(3ALL _<_./ _)" 10)
+ "_oex" :: "[idt, i, o] => o" ("(3EX _<_./ _)" 10)
+ "_OUNION" :: "[idt, i, i] => i" ("(3UN _<_./ _)" 10)
translations
"ALL x<a. P" == "CONST oall(a, %x. P)"
@@ -33,13 +33,13 @@
"UN x<a. B" == "CONST OUnion(a, %x. B)"
syntax (xsymbols)
- "@oall" :: "[idt, i, o] => o" ("(3\<forall>_<_./ _)" 10)
- "@oex" :: "[idt, i, o] => o" ("(3\<exists>_<_./ _)" 10)
- "@OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10)
+ "_oall" :: "[idt, i, o] => o" ("(3\<forall>_<_./ _)" 10)
+ "_oex" :: "[idt, i, o] => o" ("(3\<exists>_<_./ _)" 10)
+ "_OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10)
syntax (HTML output)
- "@oall" :: "[idt, i, o] => o" ("(3\<forall>_<_./ _)" 10)
- "@oex" :: "[idt, i, o] => o" ("(3\<exists>_<_./ _)" 10)
- "@OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10)
+ "_oall" :: "[idt, i, o] => o" ("(3\<forall>_<_./ _)" 10)
+ "_oex" :: "[idt, i, o] => o" ("(3\<exists>_<_./ _)" 10)
+ "_OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10)
subsubsection {*simplification of the new quantifiers*}
@@ -203,15 +203,15 @@
"rex(M, P) == EX x. M(x) & P(x)"
syntax
- "@rall" :: "[pttrn, i=>o, o] => o" ("(3ALL _[_]./ _)" 10)
- "@rex" :: "[pttrn, i=>o, o] => o" ("(3EX _[_]./ _)" 10)
+ "_rall" :: "[pttrn, i=>o, o] => o" ("(3ALL _[_]./ _)" 10)
+ "_rex" :: "[pttrn, i=>o, o] => o" ("(3EX _[_]./ _)" 10)
syntax (xsymbols)
- "@rall" :: "[pttrn, i=>o, o] => o" ("(3\<forall>_[_]./ _)" 10)
- "@rex" :: "[pttrn, i=>o, o] => o" ("(3\<exists>_[_]./ _)" 10)
+ "_rall" :: "[pttrn, i=>o, o] => o" ("(3\<forall>_[_]./ _)" 10)
+ "_rex" :: "[pttrn, i=>o, o] => o" ("(3\<exists>_[_]./ _)" 10)
syntax (HTML output)
- "@rall" :: "[pttrn, i=>o, o] => o" ("(3\<forall>_[_]./ _)" 10)
- "@rex" :: "[pttrn, i=>o, o] => o" ("(3\<exists>_[_]./ _)" 10)
+ "_rall" :: "[pttrn, i=>o, o] => o" ("(3\<forall>_[_]./ _)" 10)
+ "_rex" :: "[pttrn, i=>o, o] => o" ("(3\<exists>_[_]./ _)" 10)
translations
"ALL x[M]. P" == "CONST rall(M, %x. P)"
--- a/src/ZF/Tools/numeral_syntax.ML Thu Feb 11 12:26:50 2010 -0800
+++ b/src/ZF/Tools/numeral_syntax.ML Thu Feb 11 23:50:38 2010 +0100
@@ -7,92 +7,83 @@
signature NUMERAL_SYNTAX =
sig
- val dest_bin : term -> int
- val mk_bin : int -> term
- val int_tr : term list -> term
- val int_tr' : bool -> typ -> term list -> term
- val setup : theory -> theory
+ val make_binary: int -> int list
+ val dest_binary: int list -> int
+ val int_tr: term list -> term
+ val int_tr': bool -> typ -> term list -> term
+ val setup: theory -> theory
end;
structure NumeralSyntax: NUMERAL_SYNTAX =
struct
-(* Bits *)
+(* bits *)
-fun mk_bit 0 = @{term "0"}
- | mk_bit 1 = @{term "succ(0)"}
+fun mk_bit 0 = Syntax.const @{const_syntax "0"}
+ | mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax 0}
| mk_bit _ = sys_error "mk_bit";
-fun dest_bit (Const (@{const_name "0"}, _)) = 0
- | dest_bit (Const (@{const_name succ}, _) $ Const (@{const_name "0"}, _)) = 1
+fun dest_bit (Const (@{const_syntax "0"}, _)) = 0
+ | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax "0"}, _)) = 1
| dest_bit _ = raise Match;
-(* Bit strings *) (*we try to handle superfluous leading digits nicely*)
+(* bit strings *)
+
+fun make_binary 0 = []
+ | make_binary ~1 = [~1]
+ | make_binary n = (n mod 2) :: make_binary (n div 2);
+fun dest_binary [] = 0
+ | dest_binary (b :: bs) = b + 2 * dest_binary bs;
+
+
+(*try to handle superfluous leading digits nicely*)
fun prefix_len _ [] = 0
| prefix_len pred (x :: xs) =
if pred x then 1 + prefix_len pred xs else 0;
fun mk_bin i =
- let fun bin_of_int 0 = []
- | bin_of_int ~1 = [~1]
- | bin_of_int n = (n mod 2) :: bin_of_int (n div 2);
-
- fun term_of [] = @{const Pls}
- | term_of [~1] = @{const Min}
- | term_of (b :: bs) = @{const Bit} $ term_of bs $ mk_bit b;
- in
- term_of (bin_of_int i)
- end;
+ let
+ fun term_of [] = Syntax.const @{const_syntax Pls}
+ | term_of [~1] = Syntax.const @{const_syntax Min}
+ | term_of (b :: bs) = Syntax.const @{const_syntax Bit} $ term_of bs $ mk_bit b;
+ in term_of (make_binary i) end;
-(*we consider all "spellings", since they could vary depending on the caller*)
-fun bin_of (Const ("Pls", _)) = []
- | bin_of (Const ("bin.Pls", _)) = []
- | bin_of (Const ("Bin.bin.Pls", _)) = []
- | bin_of (Const ("Min", _)) = [~1]
- | bin_of (Const ("bin.Min", _)) = [~1]
- | bin_of (Const ("Bin.bin.Min", _)) = [~1]
- | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
- | bin_of (Const ("bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
- | bin_of (Const ("Bin.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
+fun bin_of (Const (@{const_syntax Pls}, _)) = []
+ | bin_of (Const (@{const_syntax Min}, _)) = [~1]
+ | bin_of (Const (@{const_syntax Bit}, _) $ bs $ b) = dest_bit b :: bin_of bs
| bin_of _ = raise Match;
-(*Convert a list of bits to an integer*)
-fun integ_of [] = 0
- | integ_of (b :: bs) = b + 2 * integ_of bs;
-
-val dest_bin = integ_of o bin_of;
-
-(*leading 0s and (for negative numbers) -1s cause complications, though they
+(*Leading 0s and (for negative numbers) -1s cause complications, though they
should never arise in normal use. The formalization used in HOL prevents
them altogether.*)
fun show_int t =
let
val rev_digs = bin_of t;
val (sign, zs) =
- (case rev rev_digs of
- ~1 :: bs => ("-", prefix_len (equal 1) bs)
- | bs => ("", prefix_len (equal 0) bs));
- val num = string_of_int (abs (integ_of rev_digs));
+ (case rev rev_digs of
+ ~1 :: bs => ("-", prefix_len (equal 1) bs)
+ | bs => ("", prefix_len (equal 0) bs));
+ val num = string_of_int (abs (dest_binary rev_digs));
in
"#" ^ sign ^ implode (replicate zs "0") ^ num
end;
-
(* translation of integer constant tokens to and from binary *)
fun int_tr (*"_Int"*) [t as Free (str, _)] =
- Syntax.const "integ_of" $ mk_bin (#value (Syntax.read_xnum str))
+ Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Syntax.read_xnum str))
| int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
-fun int_tr' _ _ (*"integ_of"*) [t] = Syntax.const "_Int" $ Syntax.free (show_int t)
- | int_tr' (_:bool) (_:typ) _ = raise Match;
+fun int_tr' _ _ (*"integ_of"*) [t] =
+ Syntax.const @{syntax_const "_Int"} $ Syntax.free (show_int t)
+ | int_tr' (_: bool) (_: typ) _ = raise Match;
val setup =
- (Sign.add_trfuns ([], [("_Int", int_tr)], [], []) #>
- Sign.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]);
+ (Sign.add_trfuns ([], [(@{syntax_const "_Int"}, int_tr)], [], []) #>
+ Sign.add_trfunsT [(@{const_syntax integ_of}, int_tr')]);
end;
--- a/src/ZF/UNITY/Union.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/ZF/UNITY/Union.thy Thu Feb 11 23:50:38 2010 +0100
@@ -41,8 +41,8 @@
SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) --> G \<in> X)"
syntax
- "@JOIN1" :: "[pttrns, i] => i" ("(3JN _./ _)" 10)
- "@JOIN" :: "[pttrn, i, i] => i" ("(3JN _:_./ _)" 10)
+ "_JOIN1" :: "[pttrns, i] => i" ("(3JN _./ _)" 10)
+ "_JOIN" :: "[pttrn, i, i] => i" ("(3JN _:_./ _)" 10)
translations
"JN x:A. B" == "CONST JOIN(A, (%x. B))"
@@ -54,8 +54,8 @@
Join (infixl "\<squnion>" 65)
syntax (xsymbols)
- "@JOIN1" :: "[pttrns, i] => i" ("(3\<Squnion> _./ _)" 10)
- "@JOIN" :: "[pttrn, i, i] => i" ("(3\<Squnion> _ \<in> _./ _)" 10)
+ "_JOIN1" :: "[pttrns, i] => i" ("(3\<Squnion> _./ _)" 10)
+ "_JOIN" :: "[pttrn, i, i] => i" ("(3\<Squnion> _ \<in> _./ _)" 10)
subsection{*SKIP*}
--- a/src/ZF/ZF.thy Thu Feb 11 12:26:50 2010 -0800
+++ b/src/ZF/ZF.thy Thu Feb 11 23:50:38 2010 +0100
@@ -105,26 +105,26 @@
syntax
"" :: "i => is" ("_")
- "@Enum" :: "[i, is] => is" ("_,/ _")
+ "_Enum" :: "[i, is] => is" ("_,/ _")
- "@Finset" :: "is => i" ("{(_)}")
- "@Tuple" :: "[i, is] => i" ("<(_,/ _)>")
- "@Collect" :: "[pttrn, i, o] => i" ("(1{_: _ ./ _})")
- "@Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
- "@RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _: _})" [51,0,51])
- "@INTER" :: "[pttrn, i, i] => i" ("(3INT _:_./ _)" 10)
- "@UNION" :: "[pttrn, i, i] => i" ("(3UN _:_./ _)" 10)
- "@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)
+ "_Finset" :: "is => i" ("{(_)}")
+ "_Tuple" :: "[i, is] => i" ("<(_,/ _)>")
+ "_Collect" :: "[pttrn, i, o] => i" ("(1{_: _ ./ _})")
+ "_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
+ "_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _: _})" [51,0,51])
+ "_INTER" :: "[pttrn, i, i] => i" ("(3INT _:_./ _)" 10)
+ "_UNION" :: "[pttrn, i, i] => i" ("(3UN _:_./ _)" 10)
+ "_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)
(** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
- "@pattern" :: "patterns => pttrn" ("<_>")
+ "_pattern" :: "patterns => pttrn" ("<_>")
"" :: "pttrn => patterns" ("_")
- "@patterns" :: "[pttrn, patterns] => patterns" ("_,/_")
+ "_patterns" :: "[pttrn, patterns] => patterns" ("_,/_")
translations
"{x, xs}" == "CONST cons(x, {xs})"
@@ -158,18 +158,18 @@
Inter ("\<Inter>_" [90] 90)
syntax (xsymbols)
- "@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\<Pi>_\<in>_./ _)" 10)
- "@SUM" :: "[pttrn, i, i] => i" ("(3\<Sigma>_\<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)
- "@Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>")
- "@pattern" :: "patterns => pttrn" ("\<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\<Pi>_\<in>_./ _)" 10)
+ "_SUM" :: "[pttrn, i, i] => i" ("(3\<Sigma>_\<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)
+ "_Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>")
+ "_pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>")
notation (HTML output)
cart_prod (infixr "\<times>" 80) and
@@ -182,18 +182,18 @@
Inter ("\<Inter>_" [90] 90)
syntax (HTML output)
- "@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\<Pi>_\<in>_./ _)" 10)
- "@SUM" :: "[pttrn, i, i] => i" ("(3\<Sigma>_\<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)
- "@Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>")
- "@pattern" :: "patterns => pttrn" ("\<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\<Pi>_\<in>_./ _)" 10)
+ "_SUM" :: "[pttrn, i, i] => i" ("(3\<Sigma>_\<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)
+ "_Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>")
+ "_pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>")
finalconsts
--- a/src/ZF/int_arith.ML Thu Feb 11 12:26:50 2010 -0800
+++ b/src/ZF/int_arith.ML Thu Feb 11 23:50:38 2010 +0100
@@ -7,15 +7,40 @@
structure Int_Numeral_Simprocs =
struct
+(* abstract syntax operations *)
+
+fun mk_bit 0 = @{term "0"}
+ | mk_bit 1 = @{term "succ(0)"}
+ | mk_bit _ = sys_error "mk_bit";
+
+fun dest_bit @{term "0"} = 0
+ | dest_bit @{term "succ(0)"} = 1
+ | dest_bit _ = raise Match;
+
+fun mk_bin i =
+ let
+ fun term_of [] = @{term Pls}
+ | term_of [~1] = @{term Min}
+ | term_of (b :: bs) = @{term Bit} $ term_of bs $ mk_bit b;
+ in term_of (NumeralSyntax.make_binary i) end;
+
+fun dest_bin tm =
+ let
+ fun bin_of @{term Pls} = []
+ | bin_of @{term Min} = [~1]
+ | bin_of (@{term Bit} $ bs $ b) = dest_bit b :: bin_of bs
+ | bin_of _ = sys_error "dest_bin";
+ in NumeralSyntax.dest_binary (bin_of tm) end;
+
+
(*Utilities*)
-fun mk_numeral n = @{const integ_of} $ NumeralSyntax.mk_bin n;
+fun mk_numeral i = @{const integ_of} $ mk_bin i;
(*Decodes a binary INTEGER*)
fun dest_numeral (Const(@{const_name integ_of}, _) $ w) =
- (NumeralSyntax.dest_bin w
- handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
- | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
+ (dest_bin w handle SYS_ERROR _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
+ | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
fun find_first_numeral past (t::terms) =
((dest_numeral t, rev past @ terms)