--- 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
+