# HG changeset patch # User wenzelm # Date 1191443597 -7200 # Node ID 78e6a3cea367e889f749d7fc47ed6b353922cc8d # Parent c4f13ab78f9df121ad2f03f9d5eef54b9e9a777e avoid unnamed infixes; diff -r c4f13ab78f9d -r 78e6a3cea367 src/ZF/Inductive.thy --- 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) diff -r c4f13ab78f9d -r 78e6a3cea367 src/ZF/OrderType.thy --- 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 "\\" 70) +notation (xsymbols) + omult (infixl "\\" 70) -syntax (HTML output) - "op **" :: "[i,i] => i" (infixl "\\" 70) +notation (HTML output) + omult (infixl "\\" 70) subsection{*Proofs needing the combination of Ordinal.thy and Order.thy*} diff -r c4f13ab78f9d -r 78e6a3cea367 src/ZF/Tools/datatype_package.ML --- 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; diff -r c4f13ab78f9d -r 78e6a3cea367 src/ZF/Tools/induct_tacs.ML --- 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; diff -r c4f13ab78f9d -r 78e6a3cea367 src/ZF/Tools/inductive_package.ML --- 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*) diff -r c4f13ab78f9d -r 78e6a3cea367 src/ZF/Tools/typechk.ML --- 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; diff -r c4f13ab78f9d -r 78e6a3cea367 src/ZF/ZF.thy --- 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\*) - "<=" :: "[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 @@ "%.b" == "split(%x y. b)" +notation (xsymbols) + cart_prod (infixr "\" 80) and + Int (infixl "\" 70) and + Un (infixl "\" 65) and + function_space (infixr "\" 60) and + Subset (infixl "\" 50) and + mem (infixl "\" 50) and + not_mem (infixl "\" 50) and + Union ("\_" [90] 90) and + Inter ("\_" [90] 90) + syntax (xsymbols) - "op *" :: "[i, i] => i" (infixr "\" 80) - "op Int" :: "[i, i] => i" (infixl "\" 70) - "op Un" :: "[i, i] => i" (infixl "\" 65) - "op ->" :: "[i, i] => i" (infixr "\" 60) - "op <=" :: "[i, i] => o" (infixl "\" 50) - "op :" :: "[i, i] => o" (infixl "\" 50) - "op ~:" :: "[i, i] => o" (infixl "\" 50) "@Collect" :: "[pttrn, i, o] => i" ("(1{_ \ _ ./ _})") "@Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \ _, _})") "@RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \ _})" [51,0,51]) "@UNION" :: "[pttrn, i, i] => i" ("(3\_\_./ _)" 10) "@INTER" :: "[pttrn, i, i] => i" ("(3\_\_./ _)" 10) - Union :: "i =>i" ("\_" [90] 90) - Inter :: "i =>i" ("\_" [90] 90) "@PROD" :: "[pttrn, i, i] => i" ("(3\_\_./ _)" 10) "@SUM" :: "[pttrn, i, i] => i" ("(3\_\_./ _)" 10) "@lam" :: "[pttrn, i, i] => i" ("(3\_\_./ _)" 10) @@ -168,20 +172,22 @@ "@Tuple" :: "[i, is] => i" ("\(_,/ _)\") "@pattern" :: "patterns => pttrn" ("\_\") +notation (HTML output) + cart_prod (infixr "\" 80) and + Int (infixl "\" 70) and + Un (infixl "\" 65) and + Subset (infixl "\" 50) and + mem (infixl "\" 50) and + not_mem (infixl "\" 50) and + Union ("\_" [90] 90) and + Inter ("\_" [90] 90) + syntax (HTML output) - "op *" :: "[i, i] => i" (infixr "\" 80) - "op Int" :: "[i, i] => i" (infixl "\" 70) - "op Un" :: "[i, i] => i" (infixl "\" 65) - "op <=" :: "[i, i] => o" (infixl "\" 50) - "op :" :: "[i, i] => o" (infixl "\" 50) - "op ~:" :: "[i, i] => o" (infixl "\" 50) "@Collect" :: "[pttrn, i, o] => i" ("(1{_ \ _ ./ _})") "@Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \ _, _})") "@RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \ _})" [51,0,51]) "@UNION" :: "[pttrn, i, i] => i" ("(3\_\_./ _)" 10) "@INTER" :: "[pttrn, i, i] => i" ("(3\_\_./ _)" 10) - Union :: "i =>i" ("\_" [90] 90) - Inter :: "i =>i" ("\_" [90] 90) "@PROD" :: "[pttrn, i, i] => i" ("(3\_\_./ _)" 10) "@SUM" :: "[pttrn, i, i] => i" ("(3\_\_./ _)" 10) "@lam" :: "[pttrn, i, i] => i" ("(3\_\_./ _)" 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. \x\A. \y. z = }" -(* Pattern-matching and 'Dependent' type operators *) - -print_translation {* - [("Pi", dependent_tr' ("@PROD", "op ->")), - ("Sigma", dependent_tr' ("@SUM", "op *"))]; -*} subsection {* Substitution*} diff -r c4f13ab78f9d -r 78e6a3cea367 src/ZF/ind_syntax.ML --- 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) diff -r c4f13ab78f9d -r 78e6a3cea367 src/ZF/simpdata.ML --- 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);