# HG changeset patch # User schirmer # Date 1083619337 -7200 # Node ID 2f885b7e5ba725e1721b28e0c2e4e167d42f38d7 # Parent 2c9b463044ecb0c60f15119eabb6b034ba6759ca reimplementation of HOL records; only one type is created for each record extension, instead of one type for each field. See NEWS. diff -r 2c9b463044ec -r 2f885b7e5ba7 NEWS --- a/NEWS Sat May 01 22:28:51 2004 +0200 +++ b/NEWS Mon May 03 23:22:17 2004 +0200 @@ -19,6 +19,7 @@ depend on the signature of the theory context being presently used for parsing/printing, see also isar-ref manual. + * Pure: improved indexed syntax and implicit structures. First of all, indexed syntax provides a notational device for subscripted application, using the new syntax \<^bsub>term\<^esub> for arbitrary @@ -30,6 +31,17 @@ * Pure: tuned internal renaming of symbolic identifiers -- attach primes instead of base 26 numbers. +*** HOL *** + +* Records: + Reimplementation of records to avoid performance problems for + type inference. Records are no longer composed of nested field types, + but of nested extension types. Therefore the record type only grows + linear in the number of extensions and not in the number of fields. + The top-level (users) view on records is preserved. + Potential INCOMPATIBILITY only in strange cases, where the theory + depends on the old record representation. The type generated for + a record is called _ext_type. *** HOLCF *** diff -r 2c9b463044ec -r 2f885b7e5ba7 src/HOL/Bali/DeclConcepts.thy --- a/src/HOL/Bali/DeclConcepts.thy Sat May 01 22:28:51 2004 +0200 +++ b/src/HOL/Bali/DeclConcepts.thy Mon May 03 23:22:17 2004 +0200 @@ -92,7 +92,7 @@ lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a" by (simp add: acc_modi_accmodi_def) -instance access_field_type:: ("type","type") has_accmodi .. +instance decl_ext_type:: ("type") has_accmodi .. defs (overloaded) decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \ access d" @@ -130,7 +130,7 @@ axclass has_declclass < "type" consts declclass:: "'a::has_declclass \ qtname" -instance pid_field_type::("type","type") has_declclass .. +instance qtname_ext_type::("type") has_declclass .. defs (overloaded) qtname_declclass_def: "declclass (q::qtname) \ q" @@ -153,17 +153,17 @@ axclass has_static < "type" consts is_static :: "'a::has_static \ bool" -instance access_field_type :: ("type","has_static") has_static .. +instance decl_ext_type :: ("has_static") has_static .. defs (overloaded) decl_is_static_def: "is_static (m::('a::has_static) decl_scheme) \ is_static (Decl.decl.more m)" -instance static_field_type :: ("type","type") has_static .. +instance member_ext_type :: ("type") has_static .. defs (overloaded) static_field_type_is_static_def: - "is_static (m::(bool,'b::type) static_field_type) \ static_val m" + "is_static (m::('b::type) member_ext_type) \ static_val m" lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m" apply (cases m) @@ -401,37 +401,30 @@ axclass has_resTy < "type" consts resTy:: "'a::has_resTy \ ty" -instance access_field_type :: ("type","has_resTy") has_resTy .. +instance decl_ext_type :: ("has_resTy") has_resTy .. defs (overloaded) decl_resTy_def: "resTy (m::('a::has_resTy) decl_scheme) \ resTy (Decl.decl.more m)" -instance static_field_type :: ("type","has_resTy") has_resTy .. - -defs (overloaded) -static_field_type_resTy_def: - "resTy (m::(bool,'b::has_resTy) static_field_type) - \ resTy (static_more m)" - -instance pars_field_type :: ("type","has_resTy") has_resTy .. +instance member_ext_type :: ("has_resTy") has_resTy .. defs (overloaded) -pars_field_type_resTy_def: - "resTy (m::(vname list,'b::has_resTy) pars_field_type) - \ resTy (pars_more m)" +member_ext_type_resTy_def: + "resTy (m::('b::has_resTy) member_ext_type) + \ resTy (member.more_val m)" -instance resT_field_type :: ("type","type") has_resTy .. +instance mhead_ext_type :: ("type") has_resTy .. defs (overloaded) -resT_field_type_resTy_def: - "resTy (m::(ty,'b::type) resT_field_type) +mhead_ext_type_resTy_def: + "resTy (m::('b mhead_ext_type)) \ resT_val m" lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m" apply (cases m) -apply (simp add: decl_resTy_def static_field_type_resTy_def - pars_field_type_resTy_def resT_field_type_resTy_def +apply (simp add: decl_resTy_def member_ext_type_resTy_def + mhead_ext_type_resTy_def member.dest_convs mhead.dest_convs) done diff -r 2c9b463044ec -r 2f885b7e5ba7 src/HOL/Bali/Name.thy --- a/src/HOL/Bali/Name.thy Sat May 01 22:28:51 2004 +0200 +++ b/src/HOL/Bali/Name.thy Mon May 03 23:22:17 2004 +0200 @@ -80,7 +80,7 @@ consts qtname:: "'a::has_qtname \ qtname" (* Declare qtname as instance of has_qtname *) -instance pid_field_type::(has_pname,"type") has_qtname .. +instance qtname_ext_type::("type") has_qtname .. defs (overloaded) qtname_qtname_def: "qtname (q::qtname) \ q" diff -r 2c9b463044ec -r 2f885b7e5ba7 src/HOL/Bali/TypeRel.thy --- a/src/HOL/Bali/TypeRel.thy Sat May 01 22:28:51 2004 +0200 +++ b/src/HOL/Bali/TypeRel.thy Mon May 03 23:22:17 2004 +0200 @@ -545,7 +545,7 @@ lemma widen_Object:"\isrtype G T;ws_prog G\ \ G\RefT T \ Class Object" apply (case_tac T) apply (auto) -apply (subgoal_tac "G\pid_field_type\\<^sub>C Object") +apply (subgoal_tac "G\qtname_ext_type\\<^sub>C Object") apply (auto intro: subcls_ObjectI) done diff -r 2c9b463044ec -r 2f885b7e5ba7 src/HOL/Bali/TypeSafe.thy --- a/src/HOL/Bali/TypeSafe.thy Sat May 01 22:28:51 2004 +0200 +++ b/src/HOL/Bali/TypeSafe.thy Mon May 03 23:22:17 2004 +0200 @@ -776,12 +776,8 @@ apply (force intro: var_tys_Some_eq [THEN iffD2]) done -lemma obj_split: "\ obj. \ t vs. obj = \tag=t,values=vs\" -proof record_split - fix tag values more - show "\t vs. \tag = tag, values = values, \ = more\ = \tag = t, values = vs\" - by auto -qed +lemma obj_split: "\ t vs. obj = \tag=t,values=vs\" + by (cases obj) auto lemma AVar_lemma2: "error_free state \ error_free @@ -3602,7 +3598,7 @@ show "G\statC\\<^sub>C statDeclC" by (auto dest!: accfield_fields dest: fields_declC) from accfield - show fld: "table_of (fields G statC) (fn, statDeclC) = Some f" + show fld: "table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some f" by (auto dest!: accfield_fields) from wf show "wf_prog G" . from conf_a s2 show "x2 = None \ G,store2\a\\Class statC" diff -r 2c9b463044ec -r 2f885b7e5ba7 src/HOL/Record.thy --- a/src/HOL/Record.thy Sat May 01 22:28:51 2004 +0200 +++ b/src/HOL/Record.thy Mon May 03 23:22:17 2004 +0200 @@ -1,88 +1,32 @@ (* Title: HOL/Record.thy ID: $Id$ - Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen + Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen *) -header {* Extensible records with structural subtyping *} - theory Record = Product_Type files ("Tools/record_package.ML"): - -subsection {* Abstract product types *} - -locale product_type = - fixes Rep and Abs and pair and dest1 and dest2 - assumes "typedef": "type_definition Rep Abs UNIV" - and pair: "pair == (\a b. Abs (a, b))" - and dest1: "dest1 == (\p. fst (Rep p))" - and dest2: "dest2 == (\p. snd (Rep p))" - -lemma (in product_type) - "inject": "(pair x y = pair x' y') = (x = x' \ y = y')" - by (simp add: pair type_definition.Abs_inject [OF "typedef"]) - -lemma (in product_type) conv1: "dest1 (pair x y) = x" - by (simp add: pair dest1 type_definition.Abs_inverse [OF "typedef"]) - -lemma (in product_type) conv2: "dest2 (pair x y) = y" - by (simp add: pair dest2 type_definition.Abs_inverse [OF "typedef"]) - -lemma (in product_type) induct [induct type]: - assumes hyp: "!!x y. P (pair x y)" - shows "P p" -proof (rule type_definition.Abs_induct [OF "typedef"]) - fix q show "P (Abs q)" - proof (induct q) - fix x y have "P (pair x y)" by (rule hyp) - also have "pair x y = Abs (x, y)" by (simp only: pair) - finally show "P (Abs (x, y))" . - qed -qed +ML {* +val [h1, h2] = Goal "PROP Goal (\x. PROP P x) \ (PROP P x \ PROP Q) \ PROP Q"; +by (rtac h2 1); +by (rtac (gen_all (h1 RS Drule.rev_triv_goal)) 1); +qed "meta_allE"; +*} -lemma (in product_type) cases [cases type]: - "(!!x y. p = pair x y ==> C) ==> C" - by (induct p) (auto simp add: "inject") - -lemma (in product_type) surjective_pairing: - "p = pair (dest1 p) (dest2 p)" - by (induct p) (simp only: conv1 conv2) +lemma prop_subst: "s = t \ PROP P t \ PROP P s" + by simp -lemma (in product_type) split_paired_all: - "(!!x. PROP P x) == (!!a b. PROP P (pair a b))" -proof - fix a b - assume "!!x. PROP P x" - thus "PROP P (pair a b)" . -next - fix x - assume "!!a b. PROP P (pair a b)" - hence "PROP P (pair (dest1 x) (dest2 x))" . - thus "PROP P x" by (simp only: surjective_pairing [symmetric]) -qed +lemma rec_UNIV_I: "\x. x\UNIV \ True" + by simp -lemma (in product_type) split_paired_All: - "(ALL x. P x) = (ALL a b. P (pair a b))" -proof - fix a b - assume "ALL x. P x" - thus "ALL a b. P (pair a b)" by rules -next - assume P: "ALL a b. P (pair a b)" - show "ALL x. P x" - proof - fix x - from P have "P (pair (dest1 x) (dest2 x))" by rules - thus "P x" by (simp only: surjective_pairing [symmetric]) - qed -qed +lemma rec_True_simp: "(True \ PROP P) \ PROP P" + by simp subsection {* Concrete record syntax *} nonterminals ident field_type field_types field fields update updates - syntax "_constify" :: "id => ident" ("_") "_constify" :: "longid => ident" ("_") @@ -112,10 +56,27 @@ "_record_scheme" :: "[fields, 'a] => 'a" ("(3\_,/ (2\ =/ _)\)") "_record_update" :: "['a, updates] => 'b" ("_/(3\_\)" [900,0] 900) +(* -subsection {* Package setup *} + "_structure" :: "fields => 'a" ("(3{| _ |})") + "_structure_scheme" :: "[fields, 'a] => 'a" ("(3{| _,/ (2... =/ _) |})") + + "_structure_update_name":: idt + "_structure_update" :: "['a, updates] \ 'b" ("_/(3{| _ |})" [900,0] 900) -use "Tools/record_package.ML" -setup RecordPackage.setup + "_structure_type" :: "field_types => type" ("(3{| _ |})") + "_structure_type_scheme" :: "[field_types, type] => type" + ("(3{| _,/ (2... ::/ _) |})") +syntax (xsymbols) + + "_structure_scheme" :: "[fields, 'a] => 'a" ("(3{|_,/ (2\ =/ _)|})") + + "_structure_type_scheme" :: "[field_types, type] => type" + ("(3{|_,/ (2\ ::/ _)|})") + +*) +use "Tools/record_package.ML"; +setup RecordPackage.setup; end + diff -r 2c9b463044ec -r 2f885b7e5ba7 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Sat May 01 22:28:51 2004 +0200 +++ b/src/HOL/Tools/record_package.ML Mon May 03 23:22:17 2004 +0200 @@ -10,10 +10,15 @@ sig val record_simproc: simproc val record_eq_simproc: simproc + val record_upd_simproc: simproc + val record_split_simproc: (term -> bool) -> simproc + val record_ex_sel_eq_simproc: simproc val record_split_tac: int -> tactic + val record_split_simp_tac: (term -> bool) -> int -> tactic val record_split_name: string val record_split_wrapper: string * wrapper - val print_record_type_abbr: bool ref + val print_record_type_abbr: bool ref + val print_record_type_as_fields: bool ref end; signature RECORD_PACKAGE = @@ -21,59 +26,73 @@ include BASIC_RECORD_PACKAGE val quiet_mode: bool ref val updateN: string - val mk_fieldT: (string * typ) * typ -> typ - val dest_fieldT: typ -> (string * typ) * typ - val dest_fieldTs: typ -> (string * typ) list - val last_fieldT: typ -> (string * typ) option - val last_field: Sign.sg -> string -> (string * typ) option - val get_parents: Sign.sg -> string -> string list - val mk_field: (string * term) * term -> term - val mk_fst: term -> term - val mk_snd: term -> term - val mk_recordT: (string * typ) list * typ -> typ - val dest_recordT: typ -> (string * typ) list * typ - val mk_record: (string * term) list * term -> term - val mk_sel: term -> string -> term - val mk_update: term -> string * term -> term + val ext_typeN: string + val last_extT: typ -> (string * typ list) option + val dest_recTs : typ -> (string * typ list) list + val get_extension: Sign.sg -> Symtab.key -> (string * typ list) option val print_records: theory -> unit - val add_record: (string list * bstring) -> string option - -> (bstring * string * mixfix) list -> theory -> theory * {simps: thm list, iffs: thm list} - val add_record_i: (string list * bstring) -> (typ list * string) option - -> (bstring * typ * mixfix) list -> theory -> theory * {simps: thm list, iffs: thm list} + val add_record: string list * string -> string option -> (string * string * mixfix) list + -> theory -> theory + val add_record_i: string list * string -> (typ list * string) option + -> (string * typ * mixfix) list -> theory -> theory val setup: (theory -> theory) list - val record_upd_simproc: simproc - val record_split_simproc: (term -> bool) -> simproc - val record_ex_sel_eq_simproc: simproc - val record_split_simp_tac: (term -> bool) -> int -> tactic end; -structure RecordPackage: RECORD_PACKAGE = + +structure RecordPackage :RECORD_PACKAGE = struct - -(*** theory context references ***) - -val product_typeN = "Record.product_type"; - -val product_type_intro = thm "product_type.intro"; -val product_type_inject = thm "product_type.inject"; -val product_type_conv1 = thm "product_type.conv1"; -val product_type_conv2 = thm "product_type.conv2"; -val product_type_induct = thm "product_type.induct"; -val product_type_cases = thm "product_type.cases"; -val product_type_split_paired_all = thm "product_type.split_paired_all"; -val product_type_split_paired_All = thm "product_type.split_paired_All"; +val rec_UNIV_I = thm "rec_UNIV_I"; +val rec_True_simp = thm "rec_True_simp"; +val Pair_eq = thm "Product_Type.Pair_eq"; +val atomize_all = thm "HOL.atomize_all"; +val atomize_imp = thm "HOL.atomize_imp"; +val triv_goal = thm "triv_goal"; +val prop_subst = thm "prop_subst"; +val Pair_sel_convs = [fst_conv,snd_conv]; +(** name components **) + +val rN = "r"; +val moreN = "more"; +val schemeN = "_scheme"; +val ext_typeN = "_ext_type"; +val extN ="_ext"; +val ext_dest = "_val"; +val updateN = "_update"; +val schemeN = "_scheme"; +val makeN = "make"; +val fields_selN = "fields"; +val extendN = "extend"; +val truncateN = "truncate"; + +(*see typedef_package.ML*) +val RepN = "Rep_"; +val AbsN = "Abs_"; + (*** utilities ***) + +fun last [] = error "RecordPackage.last: empty list" + | last [x] = x + | last (x::xs) = last xs; + +fun but_last [] = error "RecordPackage.but_last: empty list" + | but_last [x] = [] + | but_last (x::xs) = x::but_last xs; + +fun remdups [] = [] + | remdups (x::xs) = x::remdups (filter_out (fn y => y=x) xs); + +fun is_suffix sfx s = is_some (try (unsuffix sfx) s); + (* messages *) val quiet_mode = ref false; fun message s = if ! quiet_mode then () else writeln s; - (* syntax *) fun prune n xs = Library.drop (n, xs); @@ -91,332 +110,66 @@ val (op ===) = Trueprop o HOLogic.mk_eq; val (op ==>) = Logic.mk_implies; - -(* attributes *) - -fun case_names_fields x = RuleCases.case_names ["fields"] x; -fun induct_type_global name = [case_names_fields, InductAttrib.induct_type_global name]; -fun cases_type_global name = [case_names_fields, InductAttrib.cases_type_global name]; - - -(* tactics *) - -fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps)); - -(* do case analysis / induction on last parameter of ith subgoal (or s) *) - -fun try_param_tac s rule i st = - let - val cert = cterm_of (Thm.sign_of_thm st); - val g = nth_elem (i - 1, prems_of st); - val params = Logic.strip_params g; - val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g); - val rule' = Thm.lift_rule (st, i) rule; - val (P, ys) = strip_comb (HOLogic.dest_Trueprop - (Logic.strip_assums_concl (prop_of rule'))); - val (x, ca) = (case rev (drop (length params, ys)) of - [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop - (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true) - | [x] => (head_of x, false)); - val rule'' = cterm_instantiate (map (pairself cert) (case (rev params) of - [] => (case assoc (map dest_Free (term_frees (prop_of st)), s) of - None => sys_error "try_param_tac: no such variable" - | Some T => [(P, if ca then concl else lambda (Free (s, T)) concl), - (x, Free (s, T))]) - | (_, T) :: _ => [(P, list_abs (params, if ca then concl - else incr_boundvars 1 (Abs (s, T, concl)))), - (x, list_abs (params, Bound 0))])) rule' - in compose_tac (false, rule'', nprems_of rule) i st end; - - - -(*** code generator data ***) - -val [prod_code, fst_code, snd_code] = - map (Codegen.parse_mixfix (K (Bound 0))) ["(_,/ _)", "fst", "snd"]; -val prodT_code = Codegen.parse_mixfix (K dummyT) "(_ */ _)"; - - - -(*** syntax operations ***) - -(** name components **) - -val rN = "r"; -val moreN = "more"; -val schemeN = "_scheme"; -val field_typeN = "_field_type"; -val fieldN = "_field"; -val fstN = "_val"; -val sndN = "_more"; -val updateN = "_update"; -val makeN = "make"; -val fieldsN = "fields"; -val extendN = "extend"; -val truncateN = "truncate"; - - -(*see typedef_package.ML*) -val RepN = "Rep_"; -val AbsN = "Abs_"; - - - -(** tuple operations **) - -(* types *) - -fun mk_fieldT ((c, T), U) = Type (suffix field_typeN c, [T, U]); - -fun dest_fieldT (typ as Type (c_field_type, [T, U])) = - (case try (unsuffix field_typeN) c_field_type of - None => raise TYPE ("dest_fieldT", [typ], []) - | Some c => ((c, T), U)) - | dest_fieldT typ = raise TYPE ("dest_fieldT", [typ], []); - -fun dest_fieldTs T = - let val ((c, T), U) = dest_fieldT T - in (c, T) :: dest_fieldTs U - end handle TYPE _ => []; - -fun last_fieldT T = - let val ((c, T), U) = dest_fieldT T - in (case last_fieldT U of - None => Some (c,T) - | Some l => Some l) - end handle TYPE _ => None - (* morphisms *) -fun mk_Rep U (c, T) = - Const (suffix field_typeN (prefix_base RepN c), - mk_fieldT ((c, T), U) --> HOLogic.mk_prodT (T, U)); +fun mk_RepN name = suffix ext_typeN (prefix_base RepN name); +fun mk_AbsN name = suffix ext_typeN (prefix_base AbsN name); -fun mk_Abs U (c, T) = - Const (suffix field_typeN (prefix_base AbsN c), - HOLogic.mk_prodT (T, U) --> mk_fieldT ((c, T), U)); - +fun mk_Rep name repT absT = + Const (suffix ext_typeN (prefix_base RepN name),absT --> repT); -(* constructors *) +fun mk_Abs name repT absT = + Const (mk_AbsN name,repT --> absT); -fun mk_fieldC U (c, T) = (suffix fieldN c, T --> U --> mk_fieldT ((c, T), U)); +(* constructor *) -fun mk_field ((c, t), u) = - let val T = fastype_of t and U = fastype_of u - in Const (suffix fieldN c, [T, U] ---> mk_fieldT ((c, T), U)) $ t $ u end; +fun mk_extC (name,T) Ts = (suffix extN name, Ts ---> T); +fun mk_ext (name,T) ts = + let val Ts = map fastype_of ts + in list_comb (Const (mk_extC (name,T) Ts),ts) end; -(* destructors *) +(* selector *) + +fun mk_selC sT (c,T) = (c,sT --> T); -fun mk_fstC U (c, T) = (suffix fstN c, mk_fieldT ((c, T), U) --> T); -fun mk_sndC U (c, T) = (suffix sndN c, mk_fieldT ((c, T), U) --> U); +fun mk_sel s (c,T) = + let val sT = fastype_of s + in Const (mk_selC sT (c,T)) $ s end; -fun dest_field fst_or_snd p = - let - val pT = fastype_of p; - val ((c, T), U) = dest_fieldT pT; - val (destN, destT) = if fst_or_snd then (fstN, T) else (sndN, U); - in Const (suffix destN c, pT --> destT) $ p end; +(* updates *) + +fun mk_updC sT (c,T) = (suffix updateN c, T --> sT --> sT); -val mk_fst = dest_field true; -val mk_snd = dest_field false; - - - -(** record operations **) +fun mk_upd c v s = + let val sT = fastype_of s; + val vT = fastype_of v; + in Const (mk_updC sT (c, vT)) $ v $ s end; (* types *) -val mk_recordT = foldr mk_fieldT; - -fun dest_recordT T = - (case try dest_fieldT T of - None => ([], T) - | Some (c_T, U) => apfst (cons c_T) (dest_recordT U)); - -fun find_fieldT c rT = - (case assoc (fst (dest_recordT rT), c) of - None => raise TYPE ("find_field: " ^ c, [rT], []) - | Some T => T); - - -(* constructors *) - -val mk_record = foldr mk_field; - - -(* selectors *) - -fun mk_selC rT (c, T) = (c, rT --> T); - -fun mk_sel r c = - let val rT = fastype_of r - in Const (mk_selC rT (c, find_fieldT c rT)) $ r end; - -fun mk_named_sels names r = names ~~ map (mk_sel r) names; - -val mk_moreC = mk_selC; - -fun mk_more r c = - let val rT = fastype_of r - in Const (mk_moreC rT (c, snd (dest_recordT rT))) $ r end; - - -(* updates *) - -fun mk_updateC rT (c, T) = (suffix updateN c, T --> rT --> rT); - -fun mk_update r (c, x) = - let val rT = fastype_of r - in Const (mk_updateC rT (c, find_fieldT c rT)) $ x $ r end; - -val mk_more_updateC = mk_updateC; +fun dest_recT (typ as Type (c_ext_type, Ts as (T::_))) = + (case try (unsuffix ext_typeN) c_ext_type of + None => raise TYPE ("RecordPackage.dest_recT", [typ], []) + | Some c => ((c, Ts), last Ts)) + | dest_recT typ = raise TYPE ("RecordPackage.dest_recT", [typ], []); -fun mk_more_update r (c, x) = - let val rT = fastype_of r - in Const (mk_more_updateC rT (c, snd (dest_recordT rT))) $ x $ r end; - - - -(** concrete syntax for records **) - -(* parse translations *) - -fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) = - if c = mark then Syntax.const (suffix sfx name) $ arg - else raise TERM ("gen_field_tr: " ^ mark, [t]) - | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]); - -fun gen_fields_tr sep mark sfx (tm as Const (c, _) $ t $ u) = - if c = sep then gen_field_tr mark sfx t :: gen_fields_tr sep mark sfx u - else [gen_field_tr mark sfx tm] - | gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm]; - -fun gen_record_tr sep mark sfx unit [t] = foldr (op $) (gen_fields_tr sep mark sfx t, unit) - | gen_record_tr _ _ _ _ ts = raise TERM ("gen_record_tr", ts); - -fun gen_record_scheme_tr sep mark sfx [t, more] = foldr (op $) (gen_fields_tr sep mark sfx t, more) - | gen_record_scheme_tr _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts); - - -val record_type_tr = gen_record_tr "_field_types" "_field_type" field_typeN (Syntax.const "unit"); -val record_type_scheme_tr = gen_record_scheme_tr "_field_types" "_field_type" field_typeN; - -val record_tr = gen_record_tr "_fields" "_field" fieldN HOLogic.unit; -val record_scheme_tr = gen_record_scheme_tr "_fields" "_field" fieldN; - -fun record_update_tr [t, u] = - foldr (op $) (rev (gen_fields_tr "_updates" "_update" updateN u), t) - | record_update_tr ts = raise TERM ("record_update_tr", ts); - - -fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts - | update_name_tr (Const (x, T) :: ts) = Const (suffix updateN x, T) $$ ts - | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) = - (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy")) $$ ts - | update_name_tr ts = raise TERM ("update_name_tr", ts); - +fun is_recT T = + (case try dest_recT T of None => false | Some _ => true); -val parse_translation = - [("_record_type", record_type_tr), - ("_record_type_scheme", record_type_scheme_tr), - ("_record", record_tr), - ("_record_scheme", record_scheme_tr), - ("_record_update", record_update_tr), - ("_update_name", update_name_tr)]; - - -(* print translations *) - - -val print_record_type_abbr = ref true; - -fun gen_fields_tr' mark sfx (tm as Const (name_field, _) $ t $ u) = - (case try (unsuffix sfx) name_field of - Some name => - apfst (cons (Syntax.const mark $ Syntax.free name $ t)) (gen_fields_tr' mark sfx u) - | None => ([], tm)) - | gen_fields_tr' _ _ tm = ([], tm); - -fun gen_record_tr' sep mark sfx is_unit record record_scheme tm = - let - val (ts, u) = gen_fields_tr' mark sfx tm; - val t' = foldr1 (fn (v, w) => Syntax.const sep $ v $ w) ts; - in - if is_unit u then Syntax.const record $ t' - else Syntax.const record_scheme $ t' $ u - end; - - -val record_type_tr' = - gen_record_tr' "_field_types" "_field_type" field_typeN - (fn Const ("unit", _) => true | _ => false) "_record_type" "_record_type_scheme"; - - -(* record_type_abbr_tr' tries to reconstruct the record name type abbreviation from *) -(* the (nested) field types. *) -fun record_type_abbr_tr' sg abbr alphas zeta lastF rec_schemeT tm = - let - (* tm is term representation of a (nested) field type. We first reconstruct the *) - (* type from tm so that we can continue on the type level rather then the term level.*) - - fun get_sort xs n = (case assoc (xs,n) of - Some s => s - | None => Sign.defaultS sg); - - val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm); - val tsig = Sign.tsig_of sg; +fun dest_recTs T = + let val ((c, Ts), U) = dest_recT T + in (c, Ts) :: dest_recTs U + end handle TYPE _ => []; - fun mk_type_abbr subst name alphas = - let val abbrT = Type (name, map (fn a => TVar ((a,0),logicS)) alphas); - in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end; - - fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T)) - - in if !print_record_type_abbr - then (case last_fieldT T of - Some (name,_) - => if name = lastF - then - let val subst = unify rec_schemeT T - in - if HOLogic.is_unitT (Envir.norm_type subst (TVar((zeta,0),Sign.defaultS sg))) - then mk_type_abbr subst abbr alphas - else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta]) - end handle TUNIFY => record_type_tr' tm - else raise Match (* give print translation of specialised record a chance *) - | _ => record_type_tr' tm) - else record_type_tr' tm - end +fun last_extT T = + let val ((c, Ts), U) = dest_recT T + in (case last_extT U of + None => Some (c,Ts) + | Some l => Some l) + end handle TYPE _ => None - -fun gen_record_type_abbr_tr' sg abbr alphas zeta lastF rec_schemeT name = - let val name_sfx = suffix field_typeN name - val tr' = record_type_abbr_tr' sg abbr alphas zeta lastF rec_schemeT - in (name_sfx, fn [t,u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end; - -val record_tr' = - gen_record_tr' "_fields" "_field" fieldN - (fn Const ("Unity", _) => true | _ => false) "_record" "_record_scheme"; - -fun record_update_tr' tm = - let val (ts, u) = gen_fields_tr' "_update" updateN tm in - Syntax.const "_record_update" $ u $ - foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts) - end; - -fun gen_field_tr' sfx tr' name = - let val name_sfx = suffix sfx name - in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end; - -fun print_translation names = - map (gen_field_tr' fieldN record_tr') names @ - map (gen_field_tr' updateN record_update_tr') names; - -fun print_translation_field_types names = - map (gen_field_tr' field_typeN record_type_tr') names - - +fun rec_id T = foldl (fn (s,(c,T)) => s ^ c) ("",dest_recTs T); (*** extend theory by record definition ***) @@ -428,29 +181,26 @@ {args: (string * sort) list, parent: (typ list * string) option, fields: (string * typ) list, - field_inducts: thm list, - field_cases: thm list, - field_splits: thm list, - simps: thm list}; + extension: (string * typ list), + induct: thm + }; -fun make_record_info args parent fields field_inducts field_cases field_splits simps = - {args = args, parent = parent, fields = fields, field_inducts = field_inducts, - field_cases = field_cases, field_splits = field_splits, simps = simps}: record_info; +fun make_record_info args parent fields extension induct = + {args = args, parent = parent, fields = fields, extension = extension, + induct = induct}: record_info; + type parent_info = {name: string, fields: (string * typ) list, - field_inducts: thm list, - field_cases: thm list, - field_splits: thm list, - simps: thm list}; + extension: (string * typ list), + induct: thm +}; -fun make_parent_info name fields field_inducts field_cases field_splits simps = - {name = name, fields = fields, field_inducts = field_inducts, - field_cases = field_cases, field_splits = field_splits, simps = simps}: parent_info; +fun make_parent_info name fields extension induct = + {name = name, fields = fields, extension = extension, induct = induct}: parent_info; - -(* data kind 'HOL/records' *) +(* data kind 'HOL/record' *) type record_data = {records: record_info Symtab.table, @@ -458,52 +208,54 @@ {selectors: unit Symtab.table, updates: string Symtab.table, simpset: Simplifier.simpset}, - field_splits: - {fields: unit Symtab.table, - simpset: Simplifier.simpset}, equalities: thm Symtab.table, - splits: (thm*thm*thm*thm) Symtab.table (* !!,!,EX - split-equalities,induct rule *) + splits: (thm*thm*thm*thm) Symtab.table, (* !!,!,EX - split-equalities,induct rule *) + extfields: (string*typ) list Symtab.table, (* maps extension to its fields *) + fieldext: (string*typ list) Symtab.table (* maps field to its extension *) }; -fun make_record_data records sel_upd field_splits equalities splits = - {records = records, sel_upd = sel_upd, field_splits = field_splits, - equalities = equalities, splits = splits}: record_data; +fun make_record_data records sel_upd equalities splits extfields fieldext = + {records = records, sel_upd = sel_upd, + equalities = equalities, splits = splits, + extfields = extfields, fieldext = fieldext }: record_data; structure RecordsArgs = struct - val name = "HOL/records"; + val name = "HOL/records"; type T = record_data; val empty = make_record_data Symtab.empty {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss} - {fields = Symtab.empty, simpset = HOL_basic_ss} Symtab.empty Symtab.empty; + Symtab.empty Symtab.empty Symtab.empty Symtab.empty; val copy = I; val prep_ext = I; fun merge ({records = recs1, sel_upd = {selectors = sels1, updates = upds1, simpset = ss1}, - field_splits = {fields = flds1, simpset = fld_ss1}, equalities = equalities1, - splits = splits1}, + splits = splits1, + extfields = extfields1, + fieldext = fieldext1}, {records = recs2, sel_upd = {selectors = sels2, updates = upds2, simpset = ss2}, - field_splits = {fields = flds2, simpset = fld_ss2}, equalities = equalities2, - splits = splits2}) = + splits = splits2, + extfields = extfields2, + fieldext = fieldext2}) = make_record_data (Symtab.merge (K true) (recs1, recs2)) {selectors = Symtab.merge (K true) (sels1, sels2), updates = Symtab.merge (K true) (upds1, upds2), simpset = Simplifier.merge_ss (ss1, ss2)} - {fields = Symtab.merge (K true) (flds1, flds2), - simpset = Simplifier.merge_ss (fld_ss1, fld_ss2)} (Symtab.merge Thm.eq_thm (equalities1, equalities2)) (Symtab.merge (fn ((a,b,c,d),(w,x,y,z)) => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso Thm.eq_thm (c,y) andalso Thm.eq_thm (d,z)) - (splits1, splits2)); + (splits1, splits2)) + (Symtab.merge (K true) (extfields1,extfields2)) + (Symtab.merge (K true) (fieldext1,fieldext2)); fun print sg ({records = recs, ...}: record_data) = let @@ -527,24 +279,28 @@ structure RecordsData = TheoryDataFun(RecordsArgs); val print_records = RecordsData.print; - (* access 'records' *) fun get_record thy name = Symtab.lookup (#records (RecordsData.get thy), name); fun put_record name info thy = let - val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy; + val {records, sel_upd, equalities, splits,extfields,fieldext} = RecordsData.get thy; val data = make_record_data (Symtab.update ((name, info), records)) - sel_upd field_splits equalities splits; + sel_upd equalities splits extfields fieldext; in RecordsData.put data thy end; - (* access 'sel_upd' *) fun get_sel_upd sg = #sel_upd (RecordsData.get_sg sg); fun get_selectors sg name = Symtab.lookup (#selectors (get_sel_upd sg), name); +fun is_selector sg name = + case get_selectors sg (Sign.intern_const sg name) of + None => false + | Some _ => true + + fun get_updates sg name = Symtab.lookup (#updates (get_sel_upd sg), name); fun get_simpset sg = #simpset (get_sel_upd sg); @@ -553,36 +309,22 @@ val sels = map (rpair ()) names; val upds = map (suffix updateN) names ~~ names; - val {records, sel_upd = {selectors, updates, simpset}, field_splits, - equalities, splits} = RecordsData.get thy; + val {records, sel_upd = {selectors, updates, simpset}, + equalities, splits, extfields,fieldext} = RecordsData.get thy; val data = make_record_data records {selectors = Symtab.extend (selectors, sels), updates = Symtab.extend (updates, upds), simpset = Simplifier.addsimps (simpset, simps)} - field_splits equalities splits; + equalities splits extfields fieldext; in RecordsData.put data thy end; - -(* access 'field_splits' *) - -fun add_field_splits names simps thy = - let - val {records, sel_upd, field_splits = {fields, simpset}, - equalities, splits} = RecordsData.get thy; - val flds = map (rpair ()) names; - val data = make_record_data records sel_upd - {fields = Symtab.extend (fields, flds), - simpset = Simplifier.addsimps (simpset, simps)} equalities splits; - in RecordsData.put data thy end; - - (* access 'equalities' *) fun add_record_equalities name thm thy = let - val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy; - val data = make_record_data records sel_upd field_splits - (Symtab.update_new ((name, thm), equalities)) splits; + val {records, sel_upd, equalities, splits, extfields,fieldext} = RecordsData.get thy; + val data = make_record_data records sel_upd + (Symtab.update_new ((name, thm), equalities)) splits extfields fieldext; in RecordsData.put data thy end; fun get_equalities sg name = @@ -592,28 +334,46 @@ fun add_record_splits name thmP thy = let - val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy; - val data = make_record_data records sel_upd field_splits - equalities (Symtab.update_new ((name, thmP), splits)); + val {records, sel_upd, equalities, splits, extfields,fieldext} = RecordsData.get thy; + val data = make_record_data records sel_upd + equalities (Symtab.update_new ((name, thmP), splits)) extfields fieldext; in RecordsData.put data thy end; fun get_splits sg name = Symtab.lookup (#splits (RecordsData.get_sg sg), name); -(* last field of a record *) -fun last_field sg name = - case Symtab.lookup (#records (RecordsData.get_sg sg),name) of - Some r => Some (hd (rev (#fields r))) +(* extension of a record name *) +fun get_extension sg name = + case Symtab.lookup (#records (RecordsData.get_sg sg),name) of + Some s => Some (#extension s) | None => None; -(* get parent names *) -fun get_parents sg name = - (case Symtab.lookup (#records (RecordsData.get_sg sg),name) of - Some r => (case #parent r of - Some (_,p) => p::get_parents sg p - | None => []) - | None => []) - +(* access 'extfields' *) + +fun add_extfields name fields thy = + let + val {records, sel_upd, equalities, splits, extfields, fieldext} = RecordsData.get thy; + val data = make_record_data records sel_upd + equalities splits (Symtab.update_new ((name, fields), extfields)) fieldext; + in RecordsData.put data thy end; + +fun get_extfields sg name = + Symtab.lookup (#extfields (RecordsData.get_sg sg), name); + +(* access 'fieldext' *) + +fun add_fieldext extname_types fields thy = + let + val {records, sel_upd, equalities, splits, extfields, fieldext} = RecordsData.get thy; + val fieldext' = foldl (fn (table,field) => Symtab.update_new ((field,extname_types),table)) + (fieldext,fields); + val data = make_record_data records sel_upd equalities splits extfields fieldext'; + in RecordsData.put data thy end; + + +fun get_fieldext sg name = + Symtab.lookup (#fieldext (RecordsData.get_sg sg), name); + (* parent records *) fun add_parents thy None parents = parents @@ -622,7 +382,7 @@ val sign = Theory.sign_of thy; fun err msg = error (msg ^ " parent record " ^ quote name); - val {args, parent, fields, field_inducts, field_cases, field_splits, simps} = + val {args, parent, fields, extension, induct} = (case get_record thy name of Some info => info | None => err "Unknown"); val _ = if length types <> length args then err "Bad number of arguments for" else (); @@ -634,33 +394,342 @@ val subst = Term.map_type_tfree (fn (x, _) => the (assoc (inst, x))); val parent' = apsome (apfst (map subst)) parent; val fields' = map (apsnd subst) fields; + val extension' = apsnd (map subst) extension; in conditional (not (null bads)) (fn () => err ("Ill-sorted instantiation of " ^ commas bads ^ " in")); add_parents thy parent' - (make_parent_info name fields' field_inducts field_cases field_splits simps::parents) + (make_parent_info name fields' extension' induct::parents) end; +(** concrete syntax for records **) + +(* parse translations *) + +fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) = + if c = mark then Syntax.const (suffix sfx name) $ arg + else raise TERM ("gen_field_tr: " ^ mark, [t]) + | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]); + +fun gen_fields_tr sep mark sfx (tm as Const (c, _) $ t $ u) = + if c = sep then gen_field_tr mark sfx t :: gen_fields_tr sep mark sfx u + else [gen_field_tr mark sfx tm] + | gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm]; + + +fun record_update_tr [t, u] = + foldr (op $) (rev (gen_fields_tr "_updates" "_update" updateN u), t) + | record_update_tr ts = raise TERM ("record_update_tr", ts); + +fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts + | update_name_tr (Const (x, T) :: ts) = Const (suffix updateN x, T) $$ ts + | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) = + (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy")) $$ ts + | update_name_tr ts = raise TERM ("update_name_tr", ts); + +fun dest_ext_field mark (t as (Const (c,_) $ Const (name,_) $ arg)) = + if c = mark then (name,arg) else raise TERM ("dest_ext_field: " ^ mark, [t]) + | dest_ext_field _ t = raise TERM ("dest_ext_field", [t]) + +fun dest_ext_fields sep mark (trm as (Const (c,_) $ t $ u)) = + if c = sep then dest_ext_field mark t::dest_ext_fields sep mark u + else [dest_ext_field mark trm] + | dest_ext_fields _ mark t = [dest_ext_field mark t] + +fun gen_ext_fields_tr sep mark sfx more sg t = + let + val fieldargs = dest_ext_fields sep mark t; + fun splitargs (field::fields) ((name,arg)::fargs) = + if is_suffix name field + then let val (args,rest) = splitargs fields fargs + in (arg::args,rest) end + else raise TERM ("gen_ext_fields_tr: expecting field " ^ field ^ + " but got " ^ name, [t]) + | splitargs [] (fargs as (_::_)) = ([],fargs) + | splitargs (_::_) [] = raise TERM ("gen_ext_fields_tr: expecting more fields", [t]) + | splitargs _ _ = ([],[]); + + fun mk_ext (fargs as (name,arg)::_) = + (case get_fieldext sg (Sign.intern_const sg name) of + Some (ext,_) => (case get_extfields sg ext of + Some flds + => let val (args,rest) = + splitargs (map fst (but_last flds)) fargs; + val more' = mk_ext rest; + in list_comb (Syntax.const (suffix sfx ext),args@[more']) + end + | None => raise TERM("gen_ext_fields_tr: no fields defined for " + ^ ext,[t])) + | None => raise TERM ("gen_ext_fields_tr: "^ name ^" is no proper field",[t])) + | mk_ext [] = more + + in mk_ext fieldargs end; + +fun gen_ext_type_tr sep mark sfx more sg t = + let + val fieldargs = dest_ext_fields sep mark t; + fun splitargs (field::fields) ((name,arg)::fargs) = + if is_suffix name field + then let val (args,rest) = splitargs fields fargs + in (arg::args,rest) end + else raise TERM ("gen_ext_type_tr: expecting field " ^ field ^ + " but got " ^ name, [t]) + | splitargs [] (fargs as (_::_)) = ([],fargs) + | splitargs (_::_) [] = raise TERM ("gen_ext_type_tr: expecting more fields", [t]) + | splitargs _ _ = ([],[]); + + fun get_sort xs n = (case assoc (xs,n) of + Some s => s + | None => Sign.defaultS sg); + fun to_type t = Sign.intern_typ sg + (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t); + + val tsig = Sign.tsig_of sg; + fun unify (t,env) = Type.unify tsig env t; + + fun mk_ext (fargs as (name,arg)::_) = + (case get_fieldext sg (Sign.intern_const sg name) of + Some (ext,alphas) => + (case get_extfields sg ext of + Some flds + => (let + val flds' = but_last flds; + val types = map snd flds'; + val (args,rest) = splitargs (map fst flds') fargs; + val vartypes = map Type.varifyT types; + val argtypes = map to_type args; + val (subst,_) = foldr unify (vartypes ~~ argtypes,(Vartab.empty,0)); + val alphas' = map ((Syntax.term_of_typ (! Syntax.show_sorts)) o + (Envir.norm_type subst) o Type.varifyT) + (but_last alphas); + + val more' = mk_ext rest; + in list_comb (Syntax.const (suffix sfx ext),alphas'@[more']) + end handle TUNIFY => raise + TERM ("gen_ext_type_tr: type is no proper record (extension)", [t])) + | None => raise TERM ("gen_ext_fields_tr: no fields defined for " ^ ext,[t])) + | None => raise TERM ("gen_ext_fields_tr: "^ name ^" is no proper field",[t])) + | mk_ext [] = more + + in mk_ext fieldargs end; + +fun gen_adv_record_tr sep mark sfx unit sg [t] = + gen_ext_fields_tr sep mark sfx unit sg t + | gen_adv_record_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts); + +fun gen_adv_record_scheme_tr sep mark sfx sg [t, more] = + gen_ext_fields_tr sep mark sfx more sg t + | gen_adv_record_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts); + +fun gen_adv_record_type_tr sep mark sfx unit sg [t] = + gen_ext_type_tr sep mark sfx unit sg t + | gen_adv_record_type_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts); + +fun gen_adv_record_type_scheme_tr sep mark sfx sg [t, more] = + gen_ext_type_tr sep mark sfx more sg t + | gen_adv_record_type_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts); + +val adv_record_tr = gen_adv_record_tr "_fields" "_field" extN HOLogic.unit; +val adv_record_scheme_tr = gen_adv_record_scheme_tr "_fields" "_field" extN; + +val adv_record_type_tr = + gen_adv_record_type_tr "_field_types" "_field_type" ext_typeN + (Syntax.term_of_typ false (HOLogic.unitT)); +val adv_record_type_scheme_tr = + gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN; + +val parse_translation = + [("_record_update", record_update_tr), + ("_update_name", update_name_tr)]; + +val adv_parse_translation = + [("_record",adv_record_tr), + ("_record_scheme",adv_record_scheme_tr), + ("_record_type",adv_record_type_tr), + ("_record_type_scheme",adv_record_type_scheme_tr)]; + + +(* print translations *) + +val print_record_type_abbr = ref true; +val print_record_type_as_fields = ref true; + +fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ t $ u) = + (case try (unsuffix sfx) name_field of + Some name => + apfst (cons (Syntax.const mark $ Syntax.free name $ t)) (gen_field_upds_tr' mark sfx u) + | None => ([], tm)) + | gen_field_upds_tr' _ _ tm = ([], tm); + +fun record_update_tr' tm = + let val (ts, u) = gen_field_upds_tr' "_update" updateN tm in + Syntax.const "_record_update" $ u $ + foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts) + end; + +fun gen_field_tr' sfx tr' name = + let val name_sfx = suffix sfx name + in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end; + +fun record_tr' sep mark record record_scheme unit sg t = + let + fun field_lst t = + (case strip_comb t of + (Const (ext,_),args) + => (case try (unsuffix extN) (Sign.intern_const sg ext) of + Some ext' + => (case get_extfields sg ext' of + Some flds + => (let + val (f::fs) = but_last (map fst flds); + val flds' = Sign.extern sg Sign.constK f::map NameSpace.base fs; + val (args',more) = split_last args; + in (flds'~~args')@field_lst more end + handle LIST _ => [("",t)]) + | None => [("",t)]) + | None => [("",t)]) + | _ => [("",t)]) + + val (flds,(_,more)) = split_last (field_lst t); + val flds' = map (fn (n,t)=>Syntax.const mark$Syntax.const n$t) flds; + val flds'' = foldr1 (fn (x,y) => Syntax.const sep$x$y) flds'; + + in if null flds then raise Match + else if unit more + then Syntax.const record$flds'' + else Syntax.const record_scheme$flds''$more + end + +fun gen_record_tr' name = + let val name_sfx = suffix extN name; + val unit = (fn Const ("Unity",_) => true | _ => false); + fun tr' sg ts = record_tr' "_fields" "_field" "_record" "_record_scheme" unit sg + (list_comb (Syntax.const name_sfx,ts)) + in (name_sfx,tr') + end + +fun print_translation names = + map (gen_field_tr' updateN record_update_tr') names; + +(* record_type_abbr_tr' tries to reconstruct the record name type abbreviation from *) +(* the (nested) extension types. *) +fun record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT sg tm = + let + (* tm is term representation of a (nested) field type. We first reconstruct the *) + (* type from tm so that we can continue on the type level rather then the term level.*) + + fun get_sort xs n = (case assoc (xs,n) of + Some s => s + | None => Sign.defaultS sg); + + val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm) + val tsig = Sign.tsig_of sg + + fun mk_type_abbr subst name alphas = + let val abbrT = Type (name, map (fn a => TVar ((a,0),logicS)) alphas); + in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end; + + fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T)) + + in if !print_record_type_abbr + then (case last_extT T of + Some (name,_) + => if name = lastExt + then + (let val subst = unify schemeT T + in + if HOLogic.is_unitT (Envir.norm_type subst (TVar((zeta,0),Sign.defaultS sg))) + then mk_type_abbr subst abbr alphas + else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta]) + end handle TUNIFY => default_tr' sg tm) + else raise Match (* give print translation of specialised record a chance *) + | _ => raise Match) + else default_tr' sg tm + end + +fun record_type_tr' sep mark record record_scheme sg t = + let + fun get_sort xs n = (case assoc (xs,n) of + Some s => s + | None => Sign.defaultS sg); + + val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t) + + val tsig = Sign.tsig_of sg + fun unify (t,v) = Type.unify tsig v t; + + fun term_of_type T = Syntax.term_of_typ (!Syntax.show_sorts) (Sign.extern_typ sg T); + + fun field_lst T = + (case T of + Type (ext,args) + => (case try (unsuffix ext_typeN) ext of + Some ext' + => (case get_extfields sg ext' of + Some flds + => (case get_fieldext sg (fst (hd flds)) of + Some (_,alphas) + => (let + val (f::fs) = but_last flds; + val flds' = apfst (Sign.extern sg Sign.constK) f + ::map (apfst NameSpace.base) fs; + val (args',more) = split_last args; + val alphavars = map Type.varifyT (but_last alphas); + val (subst,_)= foldr unify (alphavars~~args',(Vartab.empty,0)); + val flds'' =map (apsnd ((Envir.norm_type subst)o(Type.varifyT))) + flds'; + in flds''@field_lst more end + handle TUNIFY => [("",T)] + | LIST _=> [("",T)]) + | None => [("",T)]) + | None => [("",T)]) + | None => [("",T)]) + | _ => [("",T)]) + + val (flds,(_,moreT)) = split_last (field_lst T); + val flds' = map (fn (n,T)=>Syntax.const mark$Syntax.const n$term_of_type T) flds; + val flds'' = foldr1 (fn (x,y) => Syntax.const sep$x$y) flds'; + + in if not (!print_record_type_as_fields) orelse null flds then raise Match + else if moreT = HOLogic.unitT + then Syntax.const record$flds'' + else Syntax.const record_scheme$flds''$term_of_type moreT + end + + +fun gen_record_type_tr' name = + let val name_sfx = suffix ext_typeN name; + fun tr' sg ts = record_type_tr' "_field_types" "_field_type" + "_record_type" "_record_type_scheme" sg + (list_comb (Syntax.const name_sfx,ts)) + in (name_sfx,tr') + end + + +fun gen_record_type_abbr_tr' abbr alphas zeta lastExt schemeT name = + let val name_sfx = suffix ext_typeN name; + val default_tr' = record_type_tr' "_field_types" "_field_type" + "_record_type" "_record_type_scheme" + fun tr' sg ts = record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT sg + (list_comb (Syntax.const name_sfx,ts)) + in (name_sfx, tr') end; + (** record simprocs **) - fun quick_and_dirty_prove sg xs asms prop tac = Tactic.prove sg xs asms prop - (if ! quick_and_dirty then (K (SkipProof.cheat_tac HOL.thy)) else tac); + (if !quick_and_dirty then (K (SkipProof.cheat_tac HOL.thy)) else tac); fun prove_split_simp sg T prop = - (case last_fieldT T of - Some (name,_) => (case get_splits sg name of - Some (all_thm,_,_,_) - => let val {sel_upd={simpset,...},...} = RecordsData.get_sg sg; - in (quick_and_dirty_prove sg [] [] prop - (K (simp_tac (simpset addsimps [all_thm]) 1))) - end - | _ => error "RecordPackage.prove_split_simp: code should never been reached") - | _ => error "RecordPackage.prove_split_simp: code should never been reached") - + (case get_splits sg (rec_id T) of + Some (all_thm,_,_,_) + => let val {sel_upd={simpset,...},...} = RecordsData.get_sg sg; + in (quick_and_dirty_prove sg [] [] prop + (K (simp_tac (simpset addsimps [all_thm]) 1))) + end + | _ => error "RecordPackage.prove_split_simp:code should never been reached") (* record_simproc *) (* Simplifies selections of an record update: @@ -682,8 +751,10 @@ (case get_updates sg u of Some u_name => let fun mk_abs_var x t = (x, fastype_of t); - val {sel_upd={updates,...},...} = RecordsData.get_sg sg; - + val {sel_upd={updates,...},extfields,...} = RecordsData.get_sg sg; + fun flds T = + foldl (fn (xs,(eN,_))=>xs@(map fst (Symtab.lookup_multi (extfields,eN)))) + ([],(dest_recTs T)); fun mk_eq_terms ((upd as Const (u,Type(_,[updT,_]))) $ k $ r) = (case (Symtab.lookup (updates,u)) of None => None @@ -695,8 +766,8 @@ val kv = mk_abs_var "k" k val kb = Bound 1 in Some (upd$kb$rb,kb,[kv,rv],true) end - else if u_name mem (map fst (dest_fieldTs rangeS)) - orelse s mem (map fst (dest_fieldTs updT)) + else if u_name mem (flds rangeS) + orelse s mem (flds updT) then None else (case mk_eq_terms r of Some (trm,trm',vars,update_s) @@ -735,7 +806,7 @@ * the record first and do simplification on that (record_split_simp_tac). * e.g. r(|lots of updates|) = x * - * record_eq_simproc record_split_simp_tac + * record_eq_simproc record_split_simp_tac * Complexity: #components * #updates #updates * *) @@ -743,9 +814,9 @@ Simplifier.simproc (Theory.sign_of HOL.thy) "record_eq_simp" ["r = s"] (fn sg => fn _ => fn t => (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ => - (case last_fieldT T of - None => None - | Some (name, _) => (case get_equalities sg name of + (case rec_id T of + "" => None + | name => (case get_equalities sg name of None => None | Some thm => Some (thm RS Eq_TrueI))) | _ => None)); @@ -790,7 +861,8 @@ in (case mk_updterm updates Symtab.empty t of Some (trm,trm',vars) - => Some (prove_split_simp sg T (list_all(vars,(Logic.mk_equals (trm,trm'))))) + => Some (prove_split_simp sg T + (list_all(vars,(Logic.mk_equals (trm,trm'))))) | None => None) end | _ => None)); @@ -804,9 +876,9 @@ (fn sg => fn _ => fn t => (case t of (Const (quantifier, Type (_, [Type (_, [T, _]), _])))$trm => if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex" - then (case last_fieldT T of - None => None - | Some (name, _) + then (case rec_id T of + "" => None + | name => if P t then (case get_splits sg name of None => None @@ -821,7 +893,7 @@ | _ => None)) (* record_ex_sel_eq_simproc *) -(* record: (EX r. x = sel r) resp. (EX r. sel r = x) to True *) +(* simplifies: (EX s. x = sel s) resp. (EX s. sel s = x) to True *) val record_ex_sel_eq_simproc = Simplifier.simproc (Theory.sign_of HOL.thy) "record_ex_sel_eq_simproc" ["Ex t"] (fn sg => fn _ => fn t => @@ -830,24 +902,24 @@ addsimprocs [record_split_simproc (K true)]) 1))); in (case t of - (Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$(Const (sel,Tsel)$Bound 0)$X)) => + (Const ("Ex",Tex)$Abs(s,T,Const ("op =",Teq)$(Const (sel,Tsel)$Bound 0)$X)) => (case get_selectors sg sel of Some () => let val X' = ("x",range_type Tsel); val prop = list_all ([X'], Logic.mk_equals - (Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$ + (Const ("Ex",Tex)$Abs(s,T,Const ("op =",Teq)$ (Const (sel,Tsel)$Bound 0)$Bound 1), Const ("True",HOLogic.boolT))); in Some (prove prop) end | None => None) - |(Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$X$(Const (sel,Tsel)$Bound 0))) => + |(Const ("Ex",Tex)$Abs(s,T,Const ("op =",Teq)$X$(Const (sel,Tsel)$Bound 0))) => (case get_selectors sg sel of Some () => let val X' = ("x",range_type Tsel); val prop = list_all ([X'], Logic.mk_equals - (Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$ + (Const ("Ex",Tex)$Abs(s,T,Const ("op =",Teq)$ Bound 1$(Const (sel,Tsel)$Bound 0)), Const ("True",HOLogic.boolT))); in Some (prove prop) end @@ -855,28 +927,8 @@ | _ => None) end) -(** record field splitting **) -(* tactic *) - -fun is_fieldT fields (Type (a, [_, _])) = is_some (Symtab.lookup (fields, a)) - | is_fieldT _ _ = false; - -fun record_split_tac i st = - let - val {field_splits = {fields, simpset}, ...} = RecordsData.get_sg (Thm.sign_of_thm st); - - val has_field = exists_Const - (fn (s, Type (_, [Type (_, [T, _]), _])) => - (s = "all" orelse s = "All") andalso is_fieldT fields T - | _ => false); - - val goal = Library.nth_elem (i - 1, Thm.prems_of st); - in - if has_field goal then Simplifier.full_simp_tac simpset i st - else Seq.empty - end handle Library.LIST _ => Seq.empty; - + local val inductive_atomize = thms "induct_atomize"; @@ -891,16 +943,16 @@ fun record_split_simp_tac P i st = let val sg = Thm.sign_of_thm st; - val {sel_upd={simpset,...},field_splits={fields,...},...} + val {sel_upd={simpset,...},...} = RecordsData.get_sg sg; - val has_field = exists_Const + val has_rec = exists_Const (fn (s, Type (_, [Type (_, [T, _]), _])) => - (s = "all" orelse s = "All" orelse s = "Ex") andalso is_fieldT fields T + (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T | _ => false); val goal = Library.nth_elem (i - 1, Thm.prems_of st); - val frees = filter (is_fieldT fields o type_of) (term_frees goal); + val frees = filter (is_recT o type_of) (term_frees goal); fun mk_split_free_tac free induct_thm i = let val cfree = cterm_of sg free; @@ -913,504 +965,55 @@ end; fun split_free_tac P i (free as Free (n,T)) = - (case last_fieldT T of - None => None - | Some(name,_)=> if P free - then (case get_splits sg name of - None => None - | Some (_,_,_,induct_thm) - => Some (mk_split_free_tac free induct_thm i)) - else None) + (case rec_id T of + "" => None + | name => if P free + then (case get_splits sg name of + None => None + | Some (_,_,_,induct_thm) + => Some (mk_split_free_tac free induct_thm i)) + else None) | split_free_tac _ _ _ = None; val split_frees_tacs = mapfilter (split_free_tac P i) frees; - val simprocs = if has_field goal then [record_split_simproc P] else []; + val simprocs = if has_rec goal then [record_split_simproc P] else []; in st |> (EVERY split_frees_tacs) THEN (Simplifier.full_simp_tac (simpset addsimprocs simprocs) i) end handle Library.LIST _ => Seq.empty; end; + +(* record_split_tac *) +(* splits all records in the goal, which are quantified by ! or !!. *) +fun record_split_tac i st = + let + val sg = Thm.sign_of_thm st; + + val has_rec = exists_Const + (fn (s, Type (_, [Type (_, [T, _]), _])) => + (s = "all" orelse s = "All") andalso is_recT T + | _ => false); + + val goal = Library.nth_elem (i - 1, Thm.prems_of st); + + fun is_all t = + (case t of (Const (quantifier, _)$_) => + quantifier = "All" orelse quantifier = "all" + | _ => false); + + in if has_rec goal + then Simplifier.full_simp_tac + (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i st + else Seq.empty + end handle Library.LIST _ => Seq.empty; + (* wrapper *) val record_split_name = "record_split_tac"; val record_split_wrapper = (record_split_name, fn tac => record_split_tac ORELSE' tac); - -(* method *) - -val record_split_method = - ("record_split", Method.no_args (Method.SIMPLE_METHOD' HEADGOAL record_split_tac), - "split record fields"); - - - -(** internal theory extenders **) - -(* field_typedefs *) - -fun field_typedefs zeta moreT names theory = - let - val alpha = "'a"; - val aT = TFree (alpha, HOLogic.typeS); - val UNIV = HOLogic.mk_UNIV (HOLogic.mk_prodT (aT, moreT)); - - fun type_def (thy, name) = - let val (thy', {type_definition, set_def = Some def, ...}) = - thy |> setmp TypedefPackage.quiet_mode true - (TypedefPackage.add_typedef_i true None - (suffix field_typeN (Sign.base_name name), [alpha, zeta], Syntax.NoSyn) UNIV None - (Tactic.rtac UNIV_witness 1)) - in (thy', Tactic.rewrite_rule [def] type_definition) end - in foldl_map type_def (theory, names) end; - - -(* field_definitions *) - -fun field_definitions fields names alphas zeta moreT more vars thy = - let - val sign = Theory.sign_of thy; - val base = Sign.base_name; - - val xT = TFree (variant alphas "'x", HOLogic.typeS); - - - (* prepare declarations and definitions *) - - (*field constructors*) - val field_decls = map (mk_fieldC moreT) fields; - - fun mk_field_spec ((c, T), v) = - Term.head_of (mk_field ((c, v), more)) :== - lambda v (lambda more (mk_Abs moreT (c, T) $ (HOLogic.mk_prod (v, more)))); - val field_specs = map mk_field_spec (fields ~~ vars); - - (*field destructors*) - val dest_decls = map (mk_fstC moreT) fields @ map (mk_sndC moreT) fields; - - fun mk_dest_spec dest sel (c, T) = - let val p = Free ("p", mk_fieldT ((c, T), moreT)); - in Term.head_of (dest p) :== lambda p (sel (mk_Rep moreT (c, T) $ p)) end; - val dest_specs1 = map (mk_dest_spec mk_fst HOLogic.mk_fst) fields; - val dest_specs2 = map (mk_dest_spec mk_snd HOLogic.mk_snd) fields; - - - (* 1st stage: defs_thy *) - - val (defs_thy, (((typedefs, field_defs), dest_defs1), dest_defs2)) = - thy - |> field_typedefs zeta moreT names - |>> (Theory.add_consts_i o map (Syntax.no_syn o apfst base)) (field_decls @ dest_decls) - |>>> (PureThy.add_defs_i false o map Thm.no_attributes) field_specs - |>>> (PureThy.add_defs_i false o map Thm.no_attributes) dest_specs1 - |>>> (PureThy.add_defs_i false o map Thm.no_attributes) dest_specs2; - - val prod_types = map (fn (((a, b), c), d) => product_type_intro OF [a, b, c, d]) - (typedefs ~~ field_defs ~~ dest_defs1 ~~ dest_defs2); - - - (* 2nd stage: thms_thy *) - - fun make ren th = map (fn (prod_type, field) => Drule.standard - (Drule.rename_bvars (ren ~~ [base (fst field), moreN] handle LIST _ => []) - (th OF [prod_type]))) (prod_types ~~ fields); - - val dest_convs = make [] product_type_conv1 @ make [] product_type_conv2; - val field_injects = make [] product_type_inject; - val field_inducts = make ["x", "y"] product_type_induct; - val field_cases = make ["x", "y"] product_type_cases; - val field_splits = make ["a", "b"] product_type_split_paired_all @ - make ["a", "b"] product_type_split_paired_All; - - val (thms_thy, [field_defs', dest_defs', dest_convs', field_injects', - field_splits', field_inducts', field_cases']) = defs_thy - |> Codegen.assoc_consts_i (flat (map (fn (s, _) => - [(suffix fieldN s, None, prod_code), - (suffix fstN s, None, fst_code), - (suffix sndN s, None, snd_code)]) fields)) - |> Codegen.assoc_types (map (fn (s, _) => - (suffix field_typeN s, prodT_code)) fields) - |> (PureThy.add_thmss o map Thm.no_attributes) - [("field_defs", field_defs), - ("dest_defs", dest_defs1 @ dest_defs2), - ("dest_convs", dest_convs), - ("field_injects", field_injects), - ("field_splits", field_splits), - ("field_inducts", field_inducts), - ("field_cases", field_cases)]; - - in (thms_thy, dest_convs', field_injects', field_splits', field_inducts', field_cases') end; - - -(* record_definition *) - -fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy = - let - val sign = Theory.sign_of thy; - - val alphas = map fst args; - val name = Sign.full_name sign bname; - val full = Sign.full_name_path sign bname; - val base = Sign.base_name; - - val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields); - - - (* basic components *) - - val ancestry = map (length o flat o map #fields) (Library.prefixes1 parents); - - val parent_fields = flat (map #fields parents); - val parent_names = map fst parent_fields; - val parent_types = map snd parent_fields; - val parent_len = length parent_fields; - val parent_xs = variantlist (map (base o fst) parent_fields, [moreN, rN]); - val parent_vars = ListPair.map Free (parent_xs, parent_types); - val parent_named_vars = parent_names ~~ parent_vars; - - val fields = map (apfst full) bfields; - val names = map fst fields; - val types = map snd fields; - val len = length fields; - val xs = variantlist (map fst bfields, moreN :: rN :: parent_xs); - val vars = ListPair.map Free (xs, types); - val named_vars = names ~~ vars; - - val all_fields = parent_fields @ fields; - val all_names = parent_names @ names; - val all_types = parent_types @ types; - val all_len = parent_len + len; - val all_xs = parent_xs @ xs; - val all_vars = parent_vars @ vars; - val all_named_vars = parent_named_vars @ named_vars; - - val zeta = variant alphas "'z"; - val moreT = TFree (zeta, HOLogic.typeS); - val more = Free (moreN, moreT); - val full_moreN = full moreN; - fun more_part t = mk_more t full_moreN; - fun more_part_update t x = mk_more_update t (full_moreN, x); - val all_types_more = all_types @ [moreT]; - val all_xs_more = all_xs @ [moreN]; - - val parent_more = funpow parent_len mk_snd; - val idxs = 0 upto (len - 1); - - val fieldsT = mk_recordT (fields, HOLogic.unitT); - fun rec_schemeT n = mk_recordT (prune n all_fields, moreT); - fun rec_scheme n = mk_record (prune n all_named_vars, more); - fun recT n = mk_recordT (prune n all_fields, HOLogic.unitT); - fun rec_ n = mk_record (prune n all_named_vars, HOLogic.unit); - fun r_scheme n = Free (rN, rec_schemeT n); - fun r n = Free (rN, recT n); - - - - (* prepare print translation functions *) - val field_tr's = - print_translation (distinct (flat (map NameSpace.accesses' (full_moreN :: names)))); - - val field_type_tr's = - let val fldnames = if parent_len = 0 then (tl names) else names; - in print_translation_field_types (distinct (flat (map NameSpace.accesses' fldnames))) - end; - - fun record_type_abbr_tr's thy = - let val trnames = NameSpace.accesses' (hd all_names) - val sg = Theory.sign_of thy - in map (gen_record_type_abbr_tr' - sg bname alphas zeta (hd (rev names)) (rec_schemeT 0)) trnames end; - - (* prepare declarations *) - - val sel_decls = map (mk_selC (rec_schemeT 0)) bfields @ - [mk_moreC (rec_schemeT 0) (moreN, moreT)]; - val update_decls = map (mk_updateC (rec_schemeT 0)) bfields @ - [mk_more_updateC (rec_schemeT 0) (moreN, moreT)]; - val make_decl = (makeN, all_types ---> recT 0); - val fields_decl = (fieldsN, types ---> fieldsT); - val extend_decl = (extendN, recT 0 --> moreT --> rec_schemeT 0); - val truncate_decl = (truncateN, rec_schemeT 0 --> recT 0); - - - (* prepare definitions *) - - (*record (scheme) type abbreviation*) - val recordT_specs = - [(suffix schemeN bname, alphas @ [zeta], rec_schemeT 0, Syntax.NoSyn), - (bname, alphas, recT 0, Syntax.NoSyn)]; - - (*selectors*) - fun mk_sel_spec (i, c) = - mk_sel (r_scheme 0) c :== mk_fst (funpow i mk_snd (parent_more (r_scheme 0))); - val sel_specs = - ListPair.map mk_sel_spec (idxs, names) @ - [more_part (r_scheme 0) :== funpow len mk_snd (parent_more (r_scheme 0))]; - - (*updates*) - val all_sels = mk_named_sels all_names (r_scheme 0); - fun mk_upd_spec (i, (c, x)) = - mk_update (r_scheme 0) (c, x) :== - mk_record (nth_update (c, x) (parent_len + i, all_sels), more_part (r_scheme 0)) - val update_specs = - ListPair.map mk_upd_spec (idxs, named_vars) @ - [more_part_update (r_scheme 0) more :== mk_record (all_sels, more)]; - - (*derived operations*) - val make_spec = Const (full makeN, all_types ---> recT 0) $$ all_vars :== - mk_record (all_named_vars, HOLogic.unit); - val fields_spec = Const (full fieldsN, types ---> fieldsT) $$ vars :== - mk_record (named_vars, HOLogic.unit); - val extend_spec = Const (full extendN, recT 0 --> moreT --> rec_schemeT 0) $ r 0 $ more :== - mk_record (mk_named_sels all_names (r 0), more); - val truncate_spec = Const (full truncateN, rec_schemeT 0 --> recT 0) $ r_scheme 0 :== - mk_record (all_sels, HOLogic.unit); - - - (* prepare propositions *) - - (*selectors*) - val sel_props = - map (fn (c, x) => mk_sel (rec_scheme 0) c === x) named_vars @ - [more_part (rec_scheme 0) === more]; - - (*updates*) - fun mk_upd_prop (i, (c, T)) = - let val x' = Free (variant all_xs (base c ^ "'"), T) in - mk_update (rec_scheme 0) (c, x') === - mk_record (nth_update (c, x') (parent_len + i, all_named_vars), more) - end; - val update_props = - ListPair.map mk_upd_prop (idxs, fields) @ - let val more' = Free (variant all_xs (moreN ^ "'"), moreT) - in [more_part_update (rec_scheme 0) more' === mk_record (all_named_vars, more')] end; - - (*equality*) - fun mk_sel_eq (t, T) = - let val t' = Term.abstract_over (r_scheme 0, t) - in Trueprop (HOLogic.eq_const T $ Term.incr_boundvars 1 t' $ t') end; - val sel_eqs = map2 mk_sel_eq - (map (mk_sel (r_scheme 0)) all_names @ [more_part (r_scheme 0)], all_types @ [moreT]); - val equality_prop = - Term.all (rec_schemeT 0) $ (Abs ("r", rec_schemeT 0, - Term.all (rec_schemeT 0) $ (Abs ("r'", rec_schemeT 0, - Logic.list_implies (sel_eqs, - Trueprop (HOLogic.eq_const (rec_schemeT 0) $ Bound 1 $ Bound 0)))))); - - (*induct*) - fun induct_scheme_prop n = - let val P = Free ("P", rec_schemeT n --> HOLogic.boolT) in - (All (prune n all_xs_more ~~ prune n all_types_more) - (Trueprop (P $ rec_scheme n)), Trueprop (P $ r_scheme n)) - end; - fun induct_prop n = - let val P = Free ("P", recT n --> HOLogic.boolT) in - (All (prune n all_xs ~~ prune n all_types) (Trueprop (P $ rec_ n)), Trueprop (P $ r n)) - end; - - (*cases*) - val C = Trueprop (Free (variant all_xs_more "C", HOLogic.boolT)); - fun cases_scheme_prop n = - All (prune n all_xs_more ~~ prune n all_types_more) - ((r_scheme n === rec_scheme n) ==> C) ==> C; - fun cases_prop n = All (prune n all_xs ~~ prune n all_types) ((r n === rec_ n) ==> C) ==> C; - - (*split*) - fun split_scheme_meta_prop n = - let val P = Free ("P", rec_schemeT n --> Term.propT) in - equals (Term.propT) $ - (Term.list_all_free ([(rN,rec_schemeT n)],(P $ r_scheme n)))$ - (All (prune n all_xs_more ~~ prune n all_types_more) (P $ rec_scheme n)) - end; - - fun split_scheme_object_prop n = - let val P = Free ("P", rec_schemeT n --> HOLogic.boolT) - val ALL = foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) - in - Trueprop ( - HOLogic.eq_const (HOLogic.boolT) $ - (HOLogic.mk_all ((rN,rec_schemeT n,P $ r_scheme n)))$ - (ALL (prune n all_xs_more ~~ prune n all_types_more,P $ rec_scheme n))) - end; - - fun split_scheme_object_ex_prop n = - let val P = Free ("P", rec_schemeT n --> HOLogic.boolT) - val EX = foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) - in - Trueprop ( - HOLogic.eq_const (HOLogic.boolT) $ - (HOLogic.mk_exists ((rN,rec_schemeT n,P $ r_scheme n)))$ - (EX (prune n all_xs_more ~~ prune n all_types_more,P $ rec_scheme n))) - end; - (* 1st stage: fields_thy *) - - val (fields_thy, field_simps, field_injects, field_splits, field_inducts, field_cases) = - thy - |> Theory.add_path bname - |> field_definitions fields names alphas zeta moreT more vars; - - val all_field_inducts = flat (map #field_inducts parents) @ field_inducts; - val all_field_cases = flat (map #field_cases parents) @ field_cases; - val all_field_splits = flat (map #field_splits parents) @ field_splits - - - (* 2nd stage: defs_thy *) - - - - - val (defs_thy, (((sel_defs, update_defs), derived_defs))) = - fields_thy - |> Theory.add_trfuns - ([],[],record_type_abbr_tr's fields_thy @ field_type_tr's @ field_tr's, []) - |> add_field_splits (map (suffix field_typeN) names) field_splits - |> Theory.parent_path - |> Theory.add_tyabbrs_i recordT_specs - |> Theory.add_path bname - |> Theory.add_consts_i - (map2 (fn ((x, T), mx) => (x, T, mx)) (sel_decls, field_syntax @ [Syntax.NoSyn])) - |> (Theory.add_consts_i o map Syntax.no_syn) - (update_decls @ [make_decl, fields_decl, extend_decl, truncate_decl]) - |> (PureThy.add_defs_i false o map Thm.no_attributes) sel_specs - |>>> (PureThy.add_defs_i false o map Thm.no_attributes) update_specs - |>>> (PureThy.add_defs_i false o map Thm.no_attributes) - [make_spec, fields_spec, extend_spec, truncate_spec] - |>> Theory.hide_consts false [full makeN, full fieldsN, full extendN, full truncateN, - full moreN, full (suffix updateN moreN)]; - - - (* 3rd stage: thms_thy *) - - val prove_standard = Tactic.prove_standard (Theory.sign_of defs_thy); - fun prove_simp simps = - let val tac = simp_all_tac HOL_basic_ss simps - in fn prop => prove_standard [] [] prop (K tac) end; - - val parent_simps = flat (map #simps parents); - val sel_convs = map (prove_simp (parent_simps @ sel_defs @ field_simps)) sel_props; - val update_convs = map (prove_simp (parent_simps @ update_defs @ sel_convs)) update_props; - - fun induct_scheme n = - let val (assm, concl) = induct_scheme_prop n in - prove_standard [] [assm] concl (fn prems => - EVERY (map (fn rule => try_param_tac rN rule 1) (prune n all_field_inducts)) - THEN resolve_tac prems 1) - end; - - fun cases_scheme n = - prove_standard [] [] (cases_scheme_prop n) (fn _ => - EVERY (map (fn rule => try_param_tac rN rule 1) (prune n all_field_cases)) - THEN simp_all_tac HOL_basic_ss []); - - fun split_scheme_meta n = - prove_standard [] [] (split_scheme_meta_prop n) (fn _ => - Simplifier.full_simp_tac (HOL_basic_ss addsimps all_field_splits) 1); - - fun split_scheme_object induct_scheme n = - prove_standard [] [] (split_scheme_object_prop n) (fn _ => - EVERY [rtac iffI 1, - REPEAT (rtac allI 1), etac allE 1, atac 1, - rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]); - - fun split_scheme_object_ex split_scheme_meta n = - prove_standard [] [] (split_scheme_object_ex_prop n) (fn _ => - fast_simp_tac (claset_of HOL.thy, - HOL_basic_ss addsimps [split_scheme_meta]) 1); - - val induct_scheme0 = induct_scheme 0; - val cases_scheme0 = cases_scheme 0; - val split_scheme_meta0 = split_scheme_meta 0; - val split_scheme_object0 = split_scheme_object induct_scheme0 0; - val split_scheme_object_ex0 = split_scheme_object_ex split_scheme_meta0 0; - val more_induct_scheme = map induct_scheme ancestry; - val more_cases_scheme = map cases_scheme ancestry; - - val (thms_thy, (([sel_convs', update_convs', sel_defs', update_defs', _, - [split_scheme_meta',split_scheme_object', - split_scheme_object_ex',split_scheme_free']], - [induct_scheme', cases_scheme']), [more_induct_scheme', more_cases_scheme'])) = - defs_thy - |> (PureThy.add_thmss o map Thm.no_attributes) - [("select_convs", sel_convs), - ("update_convs", update_convs), - ("select_defs", sel_defs), - ("update_defs", update_defs), - ("defs", derived_defs), - ("splits",[split_scheme_meta0,split_scheme_object0, - split_scheme_object_ex0,induct_scheme0])] - |>>> PureThy.add_thms - [(("induct_scheme", induct_scheme0), induct_type_global (suffix schemeN name)), - (("cases_scheme", cases_scheme0), cases_type_global (suffix schemeN name))] - |>>> PureThy.add_thmss - [(("more_induct_scheme", more_induct_scheme), induct_type_global ""), - (("more_cases_scheme", more_cases_scheme), cases_type_global "")]; - - - (* 4th stage: more_thms_thy *) - - val prove_standard = Tactic.prove_standard (Theory.sign_of thms_thy); - - fun induct (n, scheme) = - let val (assm, concl) = induct_prop n in - prove_standard [] [assm] concl (fn prems => - res_inst_tac [(rN, rN)] scheme 1 - THEN try_param_tac "more" unit_induct 1 - THEN resolve_tac prems 1) - end; - - fun cases (n, scheme) = - prove_standard [] [] (cases_prop n) (fn _ => - res_inst_tac [(rN, rN)] scheme 1 - THEN simp_all_tac HOL_basic_ss [unit_all_eq1]); - - val induct0 = induct (0, induct_scheme'); - val cases0 = cases (0, cases_scheme'); - val more_induct = map induct (ancestry ~~ more_induct_scheme'); - val more_cases = map cases (ancestry ~~ more_cases_scheme'); - - val equality = prove_standard [] [] equality_prop (fn _ => - fn st => let val [r, r'] = map #1 (rev (Tactic.innermost_params 1 st)) in - st |> (res_inst_tac [(rN, r)] cases_scheme' 1 - THEN res_inst_tac [(rN, r')] cases_scheme' 1 - THEN simp_all_tac HOL_basic_ss (parent_simps @ sel_convs)) - end); - - val (more_thms_thy, [_, _, equality']) = - thms_thy |> PureThy.add_thms - [(("induct", induct0), induct_type_global name), - (("cases", cases0), cases_type_global name), - (("equality", equality), [ContextRules.intro_bang_global None])] - |>> (#1 oo PureThy.add_thmss) - [(("more_induct", more_induct), induct_type_global ""), - (("more_cases", more_cases), cases_type_global "")]; - - val simps = sel_convs' @ update_convs'; - val iffs = field_injects; - - val more_thms_thy' = - more_thms_thy |> (#1 oo PureThy.add_thmss) - [(("simps", simps), [Simplifier.simp_add_global]), - (("iffs", iffs), [iff_add_global])]; - - - (* 5th stage: final_thy *) - - val final_thy = - more_thms_thy' - |> put_record name (make_record_info args parent fields field_inducts field_cases - field_splits (field_simps @ simps)) - |> put_sel_upd (names @ [full_moreN]) simps - |> add_record_equalities (snd (split_last names)) equality' - |> add_record_splits (snd (split_last names)) - (split_scheme_meta',split_scheme_object', - split_scheme_object_ex',split_scheme_free') - |> Theory.parent_path; - - in (final_thy, {simps = simps, iffs = iffs}) end; - - - (** theory extender interface **) (* prepare arguments *) @@ -1432,15 +1035,581 @@ let val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle TYPE (msg, _, _) => error msg in (Term.add_typ_tfrees (T, env), T) end; +(* attributes *) + +fun case_names_fields x = RuleCases.case_names ["fields"] x; +fun induct_type_global name = [case_names_fields, InductAttrib.induct_type_global name]; +fun cases_type_global name = [case_names_fields, InductAttrib.cases_type_global name]; + +(* tactics *) + +fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps)); + +(* do case analysis / induction according to rule on last parameter of ith subgoal + * (or on s if there are no parameters); + * Instatiation of record variable (and predicate) in rule is calculated to + * avoid problems with higher order unification. + *) + +fun try_param_tac s rule i st = + let + val cert = cterm_of (Thm.sign_of_thm st); + val g = nth_elem (i - 1, prems_of st); + val params = Logic.strip_params g; + val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g); + val rule' = Thm.lift_rule (st, i) rule; + val (P, ys) = strip_comb (HOLogic.dest_Trueprop + (Logic.strip_assums_concl (prop_of rule'))); + (* ca indicates if rule is a case analysis or induction rule *) + val (x, ca) = (case rev (drop (length params, ys)) of + [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop + (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true) + | [x] => (head_of x, false)); + val rule'' = cterm_instantiate (map (pairself cert) (case (rev params) of + [] => (case assoc (map dest_Free (term_frees (prop_of st)), s) of + None => sys_error "try_param_tac: no such variable" + | Some T => [(P, if ca then concl else lambda (Free (s, T)) concl), + (x, Free (s, T))]) + | (_, T) :: _ => [(P, list_abs (params, if ca then concl + else incr_boundvars 1 (Abs (s, T, concl)))), + (x, list_abs (params, Bound 0))])) rule' + in compose_tac (false, rule'', nprems_of rule) i st end; + +fun extension_typedef name repT alphas thy = + let + val UNIV = HOLogic.mk_UNIV repT; + + val (thy',{set_def=Some def, Abs_induct = abs_induct, + Abs_inject=abs_inject, Abs_inverse = abs_inverse,...}) = + thy |> setmp TypedefPackage.quiet_mode true + (TypedefPackage.add_typedef_i true None + (suffix ext_typeN (Sign.base_name name), alphas, Syntax.NoSyn) UNIV None + (Tactic.rtac UNIV_witness 1)) + val rewrite_rule = Tactic.rewrite_rule [def, rec_UNIV_I, rec_True_simp]; + in (thy',map rewrite_rule [abs_inject, abs_inverse, abs_induct]) + end; + +fun extension_definition full name fields names alphas zeta moreT more vars thy = + let + val base = Sign.base_name; + + val fieldTs = (map snd fields); + val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) (alphas@[zeta]); + val extT_name = suffix ext_typeN name + val extT = Type (extT_name, alphas_zetaTs); + val repT = foldr1 HOLogic.mk_prodT (fieldTs@[moreT]); + val fields_more = fields@[(full moreN,moreT)]; + val bfields_more = map (apfst base) fields_more; + val r = Free (rN,extT) + val len = length fields; + val idxms = 0 upto len; + + (* prepare declarations and definitions *) + + (*fields constructor*) + val ext_decl = (mk_extC (name,extT) (fieldTs@[moreT])); + val ext_spec = Const ext_decl :== + (foldr (uncurry lambda) + (vars@[more],(mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more]))))) + + (*destructors*) + val dest_decls = map (mk_selC extT o (apfst (suffix ext_dest))) bfields_more; + + fun mk_dest_spec (i, (c,T)) = + let val snds = (funpow i HOLogic.mk_snd (mk_Rep name repT extT $ r)) + in Const (mk_selC extT (suffix ext_dest c,T)) + :== (lambda r (if i=len then snds else HOLogic.mk_fst snds)) + end; + val dest_specs = + ListPair.map mk_dest_spec (idxms, fields_more); + + (* code generator data *) + (* Representation as nested pairs is revealed for codegeneration *) + val [rep_code,abs_code] = map (Codegen.parse_mixfix (K (Bound 0))) ["I","I"]; + val ext_type_code = Codegen.parse_mixfix (K dummyT) "_"; + + (* 1st stage: defs_thy *) + val (defs_thy, ([abs_inject, abs_inverse, abs_induct],ext_def::dest_defs)) = + thy + |> extension_typedef name repT (alphas@[zeta]) + |>> Codegen.assoc_consts_i + [(mk_AbsN name,None,abs_code), + (mk_RepN name,None,rep_code)] + |>> Codegen.assoc_types [(extT_name,ext_type_code)] + |>> Theory.add_consts_i (map Syntax.no_syn ((apfst base ext_decl)::dest_decls)) + |>>> PureThy.add_defs_i false (map Thm.no_attributes (ext_spec::dest_specs)) + + + (* prepare propositions *) + + val vars_more = vars@[more]; + val named_vars_more = (names@[full moreN])~~vars_more; + val ext = list_comb (Const ext_decl,vars_more); + val s = Free (rN, extT); + val P = Free (variant (map (fn (Free (x,_))=>x) vars_more) "P", extT-->HOLogic.boolT); + val C = Free (variant (map (fn (Free (x,_))=>x) vars_more) "C", HOLogic.boolT); + + val inject_prop = + let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more; + in All (map dest_Free (vars_more@vars_more')) + ((HOLogic.eq_const extT $ + list_comb (Const ext_decl,vars_more)$list_comb (Const ext_decl,vars_more')) + === + foldr1 HOLogic.mk_conj (map HOLogic.mk_eq (vars_more ~~ vars_more'))) + end; + + val induct_prop = + All (map dest_Free vars_more) (Trueprop (P $ ext)) ==> Trueprop (P $ s); + + val cases_prop = + (All (map dest_Free vars_more) + (Trueprop (HOLogic.mk_eq (s,ext)) ==> Trueprop C)) + ==> Trueprop C; + + (*destructors*) + val dest_conv_props = + map (fn (c, x as Free (_,T)) => mk_sel ext (suffix ext_dest c,T) === x) named_vars_more; + + val prove_standard = Tactic.prove_standard (Theory.sign_of defs_thy); + fun prove_simp simps = + let val tac = simp_all_tac HOL_ss simps + in fn prop => prove_standard [] [] prop (K tac) end; + + (* prove propositions *) + + val inject = (prove_simp [ext_def,abs_inject,Pair_eq] inject_prop); + + val induct = + prove_standard [] [] induct_prop (fn prems => + EVERY [try_param_tac rN abs_induct 1, + asm_full_simp_tac (HOL_ss addsimps [ext_def,split_paired_all]) 1]); + + val cases = + prove_standard [] [] cases_prop (fn prems => + EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1, + try_param_tac rN induct 1, + rtac impI 1, + REPEAT (etac allE 1), + etac mp 1, + rtac refl 1]) + + val dest_convs = map (prove_simp + ([ext_def,abs_inverse]@Pair_sel_convs@dest_defs)) dest_conv_props; + + val (thm_thy,([inject',induct',cases'],[dest_convs'])) = + defs_thy + |> (PureThy.add_thms o map Thm.no_attributes) + [("ext_inject", inject), + ("ext_induct", induct), + ("ext_cases", cases)] + |>>> (PureThy.add_thmss o map Thm.no_attributes) + [("dest_convs",dest_convs)] + + in (thm_thy,extT,induct',inject',dest_convs') + end; + +fun chunks [] [] = [] + | chunks [] xs = [xs] + | chunks (l::ls) xs = take (l,xs)::chunks ls (drop (l,xs)); + +fun chop_last [] = error "last: list should not be empty" + | chop_last [x] = ([],x) + | chop_last (x::xs) = let val (tl,l) = chop_last xs in (x::tl,l) end; + +fun subst_last s [] = error "subst_last: list should not be empty" + | subst_last s ([x]) = [s] + | subst_last s (x::xs) = (x::subst_last s xs); + +(* mk_recordT builds up the record type from the current extension tpye extT and a list + * of parent extensions, starting with the root of the record hierarchy +*) +fun mk_recordT extT parent_exts = + foldr (fn ((parent,Ts),T) => Type (parent, subst_last T Ts)) (parent_exts,extT); + +(* record_definition *) + +fun record_definition (args, bname) parent parents raw_fields thy = + let + val sign = Theory.sign_of thy; + + val alphas = map fst args; + val name = Sign.full_name sign bname; + val full = Sign.full_name_path sign bname; + val base = Sign.base_name; + + val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields); + + val parent_fields = flat (map #fields parents); + val parent_chunks = map (length o #fields) parents; + val parent_names = map fst parent_fields; + val parent_types = map snd parent_fields; + val parent_fields_len = length parent_fields; + val parent_variants = variantlist (map base parent_names, [moreN, rN, rN ^ "'"]); + val parent_vars = ListPair.map Free (parent_variants, parent_types); + val parent_len = length parents; + val parents_idx = (map #name parents) ~~ (0 upto (parent_len - 1)); + + val fields = map (apfst full) bfields; + val names = map fst fields; + val extN = full bname; + val types = map snd fields; + val alphas_fields = foldr add_typ_tfree_names (types,[]); + val alphas_ext = alphas inter alphas_fields; + val len = length fields; + val variants = variantlist (map fst bfields, moreN::rN::rN ^ "'"::parent_variants); + val vars = ListPair.map Free (variants, types); + val named_vars = names ~~ vars; + val idxs = 0 upto (len - 1); + val idxms = 0 upto len; + + val all_fields = parent_fields @ fields; + val all_names = parent_names @ names; + val all_types = parent_types @ types; + val all_len = parent_fields_len + len; + val all_variants = parent_variants @ variants; + val all_vars = parent_vars @ vars; + val all_named_vars = (parent_names ~~ parent_vars) @ named_vars; + + + val zeta = variant alphas "'z"; + val moreT = TFree (zeta, HOLogic.typeS); + val more = Free (moreN, moreT); + val full_moreN = full moreN; + val bfields_more = bfields @ [(moreN,moreT)]; + val fields_more = fields @ [(full_moreN,moreT)]; + val vars_more = vars @ [more]; + val named_vars_more = named_vars @[(full_moreN,more)]; + val all_vars_more = all_vars @ [more]; + val all_named_vars_more = all_named_vars @ [(full_moreN,more)]; + + (* 1st stage: extension_thy *) + + val (extension_thy,extT,ext_induct,ext_inject,ext_dest_convs) = + thy + |> Theory.add_path bname + |> extension_definition full extN fields names alphas_ext zeta moreT more vars; + + + val Type extension_scheme = extT; + val extension_name = unsuffix ext_typeN (fst extension_scheme); + val extension = let val (n,Ts) = extension_scheme in (n,subst_last HOLogic.unitT Ts) end; + val extension_names = + (map ((unsuffix ext_typeN) o fst o #extension) parents) @ [extN]; + val extension_id = foldl (op ^) ("",extension_names); + + + fun rec_schemeT n = mk_recordT extT (map #extension (prune n parents)); + val rec_schemeT0 = rec_schemeT 0; + + fun recT n = + let val (c,Ts) = extension + in mk_recordT (Type (c,subst_last HOLogic.unitT Ts))(map #extension (prune n parents)) + end; + val recT0 = recT 0; + + fun mk_rec args n = + let val (args',more) = chop_last args; + fun mk_ext' (((name,T),args),more) = mk_ext (name,T) (args@[more]); + fun build Ts = + foldr mk_ext' (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args')),more) + in + if more = HOLogic.unit + then build (map recT (0 upto parent_len)) + else build (map rec_schemeT (0 upto parent_len)) + end; + + val r_rec0 = mk_rec all_vars_more 0; + val r_rec_unit0 = mk_rec (all_vars@[HOLogic.unit]) 0; + + fun r n = Free (rN, rec_schemeT n) + val r0 = r 0; + fun r_unit n = Free (rN, recT n) + val r_unit0 = r_unit 0; + + (* prepare print translation functions *) + val field_tr's = + print_translation (distinct (flat (map NameSpace.accesses' (full_moreN :: names)))); + + val adv_ext_tr's = + let + val trnames = NameSpace.accesses' extN; + in map (gen_record_tr') trnames end; + + val adv_record_type_abbr_tr's = + let val trnames = NameSpace.accesses' (hd extension_names); + val lastExt = (unsuffix ext_typeN (fst extension)); + in map (gen_record_type_abbr_tr' bname alphas zeta lastExt rec_schemeT0) trnames + end; + + val adv_record_type_tr's = + let val trnames = if parent_len > 0 then NameSpace.accesses' extN else []; + (* avoid conflict with adv_record_type_abbr_tr's *) + in map (gen_record_type_tr') trnames + end; + + + (* prepare declarations *) + + val sel_decls = map (mk_selC rec_schemeT0) bfields_more; + val upd_decls = map (mk_updC rec_schemeT0) bfields_more; + val make_decl = (makeN, all_types ---> recT0); + val fields_decl = (fields_selN, types ---> Type extension); + val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0); + val truncate_decl = (truncateN, rec_schemeT0 --> recT0); + + (* prepare definitions *) + + fun parent_more s = + if null parents then s + else mk_sel s (NameSpace.append (#name (hd (rev parents))) moreN, extT); + + fun parent_more_upd v s = + if null parents then v + else let val mp = (NameSpace.append (#name (hd (rev parents))) moreN); + in mk_upd mp v s end; + + (*record (scheme) type abbreviation*) + val recordT_specs = + [(suffix schemeN bname, alphas @ [zeta], rec_schemeT0, Syntax.NoSyn), + (bname, alphas, recT0, Syntax.NoSyn)]; + + (*selectors*) + fun mk_sel_spec (c,T) = + Const (mk_selC rec_schemeT0 (c,T)) + :== (lambda r0 (Const (mk_selC extT (suffix ext_dest c,T))$parent_more r0)); + val sel_specs = map mk_sel_spec fields_more; + + (*updates*) + fun mk_upd_spec (c,T) = + let + val args = map (fn (n,nT) => if n=c then Free (base c,T) else (mk_sel r0 (n,nT))) + fields_more; + val new = mk_ext (extN,extT) args; + in Const (mk_updC rec_schemeT0 (c,T)) + :== (lambda (Free (base c,T)) (lambda r0 (parent_more_upd new r0))) + end; + val upd_specs = map mk_upd_spec fields_more; + + (*derived operations*) + val make_spec = Const (full makeN, all_types ---> recT0) $$ all_vars :== + mk_rec (all_vars @ [HOLogic.unit]) 0; + val fields_spec = Const (full fields_selN, types ---> Type extension) $$ vars :== + mk_rec (all_vars @ [HOLogic.unit]) parent_len; + val extend_spec = + Const (full extendN, recT0-->moreT-->rec_schemeT0) $ r_unit0 $ more :== + mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0; + val truncate_spec = Const (full truncateN, rec_schemeT0 --> recT0) $ r0 :== + mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0; + + (* 2st stage: defs_thy *) + + val (defs_thy,((sel_defs,upd_defs),derived_defs)) = + extension_thy + |> Theory.add_trfuns + ([],[],field_tr's, []) + |> Theory.add_advanced_trfuns + ([],[],adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's,[]) + + |> Theory.parent_path + |> Theory.add_tyabbrs_i recordT_specs + |> Theory.add_path bname + |> Theory.add_consts_i + (map2 (fn ((x, T), mx) => (x, T, mx)) (sel_decls, field_syntax @ [Syntax.NoSyn])) + |> (Theory.add_consts_i o map Syntax.no_syn) + (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl]) + |> (PureThy.add_defs_i false o map Thm.no_attributes) sel_specs + |>>> (PureThy.add_defs_i false o map Thm.no_attributes) upd_specs + |>>> (PureThy.add_defs_i false o map Thm.no_attributes) + [make_spec, fields_spec, extend_spec, truncate_spec]; + + + (* prepare propositions *) + val P = Free (variant all_variants "P", rec_schemeT0-->HOLogic.boolT); + val C = Free (variant all_variants "C", HOLogic.boolT); + val P_unit = Free (variant all_variants "P", recT0-->HOLogic.boolT); + + (*selectors*) + val sel_conv_props = + map (fn (c, x as Free (_,T)) => mk_sel r_rec0 (c,T) === x) named_vars_more; + + (*updates*) + fun mk_upd_prop (i,(c,T)) = + let val x' = Free (variant all_variants (base c ^ "'"),T) + val args' = nth_update x' (parent_fields_len + i, all_vars_more) + in mk_upd c x' r_rec0 === mk_rec args' 0 end; + val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more); + + (*induct*) + val induct_scheme_prop = + All (map dest_Free all_vars_more) (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0); + val induct_prop = + (All (map dest_Free all_vars) (Trueprop (P_unit $ r_rec_unit0)), + Trueprop (P_unit $ r_unit0)); + + (*surjective*) + val surjective_prop = + let val args = map (fn (c,Free (_,T)) => mk_sel r0 (c,T)) all_named_vars_more + in r0 === mk_rec args 0 end; + + (*cases*) + val cases_scheme_prop = + (All (map dest_Free all_vars_more) + (Trueprop (HOLogic.mk_eq (r0,r_rec0)) ==> Trueprop C)) + ==> Trueprop C; + + val cases_prop = + (All (map dest_Free all_vars) + (Trueprop (HOLogic.mk_eq (r_unit0,r_rec_unit0)) ==> Trueprop C)) + ==> Trueprop C; + + (*split*) + val split_meta_prop = + let val P = Free (variant all_variants "P", rec_schemeT0-->Term.propT) in + Logic.mk_equals + (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0)) + end; + + val split_object_prop = + let fun ALL vs t = foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) (vs,t) + in (ALL [dest_Free r0] (P $ r0)) === (ALL (map dest_Free all_vars_more) (P $ r_rec0)) + end; + + + val split_ex_prop = + let fun EX vs t = foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) (vs,t) + in (EX [dest_Free r0] (P $ r0)) === (EX (map dest_Free all_vars_more) (P $ r_rec0)) + end; + + (*equality*) + val equality_prop = + let + val s' = Free (rN ^ "'", rec_schemeT0) + fun mk_sel_eq (c,Free (_,T)) = mk_sel r0 (c,T) === mk_sel s' (c,T) + val seleqs = map mk_sel_eq all_named_vars_more + in All (map dest_Free [r0,s']) (Logic.list_implies (seleqs,r0 === s')) end; + + (* 3rd stage: thms_thy *) + + val prove_standard = Tactic.prove_standard (Theory.sign_of defs_thy); + fun prove_simp ss simps = + let val tac = simp_all_tac ss simps + in fn prop => prove_standard [] [] prop (K tac) end; + + val ss = get_simpset (sign_of defs_thy); + val sel_convs = map (prove_simp ss + (sel_defs@ext_dest_convs)) sel_conv_props; + + val upd_convs = map (prove_simp ss (sel_convs@upd_defs)) + upd_conv_props; + + val parent_induct = if null parents then [] else [#induct (hd (rev parents))]; + + val induct_scheme = prove_standard [] [] induct_scheme_prop (fn prems => + (EVERY [if null parent_induct + then all_tac else try_param_tac rN (hd parent_induct) 1, + try_param_tac rN ext_induct 1, + asm_simp_tac HOL_basic_ss 1])); + + val induct = + let val (assm, concl) = induct_prop; + in + prove_standard [] [assm] concl (fn prems => + try_param_tac rN induct_scheme 1 + THEN try_param_tac "more" unit_induct 1 + THEN resolve_tac prems 1) + end; + + val surjective = + prove_standard [] [] surjective_prop (fn prems => + (EVERY [try_param_tac rN induct_scheme 1, + simp_tac (ss addsimps sel_convs) 1])) + + val cases_scheme = + prove_standard [] [] cases_scheme_prop (fn prems => + EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1, + try_param_tac rN induct_scheme 1, + rtac impI 1, + REPEAT (etac allE 1), + etac mp 1, + rtac refl 1]) + + val cases = + prove_standard [] [] cases_prop (fn _ => + try_param_tac rN cases_scheme 1 + THEN simp_all_tac HOL_basic_ss [unit_all_eq1]); + + val split_meta = + prove_standard [] [] split_meta_prop (fn prems => + EVERY [rtac equal_intr_rule 1, + rtac meta_allE 1, etac triv_goal 1, atac 1, + rtac (prop_subst OF [surjective]) 1, + REPEAT (EVERY [rtac meta_allE 1, etac triv_goal 1, etac thin_rl 1]), + atac 1]); + + val split_object = + prove_standard [] [] split_object_prop (fn prems => + EVERY [rtac iffI 1, + REPEAT (rtac allI 1), etac allE 1, atac 1, + rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]); + + val split_ex = + prove_standard [] [] split_ex_prop (fn prems => + fast_simp_tac (claset_of HOL.thy, + HOL_basic_ss addsimps [split_meta]) 1); + + val equality = prove_standard [] [] equality_prop (fn _ => + fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in + st |> (res_inst_tac [(rN, s)] cases_scheme 1 + THEN res_inst_tac [(rN, s')] cases_scheme 1 + THEN simp_all_tac ss (sel_convs)) + end); + + val (thms_thy,(([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'], + derived_defs'], + [surjective',equality']),[induct_scheme',induct',cases_scheme',cases'])) = + defs_thy + |> (PureThy.add_thmss o map Thm.no_attributes) + [("select_convs", sel_convs), + ("update_convs", upd_convs), + ("select_defs", sel_defs), + ("update_defs", upd_defs), + ("splits", [split_meta,split_object,split_ex]), + ("defs", derived_defs)] + |>>> (PureThy.add_thms o map Thm.no_attributes) + [("surjective", surjective), + ("equality", equality)] + |>>> PureThy.add_thms + [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)), + (("induct", induct), induct_type_global name), + (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)), + (("cases", cases), cases_type_global name)]; + + + val sel_upd_simps = sel_convs' @ upd_convs'; + val iffs = [ext_inject] + val final_thy = + thms_thy + |> (#1 oo PureThy.add_thmss) + [(("simps", sel_upd_simps), [Simplifier.simp_add_global]), + (("iffs",iffs), [iff_add_global])] + |> put_record name (make_record_info args parent fields extension induct_scheme') + |> put_sel_upd (names @ [full_moreN]) sel_upd_simps + |> add_record_equalities extension_id equality' + |> add_record_splits extension_id (split_meta',split_object',split_ex',induct_scheme') + |> add_extfields extension_name (fields @ [(full_moreN,moreT)]) + |> add_fieldext (extension_name,snd extension) (names @ [full_moreN]) + |> Theory.parent_path; + + in final_thy + end; (* add_record *) (*we do all preparations and error checks here, deferring the real work to record_definition*) - fun gen_add_record prep_typ prep_raw_parent (params, bname) raw_parent raw_fields thy = let - val _ = Theory.requires thy "Record" "record definitions"; + val _ = Theory.requires thy "Record" "record definitions"; val sign = Theory.sign_of thy; val _ = message ("Defining record " ^ quote bname ^ " ..."); @@ -1479,7 +1648,7 @@ (* errors *) val name = Sign.full_name sign bname; - val err_dup_record = + val err_dup_record = if is_none (get_record thy name) then [] else ["Duplicate definition of record " ^ quote name]; @@ -1513,7 +1682,7 @@ err_dup_record @ err_dup_parms @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields @ err_dup_sorts; in - if null errs then () else error (cat_lines errs); + if null errs then () else error (cat_lines errs) ; thy |> record_definition (args, bname) parent parents bfields end handle ERROR => error ("Failed to define record " ^ quote bname); @@ -1521,19 +1690,15 @@ val add_record = gen_add_record read_typ read_raw_parent; val add_record_i = gen_add_record cert_typ (K I); - -(** package setup **) - (* setup theory *) val setup = [RecordsData.init, Theory.add_trfuns ([], parse_translation, [], []), - Method.add_methods [record_split_method], + Theory.add_advanced_trfuns ([], adv_parse_translation, [], []), Simplifier.change_simpset_of Simplifier.addsimprocs [record_simproc, record_eq_simproc]]; - (* outer syntax *) local structure P = OuterParse and K = OuterSyntax.Keyword in @@ -1543,8 +1708,8 @@ (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const); val recordP = - OuterSyntax.command "record" "define extensible record" K.thy_decl - (record_decl >> (fn (x, (y, z)) => Toplevel.theory (#1 o add_record x y z))); + OuterSyntax.command "record" "define extensible record" K.thy_decl + (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z))); val _ = OuterSyntax.add_parsers [recordP]; diff -r 2c9b463044ec -r 2f885b7e5ba7 src/HOL/ex/Records.thy --- a/src/HOL/ex/Records.thy Sat May 01 22:28:51 2004 +0200 +++ b/src/HOL/ex/Records.thy Mon May 03 23:22:17 2004 +0200 @@ -1,6 +1,7 @@ (* Title: HOL/ex/Records.thy ID: $Id$ - Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen + Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, + TU Muenchen License: GPL (GNU GENERAL PUBLIC LICENSE) *) @@ -19,6 +20,7 @@ following theorems: *} + thm "point.simps" thm "point.iffs" thm "point.defs" @@ -28,10 +30,10 @@ automatically to the standard simpset, @{thm [source] point.iffs} is added to the Classical Reasoner and Simplifier context. - \medskip Record declarations define new type abbreviations: + \medskip Record declarations define new types and type abbreviations: @{text [display] -" point = (| xpos :: nat, ypos :: nat |) - 'a point_scheme = (| xpos :: nat, ypos :: nat, ... :: 'a |)"} +" point = \xpos :: nat, ypos :: nat\ = () point_ext_type + 'a point_scheme = \xpos :: nat, ypos :: nat, ... :: 'a\ = 'a point_ext_type"} *} consts foo1 :: point @@ -107,7 +109,7 @@ induction. *} -lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)" +lemma "r(| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)" proof (cases r) fix xpos ypos more assume "r = (| xpos = xpos, ypos = ypos, ... = more |)" @@ -174,10 +176,12 @@ text {* - The record declaration defines new type constructors: + The record declaration defines a new type constructure and abbreviations: @{text [display] -" cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) - 'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |)"} +" cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) = + () cpoint_ext_type point_ext_type + 'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |) = + 'a cpoint_ext_type point_ext_type"} *} consts foo6 :: cpoint diff -r 2c9b463044ec -r 2f885b7e5ba7 src/HOL/thy_syntax.ML --- a/src/HOL/thy_syntax.ML Sat May 01 22:28:51 2004 +0200 +++ b/src/HOL/thy_syntax.ML Mon May 03 23:22:17 2004 +0200 @@ -277,7 +277,7 @@ val _ = ThySyn.add_syntax ["intrs", "monos", "congs", "simpset", "|", "and", "distinct", "inject", "induct"] [axm_section "typedef" "|> TypedefPackage.add_typedef_x" typedef_decl, - section "record" "|> (#1 oooo RecordPackage.add_record)" record_decl, + section "record" "|> RecordPackage.add_record" record_decl, section "inductive" "" (inductive_decl false), section "coinductive" "" (inductive_decl true), section "datatype" "" datatype_decl, diff -r 2c9b463044ec -r 2f885b7e5ba7 src/Pure/sign.ML --- a/src/Pure/sign.ML Sat May 01 22:28:51 2004 +0200 +++ b/src/Pure/sign.ML Mon May 03 23:22:17 2004 +0200 @@ -61,6 +61,7 @@ val extern: sg -> string -> string -> xstring val cond_extern: sg -> string -> string -> xstring val cond_extern_table: sg -> string -> 'a Symtab.table -> (xstring * 'a) list + val extern_typ: sg -> typ -> typ val intern_class: sg -> xclass -> class val intern_tycon: sg -> xstring -> string val intern_const: sg -> xstring -> string @@ -551,6 +552,9 @@ val cond_extern = cond_extrn o spaces_of; fun cond_extern_table sg = cond_extrn_table (spaces_of sg); + fun extern_typ (sg as Sg (_, {spaces, ...})) T = + if ! NameSpace.long_names then T else extrn_typ spaces T; + val intern_class = intrn_class o spaces_of; val intern_sort = intrn_sort o spaces_of; val intern_typ = intrn_typ o spaces_of; @@ -596,9 +600,8 @@ fun pretty_term sg = pretty_term' (syn_of sg) sg; -fun pretty_typ (sg as Sg (_, {spaces, ...})) T = - Syntax.pretty_typ (syn_of sg) - (if ! NameSpace.long_names then T else extrn_typ spaces T); +fun pretty_typ sg T = + Syntax.pretty_typ (syn_of sg) (extern_typ sg T); fun pretty_sort (sg as Sg (_, {spaces, ...})) S = Syntax.pretty_sort (syn_of sg)