diff -r 2c9b463044ec -r 2f885b7e5ba7 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Sat May 01 22:28:51 2004 +0200
+++ b/src/HOL/Record.thy	Mon May 03 23:22:17 2004 +0200
@@ -1,88 +1,32 @@
 (*  Title:      HOL/Record.thy
     ID:         $Id$
-    Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
+    Author:     Wolfgang Naraschewski, Norbert Schirmer  and Markus Wenzel, TU Muenchen
 *)
 
-header {* Extensible records with structural subtyping *}
-
 theory Record = Product_Type
 files ("Tools/record_package.ML"):
 
-
-subsection {* Abstract product types *}
-
-locale product_type =
-  fixes Rep and Abs and pair and dest1 and dest2
-  assumes "typedef": "type_definition Rep Abs UNIV"
-    and pair: "pair == (\<lambda>a b. Abs (a, b))"
-    and dest1: "dest1 == (\<lambda>p. fst (Rep p))"
-    and dest2: "dest2 == (\<lambda>p. snd (Rep p))"
-
-lemma (in product_type)
-    "inject": "(pair x y = pair x' y') = (x = x' \<and> y = y')"
-  by (simp add: pair type_definition.Abs_inject [OF "typedef"])
-
-lemma (in product_type) conv1: "dest1 (pair x y) = x"
-  by (simp add: pair dest1 type_definition.Abs_inverse [OF "typedef"])
-
-lemma (in product_type) conv2: "dest2 (pair x y) = y"
-  by (simp add: pair dest2 type_definition.Abs_inverse [OF "typedef"])
-
-lemma (in product_type) induct [induct type]:
-  assumes hyp: "!!x y. P (pair x y)"
-  shows "P p"
-proof (rule type_definition.Abs_induct [OF "typedef"])
-  fix q show "P (Abs q)"
-  proof (induct q)
-    fix x y have "P (pair x y)" by (rule hyp)
-    also have "pair x y = Abs (x, y)" by (simp only: pair)
-    finally show "P (Abs (x, y))" .
-  qed
-qed
+ML {*
+val [h1, h2] = Goal "PROP Goal (\<And>x. PROP P x) \<Longrightarrow> (PROP P x \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q";
+by (rtac h2 1);
+by (rtac (gen_all (h1 RS Drule.rev_triv_goal)) 1);
+qed "meta_allE";
+*}
 
-lemma (in product_type) cases [cases type]:
-    "(!!x y. p = pair x y ==> C) ==> C"
-  by (induct p) (auto simp add: "inject")
-
-lemma (in product_type) surjective_pairing:
-    "p = pair (dest1 p) (dest2 p)"
-  by (induct p) (simp only: conv1 conv2)
+lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
+  by simp
 
-lemma (in product_type) split_paired_all:
-  "(!!x. PROP P x) == (!!a b. PROP P (pair a b))"
-proof
-  fix a b
-  assume "!!x. PROP P x"
-  thus "PROP P (pair a b)" .
-next
-  fix x
-  assume "!!a b. PROP P (pair a b)"
-  hence "PROP P (pair (dest1 x) (dest2 x))" .
-  thus "PROP P x" by (simp only: surjective_pairing [symmetric])
-qed
+lemma rec_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
+  by simp
 
-lemma (in product_type) split_paired_All:
-  "(ALL x. P x) = (ALL a b. P (pair a b))"
-proof
-  fix a b
-  assume "ALL x. P x"
-  thus "ALL a b. P (pair a b)" by rules
-next
-  assume P: "ALL a b. P (pair a b)"
-  show "ALL x. P x"
-  proof
-    fix x
-    from P have "P (pair (dest1 x) (dest2 x))" by rules
-    thus "P x" by (simp only: surjective_pairing [symmetric])
-  qed
-qed
+lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
+  by simp
 
 
 subsection {* Concrete record syntax *}
 
 nonterminals
   ident field_type field_types field fields update updates
-
 syntax
   "_constify"           :: "id => ident"                        ("_")
   "_constify"           :: "longid => ident"                    ("_")
@@ -112,10 +56,27 @@
   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
 
+(* 
 
-subsection {* Package setup *}
+  "_structure"             :: "fields => 'a"          ("(3{| _ |})")
+  "_structure_scheme"      :: "[fields, 'a] => 'a"    ("(3{| _,/ (2... =/ _) |})")
+  
+  "_structure_update_name":: idt
+  "_structure_update"  :: "['a, updates] \<Rightarrow> 'b"    ("_/(3{| _ |})" [900,0] 900)
 
-use "Tools/record_package.ML"
-setup RecordPackage.setup
+  "_structure_type"        :: "field_types => type"    ("(3{| _ |})")
+  "_structure_type_scheme" :: "[field_types, type] => type" 
+                                      ("(3{| _,/ (2... ::/ _) |})")
+syntax (xsymbols)
+
+ "_structure_scheme"   :: "[fields, 'a] => 'a"       ("(3{|_,/ (2\<dots> =/ _)|})")
+
+  "_structure_type_scheme" :: "[field_types, type] => type"        
+                                      ("(3{|_,/ (2\<dots> ::/ _)|})")
+
+*)
+use "Tools/record_package.ML";
+setup RecordPackage.setup;
 
 end
+