# HG changeset patch # User wenzelm # Date 1265925622 -3600 # Node ID 446c5063e4fdcdd9b2abb56326c447844e4fd920 # Parent b1fd1d756e208da4d9042998a096bb7f8cc3d0e6 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning; diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Complete_Lattice.thy --- a/src/HOL/Complete_Lattice.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/Complete_Lattice.thy Thu Feb 11 23:00:22 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 \ 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\_./ _)" [0, 10] 10) - "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" [0, 10] 10) + "_UNION1" :: "pttrns => 'b set => 'b set" ("(3\_./ _)" [0, 10] 10) + "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" [0, 10] 10) syntax (latex output) - "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10) - "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\(00\<^bsub>_\_\<^esub>)/ _)" [0, 10] 10) + "_UNION1" :: "pttrns => 'b set => 'b set" ("(3\(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10) + "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\(00\<^bsub>_\_\<^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: "(\x\A. B x) = \(B`A)" @@ -518,16 +518,16 @@ "INTER \ 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\_./ _)" [0, 10] 10) - "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" [0, 10] 10) + "_INTER1" :: "pttrns => 'b set => 'b set" ("(3\_./ _)" [0, 10] 10) + "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" [0, 10] 10) syntax (latex output) - "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10) - "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\(00\<^bsub>_\_\<^esub>)/ _)" [0, 10] 10) + "_INTER1" :: "pttrns => 'b set => 'b set" ("(3\(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10) + "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\(00\<^bsub>_\_\<^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: "(\x\A. B x) = \(B`A)" diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/Finite_Set.thy Thu Feb 11 23:00:22 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 *} diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Fun.thy --- a/src/HOL/Fun.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/Fun.thy Thu Feb 11 23:00:22 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)" diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/HOL.thy Thu Feb 11 23:00:22 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_ \/ _)" 10) diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/Hilbert_Choice.thy Thu Feb 11 23:00:22 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) diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/Inductive.thy Thu Feb 11 23:00:22 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 diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Library/Coinductive_List.thy --- a/src/HOL/Library/Coinductive_List.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/Library/Coinductive_List.thy Thu Feb 11 23:00:22 2010 +0100 @@ -204,7 +204,7 @@ LNil :: logic LCons :: logic translations - "case p of LNil \ a | LCons x l \ b" \ "CONST llist_case a (\x l. b) p" + "case p of XCONST LNil \ a | XCONST LCons x l \ b" \ "CONST llist_case a (\x l. b) p" lemma llist_case_LNil [simp, code]: "llist_case c d LNil = c" by (simp add: llist_case_def LNil_def diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Library/Numeral_Type.thy --- a/src/HOL/Library/Numeral_Type.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/Library/Numeral_Type.thy Thu Feb 11 23:00:22 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; *} diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Library/OptionalSugar.thy --- a/src/HOL/Library/OptionalSugar.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/Library/OptionalSugar.thy Thu Feb 11 23:00:22 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 \ 'a list \ 'a list" (infixl "\<^raw:\isacharat>" 65) + "_appendL" :: "'a list \ 'a list \ '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 *) diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Library/State_Monad.thy --- a/src/HOL/Library/State_Monad.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/Library/State_Monad.thy Thu Feb 11 23:00:22 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 {* diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/List.thy --- a/src/HOL/List.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/List.thy Thu Feb 11 23:00:22 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 \ '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[_\_ ./ _])") + "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\_ ./ _])") syntax (HTML output) - "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\_ ./ _])") + "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\_ ./ _])") primrec foldl :: "('b \ 'a \ 'b) \ 'b \ 'a list \ '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\xs]" term "[e x y. x\xs, y\ys]" @@ -418,9 +426,11 @@ term "[(x,y,z). x\xs, x>b, y\ys]" term "[(x,y,z). x\xs, y\ys,y>x]" term "[(x,y,z). x\xs, y\ys,z\zs]" +(* term "[(x,y). x\xs, let xx = x+x, y\ys, y \ xx]" *) + subsubsection {* @{const Nil} and @{const Cons} *} lemma not_Cons_self [simp]: @@ -1019,6 +1029,7 @@ "set xs - {y} = set (filter (\x. \ (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"\"}*} 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 \ 'a list \ 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" diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Map.thy --- a/src/HOL/Map.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/Map.thy Thu Feb 11 23:00:22 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" diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/Orderings.thy Thu Feb 11 23:00:22 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 *} diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/Product_Type.thy Thu Feb 11 23:00:22 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 "\(x,y). f x y" and "split (\x. f x)" as "\(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 "\" 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 diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Set.thy --- a/src/HOL/Set.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/Set.thy Thu Feb 11 23:00:22 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{_ \/ _./ _})") - + "_Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ \/ _./ _})") 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 \ x \ 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\!_\_./ _)" [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 {* diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/SetInterval.thy Thu Feb 11 23:00:22 2010 +0100 @@ -54,22 +54,22 @@ @{term"{m.. '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\ _\_./ _)" 10) - "@UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\ _<_./ _)" 10) - "@INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\ _\_./ _)" 10) - "@INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\ _<_./ _)" 10) + "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\ _\_./ _)" 10) + "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\ _<_./ _)" 10) + "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\ _\_./ _)" 10) + "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\ _<_./ _)" 10) syntax (latex output) - "@UNION_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ \ _)/ _)" 10) - "@UNION_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ < _)/ _)" 10) - "@INTER_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ \ _)/ _)" 10) - "@INTER_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ < _)/ _)" 10) + "_UNION_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ \ _)/ _)" 10) + "_UNION_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ < _)/ _)" 10) + "_INTER_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ \ _)/ _)" 10) + "_INTER_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ < _)/ _)" 10) translations "UN i<=n. A" == "UN i:{..n}. A" diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/String.thy --- a/src/HOL/String.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/String.thy Thu Feb 11 23:00:22 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 diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Tools/float_syntax.ML --- a/src/HOL/Tools/float_syntax.ML Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/Tools/float_syntax.ML Thu Feb 11 23:00:22 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; diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Tools/numeral_syntax.ML --- a/src/HOL/Tools/numeral_syntax.ML Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/Tools/numeral_syntax.ML Thu Feb 11 23:00:22 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; diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Tools/string_syntax.ML --- a/src/HOL/Tools/string_syntax.ML Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/Tools/string_syntax.ML Thu Feb 11 23:00:22 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; diff -r b1fd1d756e20 -r 446c5063e4fd src/HOL/Typerep.thy --- a/src/HOL/Typerep.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOL/Typerep.thy Thu Feb 11 23:00:22 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 {* diff -r b1fd1d756e20 -r 446c5063e4fd src/HOLCF/Cfun.thy --- a/src/HOLCF/Cfun.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOLCF/Cfun.thy Thu Feb 11 23:00:22 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] \ logic" ("(3\ _./ _)" [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 *} diff -r b1fd1d756e20 -r 446c5063e4fd src/HOLCF/Fixrec.thy --- a/src/HOLCF/Fixrec.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOLCF/Fixrec.thy Thu Feb 11 23:00:22 2010 +0100 @@ -226,10 +226,10 @@ "_variable _noargs r" => "CONST unit_when\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; *} diff -r b1fd1d756e20 -r 446c5063e4fd src/HOLCF/Sprod.thy --- a/src/HOLCF/Sprod.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOLCF/Sprod.thy Thu Feb 11 23:00:22 2010 +0100 @@ -51,7 +51,7 @@ "ssplit = (\ f. strictify\(\ p. f\(sfst\p)\(ssnd\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\x\y"