--- a/src/ZF/Inductive.thy Wed Oct 03 21:29:05 2007 +0200
+++ b/src/ZF/Inductive.thy Wed Oct 03 22:33:17 2007 +0200
@@ -54,7 +54,7 @@
structure Standard_Sum =
struct
- val sum = Const("op +", [iT,iT]--->iT)
+ val sum = Const(@{const_name sum}, [iT,iT]--->iT)
val inl = Const("Inl", iT-->iT)
val inr = Const("Inr", iT-->iT)
val elim = Const("case", [iT-->iT, iT-->iT, iT]--->iT)
--- a/src/ZF/OrderType.thy Wed Oct 03 21:29:05 2007 +0200
+++ b/src/ZF/OrderType.thy Wed Oct 03 22:33:17 2007 +0200
@@ -45,11 +45,11 @@
"i -- j == ordertype(i-j, Memrel(i))"
-syntax (xsymbols)
- "op **" :: "[i,i] => i" (infixl "\<times>\<times>" 70)
+notation (xsymbols)
+ omult (infixl "\<times>\<times>" 70)
-syntax (HTML output)
- "op **" :: "[i,i] => i" (infixl "\<times>\<times>" 70)
+notation (HTML output)
+ omult (infixl "\<times>\<times>" 70)
subsection{*Proofs needing the combination of Ordinal.thy and Order.thy*}
--- a/src/ZF/Tools/datatype_package.ML Wed Oct 03 21:29:05 2007 +0200
+++ b/src/ZF/Tools/datatype_package.ML Wed Oct 03 22:33:17 2007 +0200
@@ -174,7 +174,7 @@
(*Find each recursive argument and add a recursive call for it*)
fun rec_args [] = []
- | rec_args ((Const("op :",_)$arg$X)::prems) =
+ | rec_args ((Const(@{const_name mem},_)$arg$X)::prems) =
(case head_of X of
Const(a,_) => (*recursive occurrence?*)
if a mem_string rec_names
@@ -293,7 +293,7 @@
| SOME recursor_def =>
let
(*Replace subterms rec`x (where rec is a Free var) by recursor_tm(x) *)
- fun subst_rec (Const("op `",_) $ Free _ $ arg) = recursor_tm $ arg
+ fun subst_rec (Const(@{const_name apply},_) $ Free _ $ arg) = recursor_tm $ arg
| subst_rec tm =
let val (head, args) = strip_comb tm
in list_comb (head, map subst_rec args) end;
--- a/src/ZF/Tools/induct_tacs.ML Wed Oct 03 21:29:05 2007 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Wed Oct 03 22:33:17 2007 +0200
@@ -72,7 +72,7 @@
exception Find_tname of string
fun find_tname var Bi =
- let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) =
+ let fun mk_pair (Const(@{const_name mem},_) $ Free (v,_) $ A) =
(v, #1 (dest_Const (head_of A)))
| mk_pair _ = raise Match
val pairs = List.mapPartial (try (mk_pair o FOLogic.dest_Trueprop))
@@ -97,7 +97,7 @@
val rule =
if exh then #exhaustion (datatype_info thy tn)
else #induct (datatype_info thy tn)
- val (Const("op :",_) $ Var(ixn,_) $ _) =
+ val (Const(@{const_name mem},_) $ Var(ixn,_) $ _) =
(case prems_of rule of
[] => error "induction is not available for this datatype"
| major::_ => FOLogic.dest_Trueprop major)
@@ -126,7 +126,7 @@
map (head_of o const_of o FOLogic.dest_Trueprop o
#prop o rep_thm) case_eqns;
- val Const ("op :", _) $ _ $ data =
+ val Const (@{const_name mem}, _) $ _ $ data =
FOLogic.dest_Trueprop (hd (prems_of elim));
val Const(big_rec_name, _) = head_of data;
--- a/src/ZF/Tools/inductive_package.ML Wed Oct 03 21:29:05 2007 +0200
+++ b/src/ZF/Tools/inductive_package.ML Wed Oct 03 22:33:17 2007 +0200
@@ -286,7 +286,7 @@
ind_alist = [(rec_tm1,pred1),...] associates predicates with rec ops
prem is a premise of an intr rule*)
fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $
- (Const("op :",_)$t$X), iprems) =
+ (Const(@{const_name mem},_)$t$X), iprems) =
(case AList.lookup (op aconv) ind_alist X of
SOME pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
| NONE => (*possibly membership in M(rec_tm), for M monotone*)
--- a/src/ZF/Tools/typechk.ML Wed Oct 03 21:29:05 2007 +0200
+++ b/src/ZF/Tools/typechk.ML Wed Oct 03 22:33:17 2007 +0200
@@ -76,7 +76,7 @@
if length rls <= maxr then resolve_tac rls i else no_tac
end);
-fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) =
+fun is_rigid_elem (Const("Trueprop",_) $ (Const(@{const_name mem},_) $ a $ _)) =
not (is_Var (head_of a))
| is_rigid_elem _ = false;
--- a/src/ZF/ZF.thy Wed Oct 03 21:29:05 2007 +0200
+++ b/src/ZF/ZF.thy Wed Oct 03 22:33:17 2007 +0200
@@ -43,11 +43,9 @@
The :: "(i => o) => i" (binder "THE " 10)
If :: "[o, i, i] => i" ("(if (_)/ then (_)/ else (_))" [10] 10)
-syntax
- old_if :: "[o, i, i] => i" ("if '(_,_,_')")
-
-translations
- "if(P,a,b)" => "If(P,a,b)"
+abbreviation (input)
+ old_if :: "[o, i, i] => i" ("if '(_,_,_')") where
+ "if(P,a,b) == If(P,a,b)"
text {*Finite Sets *}
@@ -75,24 +73,33 @@
field :: "i => i"
converse :: "i => i"
relation :: "i => o" --{*recognizes sets of pairs*}
- function :: "i => o" --{*recognizes functions; can have non-pairs*}
+ "function" :: "i => o" --{*recognizes functions; can have non-pairs*}
Lambda :: "[i, i => i] => i"
restrict :: "[i, i] => i"
text {*Infixes in order of decreasing precedence *}
consts
- "``" :: "[i, i] => i" (infixl 90) --{*image*}
- "-``" :: "[i, i] => i" (infixl 90) --{*inverse image*}
- "`" :: "[i, i] => i" (infixl 90) --{*function application*}
-(*"*" :: "[i, i] => i" (infixr 80) [virtual] Cartesian product*)
- "Int" :: "[i, i] => i" (infixl 70) --{*binary intersection*}
- "Un" :: "[i, i] => i" (infixl 65) --{*binary union*}
- "-" :: "[i, i] => i" (infixl 65) --{*set difference*}
-(*"->" :: "[i, i] => i" (infixr 60) [virtual] function spac\<epsilon>*)
- "<=" :: "[i, i] => o" (infixl 50) --{*subset relation*}
- ":" :: "[i, i] => o" (infixl 50) --{*membership relation*}
-(*"~:" :: "[i, i] => o" (infixl 50) (*negated membership relation*)*)
+ Image :: "[i, i] => i" (infixl "``" 90) --{*image*}
+ vimage :: "[i, i] => i" (infixl "-``" 90) --{*inverse image*}
+ "apply" :: "[i, i] => i" (infixl "`" 90) --{*function application*}
+ "Int" :: "[i, i] => i" (infixl "Int" 70) --{*binary intersection*}
+ "Un" :: "[i, i] => i" (infixl "Un" 65) --{*binary union*}
+ Diff :: "[i, i] => i" (infixl "-" 65) --{*set difference*}
+ Subset :: "[i, i] => o" (infixl "<=" 50) --{*subset relation*}
+ mem :: "[i, i] => o" (infixl ":" 50) --{*membership relation*}
+
+abbreviation
+ not_mem :: "[i, i] => o" (infixl "~:" 50) --{*negated membership relation*}
+ where "x ~: y == ~ (x : y)"
+
+abbreviation
+ cart_prod :: "[i, i] => i" (infixr "*" 80) --{*Cartesian product*}
+ where "A * B == Sigma(A, %_. B)"
+
+abbreviation
+ function_space :: "[i, i] => i" (infixr "->" 60) --{*function space*}
+ where "A -> B == Pi(A, %_. B)"
nonterminals "is" patterns
@@ -100,7 +107,7 @@
syntax
"" :: "i => is" ("_")
"@Enum" :: "[i, is] => is" ("_,/ _")
- "~:" :: "[i, i] => o" (infixl 50)
+
"@Finset" :: "is => i" ("{(_)}")
"@Tuple" :: "[i, is] => i" ("<(_,/ _)>")
"@Collect" :: "[pttrn, i, o] => i" ("(1{_: _ ./ _})")
@@ -110,8 +117,6 @@
"@UNION" :: "[pttrn, i, i] => i" ("(3UN _:_./ _)" 10)
"@PROD" :: "[pttrn, i, i] => i" ("(3PROD _:_./ _)" 10)
"@SUM" :: "[pttrn, i, i] => i" ("(3SUM _:_./ _)" 10)
- "->" :: "[i, i] => i" (infixr 60)
- "*" :: "[i, i] => i" (infixr 80)
"@lam" :: "[pttrn, i, i] => i" ("(3lam _:_./ _)" 10)
"@Ball" :: "[pttrn, i, o] => o" ("(3ALL _:_./ _)" 10)
"@Bex" :: "[pttrn, i, o] => o" ("(3EX _:_./ _)" 10)
@@ -123,7 +128,6 @@
"@patterns" :: "[pttrn, patterns] => patterns" ("_,/_")
translations
- "x ~: y" == "~ (x : y)"
"{x, xs}" == "cons(x, {xs})"
"{x}" == "cons(x, 0)"
"{x:A. P}" == "Collect(A, %x. P)"
@@ -131,10 +135,8 @@
"{b. x:A}" == "RepFun(A, %x. b)"
"INT x:A. B" == "Inter({B. x:A})"
"UN x:A. B" == "Union({B. x:A})"
- "PROD x:A. B" => "Pi(A, %x. B)"
- "SUM x:A. B" => "Sigma(A, %x. B)"
- "A -> B" => "Pi(A, %_. B)"
- "A * B" => "Sigma(A, %_. B)"
+ "PROD x:A. B" == "Pi(A, %x. B)"
+ "SUM x:A. B" == "Sigma(A, %x. B)"
"lam x:A. f" == "Lambda(A, %x. f)"
"ALL x:A. P" == "Ball(A, %x. P)"
"EX x:A. P" == "Bex(A, %x. P)"
@@ -145,21 +147,23 @@
"%<x,y>.b" == "split(%x y. b)"
+notation (xsymbols)
+ cart_prod (infixr "\<times>" 80) and
+ Int (infixl "\<inter>" 70) and
+ Un (infixl "\<union>" 65) and
+ function_space (infixr "\<rightarrow>" 60) and
+ Subset (infixl "\<subseteq>" 50) and
+ mem (infixl "\<in>" 50) and
+ not_mem (infixl "\<notin>" 50) and
+ Union ("\<Union>_" [90] 90) and
+ Inter ("\<Inter>_" [90] 90)
+
syntax (xsymbols)
- "op *" :: "[i, i] => i" (infixr "\<times>" 80)
- "op Int" :: "[i, i] => i" (infixl "\<inter>" 70)
- "op Un" :: "[i, i] => i" (infixl "\<union>" 65)
- "op ->" :: "[i, i] => i" (infixr "\<rightarrow>" 60)
- "op <=" :: "[i, i] => o" (infixl "\<subseteq>" 50)
- "op :" :: "[i, i] => o" (infixl "\<in>" 50)
- "op ~:" :: "[i, i] => o" (infixl "\<notin>" 50)
"@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)
- Union :: "i =>i" ("\<Union>_" [90] 90)
- Inter :: "i =>i" ("\<Inter>_" [90] 90)
"@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)
@@ -168,20 +172,22 @@
"@Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>")
"@pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>")
+notation (HTML output)
+ cart_prod (infixr "\<times>" 80) and
+ Int (infixl "\<inter>" 70) and
+ Un (infixl "\<union>" 65) and
+ Subset (infixl "\<subseteq>" 50) and
+ mem (infixl "\<in>" 50) and
+ not_mem (infixl "\<notin>" 50) and
+ Union ("\<Union>_" [90] 90) and
+ Inter ("\<Inter>_" [90] 90)
+
syntax (HTML output)
- "op *" :: "[i, i] => i" (infixr "\<times>" 80)
- "op Int" :: "[i, i] => i" (infixl "\<inter>" 70)
- "op Un" :: "[i, i] => i" (infixl "\<union>" 65)
- "op <=" :: "[i, i] => o" (infixl "\<subseteq>" 50)
- "op :" :: "[i, i] => o" (infixl "\<in>" 50)
- "op ~:" :: "[i, i] => o" (infixl "\<notin>" 50)
"@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)
- Union :: "i =>i" ("\<Union>_" [90] 90)
- Inter :: "i =>i" ("\<Inter>_" [90] 90)
"@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)
@@ -192,8 +198,7 @@
finalconsts
- 0 Pow Inf Union PrimReplace
- "op :"
+ 0 Pow Inf Union PrimReplace mem
defs
(*don't try to use constdefs: the declaration order is tightly constrained*)
@@ -293,12 +298,6 @@
(* Restrict the relation r to the domain A *)
restrict_def: "restrict(r,A) == {z : r. \<exists>x\<in>A. \<exists>y. z = <x,y>}"
-(* Pattern-matching and 'Dependent' type operators *)
-
-print_translation {*
- [("Pi", dependent_tr' ("@PROD", "op ->")),
- ("Sigma", dependent_tr' ("@SUM", "op *"))];
-*}
subsection {* Substitution*}
--- a/src/ZF/ind_syntax.ML Wed Oct 03 21:29:05 2007 +0200
+++ b/src/ZF/ind_syntax.ML Wed Oct 03 22:33:17 2007 +0200
@@ -24,7 +24,7 @@
val iT = Type("i",[]);
-val mem_const = Const("op :", [iT,iT]--->FOLogic.oT);
+val mem_const = @{term mem};
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
fun mk_all_imp (A,P) =
@@ -34,7 +34,7 @@
val Part_const = Const("Part", [iT,iT-->iT]--->iT);
-val apply_const = Const("op `", [iT,iT]--->iT);
+val apply_const = @{term apply};
val Vrecursor_const = Const("Univ.Vrecursor", [[iT,iT]--->iT, iT]--->iT);
@@ -44,14 +44,14 @@
(*simple error-checking in the premises of an inductive definition*)
fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
error"Premises may not be conjuctive"
- | chk_prem rec_hd (Const("op :",_) $ t $ X) =
+ | chk_prem rec_hd (Const(@{const_name mem},_) $ t $ X) =
(Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
| chk_prem rec_hd t =
(Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ());
(*Return the conclusion of a rule, of the form t:X*)
fun rule_concl rl =
- let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) =
+ let val Const("Trueprop",_) $ (Const(@{const_name mem},_) $ t $ X) =
Logic.strip_imp_concl rl
in (t,X) end;
@@ -74,7 +74,7 @@
type constructor_spec =
((string * typ * mixfix) * string * term list * term list);
-fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
+fun dest_mem (Const(@{const_name mem},_) $ x $ A) = (x,A)
| dest_mem _ = error "Constructor specifications must have the form x:A";
(*read a constructor specification*)
@@ -102,7 +102,7 @@
fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);
-fun mk_Un (t1, t2) = Const("op Un", [iT,iT]--->iT) $ t1 $ t2;
+fun mk_Un (t1, t2) = Const(@{const_name Un}, [iT,iT]--->iT) $ t1 $ t2;
val empty = Const("0", iT)
and univ = Const("Univ.univ", iT-->iT)
--- a/src/ZF/simpdata.ML Wed Oct 03 21:29:05 2007 +0200
+++ b/src/ZF/simpdata.ML Wed Oct 03 22:33:17 2007 +0200
@@ -23,7 +23,7 @@
in case concl_of th of
Const("Trueprop",_) $ P =>
(case P of
- Const("op :",_) $ a $ b => tryrules mem_pairs b
+ Const(@{const_name mem},_) $ a $ b => tryrules mem_pairs b
| Const("True",_) => []
| Const("False",_) => []
| A => tryrules conn_pairs A)
@@ -40,8 +40,8 @@
(*Analyse a:b, where b is rigid*)
val ZF_mem_pairs =
[("Collect", [CollectD1,CollectD2]),
- ("op -", [DiffD1,DiffD2]),
- ("op Int", [IntD1,IntD2])];
+ (@{const_name Diff}, [DiffD1,DiffD2]),
+ (@{const_name Int}, [IntD1,IntD2])];
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);