1.1 --- a/NEWS Sat May 01 22:28:51 2004 +0200
1.2 +++ b/NEWS Mon May 03 23:22:17 2004 +0200
1.3 @@ -19,6 +19,7 @@
1.4 depend on the signature of the theory context being presently used for
1.5 parsing/printing, see also isar-ref manual.
1.6
1.7 +
1.8 * Pure: improved indexed syntax and implicit structures. First of
1.9 all, indexed syntax provides a notational device for subscripted
1.10 application, using the new syntax \<^bsub>term\<^esub> for arbitrary
1.11 @@ -30,6 +31,17 @@
1.12 * Pure: tuned internal renaming of symbolic identifiers -- attach
1.13 primes instead of base 26 numbers.
1.14
1.15 +*** HOL ***
1.16 +
1.17 +* Records:
1.18 + Reimplementation of records to avoid performance problems for
1.19 + type inference. Records are no longer composed of nested field types,
1.20 + but of nested extension types. Therefore the record type only grows
1.21 + linear in the number of extensions and not in the number of fields.
1.22 + The top-level (users) view on records is preserved.
1.23 + Potential INCOMPATIBILITY only in strange cases, where the theory
1.24 + depends on the old record representation. The type generated for
1.25 + a record is called <record_name>_ext_type.
1.26
1.27 *** HOLCF ***
1.28
2.1 --- a/src/HOL/Bali/DeclConcepts.thy Sat May 01 22:28:51 2004 +0200
2.2 +++ b/src/HOL/Bali/DeclConcepts.thy Mon May 03 23:22:17 2004 +0200
2.3 @@ -92,7 +92,7 @@
2.4 lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a"
2.5 by (simp add: acc_modi_accmodi_def)
2.6
2.7 -instance access_field_type:: ("type","type") has_accmodi ..
2.8 +instance decl_ext_type:: ("type") has_accmodi ..
2.9
2.10 defs (overloaded)
2.11 decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
2.12 @@ -130,7 +130,7 @@
2.13 axclass has_declclass < "type"
2.14 consts declclass:: "'a::has_declclass \<Rightarrow> qtname"
2.15
2.16 -instance pid_field_type::("type","type") has_declclass ..
2.17 +instance qtname_ext_type::("type") has_declclass ..
2.18
2.19 defs (overloaded)
2.20 qtname_declclass_def: "declclass (q::qtname) \<equiv> q"
2.21 @@ -153,17 +153,17 @@
2.22 axclass has_static < "type"
2.23 consts is_static :: "'a::has_static \<Rightarrow> bool"
2.24
2.25 -instance access_field_type :: ("type","has_static") has_static ..
2.26 +instance decl_ext_type :: ("has_static") has_static ..
2.27
2.28 defs (overloaded)
2.29 decl_is_static_def:
2.30 "is_static (m::('a::has_static) decl_scheme) \<equiv> is_static (Decl.decl.more m)"
2.31
2.32 -instance static_field_type :: ("type","type") has_static ..
2.33 +instance member_ext_type :: ("type") has_static ..
2.34
2.35 defs (overloaded)
2.36 static_field_type_is_static_def:
2.37 - "is_static (m::(bool,'b::type) static_field_type) \<equiv> static_val m"
2.38 + "is_static (m::('b::type) member_ext_type) \<equiv> static_val m"
2.39
2.40 lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m"
2.41 apply (cases m)
2.42 @@ -401,37 +401,30 @@
2.43 axclass has_resTy < "type"
2.44 consts resTy:: "'a::has_resTy \<Rightarrow> ty"
2.45
2.46 -instance access_field_type :: ("type","has_resTy") has_resTy ..
2.47 +instance decl_ext_type :: ("has_resTy") has_resTy ..
2.48
2.49 defs (overloaded)
2.50 decl_resTy_def:
2.51 "resTy (m::('a::has_resTy) decl_scheme) \<equiv> resTy (Decl.decl.more m)"
2.52
2.53 -instance static_field_type :: ("type","has_resTy") has_resTy ..
2.54 -
2.55 -defs (overloaded)
2.56 -static_field_type_resTy_def:
2.57 - "resTy (m::(bool,'b::has_resTy) static_field_type)
2.58 - \<equiv> resTy (static_more m)"
2.59 -
2.60 -instance pars_field_type :: ("type","has_resTy") has_resTy ..
2.61 +instance member_ext_type :: ("has_resTy") has_resTy ..
2.62
2.63 defs (overloaded)
2.64 -pars_field_type_resTy_def:
2.65 - "resTy (m::(vname list,'b::has_resTy) pars_field_type)
2.66 - \<equiv> resTy (pars_more m)"
2.67 +member_ext_type_resTy_def:
2.68 + "resTy (m::('b::has_resTy) member_ext_type)
2.69 + \<equiv> resTy (member.more_val m)"
2.70
2.71 -instance resT_field_type :: ("type","type") has_resTy ..
2.72 +instance mhead_ext_type :: ("type") has_resTy ..
2.73
2.74 defs (overloaded)
2.75 -resT_field_type_resTy_def:
2.76 - "resTy (m::(ty,'b::type) resT_field_type)
2.77 +mhead_ext_type_resTy_def:
2.78 + "resTy (m::('b mhead_ext_type))
2.79 \<equiv> resT_val m"
2.80
2.81 lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m"
2.82 apply (cases m)
2.83 -apply (simp add: decl_resTy_def static_field_type_resTy_def
2.84 - pars_field_type_resTy_def resT_field_type_resTy_def
2.85 +apply (simp add: decl_resTy_def member_ext_type_resTy_def
2.86 + mhead_ext_type_resTy_def
2.87 member.dest_convs mhead.dest_convs)
2.88 done
2.89
3.1 --- a/src/HOL/Bali/Name.thy Sat May 01 22:28:51 2004 +0200
3.2 +++ b/src/HOL/Bali/Name.thy Mon May 03 23:22:17 2004 +0200
3.3 @@ -80,7 +80,7 @@
3.4 consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
3.5
3.6 (* Declare qtname as instance of has_qtname *)
3.7 -instance pid_field_type::(has_pname,"type") has_qtname ..
3.8 +instance qtname_ext_type::("type") has_qtname ..
3.9
3.10 defs (overloaded)
3.11 qtname_qtname_def: "qtname (q::qtname) \<equiv> q"
4.1 --- a/src/HOL/Bali/TypeRel.thy Sat May 01 22:28:51 2004 +0200
4.2 +++ b/src/HOL/Bali/TypeRel.thy Mon May 03 23:22:17 2004 +0200
4.3 @@ -545,7 +545,7 @@
4.4 lemma widen_Object:"\<lbrakk>isrtype G T;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>RefT T \<preceq> Class Object"
4.5 apply (case_tac T)
4.6 apply (auto)
4.7 -apply (subgoal_tac "G\<turnstile>pid_field_type\<preceq>\<^sub>C Object")
4.8 +apply (subgoal_tac "G\<turnstile>qtname_ext_type\<preceq>\<^sub>C Object")
4.9 apply (auto intro: subcls_ObjectI)
4.10 done
4.11
5.1 --- a/src/HOL/Bali/TypeSafe.thy Sat May 01 22:28:51 2004 +0200
5.2 +++ b/src/HOL/Bali/TypeSafe.thy Mon May 03 23:22:17 2004 +0200
5.3 @@ -776,12 +776,8 @@
5.4 apply (force intro: var_tys_Some_eq [THEN iffD2])
5.5 done
5.6
5.7 -lemma obj_split: "\<And> obj. \<exists> t vs. obj = \<lparr>tag=t,values=vs\<rparr>"
5.8 -proof record_split
5.9 - fix tag values more
5.10 - show "\<exists>t vs. \<lparr>tag = tag, values = values, \<dots> = more\<rparr> = \<lparr>tag = t, values = vs\<rparr>"
5.11 - by auto
5.12 -qed
5.13 +lemma obj_split: "\<exists> t vs. obj = \<lparr>tag=t,values=vs\<rparr>"
5.14 + by (cases obj) auto
5.15
5.16 lemma AVar_lemma2: "error_free state
5.17 \<Longrightarrow> error_free
5.18 @@ -3602,7 +3598,7 @@
5.19 show "G\<turnstile>statC\<preceq>\<^sub>C statDeclC"
5.20 by (auto dest!: accfield_fields dest: fields_declC)
5.21 from accfield
5.22 - show fld: "table_of (fields G statC) (fn, statDeclC) = Some f"
5.23 + show fld: "table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some f"
5.24 by (auto dest!: accfield_fields)
5.25 from wf show "wf_prog G" .
5.26 from conf_a s2 show "x2 = None \<longrightarrow> G,store2\<turnstile>a\<Colon>\<preceq>Class statC"
6.1 --- a/src/HOL/Record.thy Sat May 01 22:28:51 2004 +0200
6.2 +++ b/src/HOL/Record.thy Mon May 03 23:22:17 2004 +0200
6.3 @@ -1,88 +1,32 @@
6.4 (* Title: HOL/Record.thy
6.5 ID: $Id$
6.6 - Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
6.7 + Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
6.8 *)
6.9
6.10 -header {* Extensible records with structural subtyping *}
6.11 -
6.12 theory Record = Product_Type
6.13 files ("Tools/record_package.ML"):
6.14
6.15 -
6.16 -subsection {* Abstract product types *}
6.17 -
6.18 -locale product_type =
6.19 - fixes Rep and Abs and pair and dest1 and dest2
6.20 - assumes "typedef": "type_definition Rep Abs UNIV"
6.21 - and pair: "pair == (\<lambda>a b. Abs (a, b))"
6.22 - and dest1: "dest1 == (\<lambda>p. fst (Rep p))"
6.23 - and dest2: "dest2 == (\<lambda>p. snd (Rep p))"
6.24 -
6.25 -lemma (in product_type)
6.26 - "inject": "(pair x y = pair x' y') = (x = x' \<and> y = y')"
6.27 - by (simp add: pair type_definition.Abs_inject [OF "typedef"])
6.28 -
6.29 -lemma (in product_type) conv1: "dest1 (pair x y) = x"
6.30 - by (simp add: pair dest1 type_definition.Abs_inverse [OF "typedef"])
6.31 -
6.32 -lemma (in product_type) conv2: "dest2 (pair x y) = y"
6.33 - by (simp add: pair dest2 type_definition.Abs_inverse [OF "typedef"])
6.34 -
6.35 -lemma (in product_type) induct [induct type]:
6.36 - assumes hyp: "!!x y. P (pair x y)"
6.37 - shows "P p"
6.38 -proof (rule type_definition.Abs_induct [OF "typedef"])
6.39 - fix q show "P (Abs q)"
6.40 - proof (induct q)
6.41 - fix x y have "P (pair x y)" by (rule hyp)
6.42 - also have "pair x y = Abs (x, y)" by (simp only: pair)
6.43 - finally show "P (Abs (x, y))" .
6.44 - qed
6.45 -qed
6.46 +ML {*
6.47 +val [h1, h2] = Goal "PROP Goal (\<And>x. PROP P x) \<Longrightarrow> (PROP P x \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q";
6.48 +by (rtac h2 1);
6.49 +by (rtac (gen_all (h1 RS Drule.rev_triv_goal)) 1);
6.50 +qed "meta_allE";
6.51 +*}
6.52
6.53 -lemma (in product_type) cases [cases type]:
6.54 - "(!!x y. p = pair x y ==> C) ==> C"
6.55 - by (induct p) (auto simp add: "inject")
6.56 -
6.57 -lemma (in product_type) surjective_pairing:
6.58 - "p = pair (dest1 p) (dest2 p)"
6.59 - by (induct p) (simp only: conv1 conv2)
6.60 +lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
6.61 + by simp
6.62
6.63 -lemma (in product_type) split_paired_all:
6.64 - "(!!x. PROP P x) == (!!a b. PROP P (pair a b))"
6.65 -proof
6.66 - fix a b
6.67 - assume "!!x. PROP P x"
6.68 - thus "PROP P (pair a b)" .
6.69 -next
6.70 - fix x
6.71 - assume "!!a b. PROP P (pair a b)"
6.72 - hence "PROP P (pair (dest1 x) (dest2 x))" .
6.73 - thus "PROP P x" by (simp only: surjective_pairing [symmetric])
6.74 -qed
6.75 +lemma rec_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
6.76 + by simp
6.77
6.78 -lemma (in product_type) split_paired_All:
6.79 - "(ALL x. P x) = (ALL a b. P (pair a b))"
6.80 -proof
6.81 - fix a b
6.82 - assume "ALL x. P x"
6.83 - thus "ALL a b. P (pair a b)" by rules
6.84 -next
6.85 - assume P: "ALL a b. P (pair a b)"
6.86 - show "ALL x. P x"
6.87 - proof
6.88 - fix x
6.89 - from P have "P (pair (dest1 x) (dest2 x))" by rules
6.90 - thus "P x" by (simp only: surjective_pairing [symmetric])
6.91 - qed
6.92 -qed
6.93 +lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
6.94 + by simp
6.95
6.96
6.97 subsection {* Concrete record syntax *}
6.98
6.99 nonterminals
6.100 ident field_type field_types field fields update updates
6.101 -
6.102 syntax
6.103 "_constify" :: "id => ident" ("_")
6.104 "_constify" :: "longid => ident" ("_")
6.105 @@ -112,10 +56,27 @@
6.106 "_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
6.107 "_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
6.108
6.109 +(*
6.110
6.111 -subsection {* Package setup *}
6.112 + "_structure" :: "fields => 'a" ("(3{| _ |})")
6.113 + "_structure_scheme" :: "[fields, 'a] => 'a" ("(3{| _,/ (2... =/ _) |})")
6.114 +
6.115 + "_structure_update_name":: idt
6.116 + "_structure_update" :: "['a, updates] \<Rightarrow> 'b" ("_/(3{| _ |})" [900,0] 900)
6.117
6.118 -use "Tools/record_package.ML"
6.119 -setup RecordPackage.setup
6.120 + "_structure_type" :: "field_types => type" ("(3{| _ |})")
6.121 + "_structure_type_scheme" :: "[field_types, type] => type"
6.122 + ("(3{| _,/ (2... ::/ _) |})")
6.123 +syntax (xsymbols)
6.124 +
6.125 + "_structure_scheme" :: "[fields, 'a] => 'a" ("(3{|_,/ (2\<dots> =/ _)|})")
6.126 +
6.127 + "_structure_type_scheme" :: "[field_types, type] => type"
6.128 + ("(3{|_,/ (2\<dots> ::/ _)|})")
6.129 +
6.130 +*)
6.131 +use "Tools/record_package.ML";
6.132 +setup RecordPackage.setup;
6.133
6.134 end
6.135 +
7.1 --- a/src/HOL/Tools/record_package.ML Sat May 01 22:28:51 2004 +0200
7.2 +++ b/src/HOL/Tools/record_package.ML Mon May 03 23:22:17 2004 +0200
7.3 @@ -10,10 +10,15 @@
7.4 sig
7.5 val record_simproc: simproc
7.6 val record_eq_simproc: simproc
7.7 + val record_upd_simproc: simproc
7.8 + val record_split_simproc: (term -> bool) -> simproc
7.9 + val record_ex_sel_eq_simproc: simproc
7.10 val record_split_tac: int -> tactic
7.11 + val record_split_simp_tac: (term -> bool) -> int -> tactic
7.12 val record_split_name: string
7.13 val record_split_wrapper: string * wrapper
7.14 - val print_record_type_abbr: bool ref
7.15 + val print_record_type_abbr: bool ref
7.16 + val print_record_type_as_fields: bool ref
7.17 end;
7.18
7.19 signature RECORD_PACKAGE =
7.20 @@ -21,59 +26,73 @@
7.21 include BASIC_RECORD_PACKAGE
7.22 val quiet_mode: bool ref
7.23 val updateN: string
7.24 - val mk_fieldT: (string * typ) * typ -> typ
7.25 - val dest_fieldT: typ -> (string * typ) * typ
7.26 - val dest_fieldTs: typ -> (string * typ) list
7.27 - val last_fieldT: typ -> (string * typ) option
7.28 - val last_field: Sign.sg -> string -> (string * typ) option
7.29 - val get_parents: Sign.sg -> string -> string list
7.30 - val mk_field: (string * term) * term -> term
7.31 - val mk_fst: term -> term
7.32 - val mk_snd: term -> term
7.33 - val mk_recordT: (string * typ) list * typ -> typ
7.34 - val dest_recordT: typ -> (string * typ) list * typ
7.35 - val mk_record: (string * term) list * term -> term
7.36 - val mk_sel: term -> string -> term
7.37 - val mk_update: term -> string * term -> term
7.38 + val ext_typeN: string
7.39 + val last_extT: typ -> (string * typ list) option
7.40 + val dest_recTs : typ -> (string * typ list) list
7.41 + val get_extension: Sign.sg -> Symtab.key -> (string * typ list) option
7.42 val print_records: theory -> unit
7.43 - val add_record: (string list * bstring) -> string option
7.44 - -> (bstring * string * mixfix) list -> theory -> theory * {simps: thm list, iffs: thm list}
7.45 - val add_record_i: (string list * bstring) -> (typ list * string) option
7.46 - -> (bstring * typ * mixfix) list -> theory -> theory * {simps: thm list, iffs: thm list}
7.47 + val add_record: string list * string -> string option -> (string * string * mixfix) list
7.48 + -> theory -> theory
7.49 + val add_record_i: string list * string -> (typ list * string) option
7.50 + -> (string * typ * mixfix) list -> theory -> theory
7.51 val setup: (theory -> theory) list
7.52 - val record_upd_simproc: simproc
7.53 - val record_split_simproc: (term -> bool) -> simproc
7.54 - val record_ex_sel_eq_simproc: simproc
7.55 - val record_split_simp_tac: (term -> bool) -> int -> tactic
7.56 end;
7.57
7.58 -structure RecordPackage: RECORD_PACKAGE =
7.59 +
7.60 +structure RecordPackage :RECORD_PACKAGE =
7.61 struct
7.62
7.63 -
7.64 -(*** theory context references ***)
7.65 -
7.66 -val product_typeN = "Record.product_type";
7.67 -
7.68 -val product_type_intro = thm "product_type.intro";
7.69 -val product_type_inject = thm "product_type.inject";
7.70 -val product_type_conv1 = thm "product_type.conv1";
7.71 -val product_type_conv2 = thm "product_type.conv2";
7.72 -val product_type_induct = thm "product_type.induct";
7.73 -val product_type_cases = thm "product_type.cases";
7.74 -val product_type_split_paired_all = thm "product_type.split_paired_all";
7.75 -val product_type_split_paired_All = thm "product_type.split_paired_All";
7.76 +val rec_UNIV_I = thm "rec_UNIV_I";
7.77 +val rec_True_simp = thm "rec_True_simp";
7.78 +val Pair_eq = thm "Product_Type.Pair_eq";
7.79 +val atomize_all = thm "HOL.atomize_all";
7.80 +val atomize_imp = thm "HOL.atomize_imp";
7.81 +val triv_goal = thm "triv_goal";
7.82 +val prop_subst = thm "prop_subst";
7.83 +val Pair_sel_convs = [fst_conv,snd_conv];
7.84
7.85
7.86
7.87 +(** name components **)
7.88 +
7.89 +val rN = "r";
7.90 +val moreN = "more";
7.91 +val schemeN = "_scheme";
7.92 +val ext_typeN = "_ext_type";
7.93 +val extN ="_ext";
7.94 +val ext_dest = "_val";
7.95 +val updateN = "_update";
7.96 +val schemeN = "_scheme";
7.97 +val makeN = "make";
7.98 +val fields_selN = "fields";
7.99 +val extendN = "extend";
7.100 +val truncateN = "truncate";
7.101 +
7.102 +(*see typedef_package.ML*)
7.103 +val RepN = "Rep_";
7.104 +val AbsN = "Abs_";
7.105 +
7.106 (*** utilities ***)
7.107
7.108 +
7.109 +fun last [] = error "RecordPackage.last: empty list"
7.110 + | last [x] = x
7.111 + | last (x::xs) = last xs;
7.112 +
7.113 +fun but_last [] = error "RecordPackage.but_last: empty list"
7.114 + | but_last [x] = []
7.115 + | but_last (x::xs) = x::but_last xs;
7.116 +
7.117 +fun remdups [] = []
7.118 + | remdups (x::xs) = x::remdups (filter_out (fn y => y=x) xs);
7.119 +
7.120 +fun is_suffix sfx s = is_some (try (unsuffix sfx) s);
7.121 +
7.122 (* messages *)
7.123
7.124 val quiet_mode = ref false;
7.125 fun message s = if ! quiet_mode then () else writeln s;
7.126
7.127 -
7.128 (* syntax *)
7.129
7.130 fun prune n xs = Library.drop (n, xs);
7.131 @@ -91,332 +110,66 @@
7.132 val (op ===) = Trueprop o HOLogic.mk_eq;
7.133 val (op ==>) = Logic.mk_implies;
7.134
7.135 -
7.136 -(* attributes *)
7.137 -
7.138 -fun case_names_fields x = RuleCases.case_names ["fields"] x;
7.139 -fun induct_type_global name = [case_names_fields, InductAttrib.induct_type_global name];
7.140 -fun cases_type_global name = [case_names_fields, InductAttrib.cases_type_global name];
7.141 -
7.142 -
7.143 -(* tactics *)
7.144 -
7.145 -fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));
7.146 -
7.147 -(* do case analysis / induction on last parameter of ith subgoal (or s) *)
7.148 -
7.149 -fun try_param_tac s rule i st =
7.150 - let
7.151 - val cert = cterm_of (Thm.sign_of_thm st);
7.152 - val g = nth_elem (i - 1, prems_of st);
7.153 - val params = Logic.strip_params g;
7.154 - val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
7.155 - val rule' = Thm.lift_rule (st, i) rule;
7.156 - val (P, ys) = strip_comb (HOLogic.dest_Trueprop
7.157 - (Logic.strip_assums_concl (prop_of rule')));
7.158 - val (x, ca) = (case rev (drop (length params, ys)) of
7.159 - [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
7.160 - (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
7.161 - | [x] => (head_of x, false));
7.162 - val rule'' = cterm_instantiate (map (pairself cert) (case (rev params) of
7.163 - [] => (case assoc (map dest_Free (term_frees (prop_of st)), s) of
7.164 - None => sys_error "try_param_tac: no such variable"
7.165 - | Some T => [(P, if ca then concl else lambda (Free (s, T)) concl),
7.166 - (x, Free (s, T))])
7.167 - | (_, T) :: _ => [(P, list_abs (params, if ca then concl
7.168 - else incr_boundvars 1 (Abs (s, T, concl)))),
7.169 - (x, list_abs (params, Bound 0))])) rule'
7.170 - in compose_tac (false, rule'', nprems_of rule) i st end;
7.171 -
7.172 -
7.173 -
7.174 -(*** code generator data ***)
7.175 -
7.176 -val [prod_code, fst_code, snd_code] =
7.177 - map (Codegen.parse_mixfix (K (Bound 0))) ["(_,/ _)", "fst", "snd"];
7.178 -val prodT_code = Codegen.parse_mixfix (K dummyT) "(_ */ _)";
7.179 -
7.180 -
7.181 -
7.182 -(*** syntax operations ***)
7.183 -
7.184 -(** name components **)
7.185 -
7.186 -val rN = "r";
7.187 -val moreN = "more";
7.188 -val schemeN = "_scheme";
7.189 -val field_typeN = "_field_type";
7.190 -val fieldN = "_field";
7.191 -val fstN = "_val";
7.192 -val sndN = "_more";
7.193 -val updateN = "_update";
7.194 -val makeN = "make";
7.195 -val fieldsN = "fields";
7.196 -val extendN = "extend";
7.197 -val truncateN = "truncate";
7.198 -
7.199 -
7.200 -(*see typedef_package.ML*)
7.201 -val RepN = "Rep_";
7.202 -val AbsN = "Abs_";
7.203 -
7.204 -
7.205 -
7.206 -(** tuple operations **)
7.207 -
7.208 -(* types *)
7.209 -
7.210 -fun mk_fieldT ((c, T), U) = Type (suffix field_typeN c, [T, U]);
7.211 -
7.212 -fun dest_fieldT (typ as Type (c_field_type, [T, U])) =
7.213 - (case try (unsuffix field_typeN) c_field_type of
7.214 - None => raise TYPE ("dest_fieldT", [typ], [])
7.215 - | Some c => ((c, T), U))
7.216 - | dest_fieldT typ = raise TYPE ("dest_fieldT", [typ], []);
7.217 -
7.218 -fun dest_fieldTs T =
7.219 - let val ((c, T), U) = dest_fieldT T
7.220 - in (c, T) :: dest_fieldTs U
7.221 - end handle TYPE _ => [];
7.222 -
7.223 -fun last_fieldT T =
7.224 - let val ((c, T), U) = dest_fieldT T
7.225 - in (case last_fieldT U of
7.226 - None => Some (c,T)
7.227 - | Some l => Some l)
7.228 - end handle TYPE _ => None
7.229 -
7.230 (* morphisms *)
7.231
7.232 -fun mk_Rep U (c, T) =
7.233 - Const (suffix field_typeN (prefix_base RepN c),
7.234 - mk_fieldT ((c, T), U) --> HOLogic.mk_prodT (T, U));
7.235 +fun mk_RepN name = suffix ext_typeN (prefix_base RepN name);
7.236 +fun mk_AbsN name = suffix ext_typeN (prefix_base AbsN name);
7.237
7.238 -fun mk_Abs U (c, T) =
7.239 - Const (suffix field_typeN (prefix_base AbsN c),
7.240 - HOLogic.mk_prodT (T, U) --> mk_fieldT ((c, T), U));
7.241 -
7.242 +fun mk_Rep name repT absT =
7.243 + Const (suffix ext_typeN (prefix_base RepN name),absT --> repT);
7.244
7.245 -(* constructors *)
7.246 +fun mk_Abs name repT absT =
7.247 + Const (mk_AbsN name,repT --> absT);
7.248
7.249 -fun mk_fieldC U (c, T) = (suffix fieldN c, T --> U --> mk_fieldT ((c, T), U));
7.250 +(* constructor *)
7.251
7.252 -fun mk_field ((c, t), u) =
7.253 - let val T = fastype_of t and U = fastype_of u
7.254 - in Const (suffix fieldN c, [T, U] ---> mk_fieldT ((c, T), U)) $ t $ u end;
7.255 +fun mk_extC (name,T) Ts = (suffix extN name, Ts ---> T);
7.256
7.257 +fun mk_ext (name,T) ts =
7.258 + let val Ts = map fastype_of ts
7.259 + in list_comb (Const (mk_extC (name,T) Ts),ts) end;
7.260
7.261 -(* destructors *)
7.262 +(* selector *)
7.263 +
7.264 +fun mk_selC sT (c,T) = (c,sT --> T);
7.265
7.266 -fun mk_fstC U (c, T) = (suffix fstN c, mk_fieldT ((c, T), U) --> T);
7.267 -fun mk_sndC U (c, T) = (suffix sndN c, mk_fieldT ((c, T), U) --> U);
7.268 +fun mk_sel s (c,T) =
7.269 + let val sT = fastype_of s
7.270 + in Const (mk_selC sT (c,T)) $ s end;
7.271
7.272 -fun dest_field fst_or_snd p =
7.273 - let
7.274 - val pT = fastype_of p;
7.275 - val ((c, T), U) = dest_fieldT pT;
7.276 - val (destN, destT) = if fst_or_snd then (fstN, T) else (sndN, U);
7.277 - in Const (suffix destN c, pT --> destT) $ p end;
7.278 +(* updates *)
7.279 +
7.280 +fun mk_updC sT (c,T) = (suffix updateN c, T --> sT --> sT);
7.281
7.282 -val mk_fst = dest_field true;
7.283 -val mk_snd = dest_field false;
7.284 -
7.285 -
7.286 -
7.287 -(** record operations **)
7.288 +fun mk_upd c v s =
7.289 + let val sT = fastype_of s;
7.290 + val vT = fastype_of v;
7.291 + in Const (mk_updC sT (c, vT)) $ v $ s end;
7.292
7.293 (* types *)
7.294
7.295 -val mk_recordT = foldr mk_fieldT;
7.296 -
7.297 -fun dest_recordT T =
7.298 - (case try dest_fieldT T of
7.299 - None => ([], T)
7.300 - | Some (c_T, U) => apfst (cons c_T) (dest_recordT U));
7.301 -
7.302 -fun find_fieldT c rT =
7.303 - (case assoc (fst (dest_recordT rT), c) of
7.304 - None => raise TYPE ("find_field: " ^ c, [rT], [])
7.305 - | Some T => T);
7.306 -
7.307 -
7.308 -(* constructors *)
7.309 -
7.310 -val mk_record = foldr mk_field;
7.311 -
7.312 -
7.313 -(* selectors *)
7.314 -
7.315 -fun mk_selC rT (c, T) = (c, rT --> T);
7.316 -
7.317 -fun mk_sel r c =
7.318 - let val rT = fastype_of r
7.319 - in Const (mk_selC rT (c, find_fieldT c rT)) $ r end;
7.320 -
7.321 -fun mk_named_sels names r = names ~~ map (mk_sel r) names;
7.322 -
7.323 -val mk_moreC = mk_selC;
7.324 -
7.325 -fun mk_more r c =
7.326 - let val rT = fastype_of r
7.327 - in Const (mk_moreC rT (c, snd (dest_recordT rT))) $ r end;
7.328 -
7.329 -
7.330 -(* updates *)
7.331 -
7.332 -fun mk_updateC rT (c, T) = (suffix updateN c, T --> rT --> rT);
7.333 -
7.334 -fun mk_update r (c, x) =
7.335 - let val rT = fastype_of r
7.336 - in Const (mk_updateC rT (c, find_fieldT c rT)) $ x $ r end;
7.337 -
7.338 -val mk_more_updateC = mk_updateC;
7.339 +fun dest_recT (typ as Type (c_ext_type, Ts as (T::_))) =
7.340 + (case try (unsuffix ext_typeN) c_ext_type of
7.341 + None => raise TYPE ("RecordPackage.dest_recT", [typ], [])
7.342 + | Some c => ((c, Ts), last Ts))
7.343 + | dest_recT typ = raise TYPE ("RecordPackage.dest_recT", [typ], []);
7.344
7.345 -fun mk_more_update r (c, x) =
7.346 - let val rT = fastype_of r
7.347 - in Const (mk_more_updateC rT (c, snd (dest_recordT rT))) $ x $ r end;
7.348 -
7.349 -
7.350 -
7.351 -(** concrete syntax for records **)
7.352 -
7.353 -(* parse translations *)
7.354 -
7.355 -fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) =
7.356 - if c = mark then Syntax.const (suffix sfx name) $ arg
7.357 - else raise TERM ("gen_field_tr: " ^ mark, [t])
7.358 - | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]);
7.359 -
7.360 -fun gen_fields_tr sep mark sfx (tm as Const (c, _) $ t $ u) =
7.361 - if c = sep then gen_field_tr mark sfx t :: gen_fields_tr sep mark sfx u
7.362 - else [gen_field_tr mark sfx tm]
7.363 - | gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm];
7.364 -
7.365 -fun gen_record_tr sep mark sfx unit [t] = foldr (op $) (gen_fields_tr sep mark sfx t, unit)
7.366 - | gen_record_tr _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
7.367 -
7.368 -fun gen_record_scheme_tr sep mark sfx [t, more] = foldr (op $) (gen_fields_tr sep mark sfx t, more)
7.369 - | gen_record_scheme_tr _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
7.370 -
7.371 -
7.372 -val record_type_tr = gen_record_tr "_field_types" "_field_type" field_typeN (Syntax.const "unit");
7.373 -val record_type_scheme_tr = gen_record_scheme_tr "_field_types" "_field_type" field_typeN;
7.374 -
7.375 -val record_tr = gen_record_tr "_fields" "_field" fieldN HOLogic.unit;
7.376 -val record_scheme_tr = gen_record_scheme_tr "_fields" "_field" fieldN;
7.377 -
7.378 -fun record_update_tr [t, u] =
7.379 - foldr (op $) (rev (gen_fields_tr "_updates" "_update" updateN u), t)
7.380 - | record_update_tr ts = raise TERM ("record_update_tr", ts);
7.381 -
7.382 -
7.383 -fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts
7.384 - | update_name_tr (Const (x, T) :: ts) = Const (suffix updateN x, T) $$ ts
7.385 - | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
7.386 - (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy")) $$ ts
7.387 - | update_name_tr ts = raise TERM ("update_name_tr", ts);
7.388 -
7.389 +fun is_recT T =
7.390 + (case try dest_recT T of None => false | Some _ => true);
7.391
7.392 -val parse_translation =
7.393 - [("_record_type", record_type_tr),
7.394 - ("_record_type_scheme", record_type_scheme_tr),
7.395 - ("_record", record_tr),
7.396 - ("_record_scheme", record_scheme_tr),
7.397 - ("_record_update", record_update_tr),
7.398 - ("_update_name", update_name_tr)];
7.399 -
7.400 -
7.401 -(* print translations *)
7.402 -
7.403 -
7.404 -val print_record_type_abbr = ref true;
7.405 -
7.406 -fun gen_fields_tr' mark sfx (tm as Const (name_field, _) $ t $ u) =
7.407 - (case try (unsuffix sfx) name_field of
7.408 - Some name =>
7.409 - apfst (cons (Syntax.const mark $ Syntax.free name $ t)) (gen_fields_tr' mark sfx u)
7.410 - | None => ([], tm))
7.411 - | gen_fields_tr' _ _ tm = ([], tm);
7.412 -
7.413 -fun gen_record_tr' sep mark sfx is_unit record record_scheme tm =
7.414 - let
7.415 - val (ts, u) = gen_fields_tr' mark sfx tm;
7.416 - val t' = foldr1 (fn (v, w) => Syntax.const sep $ v $ w) ts;
7.417 - in
7.418 - if is_unit u then Syntax.const record $ t'
7.419 - else Syntax.const record_scheme $ t' $ u
7.420 - end;
7.421 -
7.422 -
7.423 -val record_type_tr' =
7.424 - gen_record_tr' "_field_types" "_field_type" field_typeN
7.425 - (fn Const ("unit", _) => true | _ => false) "_record_type" "_record_type_scheme";
7.426 -
7.427 -
7.428 -(* record_type_abbr_tr' tries to reconstruct the record name type abbreviation from *)
7.429 -(* the (nested) field types. *)
7.430 -fun record_type_abbr_tr' sg abbr alphas zeta lastF rec_schemeT tm =
7.431 - let
7.432 - (* tm is term representation of a (nested) field type. We first reconstruct the *)
7.433 - (* type from tm so that we can continue on the type level rather then the term level.*)
7.434 -
7.435 - fun get_sort xs n = (case assoc (xs,n) of
7.436 - Some s => s
7.437 - | None => Sign.defaultS sg);
7.438 -
7.439 - val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm);
7.440 - val tsig = Sign.tsig_of sg;
7.441 +fun dest_recTs T =
7.442 + let val ((c, Ts), U) = dest_recT T
7.443 + in (c, Ts) :: dest_recTs U
7.444 + end handle TYPE _ => [];
7.445
7.446 - fun mk_type_abbr subst name alphas =
7.447 - let val abbrT = Type (name, map (fn a => TVar ((a,0),logicS)) alphas);
7.448 - in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;
7.449 -
7.450 - fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T))
7.451 -
7.452 - in if !print_record_type_abbr
7.453 - then (case last_fieldT T of
7.454 - Some (name,_)
7.455 - => if name = lastF
7.456 - then
7.457 - let val subst = unify rec_schemeT T
7.458 - in
7.459 - if HOLogic.is_unitT (Envir.norm_type subst (TVar((zeta,0),Sign.defaultS sg)))
7.460 - then mk_type_abbr subst abbr alphas
7.461 - else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta])
7.462 - end handle TUNIFY => record_type_tr' tm
7.463 - else raise Match (* give print translation of specialised record a chance *)
7.464 - | _ => record_type_tr' tm)
7.465 - else record_type_tr' tm
7.466 - end
7.467 +fun last_extT T =
7.468 + let val ((c, Ts), U) = dest_recT T
7.469 + in (case last_extT U of
7.470 + None => Some (c,Ts)
7.471 + | Some l => Some l)
7.472 + end handle TYPE _ => None
7.473
7.474 -
7.475 -fun gen_record_type_abbr_tr' sg abbr alphas zeta lastF rec_schemeT name =
7.476 - let val name_sfx = suffix field_typeN name
7.477 - val tr' = record_type_abbr_tr' sg abbr alphas zeta lastF rec_schemeT
7.478 - in (name_sfx, fn [t,u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
7.479 -
7.480 -val record_tr' =
7.481 - gen_record_tr' "_fields" "_field" fieldN
7.482 - (fn Const ("Unity", _) => true | _ => false) "_record" "_record_scheme";
7.483 -
7.484 -fun record_update_tr' tm =
7.485 - let val (ts, u) = gen_fields_tr' "_update" updateN tm in
7.486 - Syntax.const "_record_update" $ u $
7.487 - foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts)
7.488 - end;
7.489 -
7.490 -fun gen_field_tr' sfx tr' name =
7.491 - let val name_sfx = suffix sfx name
7.492 - in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
7.493 -
7.494 -fun print_translation names =
7.495 - map (gen_field_tr' fieldN record_tr') names @
7.496 - map (gen_field_tr' updateN record_update_tr') names;
7.497 -
7.498 -fun print_translation_field_types names =
7.499 - map (gen_field_tr' field_typeN record_type_tr') names
7.500 -
7.501 -
7.502 +fun rec_id T = foldl (fn (s,(c,T)) => s ^ c) ("",dest_recTs T);
7.503
7.504 (*** extend theory by record definition ***)
7.505
7.506 @@ -428,29 +181,26 @@
7.507 {args: (string * sort) list,
7.508 parent: (typ list * string) option,
7.509 fields: (string * typ) list,
7.510 - field_inducts: thm list,
7.511 - field_cases: thm list,
7.512 - field_splits: thm list,
7.513 - simps: thm list};
7.514 + extension: (string * typ list),
7.515 + induct: thm
7.516 + };
7.517
7.518 -fun make_record_info args parent fields field_inducts field_cases field_splits simps =
7.519 - {args = args, parent = parent, fields = fields, field_inducts = field_inducts,
7.520 - field_cases = field_cases, field_splits = field_splits, simps = simps}: record_info;
7.521 +fun make_record_info args parent fields extension induct =
7.522 + {args = args, parent = parent, fields = fields, extension = extension,
7.523 + induct = induct}: record_info;
7.524 +
7.525
7.526 type parent_info =
7.527 {name: string,
7.528 fields: (string * typ) list,
7.529 - field_inducts: thm list,
7.530 - field_cases: thm list,
7.531 - field_splits: thm list,
7.532 - simps: thm list};
7.533 + extension: (string * typ list),
7.534 + induct: thm
7.535 +};
7.536
7.537 -fun make_parent_info name fields field_inducts field_cases field_splits simps =
7.538 - {name = name, fields = fields, field_inducts = field_inducts,
7.539 - field_cases = field_cases, field_splits = field_splits, simps = simps}: parent_info;
7.540 +fun make_parent_info name fields extension induct =
7.541 + {name = name, fields = fields, extension = extension, induct = induct}: parent_info;
7.542
7.543 -
7.544 -(* data kind 'HOL/records' *)
7.545 +(* data kind 'HOL/record' *)
7.546
7.547 type record_data =
7.548 {records: record_info Symtab.table,
7.549 @@ -458,52 +208,54 @@
7.550 {selectors: unit Symtab.table,
7.551 updates: string Symtab.table,
7.552 simpset: Simplifier.simpset},
7.553 - field_splits:
7.554 - {fields: unit Symtab.table,
7.555 - simpset: Simplifier.simpset},
7.556 equalities: thm Symtab.table,
7.557 - splits: (thm*thm*thm*thm) Symtab.table (* !!,!,EX - split-equalities,induct rule *)
7.558 + splits: (thm*thm*thm*thm) Symtab.table, (* !!,!,EX - split-equalities,induct rule *)
7.559 + extfields: (string*typ) list Symtab.table, (* maps extension to its fields *)
7.560 + fieldext: (string*typ list) Symtab.table (* maps field to its extension *)
7.561 };
7.562
7.563 -fun make_record_data records sel_upd field_splits equalities splits =
7.564 - {records = records, sel_upd = sel_upd, field_splits = field_splits,
7.565 - equalities = equalities, splits = splits}: record_data;
7.566 +fun make_record_data records sel_upd equalities splits extfields fieldext =
7.567 + {records = records, sel_upd = sel_upd,
7.568 + equalities = equalities, splits = splits,
7.569 + extfields = extfields, fieldext = fieldext }: record_data;
7.570
7.571 structure RecordsArgs =
7.572 struct
7.573 - val name = "HOL/records";
7.574 + val name = "HOL/records";
7.575 type T = record_data;
7.576
7.577 val empty =
7.578 make_record_data Symtab.empty
7.579 {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss}
7.580 - {fields = Symtab.empty, simpset = HOL_basic_ss} Symtab.empty Symtab.empty;
7.581 + Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
7.582
7.583 val copy = I;
7.584 val prep_ext = I;
7.585 fun merge
7.586 ({records = recs1,
7.587 sel_upd = {selectors = sels1, updates = upds1, simpset = ss1},
7.588 - field_splits = {fields = flds1, simpset = fld_ss1},
7.589 equalities = equalities1,
7.590 - splits = splits1},
7.591 + splits = splits1,
7.592 + extfields = extfields1,
7.593 + fieldext = fieldext1},
7.594 {records = recs2,
7.595 sel_upd = {selectors = sels2, updates = upds2, simpset = ss2},
7.596 - field_splits = {fields = flds2, simpset = fld_ss2},
7.597 equalities = equalities2,
7.598 - splits = splits2}) =
7.599 + splits = splits2,
7.600 + extfields = extfields2,
7.601 + fieldext = fieldext2}) =
7.602 make_record_data
7.603 (Symtab.merge (K true) (recs1, recs2))
7.604 {selectors = Symtab.merge (K true) (sels1, sels2),
7.605 updates = Symtab.merge (K true) (upds1, upds2),
7.606 simpset = Simplifier.merge_ss (ss1, ss2)}
7.607 - {fields = Symtab.merge (K true) (flds1, flds2),
7.608 - simpset = Simplifier.merge_ss (fld_ss1, fld_ss2)}
7.609 (Symtab.merge Thm.eq_thm (equalities1, equalities2))
7.610 (Symtab.merge (fn ((a,b,c,d),(w,x,y,z))
7.611 => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso
7.612 Thm.eq_thm (c,y) andalso Thm.eq_thm (d,z))
7.613 - (splits1, splits2));
7.614 + (splits1, splits2))
7.615 + (Symtab.merge (K true) (extfields1,extfields2))
7.616 + (Symtab.merge (K true) (fieldext1,fieldext2));
7.617
7.618 fun print sg ({records = recs, ...}: record_data) =
7.619 let
7.620 @@ -527,24 +279,28 @@
7.621 structure RecordsData = TheoryDataFun(RecordsArgs);
7.622 val print_records = RecordsData.print;
7.623
7.624 -
7.625 (* access 'records' *)
7.626
7.627 fun get_record thy name = Symtab.lookup (#records (RecordsData.get thy), name);
7.628
7.629 fun put_record name info thy =
7.630 let
7.631 - val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy;
7.632 + val {records, sel_upd, equalities, splits,extfields,fieldext} = RecordsData.get thy;
7.633 val data = make_record_data (Symtab.update ((name, info), records))
7.634 - sel_upd field_splits equalities splits;
7.635 + sel_upd equalities splits extfields fieldext;
7.636 in RecordsData.put data thy end;
7.637
7.638 -
7.639 (* access 'sel_upd' *)
7.640
7.641 fun get_sel_upd sg = #sel_upd (RecordsData.get_sg sg);
7.642
7.643 fun get_selectors sg name = Symtab.lookup (#selectors (get_sel_upd sg), name);
7.644 +fun is_selector sg name =
7.645 + case get_selectors sg (Sign.intern_const sg name) of
7.646 + None => false
7.647 + | Some _ => true
7.648 +
7.649 +
7.650 fun get_updates sg name = Symtab.lookup (#updates (get_sel_upd sg), name);
7.651 fun get_simpset sg = #simpset (get_sel_upd sg);
7.652
7.653 @@ -553,36 +309,22 @@
7.654 val sels = map (rpair ()) names;
7.655 val upds = map (suffix updateN) names ~~ names;
7.656
7.657 - val {records, sel_upd = {selectors, updates, simpset}, field_splits,
7.658 - equalities, splits} = RecordsData.get thy;
7.659 + val {records, sel_upd = {selectors, updates, simpset},
7.660 + equalities, splits, extfields,fieldext} = RecordsData.get thy;
7.661 val data = make_record_data records
7.662 {selectors = Symtab.extend (selectors, sels),
7.663 updates = Symtab.extend (updates, upds),
7.664 simpset = Simplifier.addsimps (simpset, simps)}
7.665 - field_splits equalities splits;
7.666 + equalities splits extfields fieldext;
7.667 in RecordsData.put data thy end;
7.668
7.669 -
7.670 -(* access 'field_splits' *)
7.671 -
7.672 -fun add_field_splits names simps thy =
7.673 - let
7.674 - val {records, sel_upd, field_splits = {fields, simpset},
7.675 - equalities, splits} = RecordsData.get thy;
7.676 - val flds = map (rpair ()) names;
7.677 - val data = make_record_data records sel_upd
7.678 - {fields = Symtab.extend (fields, flds),
7.679 - simpset = Simplifier.addsimps (simpset, simps)} equalities splits;
7.680 - in RecordsData.put data thy end;
7.681 -
7.682 -
7.683 (* access 'equalities' *)
7.684
7.685 fun add_record_equalities name thm thy =
7.686 let
7.687 - val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy;
7.688 - val data = make_record_data records sel_upd field_splits
7.689 - (Symtab.update_new ((name, thm), equalities)) splits;
7.690 + val {records, sel_upd, equalities, splits, extfields,fieldext} = RecordsData.get thy;
7.691 + val data = make_record_data records sel_upd
7.692 + (Symtab.update_new ((name, thm), equalities)) splits extfields fieldext;
7.693 in RecordsData.put data thy end;
7.694
7.695 fun get_equalities sg name =
7.696 @@ -592,28 +334,46 @@
7.697
7.698 fun add_record_splits name thmP thy =
7.699 let
7.700 - val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy;
7.701 - val data = make_record_data records sel_upd field_splits
7.702 - equalities (Symtab.update_new ((name, thmP), splits));
7.703 + val {records, sel_upd, equalities, splits, extfields,fieldext} = RecordsData.get thy;
7.704 + val data = make_record_data records sel_upd
7.705 + equalities (Symtab.update_new ((name, thmP), splits)) extfields fieldext;
7.706 in RecordsData.put data thy end;
7.707
7.708 fun get_splits sg name =
7.709 Symtab.lookup (#splits (RecordsData.get_sg sg), name);
7.710
7.711 -(* last field of a record *)
7.712 -fun last_field sg name =
7.713 - case Symtab.lookup (#records (RecordsData.get_sg sg),name) of
7.714 - Some r => Some (hd (rev (#fields r)))
7.715 +(* extension of a record name *)
7.716 +fun get_extension sg name =
7.717 + case Symtab.lookup (#records (RecordsData.get_sg sg),name) of
7.718 + Some s => Some (#extension s)
7.719 | None => None;
7.720
7.721 -(* get parent names *)
7.722 -fun get_parents sg name =
7.723 - (case Symtab.lookup (#records (RecordsData.get_sg sg),name) of
7.724 - Some r => (case #parent r of
7.725 - Some (_,p) => p::get_parents sg p
7.726 - | None => [])
7.727 - | None => [])
7.728 -
7.729 +(* access 'extfields' *)
7.730 +
7.731 +fun add_extfields name fields thy =
7.732 + let
7.733 + val {records, sel_upd, equalities, splits, extfields, fieldext} = RecordsData.get thy;
7.734 + val data = make_record_data records sel_upd
7.735 + equalities splits (Symtab.update_new ((name, fields), extfields)) fieldext;
7.736 + in RecordsData.put data thy end;
7.737 +
7.738 +fun get_extfields sg name =
7.739 + Symtab.lookup (#extfields (RecordsData.get_sg sg), name);
7.740 +
7.741 +(* access 'fieldext' *)
7.742 +
7.743 +fun add_fieldext extname_types fields thy =
7.744 + let
7.745 + val {records, sel_upd, equalities, splits, extfields, fieldext} = RecordsData.get thy;
7.746 + val fieldext' = foldl (fn (table,field) => Symtab.update_new ((field,extname_types),table))
7.747 + (fieldext,fields);
7.748 + val data = make_record_data records sel_upd equalities splits extfields fieldext';
7.749 + in RecordsData.put data thy end;
7.750 +
7.751 +
7.752 +fun get_fieldext sg name =
7.753 + Symtab.lookup (#fieldext (RecordsData.get_sg sg), name);
7.754 +
7.755 (* parent records *)
7.756
7.757 fun add_parents thy None parents = parents
7.758 @@ -622,7 +382,7 @@
7.759 val sign = Theory.sign_of thy;
7.760 fun err msg = error (msg ^ " parent record " ^ quote name);
7.761
7.762 - val {args, parent, fields, field_inducts, field_cases, field_splits, simps} =
7.763 + val {args, parent, fields, extension, induct} =
7.764 (case get_record thy name of Some info => info | None => err "Unknown");
7.765 val _ = if length types <> length args then err "Bad number of arguments for" else ();
7.766
7.767 @@ -634,33 +394,342 @@
7.768 val subst = Term.map_type_tfree (fn (x, _) => the (assoc (inst, x)));
7.769 val parent' = apsome (apfst (map subst)) parent;
7.770 val fields' = map (apsnd subst) fields;
7.771 + val extension' = apsnd (map subst) extension;
7.772 in
7.773 conditional (not (null bads)) (fn () =>
7.774 err ("Ill-sorted instantiation of " ^ commas bads ^ " in"));
7.775 add_parents thy parent'
7.776 - (make_parent_info name fields' field_inducts field_cases field_splits simps::parents)
7.777 + (make_parent_info name fields' extension' induct::parents)
7.778 end;
7.779
7.780
7.781 +(** concrete syntax for records **)
7.782 +
7.783 +(* parse translations *)
7.784 +
7.785 +fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) =
7.786 + if c = mark then Syntax.const (suffix sfx name) $ arg
7.787 + else raise TERM ("gen_field_tr: " ^ mark, [t])
7.788 + | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]);
7.789 +
7.790 +fun gen_fields_tr sep mark sfx (tm as Const (c, _) $ t $ u) =
7.791 + if c = sep then gen_field_tr mark sfx t :: gen_fields_tr sep mark sfx u
7.792 + else [gen_field_tr mark sfx tm]
7.793 + | gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm];
7.794 +
7.795 +
7.796 +fun record_update_tr [t, u] =
7.797 + foldr (op $) (rev (gen_fields_tr "_updates" "_update" updateN u), t)
7.798 + | record_update_tr ts = raise TERM ("record_update_tr", ts);
7.799 +
7.800 +fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts
7.801 + | update_name_tr (Const (x, T) :: ts) = Const (suffix updateN x, T) $$ ts
7.802 + | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
7.803 + (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy")) $$ ts
7.804 + | update_name_tr ts = raise TERM ("update_name_tr", ts);
7.805 +
7.806 +fun dest_ext_field mark (t as (Const (c,_) $ Const (name,_) $ arg)) =
7.807 + if c = mark then (name,arg) else raise TERM ("dest_ext_field: " ^ mark, [t])
7.808 + | dest_ext_field _ t = raise TERM ("dest_ext_field", [t])
7.809 +
7.810 +fun dest_ext_fields sep mark (trm as (Const (c,_) $ t $ u)) =
7.811 + if c = sep then dest_ext_field mark t::dest_ext_fields sep mark u
7.812 + else [dest_ext_field mark trm]
7.813 + | dest_ext_fields _ mark t = [dest_ext_field mark t]
7.814 +
7.815 +fun gen_ext_fields_tr sep mark sfx more sg t =
7.816 + let
7.817 + val fieldargs = dest_ext_fields sep mark t;
7.818 + fun splitargs (field::fields) ((name,arg)::fargs) =
7.819 + if is_suffix name field
7.820 + then let val (args,rest) = splitargs fields fargs
7.821 + in (arg::args,rest) end
7.822 + else raise TERM ("gen_ext_fields_tr: expecting field " ^ field ^
7.823 + " but got " ^ name, [t])
7.824 + | splitargs [] (fargs as (_::_)) = ([],fargs)
7.825 + | splitargs (_::_) [] = raise TERM ("gen_ext_fields_tr: expecting more fields", [t])
7.826 + | splitargs _ _ = ([],[]);
7.827 +
7.828 + fun mk_ext (fargs as (name,arg)::_) =
7.829 + (case get_fieldext sg (Sign.intern_const sg name) of
7.830 + Some (ext,_) => (case get_extfields sg ext of
7.831 + Some flds
7.832 + => let val (args,rest) =
7.833 + splitargs (map fst (but_last flds)) fargs;
7.834 + val more' = mk_ext rest;
7.835 + in list_comb (Syntax.const (suffix sfx ext),args@[more'])
7.836 + end
7.837 + | None => raise TERM("gen_ext_fields_tr: no fields defined for "
7.838 + ^ ext,[t]))
7.839 + | None => raise TERM ("gen_ext_fields_tr: "^ name ^" is no proper field",[t]))
7.840 + | mk_ext [] = more
7.841 +
7.842 + in mk_ext fieldargs end;
7.843 +
7.844 +fun gen_ext_type_tr sep mark sfx more sg t =
7.845 + let
7.846 + val fieldargs = dest_ext_fields sep mark t;
7.847 + fun splitargs (field::fields) ((name,arg)::fargs) =
7.848 + if is_suffix name field
7.849 + then let val (args,rest) = splitargs fields fargs
7.850 + in (arg::args,rest) end
7.851 + else raise TERM ("gen_ext_type_tr: expecting field " ^ field ^
7.852 + " but got " ^ name, [t])
7.853 + | splitargs [] (fargs as (_::_)) = ([],fargs)
7.854 + | splitargs (_::_) [] = raise TERM ("gen_ext_type_tr: expecting more fields", [t])
7.855 + | splitargs _ _ = ([],[]);
7.856 +
7.857 + fun get_sort xs n = (case assoc (xs,n) of
7.858 + Some s => s
7.859 + | None => Sign.defaultS sg);
7.860 + fun to_type t = Sign.intern_typ sg
7.861 + (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t);
7.862 +
7.863 + val tsig = Sign.tsig_of sg;
7.864 + fun unify (t,env) = Type.unify tsig env t;
7.865 +
7.866 + fun mk_ext (fargs as (name,arg)::_) =
7.867 + (case get_fieldext sg (Sign.intern_const sg name) of
7.868 + Some (ext,alphas) =>
7.869 + (case get_extfields sg ext of
7.870 + Some flds
7.871 + => (let
7.872 + val flds' = but_last flds;
7.873 + val types = map snd flds';
7.874 + val (args,rest) = splitargs (map fst flds') fargs;
7.875 + val vartypes = map Type.varifyT types;
7.876 + val argtypes = map to_type args;
7.877 + val (subst,_) = foldr unify (vartypes ~~ argtypes,(Vartab.empty,0));
7.878 + val alphas' = map ((Syntax.term_of_typ (! Syntax.show_sorts)) o
7.879 + (Envir.norm_type subst) o Type.varifyT)
7.880 + (but_last alphas);
7.881 +
7.882 + val more' = mk_ext rest;
7.883 + in list_comb (Syntax.const (suffix sfx ext),alphas'@[more'])
7.884 + end handle TUNIFY => raise
7.885 + TERM ("gen_ext_type_tr: type is no proper record (extension)", [t]))
7.886 + | None => raise TERM ("gen_ext_fields_tr: no fields defined for " ^ ext,[t]))
7.887 + | None => raise TERM ("gen_ext_fields_tr: "^ name ^" is no proper field",[t]))
7.888 + | mk_ext [] = more
7.889 +
7.890 + in mk_ext fieldargs end;
7.891 +
7.892 +fun gen_adv_record_tr sep mark sfx unit sg [t] =
7.893 + gen_ext_fields_tr sep mark sfx unit sg t
7.894 + | gen_adv_record_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
7.895 +
7.896 +fun gen_adv_record_scheme_tr sep mark sfx sg [t, more] =
7.897 + gen_ext_fields_tr sep mark sfx more sg t
7.898 + | gen_adv_record_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
7.899 +
7.900 +fun gen_adv_record_type_tr sep mark sfx unit sg [t] =
7.901 + gen_ext_type_tr sep mark sfx unit sg t
7.902 + | gen_adv_record_type_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
7.903 +
7.904 +fun gen_adv_record_type_scheme_tr sep mark sfx sg [t, more] =
7.905 + gen_ext_type_tr sep mark sfx more sg t
7.906 + | gen_adv_record_type_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
7.907 +
7.908 +val adv_record_tr = gen_adv_record_tr "_fields" "_field" extN HOLogic.unit;
7.909 +val adv_record_scheme_tr = gen_adv_record_scheme_tr "_fields" "_field" extN;
7.910 +
7.911 +val adv_record_type_tr =
7.912 + gen_adv_record_type_tr "_field_types" "_field_type" ext_typeN
7.913 + (Syntax.term_of_typ false (HOLogic.unitT));
7.914 +val adv_record_type_scheme_tr =
7.915 + gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN;
7.916 +
7.917 +val parse_translation =
7.918 + [("_record_update", record_update_tr),
7.919 + ("_update_name", update_name_tr)];
7.920 +
7.921 +val adv_parse_translation =
7.922 + [("_record",adv_record_tr),
7.923 + ("_record_scheme",adv_record_scheme_tr),
7.924 + ("_record_type",adv_record_type_tr),
7.925 + ("_record_type_scheme",adv_record_type_scheme_tr)];
7.926 +
7.927 +
7.928 +(* print translations *)
7.929 +
7.930 +val print_record_type_abbr = ref true;
7.931 +val print_record_type_as_fields = ref true;
7.932 +
7.933 +fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ t $ u) =
7.934 + (case try (unsuffix sfx) name_field of
7.935 + Some name =>
7.936 + apfst (cons (Syntax.const mark $ Syntax.free name $ t)) (gen_field_upds_tr' mark sfx u)
7.937 + | None => ([], tm))
7.938 + | gen_field_upds_tr' _ _ tm = ([], tm);
7.939 +
7.940 +fun record_update_tr' tm =
7.941 + let val (ts, u) = gen_field_upds_tr' "_update" updateN tm in
7.942 + Syntax.const "_record_update" $ u $
7.943 + foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts)
7.944 + end;
7.945 +
7.946 +fun gen_field_tr' sfx tr' name =
7.947 + let val name_sfx = suffix sfx name
7.948 + in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
7.949 +
7.950 +fun record_tr' sep mark record record_scheme unit sg t =
7.951 + let
7.952 + fun field_lst t =
7.953 + (case strip_comb t of
7.954 + (Const (ext,_),args)
7.955 + => (case try (unsuffix extN) (Sign.intern_const sg ext) of
7.956 + Some ext'
7.957 + => (case get_extfields sg ext' of
7.958 + Some flds
7.959 + => (let
7.960 + val (f::fs) = but_last (map fst flds);
7.961 + val flds' = Sign.extern sg Sign.constK f::map NameSpace.base fs;
7.962 + val (args',more) = split_last args;
7.963 + in (flds'~~args')@field_lst more end
7.964 + handle LIST _ => [("",t)])
7.965 + | None => [("",t)])
7.966 + | None => [("",t)])
7.967 + | _ => [("",t)])
7.968 +
7.969 + val (flds,(_,more)) = split_last (field_lst t);
7.970 + val flds' = map (fn (n,t)=>Syntax.const mark$Syntax.const n$t) flds;
7.971 + val flds'' = foldr1 (fn (x,y) => Syntax.const sep$x$y) flds';
7.972 +
7.973 + in if null flds then raise Match
7.974 + else if unit more
7.975 + then Syntax.const record$flds''
7.976 + else Syntax.const record_scheme$flds''$more
7.977 + end
7.978 +
7.979 +fun gen_record_tr' name =
7.980 + let val name_sfx = suffix extN name;
7.981 + val unit = (fn Const ("Unity",_) => true | _ => false);
7.982 + fun tr' sg ts = record_tr' "_fields" "_field" "_record" "_record_scheme" unit sg
7.983 + (list_comb (Syntax.const name_sfx,ts))
7.984 + in (name_sfx,tr')
7.985 + end
7.986 +
7.987 +fun print_translation names =
7.988 + map (gen_field_tr' updateN record_update_tr') names;
7.989 +
7.990 +(* record_type_abbr_tr' tries to reconstruct the record name type abbreviation from *)
7.991 +(* the (nested) extension types. *)
7.992 +fun record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT sg tm =
7.993 + let
7.994 + (* tm is term representation of a (nested) field type. We first reconstruct the *)
7.995 + (* type from tm so that we can continue on the type level rather then the term level.*)
7.996 +
7.997 + fun get_sort xs n = (case assoc (xs,n) of
7.998 + Some s => s
7.999 + | None => Sign.defaultS sg);
7.1000 +
7.1001 + val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm)
7.1002 + val tsig = Sign.tsig_of sg
7.1003 +
7.1004 + fun mk_type_abbr subst name alphas =
7.1005 + let val abbrT = Type (name, map (fn a => TVar ((a,0),logicS)) alphas);
7.1006 + in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;
7.1007 +
7.1008 + fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T))
7.1009 +
7.1010 + in if !print_record_type_abbr
7.1011 + then (case last_extT T of
7.1012 + Some (name,_)
7.1013 + => if name = lastExt
7.1014 + then
7.1015 + (let val subst = unify schemeT T
7.1016 + in
7.1017 + if HOLogic.is_unitT (Envir.norm_type subst (TVar((zeta,0),Sign.defaultS sg)))
7.1018 + then mk_type_abbr subst abbr alphas
7.1019 + else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta])
7.1020 + end handle TUNIFY => default_tr' sg tm)
7.1021 + else raise Match (* give print translation of specialised record a chance *)
7.1022 + | _ => raise Match)
7.1023 + else default_tr' sg tm
7.1024 + end
7.1025 +
7.1026 +fun record_type_tr' sep mark record record_scheme sg t =
7.1027 + let
7.1028 + fun get_sort xs n = (case assoc (xs,n) of
7.1029 + Some s => s
7.1030 + | None => Sign.defaultS sg);
7.1031 +
7.1032 + val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t)
7.1033 +
7.1034 + val tsig = Sign.tsig_of sg
7.1035 + fun unify (t,v) = Type.unify tsig v t;
7.1036 +
7.1037 + fun term_of_type T = Syntax.term_of_typ (!Syntax.show_sorts) (Sign.extern_typ sg T);
7.1038 +
7.1039 + fun field_lst T =
7.1040 + (case T of
7.1041 + Type (ext,args)
7.1042 + => (case try (unsuffix ext_typeN) ext of
7.1043 + Some ext'
7.1044 + => (case get_extfields sg ext' of
7.1045 + Some flds
7.1046 + => (case get_fieldext sg (fst (hd flds)) of
7.1047 + Some (_,alphas)
7.1048 + => (let
7.1049 + val (f::fs) = but_last flds;
7.1050 + val flds' = apfst (Sign.extern sg Sign.constK) f
7.1051 + ::map (apfst NameSpace.base) fs;
7.1052 + val (args',more) = split_last args;
7.1053 + val alphavars = map Type.varifyT (but_last alphas);
7.1054 + val (subst,_)= foldr unify (alphavars~~args',(Vartab.empty,0));
7.1055 + val flds'' =map (apsnd ((Envir.norm_type subst)o(Type.varifyT)))
7.1056 + flds';
7.1057 + in flds''@field_lst more end
7.1058 + handle TUNIFY => [("",T)]
7.1059 + | LIST _=> [("",T)])
7.1060 + | None => [("",T)])
7.1061 + | None => [("",T)])
7.1062 + | None => [("",T)])
7.1063 + | _ => [("",T)])
7.1064 +
7.1065 + val (flds,(_,moreT)) = split_last (field_lst T);
7.1066 + val flds' = map (fn (n,T)=>Syntax.const mark$Syntax.const n$term_of_type T) flds;
7.1067 + val flds'' = foldr1 (fn (x,y) => Syntax.const sep$x$y) flds';
7.1068 +
7.1069 + in if not (!print_record_type_as_fields) orelse null flds then raise Match
7.1070 + else if moreT = HOLogic.unitT
7.1071 + then Syntax.const record$flds''
7.1072 + else Syntax.const record_scheme$flds''$term_of_type moreT
7.1073 + end
7.1074 +
7.1075 +
7.1076 +fun gen_record_type_tr' name =
7.1077 + let val name_sfx = suffix ext_typeN name;
7.1078 + fun tr' sg ts = record_type_tr' "_field_types" "_field_type"
7.1079 + "_record_type" "_record_type_scheme" sg
7.1080 + (list_comb (Syntax.const name_sfx,ts))
7.1081 + in (name_sfx,tr')
7.1082 + end
7.1083 +
7.1084 +
7.1085 +fun gen_record_type_abbr_tr' abbr alphas zeta lastExt schemeT name =
7.1086 + let val name_sfx = suffix ext_typeN name;
7.1087 + val default_tr' = record_type_tr' "_field_types" "_field_type"
7.1088 + "_record_type" "_record_type_scheme"
7.1089 + fun tr' sg ts = record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT sg
7.1090 + (list_comb (Syntax.const name_sfx,ts))
7.1091 + in (name_sfx, tr') end;
7.1092 +
7.1093
7.1094 (** record simprocs **)
7.1095 -
7.1096 fun quick_and_dirty_prove sg xs asms prop tac =
7.1097 Tactic.prove sg xs asms prop
7.1098 - (if ! quick_and_dirty then (K (SkipProof.cheat_tac HOL.thy)) else tac);
7.1099 + (if !quick_and_dirty then (K (SkipProof.cheat_tac HOL.thy)) else tac);
7.1100
7.1101
7.1102 fun prove_split_simp sg T prop =
7.1103 - (case last_fieldT T of
7.1104 - Some (name,_) => (case get_splits sg name of
7.1105 - Some (all_thm,_,_,_)
7.1106 - => let val {sel_upd={simpset,...},...} = RecordsData.get_sg sg;
7.1107 - in (quick_and_dirty_prove sg [] [] prop
7.1108 - (K (simp_tac (simpset addsimps [all_thm]) 1)))
7.1109 - end
7.1110 - | _ => error "RecordPackage.prove_split_simp: code should never been reached")
7.1111 - | _ => error "RecordPackage.prove_split_simp: code should never been reached")
7.1112 -
7.1113 + (case get_splits sg (rec_id T) of
7.1114 + Some (all_thm,_,_,_)
7.1115 + => let val {sel_upd={simpset,...},...} = RecordsData.get_sg sg;
7.1116 + in (quick_and_dirty_prove sg [] [] prop
7.1117 + (K (simp_tac (simpset addsimps [all_thm]) 1)))
7.1118 + end
7.1119 + | _ => error "RecordPackage.prove_split_simp:code should never been reached")
7.1120
7.1121 (* record_simproc *)
7.1122 (* Simplifies selections of an record update:
7.1123 @@ -682,8 +751,10 @@
7.1124 (case get_updates sg u of Some u_name =>
7.1125 let
7.1126 fun mk_abs_var x t = (x, fastype_of t);
7.1127 - val {sel_upd={updates,...},...} = RecordsData.get_sg sg;
7.1128 -
7.1129 + val {sel_upd={updates,...},extfields,...} = RecordsData.get_sg sg;
7.1130 + fun flds T =
7.1131 + foldl (fn (xs,(eN,_))=>xs@(map fst (Symtab.lookup_multi (extfields,eN))))
7.1132 + ([],(dest_recTs T));
7.1133 fun mk_eq_terms ((upd as Const (u,Type(_,[updT,_]))) $ k $ r) =
7.1134 (case (Symtab.lookup (updates,u)) of
7.1135 None => None
7.1136 @@ -695,8 +766,8 @@
7.1137 val kv = mk_abs_var "k" k
7.1138 val kb = Bound 1
7.1139 in Some (upd$kb$rb,kb,[kv,rv],true) end
7.1140 - else if u_name mem (map fst (dest_fieldTs rangeS))
7.1141 - orelse s mem (map fst (dest_fieldTs updT))
7.1142 + else if u_name mem (flds rangeS)
7.1143 + orelse s mem (flds updT)
7.1144 then None
7.1145 else (case mk_eq_terms r of
7.1146 Some (trm,trm',vars,update_s)
7.1147 @@ -735,7 +806,7 @@
7.1148 * the record first and do simplification on that (record_split_simp_tac).
7.1149 * e.g. r(|lots of updates|) = x
7.1150 *
7.1151 - * record_eq_simproc record_split_simp_tac
7.1152 + * record_eq_simproc record_split_simp_tac
7.1153 * Complexity: #components * #updates #updates
7.1154 *
7.1155 *)
7.1156 @@ -743,9 +814,9 @@
7.1157 Simplifier.simproc (Theory.sign_of HOL.thy) "record_eq_simp" ["r = s"]
7.1158 (fn sg => fn _ => fn t =>
7.1159 (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ =>
7.1160 - (case last_fieldT T of
7.1161 - None => None
7.1162 - | Some (name, _) => (case get_equalities sg name of
7.1163 + (case rec_id T of
7.1164 + "" => None
7.1165 + | name => (case get_equalities sg name of
7.1166 None => None
7.1167 | Some thm => Some (thm RS Eq_TrueI)))
7.1168 | _ => None));
7.1169 @@ -790,7 +861,8 @@
7.1170
7.1171 in (case mk_updterm updates Symtab.empty t of
7.1172 Some (trm,trm',vars)
7.1173 - => Some (prove_split_simp sg T (list_all(vars,(Logic.mk_equals (trm,trm')))))
7.1174 + => Some (prove_split_simp sg T
7.1175 + (list_all(vars,(Logic.mk_equals (trm,trm')))))
7.1176 | None => None)
7.1177 end
7.1178 | _ => None));
7.1179 @@ -804,9 +876,9 @@
7.1180 (fn sg => fn _ => fn t =>
7.1181 (case t of (Const (quantifier, Type (_, [Type (_, [T, _]), _])))$trm =>
7.1182 if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex"
7.1183 - then (case last_fieldT T of
7.1184 - None => None
7.1185 - | Some (name, _)
7.1186 + then (case rec_id T of
7.1187 + "" => None
7.1188 + | name
7.1189 => if P t
7.1190 then (case get_splits sg name of
7.1191 None => None
7.1192 @@ -821,7 +893,7 @@
7.1193 | _ => None))
7.1194
7.1195 (* record_ex_sel_eq_simproc *)
7.1196 -(* record: (EX r. x = sel r) resp. (EX r. sel r = x) to True *)
7.1197 +(* simplifies: (EX s. x = sel s) resp. (EX s. sel s = x) to True *)
7.1198 val record_ex_sel_eq_simproc =
7.1199 Simplifier.simproc (Theory.sign_of HOL.thy) "record_ex_sel_eq_simproc" ["Ex t"]
7.1200 (fn sg => fn _ => fn t =>
7.1201 @@ -830,24 +902,24 @@
7.1202 addsimprocs [record_split_simproc (K true)]) 1)));
7.1203 in
7.1204 (case t of
7.1205 - (Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$(Const (sel,Tsel)$Bound 0)$X)) =>
7.1206 + (Const ("Ex",Tex)$Abs(s,T,Const ("op =",Teq)$(Const (sel,Tsel)$Bound 0)$X)) =>
7.1207 (case get_selectors sg sel of Some () =>
7.1208 let
7.1209 val X' = ("x",range_type Tsel);
7.1210 val prop = list_all ([X'],
7.1211 Logic.mk_equals
7.1212 - (Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$
7.1213 + (Const ("Ex",Tex)$Abs(s,T,Const ("op =",Teq)$
7.1214 (Const (sel,Tsel)$Bound 0)$Bound 1),
7.1215 Const ("True",HOLogic.boolT)));
7.1216 in Some (prove prop) end
7.1217 | None => None)
7.1218 - |(Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$X$(Const (sel,Tsel)$Bound 0))) =>
7.1219 + |(Const ("Ex",Tex)$Abs(s,T,Const ("op =",Teq)$X$(Const (sel,Tsel)$Bound 0))) =>
7.1220 (case get_selectors sg sel of Some () =>
7.1221 let
7.1222 val X' = ("x",range_type Tsel);
7.1223 val prop = list_all ([X'],
7.1224 Logic.mk_equals
7.1225 - (Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$
7.1226 + (Const ("Ex",Tex)$Abs(s,T,Const ("op =",Teq)$
7.1227 Bound 1$(Const (sel,Tsel)$Bound 0)),
7.1228 Const ("True",HOLogic.boolT)));
7.1229 in Some (prove prop) end
7.1230 @@ -855,28 +927,8 @@
7.1231 | _ => None)
7.1232 end)
7.1233
7.1234 -(** record field splitting **)
7.1235
7.1236 -(* tactic *)
7.1237 -
7.1238 -fun is_fieldT fields (Type (a, [_, _])) = is_some (Symtab.lookup (fields, a))
7.1239 - | is_fieldT _ _ = false;
7.1240 -
7.1241 -fun record_split_tac i st =
7.1242 - let
7.1243 - val {field_splits = {fields, simpset}, ...} = RecordsData.get_sg (Thm.sign_of_thm st);
7.1244 -
7.1245 - val has_field = exists_Const
7.1246 - (fn (s, Type (_, [Type (_, [T, _]), _])) =>
7.1247 - (s = "all" orelse s = "All") andalso is_fieldT fields T
7.1248 - | _ => false);
7.1249 -
7.1250 - val goal = Library.nth_elem (i - 1, Thm.prems_of st);
7.1251 - in
7.1252 - if has_field goal then Simplifier.full_simp_tac simpset i st
7.1253 - else Seq.empty
7.1254 - end handle Library.LIST _ => Seq.empty;
7.1255 -
7.1256 +
7.1257
7.1258 local
7.1259 val inductive_atomize = thms "induct_atomize";
7.1260 @@ -891,16 +943,16 @@
7.1261 fun record_split_simp_tac P i st =
7.1262 let
7.1263 val sg = Thm.sign_of_thm st;
7.1264 - val {sel_upd={simpset,...},field_splits={fields,...},...}
7.1265 + val {sel_upd={simpset,...},...}
7.1266 = RecordsData.get_sg sg;
7.1267
7.1268 - val has_field = exists_Const
7.1269 + val has_rec = exists_Const
7.1270 (fn (s, Type (_, [Type (_, [T, _]), _])) =>
7.1271 - (s = "all" orelse s = "All" orelse s = "Ex") andalso is_fieldT fields T
7.1272 + (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T
7.1273 | _ => false);
7.1274
7.1275 val goal = Library.nth_elem (i - 1, Thm.prems_of st);
7.1276 - val frees = filter (is_fieldT fields o type_of) (term_frees goal);
7.1277 + val frees = filter (is_recT o type_of) (term_frees goal);
7.1278
7.1279 fun mk_split_free_tac free induct_thm i =
7.1280 let val cfree = cterm_of sg free;
7.1281 @@ -913,504 +965,55 @@
7.1282 end;
7.1283
7.1284 fun split_free_tac P i (free as Free (n,T)) =
7.1285 - (case last_fieldT T of
7.1286 - None => None
7.1287 - | Some(name,_)=> if P free
7.1288 - then (case get_splits sg name of
7.1289 - None => None
7.1290 - | Some (_,_,_,induct_thm)
7.1291 - => Some (mk_split_free_tac free induct_thm i))
7.1292 - else None)
7.1293 + (case rec_id T of
7.1294 + "" => None
7.1295 + | name => if P free
7.1296 + then (case get_splits sg name of
7.1297 + None => None
7.1298 + | Some (_,_,_,induct_thm)
7.1299 + => Some (mk_split_free_tac free induct_thm i))
7.1300 + else None)
7.1301 | split_free_tac _ _ _ = None;
7.1302
7.1303 val split_frees_tacs = mapfilter (split_free_tac P i) frees;
7.1304
7.1305 - val simprocs = if has_field goal then [record_split_simproc P] else [];
7.1306 + val simprocs = if has_rec goal then [record_split_simproc P] else [];
7.1307
7.1308 in st |> (EVERY split_frees_tacs)
7.1309 THEN (Simplifier.full_simp_tac (simpset addsimprocs simprocs) i)
7.1310 end handle Library.LIST _ => Seq.empty;
7.1311 end;
7.1312
7.1313 +
7.1314 +(* record_split_tac *)
7.1315 +(* splits all records in the goal, which are quantified by ! or !!. *)
7.1316 +fun record_split_tac i st =
7.1317 + let
7.1318 + val sg = Thm.sign_of_thm st;
7.1319 +
7.1320 + val has_rec = exists_Const
7.1321 + (fn (s, Type (_, [Type (_, [T, _]), _])) =>
7.1322 + (s = "all" orelse s = "All") andalso is_recT T
7.1323 + | _ => false);
7.1324 +
7.1325 + val goal = Library.nth_elem (i - 1, Thm.prems_of st);
7.1326 +
7.1327 + fun is_all t =
7.1328 + (case t of (Const (quantifier, _)$_) =>
7.1329 + quantifier = "All" orelse quantifier = "all"
7.1330 + | _ => false);
7.1331 +
7.1332 + in if has_rec goal
7.1333 + then Simplifier.full_simp_tac
7.1334 + (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i st
7.1335 + else Seq.empty
7.1336 + end handle Library.LIST _ => Seq.empty;
7.1337 +
7.1338 (* wrapper *)
7.1339
7.1340 val record_split_name = "record_split_tac";
7.1341 val record_split_wrapper = (record_split_name, fn tac => record_split_tac ORELSE' tac);
7.1342
7.1343 -
7.1344 -(* method *)
7.1345 -
7.1346 -val record_split_method =
7.1347 - ("record_split", Method.no_args (Method.SIMPLE_METHOD' HEADGOAL record_split_tac),
7.1348 - "split record fields");
7.1349 -
7.1350 -
7.1351 -
7.1352 -(** internal theory extenders **)
7.1353 -
7.1354 -(* field_typedefs *)
7.1355 -
7.1356 -fun field_typedefs zeta moreT names theory =
7.1357 - let
7.1358 - val alpha = "'a";
7.1359 - val aT = TFree (alpha, HOLogic.typeS);
7.1360 - val UNIV = HOLogic.mk_UNIV (HOLogic.mk_prodT (aT, moreT));
7.1361 -
7.1362 - fun type_def (thy, name) =
7.1363 - let val (thy', {type_definition, set_def = Some def, ...}) =
7.1364 - thy |> setmp TypedefPackage.quiet_mode true
7.1365 - (TypedefPackage.add_typedef_i true None
7.1366 - (suffix field_typeN (Sign.base_name name), [alpha, zeta], Syntax.NoSyn) UNIV None
7.1367 - (Tactic.rtac UNIV_witness 1))
7.1368 - in (thy', Tactic.rewrite_rule [def] type_definition) end
7.1369 - in foldl_map type_def (theory, names) end;
7.1370 -
7.1371 -
7.1372 -(* field_definitions *)
7.1373 -
7.1374 -fun field_definitions fields names alphas zeta moreT more vars thy =
7.1375 - let
7.1376 - val sign = Theory.sign_of thy;
7.1377 - val base = Sign.base_name;
7.1378 -
7.1379 - val xT = TFree (variant alphas "'x", HOLogic.typeS);
7.1380 -
7.1381 -
7.1382 - (* prepare declarations and definitions *)
7.1383 -
7.1384 - (*field constructors*)
7.1385 - val field_decls = map (mk_fieldC moreT) fields;
7.1386 -
7.1387 - fun mk_field_spec ((c, T), v) =
7.1388 - Term.head_of (mk_field ((c, v), more)) :==
7.1389 - lambda v (lambda more (mk_Abs moreT (c, T) $ (HOLogic.mk_prod (v, more))));
7.1390 - val field_specs = map mk_field_spec (fields ~~ vars);
7.1391 -
7.1392 - (*field destructors*)
7.1393 - val dest_decls = map (mk_fstC moreT) fields @ map (mk_sndC moreT) fields;
7.1394 -
7.1395 - fun mk_dest_spec dest sel (c, T) =
7.1396 - let val p = Free ("p", mk_fieldT ((c, T), moreT));
7.1397 - in Term.head_of (dest p) :== lambda p (sel (mk_Rep moreT (c, T) $ p)) end;
7.1398 - val dest_specs1 = map (mk_dest_spec mk_fst HOLogic.mk_fst) fields;
7.1399 - val dest_specs2 = map (mk_dest_spec mk_snd HOLogic.mk_snd) fields;
7.1400 -
7.1401 -
7.1402 - (* 1st stage: defs_thy *)
7.1403 -
7.1404 - val (defs_thy, (((typedefs, field_defs), dest_defs1), dest_defs2)) =
7.1405 - thy
7.1406 - |> field_typedefs zeta moreT names
7.1407 - |>> (Theory.add_consts_i o map (Syntax.no_syn o apfst base)) (field_decls @ dest_decls)
7.1408 - |>>> (PureThy.add_defs_i false o map Thm.no_attributes) field_specs
7.1409 - |>>> (PureThy.add_defs_i false o map Thm.no_attributes) dest_specs1
7.1410 - |>>> (PureThy.add_defs_i false o map Thm.no_attributes) dest_specs2;
7.1411 -
7.1412 - val prod_types = map (fn (((a, b), c), d) => product_type_intro OF [a, b, c, d])
7.1413 - (typedefs ~~ field_defs ~~ dest_defs1 ~~ dest_defs2);
7.1414 -
7.1415 -
7.1416 - (* 2nd stage: thms_thy *)
7.1417 -
7.1418 - fun make ren th = map (fn (prod_type, field) => Drule.standard
7.1419 - (Drule.rename_bvars (ren ~~ [base (fst field), moreN] handle LIST _ => [])
7.1420 - (th OF [prod_type]))) (prod_types ~~ fields);
7.1421 -
7.1422 - val dest_convs = make [] product_type_conv1 @ make [] product_type_conv2;
7.1423 - val field_injects = make [] product_type_inject;
7.1424 - val field_inducts = make ["x", "y"] product_type_induct;
7.1425 - val field_cases = make ["x", "y"] product_type_cases;
7.1426 - val field_splits = make ["a", "b"] product_type_split_paired_all @
7.1427 - make ["a", "b"] product_type_split_paired_All;
7.1428 -
7.1429 - val (thms_thy, [field_defs', dest_defs', dest_convs', field_injects',
7.1430 - field_splits', field_inducts', field_cases']) = defs_thy
7.1431 - |> Codegen.assoc_consts_i (flat (map (fn (s, _) =>
7.1432 - [(suffix fieldN s, None, prod_code),
7.1433 - (suffix fstN s, None, fst_code),
7.1434 - (suffix sndN s, None, snd_code)]) fields))
7.1435 - |> Codegen.assoc_types (map (fn (s, _) =>
7.1436 - (suffix field_typeN s, prodT_code)) fields)
7.1437 - |> (PureThy.add_thmss o map Thm.no_attributes)
7.1438 - [("field_defs", field_defs),
7.1439 - ("dest_defs", dest_defs1 @ dest_defs2),
7.1440 - ("dest_convs", dest_convs),
7.1441 - ("field_injects", field_injects),
7.1442 - ("field_splits", field_splits),
7.1443 - ("field_inducts", field_inducts),
7.1444 - ("field_cases", field_cases)];
7.1445 -
7.1446 - in (thms_thy, dest_convs', field_injects', field_splits', field_inducts', field_cases') end;
7.1447 -
7.1448 -
7.1449 -(* record_definition *)
7.1450 -
7.1451 -fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy =
7.1452 - let
7.1453 - val sign = Theory.sign_of thy;
7.1454 -
7.1455 - val alphas = map fst args;
7.1456 - val name = Sign.full_name sign bname;
7.1457 - val full = Sign.full_name_path sign bname;
7.1458 - val base = Sign.base_name;
7.1459 -
7.1460 - val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
7.1461 -
7.1462 -
7.1463 - (* basic components *)
7.1464 -
7.1465 - val ancestry = map (length o flat o map #fields) (Library.prefixes1 parents);
7.1466 -
7.1467 - val parent_fields = flat (map #fields parents);
7.1468 - val parent_names = map fst parent_fields;
7.1469 - val parent_types = map snd parent_fields;
7.1470 - val parent_len = length parent_fields;
7.1471 - val parent_xs = variantlist (map (base o fst) parent_fields, [moreN, rN]);
7.1472 - val parent_vars = ListPair.map Free (parent_xs, parent_types);
7.1473 - val parent_named_vars = parent_names ~~ parent_vars;
7.1474 -
7.1475 - val fields = map (apfst full) bfields;
7.1476 - val names = map fst fields;
7.1477 - val types = map snd fields;
7.1478 - val len = length fields;
7.1479 - val xs = variantlist (map fst bfields, moreN :: rN :: parent_xs);
7.1480 - val vars = ListPair.map Free (xs, types);
7.1481 - val named_vars = names ~~ vars;
7.1482 -
7.1483 - val all_fields = parent_fields @ fields;
7.1484 - val all_names = parent_names @ names;
7.1485 - val all_types = parent_types @ types;
7.1486 - val all_len = parent_len + len;
7.1487 - val all_xs = parent_xs @ xs;
7.1488 - val all_vars = parent_vars @ vars;
7.1489 - val all_named_vars = parent_named_vars @ named_vars;
7.1490 -
7.1491 - val zeta = variant alphas "'z";
7.1492 - val moreT = TFree (zeta, HOLogic.typeS);
7.1493 - val more = Free (moreN, moreT);
7.1494 - val full_moreN = full moreN;
7.1495 - fun more_part t = mk_more t full_moreN;
7.1496 - fun more_part_update t x = mk_more_update t (full_moreN, x);
7.1497 - val all_types_more = all_types @ [moreT];
7.1498 - val all_xs_more = all_xs @ [moreN];
7.1499 -
7.1500 - val parent_more = funpow parent_len mk_snd;
7.1501 - val idxs = 0 upto (len - 1);
7.1502 -
7.1503 - val fieldsT = mk_recordT (fields, HOLogic.unitT);
7.1504 - fun rec_schemeT n = mk_recordT (prune n all_fields, moreT);
7.1505 - fun rec_scheme n = mk_record (prune n all_named_vars, more);
7.1506 - fun recT n = mk_recordT (prune n all_fields, HOLogic.unitT);
7.1507 - fun rec_ n = mk_record (prune n all_named_vars, HOLogic.unit);
7.1508 - fun r_scheme n = Free (rN, rec_schemeT n);
7.1509 - fun r n = Free (rN, recT n);
7.1510 -
7.1511 -
7.1512 -
7.1513 - (* prepare print translation functions *)
7.1514 - val field_tr's =
7.1515 - print_translation (distinct (flat (map NameSpace.accesses' (full_moreN :: names))));
7.1516 -
7.1517 - val field_type_tr's =
7.1518 - let val fldnames = if parent_len = 0 then (tl names) else names;
7.1519 - in print_translation_field_types (distinct (flat (map NameSpace.accesses' fldnames)))
7.1520 - end;
7.1521 -
7.1522 - fun record_type_abbr_tr's thy =
7.1523 - let val trnames = NameSpace.accesses' (hd all_names)
7.1524 - val sg = Theory.sign_of thy
7.1525 - in map (gen_record_type_abbr_tr'
7.1526 - sg bname alphas zeta (hd (rev names)) (rec_schemeT 0)) trnames end;
7.1527 -
7.1528 - (* prepare declarations *)
7.1529 -
7.1530 - val sel_decls = map (mk_selC (rec_schemeT 0)) bfields @
7.1531 - [mk_moreC (rec_schemeT 0) (moreN, moreT)];
7.1532 - val update_decls = map (mk_updateC (rec_schemeT 0)) bfields @
7.1533 - [mk_more_updateC (rec_schemeT 0) (moreN, moreT)];
7.1534 - val make_decl = (makeN, all_types ---> recT 0);
7.1535 - val fields_decl = (fieldsN, types ---> fieldsT);
7.1536 - val extend_decl = (extendN, recT 0 --> moreT --> rec_schemeT 0);
7.1537 - val truncate_decl = (truncateN, rec_schemeT 0 --> recT 0);
7.1538 -
7.1539 -
7.1540 - (* prepare definitions *)
7.1541 -
7.1542 - (*record (scheme) type abbreviation*)
7.1543 - val recordT_specs =
7.1544 - [(suffix schemeN bname, alphas @ [zeta], rec_schemeT 0, Syntax.NoSyn),
7.1545 - (bname, alphas, recT 0, Syntax.NoSyn)];
7.1546 -
7.1547 - (*selectors*)
7.1548 - fun mk_sel_spec (i, c) =
7.1549 - mk_sel (r_scheme 0) c :== mk_fst (funpow i mk_snd (parent_more (r_scheme 0)));
7.1550 - val sel_specs =
7.1551 - ListPair.map mk_sel_spec (idxs, names) @
7.1552 - [more_part (r_scheme 0) :== funpow len mk_snd (parent_more (r_scheme 0))];
7.1553 -
7.1554 - (*updates*)
7.1555 - val all_sels = mk_named_sels all_names (r_scheme 0);
7.1556 - fun mk_upd_spec (i, (c, x)) =
7.1557 - mk_update (r_scheme 0) (c, x) :==
7.1558 - mk_record (nth_update (c, x) (parent_len + i, all_sels), more_part (r_scheme 0))
7.1559 - val update_specs =
7.1560 - ListPair.map mk_upd_spec (idxs, named_vars) @
7.1561 - [more_part_update (r_scheme 0) more :== mk_record (all_sels, more)];
7.1562 -
7.1563 - (*derived operations*)
7.1564 - val make_spec = Const (full makeN, all_types ---> recT 0) $$ all_vars :==
7.1565 - mk_record (all_named_vars, HOLogic.unit);
7.1566 - val fields_spec = Const (full fieldsN, types ---> fieldsT) $$ vars :==
7.1567 - mk_record (named_vars, HOLogic.unit);
7.1568 - val extend_spec = Const (full extendN, recT 0 --> moreT --> rec_schemeT 0) $ r 0 $ more :==
7.1569 - mk_record (mk_named_sels all_names (r 0), more);
7.1570 - val truncate_spec = Const (full truncateN, rec_schemeT 0 --> recT 0) $ r_scheme 0 :==
7.1571 - mk_record (all_sels, HOLogic.unit);
7.1572 -
7.1573 -
7.1574 - (* prepare propositions *)
7.1575 -
7.1576 - (*selectors*)
7.1577 - val sel_props =
7.1578 - map (fn (c, x) => mk_sel (rec_scheme 0) c === x) named_vars @
7.1579 - [more_part (rec_scheme 0) === more];
7.1580 -
7.1581 - (*updates*)
7.1582 - fun mk_upd_prop (i, (c, T)) =
7.1583 - let val x' = Free (variant all_xs (base c ^ "'"), T) in
7.1584 - mk_update (rec_scheme 0) (c, x') ===
7.1585 - mk_record (nth_update (c, x') (parent_len + i, all_named_vars), more)
7.1586 - end;
7.1587 - val update_props =
7.1588 - ListPair.map mk_upd_prop (idxs, fields) @
7.1589 - let val more' = Free (variant all_xs (moreN ^ "'"), moreT)
7.1590 - in [more_part_update (rec_scheme 0) more' === mk_record (all_named_vars, more')] end;
7.1591 -
7.1592 - (*equality*)
7.1593 - fun mk_sel_eq (t, T) =
7.1594 - let val t' = Term.abstract_over (r_scheme 0, t)
7.1595 - in Trueprop (HOLogic.eq_const T $ Term.incr_boundvars 1 t' $ t') end;
7.1596 - val sel_eqs = map2 mk_sel_eq
7.1597 - (map (mk_sel (r_scheme 0)) all_names @ [more_part (r_scheme 0)], all_types @ [moreT]);
7.1598 - val equality_prop =
7.1599 - Term.all (rec_schemeT 0) $ (Abs ("r", rec_schemeT 0,
7.1600 - Term.all (rec_schemeT 0) $ (Abs ("r'", rec_schemeT 0,
7.1601 - Logic.list_implies (sel_eqs,
7.1602 - Trueprop (HOLogic.eq_const (rec_schemeT 0) $ Bound 1 $ Bound 0))))));
7.1603 -
7.1604 - (*induct*)
7.1605 - fun induct_scheme_prop n =
7.1606 - let val P = Free ("P", rec_schemeT n --> HOLogic.boolT) in
7.1607 - (All (prune n all_xs_more ~~ prune n all_types_more)
7.1608 - (Trueprop (P $ rec_scheme n)), Trueprop (P $ r_scheme n))
7.1609 - end;
7.1610 - fun induct_prop n =
7.1611 - let val P = Free ("P", recT n --> HOLogic.boolT) in
7.1612 - (All (prune n all_xs ~~ prune n all_types) (Trueprop (P $ rec_ n)), Trueprop (P $ r n))
7.1613 - end;
7.1614 -
7.1615 - (*cases*)
7.1616 - val C = Trueprop (Free (variant all_xs_more "C", HOLogic.boolT));
7.1617 - fun cases_scheme_prop n =
7.1618 - All (prune n all_xs_more ~~ prune n all_types_more)
7.1619 - ((r_scheme n === rec_scheme n) ==> C) ==> C;
7.1620 - fun cases_prop n = All (prune n all_xs ~~ prune n all_types) ((r n === rec_ n) ==> C) ==> C;
7.1621 -
7.1622 - (*split*)
7.1623 - fun split_scheme_meta_prop n =
7.1624 - let val P = Free ("P", rec_schemeT n --> Term.propT) in
7.1625 - equals (Term.propT) $
7.1626 - (Term.list_all_free ([(rN,rec_schemeT n)],(P $ r_scheme n)))$
7.1627 - (All (prune n all_xs_more ~~ prune n all_types_more) (P $ rec_scheme n))
7.1628 - end;
7.1629 -
7.1630 - fun split_scheme_object_prop n =
7.1631 - let val P = Free ("P", rec_schemeT n --> HOLogic.boolT)
7.1632 - val ALL = foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t))
7.1633 - in
7.1634 - Trueprop (
7.1635 - HOLogic.eq_const (HOLogic.boolT) $
7.1636 - (HOLogic.mk_all ((rN,rec_schemeT n,P $ r_scheme n)))$
7.1637 - (ALL (prune n all_xs_more ~~ prune n all_types_more,P $ rec_scheme n)))
7.1638 - end;
7.1639 -
7.1640 - fun split_scheme_object_ex_prop n =
7.1641 - let val P = Free ("P", rec_schemeT n --> HOLogic.boolT)
7.1642 - val EX = foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t))
7.1643 - in
7.1644 - Trueprop (
7.1645 - HOLogic.eq_const (HOLogic.boolT) $
7.1646 - (HOLogic.mk_exists ((rN,rec_schemeT n,P $ r_scheme n)))$
7.1647 - (EX (prune n all_xs_more ~~ prune n all_types_more,P $ rec_scheme n)))
7.1648 - end;
7.1649 - (* 1st stage: fields_thy *)
7.1650 -
7.1651 - val (fields_thy, field_simps, field_injects, field_splits, field_inducts, field_cases) =
7.1652 - thy
7.1653 - |> Theory.add_path bname
7.1654 - |> field_definitions fields names alphas zeta moreT more vars;
7.1655 -
7.1656 - val all_field_inducts = flat (map #field_inducts parents) @ field_inducts;
7.1657 - val all_field_cases = flat (map #field_cases parents) @ field_cases;
7.1658 - val all_field_splits = flat (map #field_splits parents) @ field_splits
7.1659 -
7.1660 -
7.1661 - (* 2nd stage: defs_thy *)
7.1662 -
7.1663 -
7.1664 -
7.1665 -
7.1666 - val (defs_thy, (((sel_defs, update_defs), derived_defs))) =
7.1667 - fields_thy
7.1668 - |> Theory.add_trfuns
7.1669 - ([],[],record_type_abbr_tr's fields_thy @ field_type_tr's @ field_tr's, [])
7.1670 - |> add_field_splits (map (suffix field_typeN) names) field_splits
7.1671 - |> Theory.parent_path
7.1672 - |> Theory.add_tyabbrs_i recordT_specs
7.1673 - |> Theory.add_path bname
7.1674 - |> Theory.add_consts_i
7.1675 - (map2 (fn ((x, T), mx) => (x, T, mx)) (sel_decls, field_syntax @ [Syntax.NoSyn]))
7.1676 - |> (Theory.add_consts_i o map Syntax.no_syn)
7.1677 - (update_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
7.1678 - |> (PureThy.add_defs_i false o map Thm.no_attributes) sel_specs
7.1679 - |>>> (PureThy.add_defs_i false o map Thm.no_attributes) update_specs
7.1680 - |>>> (PureThy.add_defs_i false o map Thm.no_attributes)
7.1681 - [make_spec, fields_spec, extend_spec, truncate_spec]
7.1682 - |>> Theory.hide_consts false [full makeN, full fieldsN, full extendN, full truncateN,
7.1683 - full moreN, full (suffix updateN moreN)];
7.1684 -
7.1685 -
7.1686 - (* 3rd stage: thms_thy *)
7.1687 -
7.1688 - val prove_standard = Tactic.prove_standard (Theory.sign_of defs_thy);
7.1689 - fun prove_simp simps =
7.1690 - let val tac = simp_all_tac HOL_basic_ss simps
7.1691 - in fn prop => prove_standard [] [] prop (K tac) end;
7.1692 -
7.1693 - val parent_simps = flat (map #simps parents);
7.1694 - val sel_convs = map (prove_simp (parent_simps @ sel_defs @ field_simps)) sel_props;
7.1695 - val update_convs = map (prove_simp (parent_simps @ update_defs @ sel_convs)) update_props;
7.1696 -
7.1697 - fun induct_scheme n =
7.1698 - let val (assm, concl) = induct_scheme_prop n in
7.1699 - prove_standard [] [assm] concl (fn prems =>
7.1700 - EVERY (map (fn rule => try_param_tac rN rule 1) (prune n all_field_inducts))
7.1701 - THEN resolve_tac prems 1)
7.1702 - end;
7.1703 -
7.1704 - fun cases_scheme n =
7.1705 - prove_standard [] [] (cases_scheme_prop n) (fn _ =>
7.1706 - EVERY (map (fn rule => try_param_tac rN rule 1) (prune n all_field_cases))
7.1707 - THEN simp_all_tac HOL_basic_ss []);
7.1708 -
7.1709 - fun split_scheme_meta n =
7.1710 - prove_standard [] [] (split_scheme_meta_prop n) (fn _ =>
7.1711 - Simplifier.full_simp_tac (HOL_basic_ss addsimps all_field_splits) 1);
7.1712 -
7.1713 - fun split_scheme_object induct_scheme n =
7.1714 - prove_standard [] [] (split_scheme_object_prop n) (fn _ =>
7.1715 - EVERY [rtac iffI 1,
7.1716 - REPEAT (rtac allI 1), etac allE 1, atac 1,
7.1717 - rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]);
7.1718 -
7.1719 - fun split_scheme_object_ex split_scheme_meta n =
7.1720 - prove_standard [] [] (split_scheme_object_ex_prop n) (fn _ =>
7.1721 - fast_simp_tac (claset_of HOL.thy,
7.1722 - HOL_basic_ss addsimps [split_scheme_meta]) 1);
7.1723 -
7.1724 - val induct_scheme0 = induct_scheme 0;
7.1725 - val cases_scheme0 = cases_scheme 0;
7.1726 - val split_scheme_meta0 = split_scheme_meta 0;
7.1727 - val split_scheme_object0 = split_scheme_object induct_scheme0 0;
7.1728 - val split_scheme_object_ex0 = split_scheme_object_ex split_scheme_meta0 0;
7.1729 - val more_induct_scheme = map induct_scheme ancestry;
7.1730 - val more_cases_scheme = map cases_scheme ancestry;
7.1731 -
7.1732 - val (thms_thy, (([sel_convs', update_convs', sel_defs', update_defs', _,
7.1733 - [split_scheme_meta',split_scheme_object',
7.1734 - split_scheme_object_ex',split_scheme_free']],
7.1735 - [induct_scheme', cases_scheme']), [more_induct_scheme', more_cases_scheme'])) =
7.1736 - defs_thy
7.1737 - |> (PureThy.add_thmss o map Thm.no_attributes)
7.1738 - [("select_convs", sel_convs),
7.1739 - ("update_convs", update_convs),
7.1740 - ("select_defs", sel_defs),
7.1741 - ("update_defs", update_defs),
7.1742 - ("defs", derived_defs),
7.1743 - ("splits",[split_scheme_meta0,split_scheme_object0,
7.1744 - split_scheme_object_ex0,induct_scheme0])]
7.1745 - |>>> PureThy.add_thms
7.1746 - [(("induct_scheme", induct_scheme0), induct_type_global (suffix schemeN name)),
7.1747 - (("cases_scheme", cases_scheme0), cases_type_global (suffix schemeN name))]
7.1748 - |>>> PureThy.add_thmss
7.1749 - [(("more_induct_scheme", more_induct_scheme), induct_type_global ""),
7.1750 - (("more_cases_scheme", more_cases_scheme), cases_type_global "")];
7.1751 -
7.1752 -
7.1753 - (* 4th stage: more_thms_thy *)
7.1754 -
7.1755 - val prove_standard = Tactic.prove_standard (Theory.sign_of thms_thy);
7.1756 -
7.1757 - fun induct (n, scheme) =
7.1758 - let val (assm, concl) = induct_prop n in
7.1759 - prove_standard [] [assm] concl (fn prems =>
7.1760 - res_inst_tac [(rN, rN)] scheme 1
7.1761 - THEN try_param_tac "more" unit_induct 1
7.1762 - THEN resolve_tac prems 1)
7.1763 - end;
7.1764 -
7.1765 - fun cases (n, scheme) =
7.1766 - prove_standard [] [] (cases_prop n) (fn _ =>
7.1767 - res_inst_tac [(rN, rN)] scheme 1
7.1768 - THEN simp_all_tac HOL_basic_ss [unit_all_eq1]);
7.1769 -
7.1770 - val induct0 = induct (0, induct_scheme');
7.1771 - val cases0 = cases (0, cases_scheme');
7.1772 - val more_induct = map induct (ancestry ~~ more_induct_scheme');
7.1773 - val more_cases = map cases (ancestry ~~ more_cases_scheme');
7.1774 -
7.1775 - val equality = prove_standard [] [] equality_prop (fn _ =>
7.1776 - fn st => let val [r, r'] = map #1 (rev (Tactic.innermost_params 1 st)) in
7.1777 - st |> (res_inst_tac [(rN, r)] cases_scheme' 1
7.1778 - THEN res_inst_tac [(rN, r')] cases_scheme' 1
7.1779 - THEN simp_all_tac HOL_basic_ss (parent_simps @ sel_convs))
7.1780 - end);
7.1781 -
7.1782 - val (more_thms_thy, [_, _, equality']) =
7.1783 - thms_thy |> PureThy.add_thms
7.1784 - [(("induct", induct0), induct_type_global name),
7.1785 - (("cases", cases0), cases_type_global name),
7.1786 - (("equality", equality), [ContextRules.intro_bang_global None])]
7.1787 - |>> (#1 oo PureThy.add_thmss)
7.1788 - [(("more_induct", more_induct), induct_type_global ""),
7.1789 - (("more_cases", more_cases), cases_type_global "")];
7.1790 -
7.1791 - val simps = sel_convs' @ update_convs';
7.1792 - val iffs = field_injects;
7.1793 -
7.1794 - val more_thms_thy' =
7.1795 - more_thms_thy |> (#1 oo PureThy.add_thmss)
7.1796 - [(("simps", simps), [Simplifier.simp_add_global]),
7.1797 - (("iffs", iffs), [iff_add_global])];
7.1798 -
7.1799 -
7.1800 - (* 5th stage: final_thy *)
7.1801 -
7.1802 - val final_thy =
7.1803 - more_thms_thy'
7.1804 - |> put_record name (make_record_info args parent fields field_inducts field_cases
7.1805 - field_splits (field_simps @ simps))
7.1806 - |> put_sel_upd (names @ [full_moreN]) simps
7.1807 - |> add_record_equalities (snd (split_last names)) equality'
7.1808 - |> add_record_splits (snd (split_last names))
7.1809 - (split_scheme_meta',split_scheme_object',
7.1810 - split_scheme_object_ex',split_scheme_free')
7.1811 - |> Theory.parent_path;
7.1812 -
7.1813 - in (final_thy, {simps = simps, iffs = iffs}) end;
7.1814 -
7.1815 -
7.1816 -
7.1817 (** theory extender interface **)
7.1818
7.1819 (* prepare arguments *)
7.1820 @@ -1432,15 +1035,581 @@
7.1821 let val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle TYPE (msg, _, _) => error msg
7.1822 in (Term.add_typ_tfrees (T, env), T) end;
7.1823
7.1824 +(* attributes *)
7.1825 +
7.1826 +fun case_names_fields x = RuleCases.case_names ["fields"] x;
7.1827 +fun induct_type_global name = [case_names_fields, InductAttrib.induct_type_global name];
7.1828 +fun cases_type_global name = [case_names_fields, InductAttrib.cases_type_global name];
7.1829 +
7.1830 +(* tactics *)
7.1831 +
7.1832 +fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));
7.1833 +
7.1834 +(* do case analysis / induction according to rule on last parameter of ith subgoal
7.1835 + * (or on s if there are no parameters);
7.1836 + * Instatiation of record variable (and predicate) in rule is calculated to
7.1837 + * avoid problems with higher order unification.
7.1838 + *)
7.1839 +
7.1840 +fun try_param_tac s rule i st =
7.1841 + let
7.1842 + val cert = cterm_of (Thm.sign_of_thm st);
7.1843 + val g = nth_elem (i - 1, prems_of st);
7.1844 + val params = Logic.strip_params g;
7.1845 + val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
7.1846 + val rule' = Thm.lift_rule (st, i) rule;
7.1847 + val (P, ys) = strip_comb (HOLogic.dest_Trueprop
7.1848 + (Logic.strip_assums_concl (prop_of rule')));
7.1849 + (* ca indicates if rule is a case analysis or induction rule *)
7.1850 + val (x, ca) = (case rev (drop (length params, ys)) of
7.1851 + [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
7.1852 + (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
7.1853 + | [x] => (head_of x, false));
7.1854 + val rule'' = cterm_instantiate (map (pairself cert) (case (rev params) of
7.1855 + [] => (case assoc (map dest_Free (term_frees (prop_of st)), s) of
7.1856 + None => sys_error "try_param_tac: no such variable"
7.1857 + | Some T => [(P, if ca then concl else lambda (Free (s, T)) concl),
7.1858 + (x, Free (s, T))])
7.1859 + | (_, T) :: _ => [(P, list_abs (params, if ca then concl
7.1860 + else incr_boundvars 1 (Abs (s, T, concl)))),
7.1861 + (x, list_abs (params, Bound 0))])) rule'
7.1862 + in compose_tac (false, rule'', nprems_of rule) i st end;
7.1863 +
7.1864 +fun extension_typedef name repT alphas thy =
7.1865 + let
7.1866 + val UNIV = HOLogic.mk_UNIV repT;
7.1867 +
7.1868 + val (thy',{set_def=Some def, Abs_induct = abs_induct,
7.1869 + Abs_inject=abs_inject, Abs_inverse = abs_inverse,...}) =
7.1870 + thy |> setmp TypedefPackage.quiet_mode true
7.1871 + (TypedefPackage.add_typedef_i true None
7.1872 + (suffix ext_typeN (Sign.base_name name), alphas, Syntax.NoSyn) UNIV None
7.1873 + (Tactic.rtac UNIV_witness 1))
7.1874 + val rewrite_rule = Tactic.rewrite_rule [def, rec_UNIV_I, rec_True_simp];
7.1875 + in (thy',map rewrite_rule [abs_inject, abs_inverse, abs_induct])
7.1876 + end;
7.1877 +
7.1878 +fun extension_definition full name fields names alphas zeta moreT more vars thy =
7.1879 + let
7.1880 + val base = Sign.base_name;
7.1881 +
7.1882 + val fieldTs = (map snd fields);
7.1883 + val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) (alphas@[zeta]);
7.1884 + val extT_name = suffix ext_typeN name
7.1885 + val extT = Type (extT_name, alphas_zetaTs);
7.1886 + val repT = foldr1 HOLogic.mk_prodT (fieldTs@[moreT]);
7.1887 + val fields_more = fields@[(full moreN,moreT)];
7.1888 + val bfields_more = map (apfst base) fields_more;
7.1889 + val r = Free (rN,extT)
7.1890 + val len = length fields;
7.1891 + val idxms = 0 upto len;
7.1892 +
7.1893 + (* prepare declarations and definitions *)
7.1894 +
7.1895 + (*fields constructor*)
7.1896 + val ext_decl = (mk_extC (name,extT) (fieldTs@[moreT]));
7.1897 + val ext_spec = Const ext_decl :==
7.1898 + (foldr (uncurry lambda)
7.1899 + (vars@[more],(mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more])))))
7.1900 +
7.1901 + (*destructors*)
7.1902 + val dest_decls = map (mk_selC extT o (apfst (suffix ext_dest))) bfields_more;
7.1903 +
7.1904 + fun mk_dest_spec (i, (c,T)) =
7.1905 + let val snds = (funpow i HOLogic.mk_snd (mk_Rep name repT extT $ r))
7.1906 + in Const (mk_selC extT (suffix ext_dest c,T))
7.1907 + :== (lambda r (if i=len then snds else HOLogic.mk_fst snds))
7.1908 + end;
7.1909 + val dest_specs =
7.1910 + ListPair.map mk_dest_spec (idxms, fields_more);
7.1911 +
7.1912 + (* code generator data *)
7.1913 + (* Representation as nested pairs is revealed for codegeneration *)
7.1914 + val [rep_code,abs_code] = map (Codegen.parse_mixfix (K (Bound 0))) ["I","I"];
7.1915 + val ext_type_code = Codegen.parse_mixfix (K dummyT) "_";
7.1916 +
7.1917 + (* 1st stage: defs_thy *)
7.1918 + val (defs_thy, ([abs_inject, abs_inverse, abs_induct],ext_def::dest_defs)) =
7.1919 + thy
7.1920 + |> extension_typedef name repT (alphas@[zeta])
7.1921 + |>> Codegen.assoc_consts_i
7.1922 + [(mk_AbsN name,None,abs_code),
7.1923 + (mk_RepN name,None,rep_code)]
7.1924 + |>> Codegen.assoc_types [(extT_name,ext_type_code)]
7.1925 + |>> Theory.add_consts_i (map Syntax.no_syn ((apfst base ext_decl)::dest_decls))
7.1926 + |>>> PureThy.add_defs_i false (map Thm.no_attributes (ext_spec::dest_specs))
7.1927 +
7.1928 +
7.1929 + (* prepare propositions *)
7.1930 +
7.1931 + val vars_more = vars@[more];
7.1932 + val named_vars_more = (names@[full moreN])~~vars_more;
7.1933 + val ext = list_comb (Const ext_decl,vars_more);
7.1934 + val s = Free (rN, extT);
7.1935 + val P = Free (variant (map (fn (Free (x,_))=>x) vars_more) "P", extT-->HOLogic.boolT);
7.1936 + val C = Free (variant (map (fn (Free (x,_))=>x) vars_more) "C", HOLogic.boolT);
7.1937 +
7.1938 + val inject_prop =
7.1939 + let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more;
7.1940 + in All (map dest_Free (vars_more@vars_more'))
7.1941 + ((HOLogic.eq_const extT $
7.1942 + list_comb (Const ext_decl,vars_more)$list_comb (Const ext_decl,vars_more'))
7.1943 + ===
7.1944 + foldr1 HOLogic.mk_conj (map HOLogic.mk_eq (vars_more ~~ vars_more')))
7.1945 + end;
7.1946 +
7.1947 + val induct_prop =
7.1948 + All (map dest_Free vars_more) (Trueprop (P $ ext)) ==> Trueprop (P $ s);
7.1949 +
7.1950 + val cases_prop =
7.1951 + (All (map dest_Free vars_more)
7.1952 + (Trueprop (HOLogic.mk_eq (s,ext)) ==> Trueprop C))
7.1953 + ==> Trueprop C;
7.1954 +
7.1955 + (*destructors*)
7.1956 + val dest_conv_props =
7.1957 + map (fn (c, x as Free (_,T)) => mk_sel ext (suffix ext_dest c,T) === x) named_vars_more;
7.1958 +
7.1959 + val prove_standard = Tactic.prove_standard (Theory.sign_of defs_thy);
7.1960 + fun prove_simp simps =
7.1961 + let val tac = simp_all_tac HOL_ss simps
7.1962 + in fn prop => prove_standard [] [] prop (K tac) end;
7.1963 +
7.1964 + (* prove propositions *)
7.1965 +
7.1966 + val inject = (prove_simp [ext_def,abs_inject,Pair_eq] inject_prop);
7.1967 +
7.1968 + val induct =
7.1969 + prove_standard [] [] induct_prop (fn prems =>
7.1970 + EVERY [try_param_tac rN abs_induct 1,
7.1971 + asm_full_simp_tac (HOL_ss addsimps [ext_def,split_paired_all]) 1]);
7.1972 +
7.1973 + val cases =
7.1974 + prove_standard [] [] cases_prop (fn prems =>
7.1975 + EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
7.1976 + try_param_tac rN induct 1,
7.1977 + rtac impI 1,
7.1978 + REPEAT (etac allE 1),
7.1979 + etac mp 1,
7.1980 + rtac refl 1])
7.1981 +
7.1982 + val dest_convs = map (prove_simp
7.1983 + ([ext_def,abs_inverse]@Pair_sel_convs@dest_defs)) dest_conv_props;
7.1984 +
7.1985 + val (thm_thy,([inject',induct',cases'],[dest_convs'])) =
7.1986 + defs_thy
7.1987 + |> (PureThy.add_thms o map Thm.no_attributes)
7.1988 + [("ext_inject", inject),
7.1989 + ("ext_induct", induct),
7.1990 + ("ext_cases", cases)]
7.1991 + |>>> (PureThy.add_thmss o map Thm.no_attributes)
7.1992 + [("dest_convs",dest_convs)]
7.1993 +
7.1994 + in (thm_thy,extT,induct',inject',dest_convs')
7.1995 + end;
7.1996 +
7.1997 +fun chunks [] [] = []
7.1998 + | chunks [] xs = [xs]
7.1999 + | chunks (l::ls) xs = take (l,xs)::chunks ls (drop (l,xs));
7.2000 +
7.2001 +fun chop_last [] = error "last: list should not be empty"
7.2002 + | chop_last [x] = ([],x)
7.2003 + | chop_last (x::xs) = let val (tl,l) = chop_last xs in (x::tl,l) end;
7.2004 +
7.2005 +fun subst_last s [] = error "subst_last: list should not be empty"
7.2006 + | subst_last s ([x]) = [s]
7.2007 + | subst_last s (x::xs) = (x::subst_last s xs);
7.2008 +
7.2009 +(* mk_recordT builds up the record type from the current extension tpye extT and a list
7.2010 + * of parent extensions, starting with the root of the record hierarchy
7.2011 +*)
7.2012 +fun mk_recordT extT parent_exts =
7.2013 + foldr (fn ((parent,Ts),T) => Type (parent, subst_last T Ts)) (parent_exts,extT);
7.2014 +
7.2015 +(* record_definition *)
7.2016 +
7.2017 +fun record_definition (args, bname) parent parents raw_fields thy =
7.2018 + let
7.2019 + val sign = Theory.sign_of thy;
7.2020 +
7.2021 + val alphas = map fst args;
7.2022 + val name = Sign.full_name sign bname;
7.2023 + val full = Sign.full_name_path sign bname;
7.2024 + val base = Sign.base_name;
7.2025 +
7.2026 + val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
7.2027 +
7.2028 + val parent_fields = flat (map #fields parents);
7.2029 + val parent_chunks = map (length o #fields) parents;
7.2030 + val parent_names = map fst parent_fields;
7.2031 + val parent_types = map snd parent_fields;
7.2032 + val parent_fields_len = length parent_fields;
7.2033 + val parent_variants = variantlist (map base parent_names, [moreN, rN, rN ^ "'"]);
7.2034 + val parent_vars = ListPair.map Free (parent_variants, parent_types);
7.2035 + val parent_len = length parents;
7.2036 + val parents_idx = (map #name parents) ~~ (0 upto (parent_len - 1));
7.2037 +
7.2038 + val fields = map (apfst full) bfields;
7.2039 + val names = map fst fields;
7.2040 + val extN = full bname;
7.2041 + val types = map snd fields;
7.2042 + val alphas_fields = foldr add_typ_tfree_names (types,[]);
7.2043 + val alphas_ext = alphas inter alphas_fields;
7.2044 + val len = length fields;
7.2045 + val variants = variantlist (map fst bfields, moreN::rN::rN ^ "'"::parent_variants);
7.2046 + val vars = ListPair.map Free (variants, types);
7.2047 + val named_vars = names ~~ vars;
7.2048 + val idxs = 0 upto (len - 1);
7.2049 + val idxms = 0 upto len;
7.2050 +
7.2051 + val all_fields = parent_fields @ fields;
7.2052 + val all_names = parent_names @ names;
7.2053 + val all_types = parent_types @ types;
7.2054 + val all_len = parent_fields_len + len;
7.2055 + val all_variants = parent_variants @ variants;
7.2056 + val all_vars = parent_vars @ vars;
7.2057 + val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
7.2058 +
7.2059 +
7.2060 + val zeta = variant alphas "'z";
7.2061 + val moreT = TFree (zeta, HOLogic.typeS);
7.2062 + val more = Free (moreN, moreT);
7.2063 + val full_moreN = full moreN;
7.2064 + val bfields_more = bfields @ [(moreN,moreT)];
7.2065 + val fields_more = fields @ [(full_moreN,moreT)];
7.2066 + val vars_more = vars @ [more];
7.2067 + val named_vars_more = named_vars @[(full_moreN,more)];
7.2068 + val all_vars_more = all_vars @ [more];
7.2069 + val all_named_vars_more = all_named_vars @ [(full_moreN,more)];
7.2070 +
7.2071 + (* 1st stage: extension_thy *)
7.2072 +
7.2073 + val (extension_thy,extT,ext_induct,ext_inject,ext_dest_convs) =
7.2074 + thy
7.2075 + |> Theory.add_path bname
7.2076 + |> extension_definition full extN fields names alphas_ext zeta moreT more vars;
7.2077 +
7.2078 +
7.2079 + val Type extension_scheme = extT;
7.2080 + val extension_name = unsuffix ext_typeN (fst extension_scheme);
7.2081 + val extension = let val (n,Ts) = extension_scheme in (n,subst_last HOLogic.unitT Ts) end;
7.2082 + val extension_names =
7.2083 + (map ((unsuffix ext_typeN) o fst o #extension) parents) @ [extN];
7.2084 + val extension_id = foldl (op ^) ("",extension_names);
7.2085 +
7.2086 +
7.2087 + fun rec_schemeT n = mk_recordT extT (map #extension (prune n parents));
7.2088 + val rec_schemeT0 = rec_schemeT 0;
7.2089 +
7.2090 + fun recT n =
7.2091 + let val (c,Ts) = extension
7.2092 + in mk_recordT (Type (c,subst_last HOLogic.unitT Ts))(map #extension (prune n parents))
7.2093 + end;
7.2094 + val recT0 = recT 0;
7.2095 +
7.2096 + fun mk_rec args n =
7.2097 + let val (args',more) = chop_last args;
7.2098 + fun mk_ext' (((name,T),args),more) = mk_ext (name,T) (args@[more]);
7.2099 + fun build Ts =
7.2100 + foldr mk_ext' (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args')),more)
7.2101 + in
7.2102 + if more = HOLogic.unit
7.2103 + then build (map recT (0 upto parent_len))
7.2104 + else build (map rec_schemeT (0 upto parent_len))
7.2105 + end;
7.2106 +
7.2107 + val r_rec0 = mk_rec all_vars_more 0;
7.2108 + val r_rec_unit0 = mk_rec (all_vars@[HOLogic.unit]) 0;
7.2109 +
7.2110 + fun r n = Free (rN, rec_schemeT n)
7.2111 + val r0 = r 0;
7.2112 + fun r_unit n = Free (rN, recT n)
7.2113 + val r_unit0 = r_unit 0;
7.2114 +
7.2115 + (* prepare print translation functions *)
7.2116 + val field_tr's =
7.2117 + print_translation (distinct (flat (map NameSpace.accesses' (full_moreN :: names))));
7.2118 +
7.2119 + val adv_ext_tr's =
7.2120 + let
7.2121 + val trnames = NameSpace.accesses' extN;
7.2122 + in map (gen_record_tr') trnames end;
7.2123 +
7.2124 + val adv_record_type_abbr_tr's =
7.2125 + let val trnames = NameSpace.accesses' (hd extension_names);
7.2126 + val lastExt = (unsuffix ext_typeN (fst extension));
7.2127 + in map (gen_record_type_abbr_tr' bname alphas zeta lastExt rec_schemeT0) trnames
7.2128 + end;
7.2129 +
7.2130 + val adv_record_type_tr's =
7.2131 + let val trnames = if parent_len > 0 then NameSpace.accesses' extN else [];
7.2132 + (* avoid conflict with adv_record_type_abbr_tr's *)
7.2133 + in map (gen_record_type_tr') trnames
7.2134 + end;
7.2135 +
7.2136 +
7.2137 + (* prepare declarations *)
7.2138 +
7.2139 + val sel_decls = map (mk_selC rec_schemeT0) bfields_more;
7.2140 + val upd_decls = map (mk_updC rec_schemeT0) bfields_more;
7.2141 + val make_decl = (makeN, all_types ---> recT0);
7.2142 + val fields_decl = (fields_selN, types ---> Type extension);
7.2143 + val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0);
7.2144 + val truncate_decl = (truncateN, rec_schemeT0 --> recT0);
7.2145 +
7.2146 + (* prepare definitions *)
7.2147 +
7.2148 + fun parent_more s =
7.2149 + if null parents then s
7.2150 + else mk_sel s (NameSpace.append (#name (hd (rev parents))) moreN, extT);
7.2151 +
7.2152 + fun parent_more_upd v s =
7.2153 + if null parents then v
7.2154 + else let val mp = (NameSpace.append (#name (hd (rev parents))) moreN);
7.2155 + in mk_upd mp v s end;
7.2156 +
7.2157 + (*record (scheme) type abbreviation*)
7.2158 + val recordT_specs =
7.2159 + [(suffix schemeN bname, alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
7.2160 + (bname, alphas, recT0, Syntax.NoSyn)];
7.2161 +
7.2162 + (*selectors*)
7.2163 + fun mk_sel_spec (c,T) =
7.2164 + Const (mk_selC rec_schemeT0 (c,T))
7.2165 + :== (lambda r0 (Const (mk_selC extT (suffix ext_dest c,T))$parent_more r0));
7.2166 + val sel_specs = map mk_sel_spec fields_more;
7.2167 +
7.2168 + (*updates*)
7.2169 + fun mk_upd_spec (c,T) =
7.2170 + let
7.2171 + val args = map (fn (n,nT) => if n=c then Free (base c,T) else (mk_sel r0 (n,nT)))
7.2172 + fields_more;
7.2173 + val new = mk_ext (extN,extT) args;
7.2174 + in Const (mk_updC rec_schemeT0 (c,T))
7.2175 + :== (lambda (Free (base c,T)) (lambda r0 (parent_more_upd new r0)))
7.2176 + end;
7.2177 + val upd_specs = map mk_upd_spec fields_more;
7.2178 +
7.2179 + (*derived operations*)
7.2180 + val make_spec = Const (full makeN, all_types ---> recT0) $$ all_vars :==
7.2181 + mk_rec (all_vars @ [HOLogic.unit]) 0;
7.2182 + val fields_spec = Const (full fields_selN, types ---> Type extension) $$ vars :==
7.2183 + mk_rec (all_vars @ [HOLogic.unit]) parent_len;
7.2184 + val extend_spec =
7.2185 + Const (full extendN, recT0-->moreT-->rec_schemeT0) $ r_unit0 $ more :==
7.2186 + mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
7.2187 + val truncate_spec = Const (full truncateN, rec_schemeT0 --> recT0) $ r0 :==
7.2188 + mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
7.2189 +
7.2190 + (* 2st stage: defs_thy *)
7.2191 +
7.2192 + val (defs_thy,((sel_defs,upd_defs),derived_defs)) =
7.2193 + extension_thy
7.2194 + |> Theory.add_trfuns
7.2195 + ([],[],field_tr's, [])
7.2196 + |> Theory.add_advanced_trfuns
7.2197 + ([],[],adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's,[])
7.2198 +
7.2199 + |> Theory.parent_path
7.2200 + |> Theory.add_tyabbrs_i recordT_specs
7.2201 + |> Theory.add_path bname
7.2202 + |> Theory.add_consts_i
7.2203 + (map2 (fn ((x, T), mx) => (x, T, mx)) (sel_decls, field_syntax @ [Syntax.NoSyn]))
7.2204 + |> (Theory.add_consts_i o map Syntax.no_syn)
7.2205 + (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
7.2206 + |> (PureThy.add_defs_i false o map Thm.no_attributes) sel_specs
7.2207 + |>>> (PureThy.add_defs_i false o map Thm.no_attributes) upd_specs
7.2208 + |>>> (PureThy.add_defs_i false o map Thm.no_attributes)
7.2209 + [make_spec, fields_spec, extend_spec, truncate_spec];
7.2210 +
7.2211 +
7.2212 + (* prepare propositions *)
7.2213 + val P = Free (variant all_variants "P", rec_schemeT0-->HOLogic.boolT);
7.2214 + val C = Free (variant all_variants "C", HOLogic.boolT);
7.2215 + val P_unit = Free (variant all_variants "P", recT0-->HOLogic.boolT);
7.2216 +
7.2217 + (*selectors*)
7.2218 + val sel_conv_props =
7.2219 + map (fn (c, x as Free (_,T)) => mk_sel r_rec0 (c,T) === x) named_vars_more;
7.2220 +
7.2221 + (*updates*)
7.2222 + fun mk_upd_prop (i,(c,T)) =
7.2223 + let val x' = Free (variant all_variants (base c ^ "'"),T)
7.2224 + val args' = nth_update x' (parent_fields_len + i, all_vars_more)
7.2225 + in mk_upd c x' r_rec0 === mk_rec args' 0 end;
7.2226 + val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
7.2227 +
7.2228 + (*induct*)
7.2229 + val induct_scheme_prop =
7.2230 + All (map dest_Free all_vars_more) (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0);
7.2231 + val induct_prop =
7.2232 + (All (map dest_Free all_vars) (Trueprop (P_unit $ r_rec_unit0)),
7.2233 + Trueprop (P_unit $ r_unit0));
7.2234 +
7.2235 + (*surjective*)
7.2236 + val surjective_prop =
7.2237 + let val args = map (fn (c,Free (_,T)) => mk_sel r0 (c,T)) all_named_vars_more
7.2238 + in r0 === mk_rec args 0 end;
7.2239 +
7.2240 + (*cases*)
7.2241 + val cases_scheme_prop =
7.2242 + (All (map dest_Free all_vars_more)
7.2243 + (Trueprop (HOLogic.mk_eq (r0,r_rec0)) ==> Trueprop C))
7.2244 + ==> Trueprop C;
7.2245 +
7.2246 + val cases_prop =
7.2247 + (All (map dest_Free all_vars)
7.2248 + (Trueprop (HOLogic.mk_eq (r_unit0,r_rec_unit0)) ==> Trueprop C))
7.2249 + ==> Trueprop C;
7.2250 +
7.2251 + (*split*)
7.2252 + val split_meta_prop =
7.2253 + let val P = Free (variant all_variants "P", rec_schemeT0-->Term.propT) in
7.2254 + Logic.mk_equals
7.2255 + (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
7.2256 + end;
7.2257 +
7.2258 + val split_object_prop =
7.2259 + let fun ALL vs t = foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) (vs,t)
7.2260 + in (ALL [dest_Free r0] (P $ r0)) === (ALL (map dest_Free all_vars_more) (P $ r_rec0))
7.2261 + end;
7.2262 +
7.2263 +
7.2264 + val split_ex_prop =
7.2265 + let fun EX vs t = foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) (vs,t)
7.2266 + in (EX [dest_Free r0] (P $ r0)) === (EX (map dest_Free all_vars_more) (P $ r_rec0))
7.2267 + end;
7.2268 +
7.2269 + (*equality*)
7.2270 + val equality_prop =
7.2271 + let
7.2272 + val s' = Free (rN ^ "'", rec_schemeT0)
7.2273 + fun mk_sel_eq (c,Free (_,T)) = mk_sel r0 (c,T) === mk_sel s' (c,T)
7.2274 + val seleqs = map mk_sel_eq all_named_vars_more
7.2275 + in All (map dest_Free [r0,s']) (Logic.list_implies (seleqs,r0 === s')) end;
7.2276 +
7.2277 + (* 3rd stage: thms_thy *)
7.2278 +
7.2279 + val prove_standard = Tactic.prove_standard (Theory.sign_of defs_thy);
7.2280 + fun prove_simp ss simps =
7.2281 + let val tac = simp_all_tac ss simps
7.2282 + in fn prop => prove_standard [] [] prop (K tac) end;
7.2283 +
7.2284 + val ss = get_simpset (sign_of defs_thy);
7.2285 + val sel_convs = map (prove_simp ss
7.2286 + (sel_defs@ext_dest_convs)) sel_conv_props;
7.2287 +
7.2288 + val upd_convs = map (prove_simp ss (sel_convs@upd_defs))
7.2289 + upd_conv_props;
7.2290 +
7.2291 + val parent_induct = if null parents then [] else [#induct (hd (rev parents))];
7.2292 +
7.2293 + val induct_scheme = prove_standard [] [] induct_scheme_prop (fn prems =>
7.2294 + (EVERY [if null parent_induct
7.2295 + then all_tac else try_param_tac rN (hd parent_induct) 1,
7.2296 + try_param_tac rN ext_induct 1,
7.2297 + asm_simp_tac HOL_basic_ss 1]));
7.2298 +
7.2299 + val induct =
7.2300 + let val (assm, concl) = induct_prop;
7.2301 + in
7.2302 + prove_standard [] [assm] concl (fn prems =>
7.2303 + try_param_tac rN induct_scheme 1
7.2304 + THEN try_param_tac "more" unit_induct 1
7.2305 + THEN resolve_tac prems 1)
7.2306 + end;
7.2307 +
7.2308 + val surjective =
7.2309 + prove_standard [] [] surjective_prop (fn prems =>
7.2310 + (EVERY [try_param_tac rN induct_scheme 1,
7.2311 + simp_tac (ss addsimps sel_convs) 1]))
7.2312 +
7.2313 + val cases_scheme =
7.2314 + prove_standard [] [] cases_scheme_prop (fn prems =>
7.2315 + EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
7.2316 + try_param_tac rN induct_scheme 1,
7.2317 + rtac impI 1,
7.2318 + REPEAT (etac allE 1),
7.2319 + etac mp 1,
7.2320 + rtac refl 1])
7.2321 +
7.2322 + val cases =
7.2323 + prove_standard [] [] cases_prop (fn _ =>
7.2324 + try_param_tac rN cases_scheme 1
7.2325 + THEN simp_all_tac HOL_basic_ss [unit_all_eq1]);
7.2326 +
7.2327 + val split_meta =
7.2328 + prove_standard [] [] split_meta_prop (fn prems =>
7.2329 + EVERY [rtac equal_intr_rule 1,
7.2330 + rtac meta_allE 1, etac triv_goal 1, atac 1,
7.2331 + rtac (prop_subst OF [surjective]) 1,
7.2332 + REPEAT (EVERY [rtac meta_allE 1, etac triv_goal 1, etac thin_rl 1]),
7.2333 + atac 1]);
7.2334 +
7.2335 + val split_object =
7.2336 + prove_standard [] [] split_object_prop (fn prems =>
7.2337 + EVERY [rtac iffI 1,
7.2338 + REPEAT (rtac allI 1), etac allE 1, atac 1,
7.2339 + rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]);
7.2340 +
7.2341 + val split_ex =
7.2342 + prove_standard [] [] split_ex_prop (fn prems =>
7.2343 + fast_simp_tac (claset_of HOL.thy,
7.2344 + HOL_basic_ss addsimps [split_meta]) 1);
7.2345 +
7.2346 + val equality = prove_standard [] [] equality_prop (fn _ =>
7.2347 + fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
7.2348 + st |> (res_inst_tac [(rN, s)] cases_scheme 1
7.2349 + THEN res_inst_tac [(rN, s')] cases_scheme 1
7.2350 + THEN simp_all_tac ss (sel_convs))
7.2351 + end);
7.2352 +
7.2353 + val (thms_thy,(([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],
7.2354 + derived_defs'],
7.2355 + [surjective',equality']),[induct_scheme',induct',cases_scheme',cases'])) =
7.2356 + defs_thy
7.2357 + |> (PureThy.add_thmss o map Thm.no_attributes)
7.2358 + [("select_convs", sel_convs),
7.2359 + ("update_convs", upd_convs),
7.2360 + ("select_defs", sel_defs),
7.2361 + ("update_defs", upd_defs),
7.2362 + ("splits", [split_meta,split_object,split_ex]),
7.2363 + ("defs", derived_defs)]
7.2364 + |>>> (PureThy.add_thms o map Thm.no_attributes)
7.2365 + [("surjective", surjective),
7.2366 + ("equality", equality)]
7.2367 + |>>> PureThy.add_thms
7.2368 + [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
7.2369 + (("induct", induct), induct_type_global name),
7.2370 + (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
7.2371 + (("cases", cases), cases_type_global name)];
7.2372 +
7.2373 +
7.2374 + val sel_upd_simps = sel_convs' @ upd_convs';
7.2375 + val iffs = [ext_inject]
7.2376 + val final_thy =
7.2377 + thms_thy
7.2378 + |> (#1 oo PureThy.add_thmss)
7.2379 + [(("simps", sel_upd_simps), [Simplifier.simp_add_global]),
7.2380 + (("iffs",iffs), [iff_add_global])]
7.2381 + |> put_record name (make_record_info args parent fields extension induct_scheme')
7.2382 + |> put_sel_upd (names @ [full_moreN]) sel_upd_simps
7.2383 + |> add_record_equalities extension_id equality'
7.2384 + |> add_record_splits extension_id (split_meta',split_object',split_ex',induct_scheme')
7.2385 + |> add_extfields extension_name (fields @ [(full_moreN,moreT)])
7.2386 + |> add_fieldext (extension_name,snd extension) (names @ [full_moreN])
7.2387 + |> Theory.parent_path;
7.2388 +
7.2389 + in final_thy
7.2390 + end;
7.2391
7.2392 (* add_record *)
7.2393
7.2394 (*we do all preparations and error checks here, deferring the real
7.2395 work to record_definition*)
7.2396 -
7.2397 fun gen_add_record prep_typ prep_raw_parent (params, bname) raw_parent raw_fields thy =
7.2398 let
7.2399 - val _ = Theory.requires thy "Record" "record definitions";
7.2400 + val _ = Theory.requires thy "Record" "record definitions";
7.2401 val sign = Theory.sign_of thy;
7.2402 val _ = message ("Defining record " ^ quote bname ^ " ...");
7.2403
7.2404 @@ -1479,7 +1648,7 @@
7.2405 (* errors *)
7.2406
7.2407 val name = Sign.full_name sign bname;
7.2408 - val err_dup_record =
7.2409 + val err_dup_record =
7.2410 if is_none (get_record thy name) then []
7.2411 else ["Duplicate definition of record " ^ quote name];
7.2412
7.2413 @@ -1513,7 +1682,7 @@
7.2414 err_dup_record @ err_dup_parms @ err_extra_frees @ err_no_fields @
7.2415 err_dup_fields @ err_bad_fields @ err_dup_sorts;
7.2416 in
7.2417 - if null errs then () else error (cat_lines errs);
7.2418 + if null errs then () else error (cat_lines errs) ;
7.2419 thy |> record_definition (args, bname) parent parents bfields
7.2420 end
7.2421 handle ERROR => error ("Failed to define record " ^ quote bname);
7.2422 @@ -1521,19 +1690,15 @@
7.2423 val add_record = gen_add_record read_typ read_raw_parent;
7.2424 val add_record_i = gen_add_record cert_typ (K I);
7.2425
7.2426 -
7.2427 -(** package setup **)
7.2428 -
7.2429 (* setup theory *)
7.2430
7.2431 val setup =
7.2432 [RecordsData.init,
7.2433 Theory.add_trfuns ([], parse_translation, [], []),
7.2434 - Method.add_methods [record_split_method],
7.2435 + Theory.add_advanced_trfuns ([], adv_parse_translation, [], []),
7.2436 Simplifier.change_simpset_of Simplifier.addsimprocs
7.2437 [record_simproc, record_eq_simproc]];
7.2438
7.2439 -
7.2440 (* outer syntax *)
7.2441
7.2442 local structure P = OuterParse and K = OuterSyntax.Keyword in
7.2443 @@ -1543,8 +1708,8 @@
7.2444 (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
7.2445
7.2446 val recordP =
7.2447 - OuterSyntax.command "record" "define extensible record" K.thy_decl
7.2448 - (record_decl >> (fn (x, (y, z)) => Toplevel.theory (#1 o add_record x y z)));
7.2449 + OuterSyntax.command "record" "define extensible record" K.thy_decl
7.2450 + (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z)));
7.2451
7.2452 val _ = OuterSyntax.add_parsers [recordP];
7.2453
8.1 --- a/src/HOL/ex/Records.thy Sat May 01 22:28:51 2004 +0200
8.2 +++ b/src/HOL/ex/Records.thy Mon May 03 23:22:17 2004 +0200
8.3 @@ -1,6 +1,7 @@
8.4 (* Title: HOL/ex/Records.thy
8.5 ID: $Id$
8.6 - Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
8.7 + Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel,
8.8 + TU Muenchen
8.9 License: GPL (GNU GENERAL PUBLIC LICENSE)
8.10 *)
8.11
8.12 @@ -19,6 +20,7 @@
8.13 following theorems:
8.14 *}
8.15
8.16 +
8.17 thm "point.simps"
8.18 thm "point.iffs"
8.19 thm "point.defs"
8.20 @@ -28,10 +30,10 @@
8.21 automatically to the standard simpset, @{thm [source] point.iffs} is
8.22 added to the Classical Reasoner and Simplifier context.
8.23
8.24 - \medskip Record declarations define new type abbreviations:
8.25 + \medskip Record declarations define new types and type abbreviations:
8.26 @{text [display]
8.27 -" point = (| xpos :: nat, ypos :: nat |)
8.28 - 'a point_scheme = (| xpos :: nat, ypos :: nat, ... :: 'a |)"}
8.29 +" point = \<lparr>xpos :: nat, ypos :: nat\<rparr> = () point_ext_type
8.30 + 'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr> = 'a point_ext_type"}
8.31 *}
8.32
8.33 consts foo1 :: point
8.34 @@ -107,7 +109,7 @@
8.35 induction.
8.36 *}
8.37
8.38 -lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
8.39 +lemma "r(| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
8.40 proof (cases r)
8.41 fix xpos ypos more
8.42 assume "r = (| xpos = xpos, ypos = ypos, ... = more |)"
8.43 @@ -174,10 +176,12 @@
8.44
8.45
8.46 text {*
8.47 - The record declaration defines new type constructors:
8.48 + The record declaration defines a new type constructure and abbreviations:
8.49 @{text [display]
8.50 -" cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |)
8.51 - 'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |)"}
8.52 +" cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) =
8.53 + () cpoint_ext_type point_ext_type
8.54 + 'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |) =
8.55 + 'a cpoint_ext_type point_ext_type"}
8.56 *}
8.57
8.58 consts foo6 :: cpoint
9.1 --- a/src/HOL/thy_syntax.ML Sat May 01 22:28:51 2004 +0200
9.2 +++ b/src/HOL/thy_syntax.ML Mon May 03 23:22:17 2004 +0200
9.3 @@ -277,7 +277,7 @@
9.4 val _ = ThySyn.add_syntax
9.5 ["intrs", "monos", "congs", "simpset", "|", "and", "distinct", "inject", "induct"]
9.6 [axm_section "typedef" "|> TypedefPackage.add_typedef_x" typedef_decl,
9.7 - section "record" "|> (#1 oooo RecordPackage.add_record)" record_decl,
9.8 + section "record" "|> RecordPackage.add_record" record_decl,
9.9 section "inductive" "" (inductive_decl false),
9.10 section "coinductive" "" (inductive_decl true),
9.11 section "datatype" "" datatype_decl,
10.1 --- a/src/Pure/sign.ML Sat May 01 22:28:51 2004 +0200
10.2 +++ b/src/Pure/sign.ML Mon May 03 23:22:17 2004 +0200
10.3 @@ -61,6 +61,7 @@
10.4 val extern: sg -> string -> string -> xstring
10.5 val cond_extern: sg -> string -> string -> xstring
10.6 val cond_extern_table: sg -> string -> 'a Symtab.table -> (xstring * 'a) list
10.7 + val extern_typ: sg -> typ -> typ
10.8 val intern_class: sg -> xclass -> class
10.9 val intern_tycon: sg -> xstring -> string
10.10 val intern_const: sg -> xstring -> string
10.11 @@ -551,6 +552,9 @@
10.12 val cond_extern = cond_extrn o spaces_of;
10.13 fun cond_extern_table sg = cond_extrn_table (spaces_of sg);
10.14
10.15 + fun extern_typ (sg as Sg (_, {spaces, ...})) T =
10.16 + if ! NameSpace.long_names then T else extrn_typ spaces T;
10.17 +
10.18 val intern_class = intrn_class o spaces_of;
10.19 val intern_sort = intrn_sort o spaces_of;
10.20 val intern_typ = intrn_typ o spaces_of;
10.21 @@ -596,9 +600,8 @@
10.22
10.23 fun pretty_term sg = pretty_term' (syn_of sg) sg;
10.24
10.25 -fun pretty_typ (sg as Sg (_, {spaces, ...})) T =
10.26 - Syntax.pretty_typ (syn_of sg)
10.27 - (if ! NameSpace.long_names then T else extrn_typ spaces T);
10.28 +fun pretty_typ sg T =
10.29 + Syntax.pretty_typ (syn_of sg) (extern_typ sg T);
10.30
10.31 fun pretty_sort (sg as Sg (_, {spaces, ...})) S =
10.32 Syntax.pretty_sort (syn_of sg)