tuned;
authorwenzelm
Thu Oct 18 21:22:40 2001 +0200 (2001-10-18)
changeset 11833475f772ab643
parent 11832 8fca3665d1ee
child 11834 02825c735938
tuned;
src/HOL/Record.thy
src/HOL/Tools/record_package.ML
     1.1 --- a/src/HOL/Record.thy	Thu Oct 18 21:07:29 2001 +0200
     1.2 +++ b/src/HOL/Record.thy	Thu Oct 18 21:22:40 2001 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  constdefs
     1.6    product_type :: "('p => 'a * 'b) => ('a * 'b => 'p) =>
     1.7 -    ('a => 'b => 'p) => ('p \<Rightarrow> 'a) => ('p => 'b) => bool"
     1.8 +    ('a => 'b => 'p) => ('p => 'a) => ('p => 'b) => bool"
     1.9    "product_type Rep Abs pair dest1 dest2 ==
    1.10      type_definition Rep Abs UNIV \<and>
    1.11      pair = (\<lambda>a b. Abs (a, b)) \<and>
    1.12 @@ -23,8 +23,8 @@
    1.13  lemma product_typeI:
    1.14    "type_definition Rep Abs UNIV ==>
    1.15      pair == \<lambda>a b. Abs (a, b) ==>
    1.16 -    dest1 == (\<lambda>p. fst (Rep p)) \<Longrightarrow>
    1.17 -    dest2 == (\<lambda>p. snd (Rep p)) \<Longrightarrow>
    1.18 +    dest1 == (\<lambda>p. fst (Rep p)) ==>
    1.19 +    dest2 == (\<lambda>p. snd (Rep p)) ==>
    1.20      product_type Rep Abs pair dest1 dest2"
    1.21    by (simp add: product_type_def)
    1.22  
    1.23 @@ -93,10 +93,10 @@
    1.24  
    1.25  theorem product_type_cases [cases set: product_type]:
    1.26    "product_type Rep Abs pair dest1 dest2 ==>
    1.27 -    (!!x y. p = pair x y \<Longrightarrow> C) ==> C"
    1.28 +    (!!x y. p = pair x y ==> C) ==> C"
    1.29  proof -
    1.30    assume prod_type: "product_type Rep Abs pair dest1 dest2"
    1.31 -  assume "!!x y. p = pair x y \<Longrightarrow> C"
    1.32 +  assume "!!x y. p = pair x y ==> C"
    1.33    with prod_type show C
    1.34      by (induct p) (simp only: product_type_inject [OF prod_type], blast)
    1.35  qed
    1.36 @@ -112,7 +112,7 @@
    1.37  
    1.38  theorem product_type_split_paired_all:
    1.39    "product_type Rep Abs pair dest1 dest2 ==>
    1.40 -  (\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (pair a b))"
    1.41 +  (!!x. PROP P x) == (!!a b. PROP P (pair a b))"
    1.42  proof
    1.43    fix a b
    1.44    assume "!!x. PROP P x"
    1.45 @@ -126,19 +126,13 @@
    1.46  qed
    1.47  
    1.48  
    1.49 -text {* \medskip Type class for record extensions. *}
    1.50 +subsection {* Type class for record extensions *}
    1.51  
    1.52  axclass more < "term"
    1.53  instance unit :: more ..
    1.54  
    1.55  
    1.56 -subsection {* Record package setup *}
    1.57 -
    1.58 -use "Tools/record_package.ML"
    1.59 -setup RecordPackage.setup
    1.60 -
    1.61 -
    1.62 -subsection {* Concrete syntax *}
    1.63 +subsection {* Concrete record syntax *}
    1.64  
    1.65  nonterminals
    1.66    ident field_type field_types field fields update updates
    1.67 @@ -172,17 +166,10 @@
    1.68    "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
    1.69    "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
    1.70  
    1.71 -parse_translation {*
    1.72 -  let
    1.73 -    fun update_name_tr (Free (x, T) :: ts) =
    1.74 -          Term.list_comb (Free (suffix RecordPackage.updateN x, T), ts)
    1.75 -      | update_name_tr (Const (x, T) :: ts) =
    1.76 -          Term.list_comb (Const (suffix RecordPackage.updateN x, T), ts)
    1.77 -      | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
    1.78 -          Term.list_comb (c $ update_name_tr [t] $
    1.79 -            (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts)
    1.80 -      | update_name_tr ts = raise TERM ("update_name_tr", ts);
    1.81 -  in [("_update_name", update_name_tr)] end
    1.82 -*}
    1.83 +
    1.84 +subsection {* Package setup *}
    1.85 +
    1.86 +use "Tools/record_package.ML"
    1.87 +setup RecordPackage.setup
    1.88  
    1.89  end
     2.1 --- a/src/HOL/Tools/record_package.ML	Thu Oct 18 21:07:29 2001 +0200
     2.2 +++ b/src/HOL/Tools/record_package.ML	Thu Oct 18 21:22:40 2001 +0200
     2.3 @@ -50,8 +50,6 @@
     2.4  val product_type_inject = thm "product_type_inject";
     2.5  val product_type_conv1 = thm "product_type_conv1";
     2.6  val product_type_conv2 = thm "product_type_conv2";
     2.7 -val product_type_induct = thm "product_type_induct";
     2.8 -val product_type_cases = thm "product_type_cases";
     2.9  val product_type_split_paired_all = thm "product_type_split_paired_all";
    2.10  
    2.11  
    2.12 @@ -113,13 +111,6 @@
    2.13  val AbsN = "Abs_";
    2.14  
    2.15  
    2.16 -(** generic operations **)
    2.17 -
    2.18 -(* adhoc priming of vars *)
    2.19 -
    2.20 -fun prime (Free (x, T)) = Free (x ^ "'", T)
    2.21 -  | prime t = raise TERM ("prime: no free variable", [t]);
    2.22 -
    2.23  
    2.24  (** tuple operations **)
    2.25  
    2.26 @@ -148,7 +139,7 @@
    2.27  fun mk_Abs U (c, T) =
    2.28    Const (suffix field_typeN (prefix_base AbsN c),
    2.29      HOLogic.mk_prodT (T, U) --> mk_fieldT ((c, T), U));
    2.30 -  
    2.31 +
    2.32  
    2.33  (* constructors *)
    2.34  
    2.35 @@ -266,12 +257,21 @@
    2.36    | record_update_tr ts = raise TERM ("record_update_tr", ts);
    2.37  
    2.38  
    2.39 +fun update_name_tr (Free (x, T) :: ts) = Term.list_comb (Free (suffix updateN x, T), ts)
    2.40 +  | update_name_tr (Const (x, T) :: ts) = Term.list_comb (Const (suffix updateN x, T), ts)
    2.41 +  | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
    2.42 +      Term.list_comb (c $ update_name_tr [t] $
    2.43 +        (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts)
    2.44 +  | update_name_tr ts = raise TERM ("update_name_tr", ts);
    2.45 +
    2.46 +
    2.47  val parse_translation =
    2.48   [("_record_type", record_type_tr),
    2.49    ("_record_type_scheme", record_type_scheme_tr),
    2.50    ("_record", record_tr),
    2.51    ("_record_scheme", record_scheme_tr),
    2.52 -  ("_record_update", record_update_tr)];
    2.53 +  ("_record_update", record_update_tr),
    2.54 +  ("_update_name", update_name_tr)];
    2.55  
    2.56  
    2.57  (* print translations *)