# HG changeset patch # User wenzelm # Date 1003432960 -7200 # Node ID 475f772ab6436a351f62f227892894be8f5bab84 # Parent 8fca3665d1ee165e34392d265c6d5ba69be46b64 tuned; diff -r 8fca3665d1ee -r 475f772ab643 src/HOL/Record.thy --- a/src/HOL/Record.thy Thu Oct 18 21:07:29 2001 +0200 +++ b/src/HOL/Record.thy Thu Oct 18 21:22:40 2001 +0200 @@ -13,7 +13,7 @@ constdefs product_type :: "('p => 'a * 'b) => ('a * 'b => 'p) => - ('a => 'b => 'p) => ('p \ 'a) => ('p => 'b) => bool" + ('a => 'b => 'p) => ('p => 'a) => ('p => 'b) => bool" "product_type Rep Abs pair dest1 dest2 == type_definition Rep Abs UNIV \ pair = (\a b. Abs (a, b)) \ @@ -23,8 +23,8 @@ lemma product_typeI: "type_definition Rep Abs UNIV ==> pair == \a b. Abs (a, b) ==> - dest1 == (\p. fst (Rep p)) \ - dest2 == (\p. snd (Rep p)) \ + dest1 == (\p. fst (Rep p)) ==> + dest2 == (\p. snd (Rep p)) ==> product_type Rep Abs pair dest1 dest2" by (simp add: product_type_def) @@ -93,10 +93,10 @@ theorem product_type_cases [cases set: product_type]: "product_type Rep Abs pair dest1 dest2 ==> - (!!x y. p = pair x y \ C) ==> C" + (!!x y. p = pair x y ==> C) ==> C" proof - assume prod_type: "product_type Rep Abs pair dest1 dest2" - assume "!!x y. p = pair x y \ C" + assume "!!x y. p = pair x y ==> C" with prod_type show C by (induct p) (simp only: product_type_inject [OF prod_type], blast) qed @@ -112,7 +112,7 @@ theorem product_type_split_paired_all: "product_type Rep Abs pair dest1 dest2 ==> - (\x. PROP P x) \ (\a b. PROP P (pair a b))" + (!!x. PROP P x) == (!!a b. PROP P (pair a b))" proof fix a b assume "!!x. PROP P x" @@ -126,19 +126,13 @@ qed -text {* \medskip Type class for record extensions. *} +subsection {* Type class for record extensions *} axclass more < "term" instance unit :: more .. -subsection {* Record package setup *} - -use "Tools/record_package.ML" -setup RecordPackage.setup - - -subsection {* Concrete syntax *} +subsection {* Concrete record syntax *} nonterminals ident field_type field_types field fields update updates @@ -172,17 +166,10 @@ "_record_scheme" :: "[fields, 'a] => 'a" ("(3\_,/ (2\ =/ _)\)") "_record_update" :: "['a, updates] => 'b" ("_/(3\_\)" [900,0] 900) -parse_translation {* - let - fun update_name_tr (Free (x, T) :: ts) = - Term.list_comb (Free (suffix RecordPackage.updateN x, T), ts) - | update_name_tr (Const (x, T) :: ts) = - Term.list_comb (Const (suffix RecordPackage.updateN x, T), ts) - | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) = - Term.list_comb (c $ update_name_tr [t] $ - (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts) - | update_name_tr ts = raise TERM ("update_name_tr", ts); - in [("_update_name", update_name_tr)] end -*} + +subsection {* Package setup *} + +use "Tools/record_package.ML" +setup RecordPackage.setup end diff -r 8fca3665d1ee -r 475f772ab643 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Thu Oct 18 21:07:29 2001 +0200 +++ b/src/HOL/Tools/record_package.ML Thu Oct 18 21:22:40 2001 +0200 @@ -50,8 +50,6 @@ val product_type_inject = thm "product_type_inject"; val product_type_conv1 = thm "product_type_conv1"; val product_type_conv2 = thm "product_type_conv2"; -val product_type_induct = thm "product_type_induct"; -val product_type_cases = thm "product_type_cases"; val product_type_split_paired_all = thm "product_type_split_paired_all"; @@ -113,13 +111,6 @@ val AbsN = "Abs_"; -(** generic operations **) - -(* adhoc priming of vars *) - -fun prime (Free (x, T)) = Free (x ^ "'", T) - | prime t = raise TERM ("prime: no free variable", [t]); - (** tuple operations **) @@ -148,7 +139,7 @@ fun mk_Abs U (c, T) = Const (suffix field_typeN (prefix_base AbsN c), HOLogic.mk_prodT (T, U) --> mk_fieldT ((c, T), U)); - + (* constructors *) @@ -266,12 +257,21 @@ | record_update_tr ts = raise TERM ("record_update_tr", ts); +fun update_name_tr (Free (x, T) :: ts) = Term.list_comb (Free (suffix updateN x, T), ts) + | update_name_tr (Const (x, T) :: ts) = Term.list_comb (Const (suffix updateN x, T), ts) + | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) = + Term.list_comb (c $ update_name_tr [t] $ + (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts) + | update_name_tr ts = raise TERM ("update_name_tr", ts); + + val parse_translation = [("_record_type", record_type_tr), ("_record_type_scheme", record_type_scheme_tr), ("_record", record_tr), ("_record_scheme", record_scheme_tr), - ("_record_update", record_update_tr)]; + ("_record_update", record_update_tr), + ("_update_name", update_name_tr)]; (* print translations *)