--- a/src/HOL/Record.thy Sat Aug 15 15:29:54 2009 +0200
+++ b/src/HOL/Record.thy Thu Aug 27 00:40:53 2009 +1000
@@ -1,26 +1,36 @@
(* Title: HOL/Record.thy
+ ID: $Id: Record.thy,v 1.33 2007/12/19 15:32:12 schirmer Exp $
Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
*)
header {* Extensible records with structural subtyping *}
theory Record
-imports Product_Type
-uses ("Tools/record.ML")
+imports Product_Type IsTuple
+uses ("Tools/record_package.ML")
begin
lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
by simp
-lemma rec_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
- by simp
-
-lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
- by simp
-
lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)"
by (simp add: comp_def)
+lemma meta_iffD2:
+ "\<lbrakk> PROP P \<equiv> PROP Q; PROP Q \<rbrakk> \<Longrightarrow> PROP P"
+ by simp
+
+lemma o_eq_dest_lhs:
+ "a o b = c \<Longrightarrow> a (b v) = c v"
+ by clarsimp
+
+lemma id_o_refl:
+ "id o f = f o id"
+ by simp
+
+lemma o_eq_id_dest:
+ "a o b = id o c \<Longrightarrow> a (b v) = c v"
+ by clarsimp
subsection {* Concrete record syntax *}
@@ -55,7 +65,7 @@
"_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
"_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
-use "Tools/record.ML"
-setup Record.setup
+use "Tools/record_package.ML"
+setup RecordPackage.setup
end