src/HOL/Record.thy
changeset 14700 2f885b7e5ba7
parent 14080 9a50427d7165
child 14701 62a724ce51c7
     1.1 --- a/src/HOL/Record.thy	Sat May 01 22:28:51 2004 +0200
     1.2 +++ b/src/HOL/Record.thy	Mon May 03 23:22:17 2004 +0200
     1.3 @@ -1,88 +1,32 @@
     1.4  (*  Title:      HOL/Record.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     1.7 +    Author:     Wolfgang Naraschewski, Norbert Schirmer  and Markus Wenzel, TU Muenchen
     1.8  *)
     1.9  
    1.10 -header {* Extensible records with structural subtyping *}
    1.11 -
    1.12  theory Record = Product_Type
    1.13  files ("Tools/record_package.ML"):
    1.14  
    1.15 -
    1.16 -subsection {* Abstract product types *}
    1.17 -
    1.18 -locale product_type =
    1.19 -  fixes Rep and Abs and pair and dest1 and dest2
    1.20 -  assumes "typedef": "type_definition Rep Abs UNIV"
    1.21 -    and pair: "pair == (\<lambda>a b. Abs (a, b))"
    1.22 -    and dest1: "dest1 == (\<lambda>p. fst (Rep p))"
    1.23 -    and dest2: "dest2 == (\<lambda>p. snd (Rep p))"
    1.24 -
    1.25 -lemma (in product_type)
    1.26 -    "inject": "(pair x y = pair x' y') = (x = x' \<and> y = y')"
    1.27 -  by (simp add: pair type_definition.Abs_inject [OF "typedef"])
    1.28 -
    1.29 -lemma (in product_type) conv1: "dest1 (pair x y) = x"
    1.30 -  by (simp add: pair dest1 type_definition.Abs_inverse [OF "typedef"])
    1.31 -
    1.32 -lemma (in product_type) conv2: "dest2 (pair x y) = y"
    1.33 -  by (simp add: pair dest2 type_definition.Abs_inverse [OF "typedef"])
    1.34 -
    1.35 -lemma (in product_type) induct [induct type]:
    1.36 -  assumes hyp: "!!x y. P (pair x y)"
    1.37 -  shows "P p"
    1.38 -proof (rule type_definition.Abs_induct [OF "typedef"])
    1.39 -  fix q show "P (Abs q)"
    1.40 -  proof (induct q)
    1.41 -    fix x y have "P (pair x y)" by (rule hyp)
    1.42 -    also have "pair x y = Abs (x, y)" by (simp only: pair)
    1.43 -    finally show "P (Abs (x, y))" .
    1.44 -  qed
    1.45 -qed
    1.46 +ML {*
    1.47 +val [h1, h2] = Goal "PROP Goal (\<And>x. PROP P x) \<Longrightarrow> (PROP P x \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q";
    1.48 +by (rtac h2 1);
    1.49 +by (rtac (gen_all (h1 RS Drule.rev_triv_goal)) 1);
    1.50 +qed "meta_allE";
    1.51 +*}
    1.52  
    1.53 -lemma (in product_type) cases [cases type]:
    1.54 -    "(!!x y. p = pair x y ==> C) ==> C"
    1.55 -  by (induct p) (auto simp add: "inject")
    1.56 -
    1.57 -lemma (in product_type) surjective_pairing:
    1.58 -    "p = pair (dest1 p) (dest2 p)"
    1.59 -  by (induct p) (simp only: conv1 conv2)
    1.60 +lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
    1.61 +  by simp
    1.62  
    1.63 -lemma (in product_type) split_paired_all:
    1.64 -  "(!!x. PROP P x) == (!!a b. PROP P (pair a b))"
    1.65 -proof
    1.66 -  fix a b
    1.67 -  assume "!!x. PROP P x"
    1.68 -  thus "PROP P (pair a b)" .
    1.69 -next
    1.70 -  fix x
    1.71 -  assume "!!a b. PROP P (pair a b)"
    1.72 -  hence "PROP P (pair (dest1 x) (dest2 x))" .
    1.73 -  thus "PROP P x" by (simp only: surjective_pairing [symmetric])
    1.74 -qed
    1.75 +lemma rec_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
    1.76 +  by simp
    1.77  
    1.78 -lemma (in product_type) split_paired_All:
    1.79 -  "(ALL x. P x) = (ALL a b. P (pair a b))"
    1.80 -proof
    1.81 -  fix a b
    1.82 -  assume "ALL x. P x"
    1.83 -  thus "ALL a b. P (pair a b)" by rules
    1.84 -next
    1.85 -  assume P: "ALL a b. P (pair a b)"
    1.86 -  show "ALL x. P x"
    1.87 -  proof
    1.88 -    fix x
    1.89 -    from P have "P (pair (dest1 x) (dest2 x))" by rules
    1.90 -    thus "P x" by (simp only: surjective_pairing [symmetric])
    1.91 -  qed
    1.92 -qed
    1.93 +lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
    1.94 +  by simp
    1.95  
    1.96  
    1.97  subsection {* Concrete record syntax *}
    1.98  
    1.99  nonterminals
   1.100    ident field_type field_types field fields update updates
   1.101 -
   1.102  syntax
   1.103    "_constify"           :: "id => ident"                        ("_")
   1.104    "_constify"           :: "longid => ident"                    ("_")
   1.105 @@ -112,10 +56,27 @@
   1.106    "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   1.107    "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
   1.108  
   1.109 +(* 
   1.110  
   1.111 -subsection {* Package setup *}
   1.112 +  "_structure"             :: "fields => 'a"          ("(3{| _ |})")
   1.113 +  "_structure_scheme"      :: "[fields, 'a] => 'a"    ("(3{| _,/ (2... =/ _) |})")
   1.114 +  
   1.115 +  "_structure_update_name":: idt
   1.116 +  "_structure_update"  :: "['a, updates] \<Rightarrow> 'b"    ("_/(3{| _ |})" [900,0] 900)
   1.117  
   1.118 -use "Tools/record_package.ML"
   1.119 -setup RecordPackage.setup
   1.120 +  "_structure_type"        :: "field_types => type"    ("(3{| _ |})")
   1.121 +  "_structure_type_scheme" :: "[field_types, type] => type" 
   1.122 +                                      ("(3{| _,/ (2... ::/ _) |})")
   1.123 +syntax (xsymbols)
   1.124 +
   1.125 + "_structure_scheme"   :: "[fields, 'a] => 'a"       ("(3{|_,/ (2\<dots> =/ _)|})")
   1.126 +
   1.127 +  "_structure_type_scheme" :: "[field_types, type] => type"        
   1.128 +                                      ("(3{|_,/ (2\<dots> ::/ _)|})")
   1.129 +
   1.130 +*)
   1.131 +use "Tools/record_package.ML";
   1.132 +setup RecordPackage.setup;
   1.133  
   1.134  end
   1.135 +