diff -r ea6672bff5dd -r 54fee94b2b29 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Tue Sep 29 18:14:08 2009 +0200 +++ b/src/HOL/Tools/record.ML Tue Sep 29 21:34:59 2009 +0200 @@ -35,8 +35,8 @@ val last_extT: typ -> (string * typ list) option val dest_recTs : typ -> (string * typ list) list - val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ) - val get_recT_fields: theory -> typ -> (string * typ) list * (string * typ) + val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ) + val get_recT_fields: theory -> typ -> (string * typ) list * (string * typ) val get_parent: theory -> string -> (typ list * string) option val get_extension: theory -> string -> (string * typ list) option val get_extinjects: theory -> thm list @@ -54,18 +54,17 @@ signature ISTUPLE_SUPPORT = sig - val add_istuple_type: bstring * string list -> (typ * typ) -> theory -> - (term * term * theory); - - val mk_cons_tuple: term * term -> term; - val dest_cons_tuple: term -> term * term; - - val istuple_intros_tac: theory -> int -> tactic; - - val named_cterm_instantiate: (string * cterm) list -> thm -> thm; + val add_istuple_type: bstring * string list -> (typ * typ) -> theory -> term * term * theory + + val mk_cons_tuple: term * term -> term + val dest_cons_tuple: term -> term * term + + val istuple_intros_tac: theory -> int -> tactic + + val named_cterm_instantiate: (string * cterm) list -> thm -> thm end; -structure IsTupleSupport : ISTUPLE_SUPPORT = +structure IsTupleSupport: ISTUPLE_SUPPORT = struct val isomN = "_TupleIsom"; @@ -85,13 +84,14 @@ val tup_isom_typeN = fst (dest_Type @{typ "('a, 'b, 'c) tuple_isomorphism"}); -fun named_cterm_instantiate values thm = let +fun named_cterm_instantiate values thm = + let fun match name ((name', _), _) = name = name' | match name _ = false; - fun getvar name = case (find_first (match name) - (Term.add_vars (prop_of thm) [])) - of SOME var => cterm_of (theory_of_thm thm) (Var var) - | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm]) + fun getvar name = + (case find_first (match name) (Term.add_vars (prop_of thm) []) of + SOME var => cterm_of (theory_of_thm thm) (Var var) + | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])); in cterm_instantiate (map (apfst getvar) values) thm end; @@ -120,78 +120,82 @@ |-> (fn (name, _) => `(fn thy => get_thms thy name)) end; -fun mk_cons_tuple (left, right) = let +fun mk_cons_tuple (left, right) = + let val (leftT, rightT) = (fastype_of left, fastype_of right); - val prodT = HOLogic.mk_prodT (leftT, rightT); - val isomT = Type (tup_isom_typeN, [prodT, leftT, rightT]); + val prodT = HOLogic.mk_prodT (leftT, rightT); + val isomT = Type (tup_isom_typeN, [prodT, leftT, rightT]); in - Const (istuple_consN, isomT --> leftT --> rightT --> prodT) - $ Const (fst tuple_istuple, isomT) $ left $ right + Const (istuple_consN, isomT --> leftT --> rightT --> prodT) $ + Const (fst tuple_istuple, isomT) $ left $ right end; -fun dest_cons_tuple (v as Const (ic, _) $ Const _ $ left $ right) - = if ic = istuple_consN then (left, right) - else raise TERM ("dest_cons_tuple", [v]) +fun dest_cons_tuple (v as Const (ic, _) $ Const _ $ left $ right) = + if ic = istuple_consN then (left, right) + else raise TERM ("dest_cons_tuple", [v]) | dest_cons_tuple v = raise TERM ("dest_cons_tuple", [v]); fun add_istuple_type (name, alphas) (leftT, rightT) thy = -let - val repT = HOLogic.mk_prodT (leftT, rightT); - - val (([rep_inject, abs_inverse], absC, absT), typ_thy) = - thy - |> do_typedef name repT alphas - ||> Sign.add_path name; - - (* construct a type and body for the isomorphism constant by - instantiating the theorem to which the definition will be applied *) - val intro_inst = rep_inject RS - (named_cterm_instantiate [("abst", cterm_of typ_thy absC)] - istuple_intro); - val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst)); - val isomT = fastype_of body; - val isom_bind = Binding.name (name ^ isomN); - val isom = Const (Sign.full_name typ_thy isom_bind, isomT); - val isom_spec = (name ^ isomN ^ defN, Logic.mk_equals (isom, body)); - - val ([isom_def], cdef_thy) = - typ_thy - |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)] - |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)]; - - val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro)); - val cons = Const (istuple_consN, isomT --> leftT --> rightT --> absT) - - val thm_thy = - cdef_thy - |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop - (constname isom, istuple)) - |> Sign.parent_path; -in - (isom, cons $ isom, thm_thy) -end; - -fun istuple_intros_tac thy = let - val isthms = IsTupleThms.get thy; + let + val repT = HOLogic.mk_prodT (leftT, rightT); + + val (([rep_inject, abs_inverse], absC, absT), typ_thy) = + thy + |> do_typedef name repT alphas + ||> Sign.add_path name; + + (*construct a type and body for the isomorphism constant by + instantiating the theorem to which the definition will be applied*) + val intro_inst = + rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] istuple_intro; + val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst)); + val isomT = fastype_of body; + val isom_bind = Binding.name (name ^ isomN); + val isom = Const (Sign.full_name typ_thy isom_bind, isomT); + val isom_spec = (name ^ isomN ^ defN, Logic.mk_equals (isom, body)); + + val ([isom_def], cdef_thy) = + typ_thy + |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)] + |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)]; + + val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro)); + val cons = Const (istuple_consN, isomT --> leftT --> rightT --> absT); + + val thm_thy = + cdef_thy + |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop (constname isom, istuple)) + |> Sign.parent_path; + in + (isom, cons $ isom, thm_thy) + end; + +fun istuple_intros_tac thy = + let + val isthms = IsTupleThms.get thy; fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]); - val use_istuple_thm_tac = SUBGOAL (fn (goal, n) => let + val use_istuple_thm_tac = SUBGOAL (fn (goal, n) => + let val goal' = Envir.beta_eta_contract goal; - val isom = case goal' of (Const tp $ (Const pr $ Const is)) - => if fst tp = "Trueprop" andalso fst pr = istuple_constN - then Const is - else err "unexpected goal predicate" goal' - | _ => err "unexpected goal format" goal'; - val isthm = case Symtab.lookup isthms (constname isom) of - SOME isthm => isthm - | NONE => err "no thm found for constant" isom; + val isom = + (case goal' of + Const tp $ (Const pr $ Const is) => + if fst tp = "Trueprop" andalso fst pr = istuple_constN + then Const is + else err "unexpected goal predicate" goal' + | _ => err "unexpected goal format" goal'); + val isthm = + (case Symtab.lookup isthms (constname isom) of + SOME isthm => isthm + | NONE => err "no thm found for constant" isom); in rtac isthm n end); in - fn n => resolve_from_net_tac istuple_intros n - THEN use_istuple_thm_tac n + fn n => resolve_from_net_tac istuple_intros n THEN use_istuple_thm_tac n end; end; + structure Record: RECORD = struct @@ -201,7 +205,7 @@ val atomize_imp = thm "HOL.atomize_imp"; val meta_allE = thm "Pure.meta_allE"; val prop_subst = thm "prop_subst"; -val Pair_sel_convs = [fst_conv,snd_conv]; +val Pair_sel_convs = [fst_conv, snd_conv]; val K_record_comp = @{thm "K_record_comp"}; val K_comp_convs = [@{thm o_apply}, K_record_comp] val transitive_thm = thm "transitive"; @@ -234,6 +238,8 @@ val o_eq_id_dest = thm "o_eq_id_dest"; val o_eq_dest_lhs = thm "o_eq_dest_lhs"; + + (** name components **) val rN = "r"; @@ -267,29 +273,29 @@ in map_type_tfree varify end; fun domain_type' T = - domain_type T handle Match => T; + domain_type T handle Match => T; fun range_type' T = - range_type T handle Match => T; - - -(* messages *) + range_type T handle Match => T; + + +(* messages *) (* FIXME proper context *) fun trace_thm str thm = - tracing (str ^ (Pretty.string_of (Display.pretty_thm_without_context thm))); + tracing (str ^ Pretty.string_of (Display.pretty_thm_without_context thm)); fun trace_thms str thms = - (tracing str; map (trace_thm "") thms); + (tracing str; map (trace_thm "") thms); fun trace_term str t = - tracing (str ^ Syntax.string_of_term_global Pure.thy t); + tracing (str ^ Syntax.string_of_term_global Pure.thy t); (* timing *) val timing = Unsynchronized.ref false; -fun timeit_msg s x = if !timing then (warning s; timeit x) else x (); -fun timing_msg s = if !timing then warning s else (); +fun timeit_msg s x = if ! timing then (warning s; timeit x) else x (); +fun timing_msg s = if ! timing then warning s else (); (* syntax *) @@ -315,54 +321,54 @@ fun mk_RepN name = suffix ext_typeN (prefix_base RepN name); fun mk_AbsN name = suffix ext_typeN (prefix_base AbsN name); -fun mk_Rep name repT absT = - Const (suffix ext_typeN (prefix_base RepN name),absT --> repT); +fun mk_Rep name repT absT = + Const (suffix ext_typeN (prefix_base RepN name), absT --> repT); fun mk_Abs name repT absT = - Const (mk_AbsN name,repT --> absT); + Const (mk_AbsN name, repT --> absT); (* constructor *) -fun mk_extC (name,T) Ts = (suffix extN name, Ts ---> T); - -fun mk_ext (name,T) ts = +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; + in list_comb (Const (mk_extC (name, T) Ts), ts) end; (* cases *) -fun mk_casesC (name,T,vT) Ts = (suffix casesN name, (Ts ---> vT) --> T --> vT) - -fun mk_cases (name,T,vT) f = +fun mk_casesC (name, T, vT) Ts = (suffix casesN name, (Ts ---> vT) --> T --> vT); + +fun mk_cases (name, T, vT) f = let val Ts = binder_types (fastype_of f) - in Const (mk_casesC (name,T,vT) Ts) $ f end; + in Const (mk_casesC (name, T, vT) Ts) $ f end; (* selector *) -fun mk_selC sT (c,T) = (c,sT --> T); - -fun mk_sel s (c,T) = +fun mk_selC sT (c, T) = (c, sT --> T); + +fun mk_sel s (c, T) = let val sT = fastype_of s - in Const (mk_selC sT (c,T)) $ s end; + in Const (mk_selC sT (c, T)) $ s end; (* updates *) -fun mk_updC sfx sT (c,T) = (suffix sfx c, (T --> T) --> sT --> sT); +fun mk_updC sfx sT (c, T) = (suffix sfx c, (T --> T) --> sT --> sT); fun mk_upd' sfx c v sT = let val vT = domain_type (fastype_of v); - in Const (mk_updC sfx sT (c, vT)) $ v end; - -fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s + in Const (mk_updC sfx sT (c, vT)) $ v end; + +fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s; (* types *) -fun dest_recT (typ as Type (c_ext_type, Ts as (T::_))) = +fun dest_recT (typ as Type (c_ext_type, Ts as (T :: _))) = (case try (unsuffix ext_typeN) c_ext_type of NONE => raise TYPE ("Record.dest_recT", [typ], []) | SOME c => ((c, Ts), List.last Ts)) @@ -377,16 +383,17 @@ end handle TYPE _ => []; 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 + 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 rec_id i T = - let val rTs = dest_recTs T - val rTs' = if i < 0 then rTs else Library.take (i,rTs) - in Library.foldl (fn (s,(c,T)) => s ^ c) ("",rTs') end; + let + val rTs = dest_recTs T; + val rTs' = if i < 0 then rTs else Library.take (i, rTs); + in Library.foldl (fn (s, (c, T)) => s ^ c) ("", rTs') end; (* FIXME ? *) @@ -394,7 +401,7 @@ (** record info **) -(* type record_info and parent_info *) +(* type record_info and parent_info *) type record_info = {args: (string * sort) list, @@ -402,8 +409,7 @@ fields: (string * typ) list, extension: (string * typ list), induct: thm, - extdef: thm - }; + extdef: thm}; fun make_record_info args parent fields extension induct extdef = {args = args, parent = parent, fields = fields, extension = extension, @@ -415,8 +421,7 @@ fields: (string * typ) list, extension: (string * typ list), induct: thm, - extdef: thm -}; + extdef: thm}; fun make_parent_info name fields extension induct extdef = {name = name, fields = fields, extension = extension, @@ -436,14 +441,13 @@ unfoldcong: Simplifier.simpset}, equalities: thm Symtab.table, extinjects: thm list, - extsplit: thm Symtab.table, (* maps extension name to split 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 *) -}; + extsplit: thm Symtab.table, (* maps extension name to split 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 equalities extinjects extsplit splits extfields fieldext = + records sel_upd equalities extinjects extsplit splits extfields fieldext = {records = records, sel_upd = sel_upd, equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits, extfields = extfields, fieldext = fieldext }: record_data; @@ -462,9 +466,10 @@ val extend = I; fun merge _ ({records = recs1, - sel_upd = {selectors = sels1, updates = upds1, - simpset = ss1, defset = ds1, - foldcong = fc1, unfoldcong = uc1}, + sel_upd = + {selectors = sels1, updates = upds1, + simpset = ss1, defset = ds1, + foldcong = fc1, unfoldcong = uc1}, equalities = equalities1, extinjects = extinjects1, extsplit = extsplit1, @@ -472,9 +477,10 @@ extfields = extfields1, fieldext = fieldext1}, {records = recs2, - sel_upd = {selectors = sels2, updates = upds2, - simpset = ss2, defset = ds2, - foldcong = fc2, unfoldcong = uc2}, + sel_upd = + {selectors = sels2, updates = upds2, + simpset = ss2, defset = ds2, + foldcong = fc2, unfoldcong = uc2}, equalities = equalities2, extinjects = extinjects2, extsplit = extsplit2, @@ -491,13 +497,12 @@ unfoldcong = Simplifier.merge_ss (uc1, uc2)} (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2)) (Library.merge Thm.eq_thm_prop (extinjects1, extinjects2)) - (Symtab.merge Thm.eq_thm_prop (extsplit1,extsplit2)) - (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)) - (Symtab.merge (K true) (extfields1,extfields2)) - (Symtab.merge (K true) (fieldext1,fieldext2)); + (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2)) + (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)) + (Symtab.merge (K true) (extfields1, extfields2)) + (Symtab.merge (K true) (fieldext1, fieldext2)); ); fun print_records thy = @@ -526,8 +531,8 @@ fun put_record name info thy = let - val {records, sel_upd, equalities, extinjects,extsplit,splits,extfields,fieldext} = - RecordsData.get thy; + val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = + RecordsData.get thy; val data = make_record_data (Symtab.update (name, info) records) sel_upd equalities extinjects extsplit splits extfields fieldext; in RecordsData.put data thy end; @@ -547,24 +552,23 @@ val get_foldcong_ss = get_ss_with_context (#foldcong); val get_unfoldcong_ss = get_ss_with_context (#unfoldcong); -fun get_update_details u thy = let - val sel_upd = get_sel_upd thy; - in case (Symtab.lookup (#updates sel_upd) u) of - SOME s => let - val SOME (dep, ismore) = Symtab.lookup (#selectors sel_upd) s; - in SOME (s, dep, ismore) end - | NONE => NONE end; +fun get_update_details u thy = + let val sel_upd = get_sel_upd thy in + (case Symtab.lookup (#updates sel_upd) u of + SOME s => + let val SOME (dep, ismore) = Symtab.lookup (#selectors sel_upd) s + in SOME (s, dep, ismore) end + | NONE => NONE) + end; fun put_sel_upd names more depth simps defs (folds, unfolds) thy = let - val all = names @ [more]; + val all = names @ [more]; val sels = map (rpair (depth, false)) names @ [(more, (depth, true))]; val upds = map (suffix updateN) all ~~ all; - val {records, sel_upd = {selectors, updates, simpset, - defset, foldcong, unfoldcong}, - equalities, extinjects, extsplit, splits, extfields, - fieldext} = RecordsData.get thy; + val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong}, + equalities, extinjects, extsplit, splits, extfields, fieldext} = RecordsData.get thy; val data = make_record_data records {selectors = fold Symtab.update_new sels selectors, updates = fold Symtab.update_new upds updates, @@ -575,29 +579,29 @@ equalities extinjects extsplit splits extfields fieldext; in RecordsData.put data thy end; + (* access 'equalities' *) fun add_record_equalities name thm thy = let - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = - RecordsData.get thy; + val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = + RecordsData.get thy; val data = make_record_data records sel_upd - (Symtab.update_new (name, thm) equalities) extinjects extsplit - splits extfields fieldext; + (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext; in RecordsData.put data thy end; -val get_equalities =Symtab.lookup o #equalities o RecordsData.get; +val get_equalities = Symtab.lookup o #equalities o RecordsData.get; (* access 'extinjects' *) fun add_extinjects thm thy = let - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = - RecordsData.get thy; + val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = + RecordsData.get thy; val data = - make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) extsplit - splits extfields fieldext; + make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) + extsplit splits extfields fieldext; in RecordsData.put data thy end; val get_extinjects = rev o #extinjects o RecordsData.get; @@ -607,8 +611,8 @@ fun add_extsplit name thm thy = let - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = - RecordsData.get thy; + val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = + RecordsData.get thy; val data = make_record_data records sel_upd equalities extinjects (Symtab.update_new (name, thm) extsplit) splits extfields fieldext; @@ -621,8 +625,8 @@ fun add_record_splits name thmP thy = let - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = - RecordsData.get thy; + val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = + RecordsData.get thy; val data = make_record_data records sel_upd equalities extinjects extsplit (Symtab.update_new (name, thmP) splits) extfields fieldext; @@ -641,37 +645,39 @@ fun add_extfields name fields thy = let - val {records, sel_upd, equalities, extinjects, extsplit,splits, extfields, fieldext} = - RecordsData.get thy; - val data = make_record_data records sel_upd - equalities extinjects extsplit splits - (Symtab.update_new (name, fields) extfields) fieldext; + val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = + RecordsData.get thy; + val data = + make_record_data records sel_upd + equalities extinjects extsplit splits + (Symtab.update_new (name, fields) extfields) fieldext; in RecordsData.put data thy end; val get_extfields = Symtab.lookup o #extfields o RecordsData.get; fun get_extT_fields thy T = let - val ((name,Ts),moreT) = dest_recT T; - val recname = let val (nm::recn::rst) = rev (Long_Name.explode name) - in Long_Name.implode (rev (nm::rst)) end; - val midx = maxidx_of_typs (moreT::Ts); + val ((name, Ts), moreT) = dest_recT T; + val recname = + let val (nm :: recn :: rst) = rev (Long_Name.explode name) + in Long_Name.implode (rev (nm :: rst)) end; + val midx = maxidx_of_typs (moreT :: Ts); val varifyT = varifyT midx; - val {records,extfields,...} = RecordsData.get thy; - val (flds,(more,_)) = split_last (Symtab.lookup_list extfields name); + val {records, extfields, ...} = RecordsData.get thy; + val (flds, (more, _)) = split_last (Symtab.lookup_list extfields name); val args = map varifyT (snd (#extension (the (Symtab.lookup records recname)))); val subst = fold (Sign.typ_match thy) (but_last args ~~ but_last Ts) (Vartab.empty); val flds' = map (apsnd ((Envir.norm_type subst) o varifyT)) flds; - in (flds',(more,moreT)) end; + in (flds', (more, moreT)) end; fun get_recT_fields thy T = let - val (root_flds,(root_more,root_moreT)) = get_extT_fields thy T; - val (rest_flds,rest_more) = - if is_recT root_moreT then get_recT_fields thy root_moreT - else ([],(root_more,root_moreT)); - in (root_flds@rest_flds,rest_more) end; + val (root_flds, (root_more, root_moreT)) = get_extT_fields thy T; + val (rest_flds, rest_more) = + if is_recT root_moreT then get_recT_fields thy root_moreT + else ([], (root_more, root_moreT)); + in (root_flds @ rest_flds, rest_more) end; (* access 'fieldext' *) @@ -679,14 +685,14 @@ fun add_fieldext extname_types fields thy = let val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = - RecordsData.get thy; + RecordsData.get thy; val fieldext' = fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext; - val data=make_record_data records sel_upd equalities extinjects extsplit - splits extfields fieldext'; + val data = + make_record_data records sel_upd equalities extinjects + extsplit splits extfields fieldext'; in RecordsData.put data thy end; - val get_fieldext = Symtab.lookup o #fieldext o RecordsData.get; @@ -735,7 +741,7 @@ (* parse translations *) fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) = - if c = mark then Syntax.const (suffix sfx name) $ (Abs ("_",dummyT, arg)) + if c = mark then Syntax.const (suffix sfx name) $ Abs ("_", dummyT, arg) else raise TERM ("gen_field_tr: " ^ mark, [t]) | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]); @@ -755,87 +761,88 @@ (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 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 ctxt t = let val thy = ProofContext.theory_of ctxt; val msg = "error in record input: "; + val fieldargs = dest_ext_fields sep mark t; - fun splitargs (field::fields) ((name,arg)::fargs) = + fun splitargs (field :: fields) ((name, arg) :: fargs) = if can (unsuffix name) field - then let val (args,rest) = splitargs fields fargs - in (arg::args,rest) end + then + let val (args, rest) = splitargs fields fargs + in (arg :: args, rest) end else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t]) - | splitargs [] (fargs as (_::_)) = ([],fargs) - | splitargs (_::_) [] = raise TERM (msg ^ "expecting more fields", [t]) - | splitargs _ _ = ([],[]); - - fun mk_ext (fargs as (name,arg)::_) = - (case get_fieldext thy (Sign.intern_const thy name) of - SOME (ext,_) => (case get_extfields thy 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(msg ^ "no fields defined for " - ^ ext,[t])) - | NONE => raise TERM (msg ^ name ^" is no proper field",[t])) - | mk_ext [] = more - + | splitargs [] (fargs as (_ :: _)) = ([], fargs) + | splitargs (_ :: _) [] = raise TERM (msg ^ "expecting more fields", [t]) + | splitargs _ _ = ([], []); + + fun mk_ext (fargs as (name, arg) :: _) = + (case get_fieldext thy (Sign.intern_const thy name) of + SOME (ext, _) => + (case get_extfields thy 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 (msg ^ "no fields defined for " ^ ext, [t])) + | NONE => raise TERM (msg ^ name ^" is no proper field", [t])) + | mk_ext [] = more; in mk_ext fieldargs end; fun gen_ext_type_tr sep mark sfx more ctxt t = let val thy = ProofContext.theory_of ctxt; val msg = "error in record-type input: "; + val fieldargs = dest_ext_fields sep mark t; - fun splitargs (field::fields) ((name,arg)::fargs) = - if can (unsuffix name) field - then let val (args,rest) = splitargs fields fargs - in (arg::args,rest) end + fun splitargs (field :: fields) ((name, arg) :: fargs) = + if can (unsuffix name) field then + let val (args, rest) = splitargs fields fargs + in (arg :: args, rest) end else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t]) - | splitargs [] (fargs as (_::_)) = ([],fargs) - | splitargs (_::_) [] = raise TERM (msg ^ "expecting more fields", [t]) - | splitargs _ _ = ([],[]); - - fun mk_ext (fargs as (name,arg)::_) = - (case get_fieldext thy (Sign.intern_const thy name) of - SOME (ext,alphas) => + | splitargs [] (fargs as (_ :: _)) = ([], fargs) + | splitargs (_ :: _) [] = raise TERM (msg ^ "expecting more fields", [t]) + | splitargs _ _ = ([], []); + + fun mk_ext (fargs as (name, arg) :: _) = + (case get_fieldext thy (Sign.intern_const thy name) of + SOME (ext, alphas) => (case get_extfields thy ext of - SOME flds - => (let - val flds' = but_last flds; - val types = map snd flds'; - val (args,rest) = splitargs (map fst flds') fargs; - val argtypes = map (Sign.certify_typ thy o decode_type thy) args; - val midx = fold (fn T => fn i => Int.max (maxidx_of_typ T, i)) - argtypes 0; - val varifyT = varifyT midx; - val vartypes = map varifyT types; - - val subst = fold (Sign.typ_match thy) (vartypes ~~ argtypes) - Vartab.empty; - val alphas' = map ((Syntax.term_of_typ (! Syntax.show_sorts)) o - Envir.norm_type subst o varifyT) - (but_last alphas); - - val more' = mk_ext rest; - in list_comb (Syntax.const (suffix sfx ext),alphas'@[more']) - end handle TYPE_MATCH => raise - TERM (msg ^ "type is no proper record (extension)", [t])) - | NONE => raise TERM (msg ^ "no fields defined for " ^ ext,[t])) - | NONE => raise TERM (msg ^ name ^" is no proper field",[t])) - | mk_ext [] = more + SOME flds => + (let + val flds' = but_last flds; + val types = map snd flds'; + val (args, rest) = splitargs (map fst flds') fargs; + val argtypes = map (Sign.certify_typ thy o decode_type thy) args; + val midx = fold (fn T => fn i => Int.max (maxidx_of_typ T, i)) argtypes 0; + val varifyT = varifyT midx; + val vartypes = map varifyT types; + + val subst = fold (Sign.typ_match thy) (vartypes ~~ argtypes) Vartab.empty; + val alphas' = + map (Syntax.term_of_typ (! Syntax.show_sorts) o Envir.norm_type subst o varifyT) + (but_last alphas); + + val more' = mk_ext rest; + in + list_comb (Syntax.const (suffix sfx ext), alphas' @ [more']) + end handle TYPE_MATCH => + raise TERM (msg ^ "type is no proper record (extension)", [t])) + | NONE => raise TERM (msg ^ "no fields defined for " ^ ext, [t])) + | NONE => raise TERM (msg ^ name ^" is no proper field", [t])) + | mk_ext [] = more; in mk_ext fieldargs end; @@ -856,25 +863,26 @@ | 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)); + 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; + 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)]; + [("_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 *) @@ -883,27 +891,33 @@ val print_record_type_as_fields = Unsynchronized.ref true; fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ k $ u) = - let val t = (case k of (Abs (_,_,(Abs (_,_,t)$Bound 0))) - => if null (loose_bnos t) then t else raise Match - | Abs (x,_,t) => if null (loose_bnos t) then t else raise Match - | _ => raise Match) - - (* (case k of (Const ("K_record",_)$t) => t - | Abs (x,_,Const ("K_record",_)$t$Bound 0) => t - | _ => raise Match)*) - in - (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)) - end + let + val t = + (case k of + Abs (_, _, Abs (_, _, t) $ Bound 0) => + if null (loose_bnos t) then t else raise Match + | Abs (x, _, t) => + if null (loose_bnos t) then t else raise Match + | _ => raise Match); + + (* FIXME ? *) + (* (case k of (Const ("K_record", _) $ t) => t + | Abs (x, _, Const ("K_record", _) $ t $ Bound 0) => t + | _ => raise Match)*) + in + (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)) + end | gen_field_upds_tr' _ _ tm = ([], tm); fun record_update_tr' tm = let val (ts, u) = gen_field_upds_tr' "_update" updateN tm in if null ts then raise Match - else Syntax.const "_record_update" $ u $ - foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts) + else + Syntax.const "_record_update" $ u $ + foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts) end; fun gen_field_tr' sfx tr' name = @@ -913,95 +927,96 @@ fun record_tr' sep mark record record_scheme unit ctxt t = let val thy = ProofContext.theory_of ctxt; + fun field_lst t = (case strip_comb t of - (Const (ext,_),args as (_::_)) - => (case try (unsuffix extN) (Sign.intern_const thy ext) of - SOME ext' - => (case get_extfields thy ext' of - SOME flds - => (let - val (f::fs) = but_last (map fst flds); - val flds' = Sign.extern_const thy f :: map Long_Name.base_name fs; - val (args',more) = split_last args; - in (flds'~~args')@field_lst more end - handle Library.UnequalLengths => [("",t)]) - | NONE => [("",t)]) - | NONE => [("",t)]) - | _ => [("",t)]) - - val (flds,(_,more)) = split_last (field_lst t); + (Const (ext, _), args as (_ :: _)) => + (case try (unsuffix extN) (Sign.intern_const thy ext) of + SOME ext' => + (case get_extfields thy ext' of + SOME flds => + (let + val f :: fs = but_last (map fst flds); + val flds' = Sign.extern_const thy f :: map Long_Name.base_name fs; + val (args', more) = split_last args; + in (flds' ~~ args') @ field_lst more end + handle Library.UnequalLengths => [("", t)]) + | NONE => [("", t)]) + | NONE => [("", t)]) + | _ => [("", t)]); + + val (flds, (_, more)) = split_last (field_lst t); val _ = if null flds then raise Match else (); - 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 unit more - then Syntax.const record$flds'' - else Syntax.const record_scheme$flds''$more - end + 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 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 (@{const_syntax "Product_Type.Unity"},_) => true | _ => false); - fun tr' ctxt ts = record_tr' "_fields" "_field" "_record" "_record_scheme" unit ctxt - (list_comb (Syntax.const name_sfx,ts)) - in (name_sfx,tr') - end + let + val name_sfx = suffix extN name; + val unit = (fn Const (@{const_syntax "Product_Type.Unity"}, _) => true | _ => false); + fun tr' ctxt ts = + record_tr' "_fields" "_field" "_record" "_record_scheme" unit ctxt + (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. *) +(* record_type_abbr_tr' *) + +(*try to reconstruct the record name type abbreviation from + the (nested) extension types*) fun record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt tm = let - val thy = ProofContext.theory_of ctxt; - (* 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.*) - - (* WORKAROUND: - * If a record type occurs in an error message of type inference there - * may be some internal frees donoted by ??: - * (Const "_tfree",_)$Free ("??'a",_). - - * This will unfortunately be translated to Type ("??'a",[]) instead of - * TFree ("??'a",_) by typ_of_term, which will confuse unify below. - * fixT works around. - *) - fun fixT (T as Type (x,[])) = - if String.isPrefix "??'" x then TFree (x,Sign.defaultS thy) else T - | fixT (Type (x,xs)) = Type (x,map fixT xs) - | fixT T = T; - - val T = fixT (decode_type thy tm); - val midx = maxidx_of_typ T; - val varifyT = varifyT midx; - - fun mk_type_abbr subst name alphas = - let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas); - in Syntax.term_of_typ (! Syntax.show_sorts) - (Sign.extern_typ thy (Envir.norm_type subst abbrT)) end; - - fun match rT T = (Sign.typ_match thy (varifyT rT,T) - Vartab.empty); - - in - if !print_record_type_abbr then - (case last_extT T of - SOME (name, _) => + val thy = ProofContext.theory_of ctxt; + + (*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*) + + (*WORKAROUND: + If a record type occurs in an error message of type inference there + may be some internal frees donoted by ??: + (Const "_tfree",_) $ Free ("??'a", _). + + This will unfortunately be translated to Type ("??'a", []) instead of + TFree ("??'a", _) by typ_of_term, which will confuse unify below. + fixT works around.*) + fun fixT (T as Type (x, [])) = + if String.isPrefix "??'" x then TFree (x, Sign.defaultS thy) else T + | fixT (Type (x, xs)) = Type (x, map fixT xs) + | fixT T = T; + + val T = fixT (decode_type thy tm); + val midx = maxidx_of_typ T; + val varifyT = varifyT midx; + + fun mk_type_abbr subst name alphas = + let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas) in + Syntax.term_of_typ (! Syntax.show_sorts) + (Sign.extern_typ thy (Envir.norm_type subst abbrT)) + end; + + fun match rT T = Sign.typ_match thy (varifyT rT, T) Vartab.empty; + in + if ! print_record_type_abbr then + (case last_extT T of + SOME (name, _) => if name = lastExt then - (let - val subst = match schemeT T - in + (let val subst = match schemeT T in if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, Sign.defaultS thy)))) then mk_type_abbr subst abbr alphas else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta]) - end handle TYPE_MATCH => default_tr' ctxt tm) - else raise Match (* give print translation of specialised record a chance *) - | _ => raise Match) - else default_tr' ctxt tm - end + end handle TYPE_MATCH => default_tr' ctxt tm) + else raise Match (*give print translation of specialised record a chance*) + | _ => raise Match) + else default_tr' ctxt tm + end; fun record_type_tr' sep mark record record_scheme ctxt t = let @@ -1010,62 +1025,62 @@ val T = decode_type thy t; val varifyT = varifyT (Term.maxidx_of_typ T); - fun term_of_type T = Syntax.term_of_typ (!Syntax.show_sorts) (Sign.extern_typ thy T); + fun term_of_type T = Syntax.term_of_typ (! Syntax.show_sorts) (Sign.extern_typ thy T); fun field_lst T = (case T of - Type (ext, args) - => (case try (unsuffix ext_typeN) ext of - SOME ext' - => (case get_extfields thy ext' of - SOME flds - => (case get_fieldext thy (fst (hd flds)) of - SOME (_, alphas) - => (let - val (f :: fs) = but_last flds; - val flds' = apfst (Sign.extern_const thy) f - :: map (apfst Long_Name.base_name) fs; - val (args', more) = split_last args; - val alphavars = map varifyT (but_last alphas); - val subst = fold2 (curry (Sign.typ_match thy)) - alphavars args' Vartab.empty; - val flds'' = (map o apsnd) - (Envir.norm_type subst o varifyT) flds'; - in flds'' @ field_lst more end - handle TYPE_MATCH => [("", T)] - | Library.UnequalLengths => [("", T)]) - | NONE => [("", T)]) - | NONE => [("", T)]) - | NONE => [("", T)]) - | _ => [("", T)]) + Type (ext, args) => + (case try (unsuffix ext_typeN) ext of + SOME ext' => + (case get_extfields thy ext' of + SOME flds => + (case get_fieldext thy (fst (hd flds)) of + SOME (_, alphas) => + (let + val f :: fs = but_last flds; + val flds' = apfst (Sign.extern_const thy) f :: + map (apfst Long_Name.base_name) fs; + val (args', more) = split_last args; + val alphavars = map varifyT (but_last alphas); + val subst = fold2 (curry (Sign.typ_match thy)) alphavars args' Vartab.empty; + val flds'' = (map o apsnd) (Envir.norm_type subst o varifyT) flds'; + in flds'' @ field_lst more end + handle TYPE_MATCH => [("", T)] + | Library.UnequalLengths => [("", 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' handle Empty => raise Match; - - 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 + val flds'' = + foldr1 (fn (x, y) => Syntax.const sep $ x $ y) flds' + handle Empty => raise Match; + 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' ctxt ts = record_type_tr' "_field_types" "_field_type" - "_record_type" "_record_type_scheme" ctxt - (list_comb (Syntax.const name_sfx,ts)) - in (name_sfx,tr') - end + let + val name_sfx = suffix ext_typeN name; + fun tr' ctxt ts = + record_type_tr' "_field_types" "_field_type" "_record_type" "_record_type_scheme" + ctxt (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' ctxt ts = - record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt - (list_comb (Syntax.const name_sfx,ts)) + 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' ctxt ts = + record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt + (list_comb (Syntax.const name_sfx, ts)); in (name_sfx, tr') end; @@ -1076,26 +1091,28 @@ fun quick_and_dirty_prove stndrd thy asms prop tac = - if !record_quick_and_dirty_sensitive andalso !quick_and_dirty - then Goal.prove (ProofContext.init thy) [] [] - (Logic.list_implies (map Logic.varify asms,Logic.varify prop)) - (K (SkipProof.cheat_tac @{theory HOL})) - (* standard can take quite a while for large records, thats why - * we varify the proposition manually here.*) - else let val prf = Goal.prove (ProofContext.init thy) [] asms prop tac; - in if stndrd then standard prf else prf end; + if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty then + Goal.prove (ProofContext.init thy) [] [] + (Logic.list_implies (map Logic.varify asms, Logic.varify prop)) + (K (SkipProof.cheat_tac @{theory HOL})) + (*Drule.standard can take quite a while for large records, thats why + we varify the proposition manually here.*) + else + let val prf = Goal.prove (ProofContext.init thy) [] asms prop tac + in if stndrd then standard prf else prf end; fun quick_and_dirty_prf noopt opt () = - if !record_quick_and_dirty_sensitive andalso !quick_and_dirty - then noopt () - else opt (); - -fun is_sel_upd_pair thy (Const (s, t)) (Const (u, t')) - = case (get_updates thy u) - of SOME u_name => u_name = s - | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]); - -fun mk_comp f g = let + if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty + then noopt () + else opt (); + +fun is_sel_upd_pair thy (Const (s, t)) (Const (u, t')) = + (case get_updates thy u of + SOME u_name => u_name = s + | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')])); + +fun mk_comp f g = + let val x = fastype_of g; val a = domain_type x; val b = range_type x; @@ -1103,72 +1120,87 @@ val T = (b --> c) --> ((a --> b) --> (a --> c)) in Const ("Fun.comp", T) $ f $ g end; -fun mk_comp_id f = let - val T = range_type (fastype_of f); +fun mk_comp_id f = + let val T = range_type (fastype_of f) in mk_comp (Const ("Fun.id", T --> T)) f end; fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t - | get_upd_funs _ = []; - -fun get_accupd_simps thy term defset intros_tac = let + | get_upd_funs _ = []; + +fun get_accupd_simps thy term defset intros_tac = + let val (acc, [body]) = strip_comb term; - val recT = domain_type (fastype_of acc); - val upd_funs = sort_distinct TermOrd.fast_term_ord - (get_upd_funs body); - fun get_simp upd = let - val T = domain_type (fastype_of upd); - val lhs = mk_comp acc (upd $ Free ("f", T)); - val rhs = if is_sel_upd_pair thy acc upd - then mk_comp (Free ("f", T)) acc else mk_comp_id acc; + val recT = domain_type (fastype_of acc); + val upd_funs = sort_distinct TermOrd.fast_term_ord (get_upd_funs body); + fun get_simp upd = + let + val T = domain_type (fastype_of upd); + val lhs = mk_comp acc (upd $ Free ("f", T)); + val rhs = + if is_sel_upd_pair thy acc upd + then mk_comp (Free ("f", T)) acc + else mk_comp_id acc; val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); - val othm = Goal.prove (ProofContext.init thy) [] [] prop (fn prems => - EVERY [simp_tac defset 1, - REPEAT_DETERM (intros_tac 1), - TRY (simp_tac (HOL_ss addsimps id_o_apps) 1)]); - val dest = if is_sel_upd_pair thy acc upd - then o_eq_dest else o_eq_id_dest; + val othm = + Goal.prove (ProofContext.init thy) [] [] prop + (fn prems => + EVERY + [simp_tac defset 1, + REPEAT_DETERM (intros_tac 1), + TRY (simp_tac (HOL_ss addsimps id_o_apps) 1)]); + val dest = + if is_sel_upd_pair thy acc upd + then o_eq_dest + else o_eq_id_dest; in standard (othm RS dest) end; in map get_simp upd_funs end; -structure SymSymTab = Table(type key = string * string - val ord = prod_ord fast_string_ord fast_string_ord); - -fun get_updupd_simp thy defset intros_tac u u' comp = let - val f = Free ("f", domain_type (fastype_of u)); - val f' = Free ("f'", domain_type (fastype_of u')); - val lhs = mk_comp (u $ f) (u' $ f'); - val rhs = if comp - then u $ mk_comp f f' - else mk_comp (u' $ f') (u $ f); +(* FIXME dup? *) +structure SymSymTab = + Table(type key = string * string val ord = prod_ord fast_string_ord fast_string_ord); + +fun get_updupd_simp thy defset intros_tac u u' comp = + let + val f = Free ("f", domain_type (fastype_of u)); + val f' = Free ("f'", domain_type (fastype_of u')); + val lhs = mk_comp (u $ f) (u' $ f'); + val rhs = + if comp + then u $ mk_comp f f' + else mk_comp (u' $ f') (u $ f); val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); - val othm = Goal.prove (ProofContext.init thy) [] [] prop (fn prems => - EVERY [simp_tac defset 1, - REPEAT_DETERM (intros_tac 1), - TRY (simp_tac (HOL_ss addsimps [id_apply]) 1)]); + val othm = + Goal.prove (ProofContext.init thy) [] [] prop + (fn prems => + EVERY + [simp_tac defset 1, + REPEAT_DETERM (intros_tac 1), + TRY (simp_tac (HOL_ss addsimps [id_apply]) 1)]); val dest = if comp then o_eq_dest_lhs else o_eq_dest; in standard (othm RS dest) end; -fun get_updupd_simps thy term defset intros_tac = let - val recT = fastype_of term; - val upd_funs = get_upd_funs term; - val cname = fst o dest_Const; - fun getswap u u' = get_updupd_simp thy defset intros_tac u u' - (cname u = cname u'); +fun get_updupd_simps thy term defset intros_tac = + let + val recT = fastype_of term; + val upd_funs = get_upd_funs term; + val cname = fst o dest_Const; + fun getswap u u' = get_updupd_simp thy defset intros_tac u u' (cname u = cname u'); fun build_swaps_to_eq upd [] swaps = swaps - | build_swaps_to_eq upd (u::us) swaps = let - val key = (cname u, cname upd); - val newswaps = if SymSymTab.defined swaps key then swaps - else SymSymTab.insert (K true) - (key, getswap u upd) swaps; - in if cname u = cname upd then newswaps - else build_swaps_to_eq upd us newswaps end; - fun swaps_needed [] prev seen swaps = map snd (SymSymTab.dest swaps) - | swaps_needed (u::us) prev seen swaps = - if Symtab.defined seen (cname u) - then swaps_needed us prev seen - (build_swaps_to_eq u prev swaps) - else swaps_needed us (u::prev) - (Symtab.insert (K true) (cname u, ()) seen) swaps; + | build_swaps_to_eq upd (u :: us) swaps = + let + val key = (cname u, cname upd); + val newswaps = + if SymSymTab.defined swaps key then swaps + else SymSymTab.insert (K true) (key, getswap u upd) swaps; + in + if cname u = cname upd then newswaps + else build_swaps_to_eq upd us newswaps + end; + fun swaps_needed [] prev seen swaps = map snd (SymSymTab.dest swaps) + | swaps_needed (u :: us) prev seen swaps = + if Symtab.defined seen (cname u) + then swaps_needed us prev seen (build_swaps_to_eq u prev swaps) + else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps; in swaps_needed upd_funs [] Symtab.empty SymSymTab.empty end; val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate; @@ -1177,326 +1209,351 @@ let val defset = get_sel_upd_defs thy; val in_tac = IsTupleSupport.istuple_intros_tac thy; - val prop' = Envir.beta_eta_contract prop; - val (lhs, rhs) = Logic.dest_equals (Logic.strip_assums_concl prop'); + val prop' = Envir.beta_eta_contract prop; + val (lhs, rhs) = Logic.dest_equals (Logic.strip_assums_concl prop'); val (head, args) = strip_comb lhs; - val simps = if length args = 1 - then get_accupd_simps thy lhs defset in_tac - else get_updupd_simps thy lhs defset in_tac; + val simps = + if length args = 1 + then get_accupd_simps thy lhs defset in_tac + else get_updupd_simps thy lhs defset in_tac; in - Goal.prove (ProofContext.init thy) [] [] prop' (fn prems => - simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1 - THEN TRY (simp_tac (HOL_basic_ss addsimps ex_simps - addsimprocs ex_simprs) 1)) + Goal.prove (ProofContext.init thy) [] [] prop' + (fn prems => + simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1 THEN + TRY (simp_tac (HOL_basic_ss addsimps ex_simps addsimprocs ex_simprs) 1)) end; local -fun eq (s1:string) (s2:string) = (s1 = s2); + +fun eq (s1: string) (s2: string) = (s1 = s2); + fun has_field extfields f T = - exists (fn (eN,_) => exists (eq f o fst) (Symtab.lookup_list extfields eN)) - (dest_recTs T); - -fun K_skeleton n (T as Type (_,[_,kT])) (b as Bound i) (Abs (x,xT,t)) = - if null (loose_bnos t) then ((n,kT),(Abs (x,xT,Bound (i+1)))) else ((n,T),b) - | K_skeleton n T b _ = ((n,T),b); + exists (fn (eN, _) => exists (eq f o fst) (Symtab.lookup_list extfields eN)) (dest_recTs T); + +fun K_skeleton n (T as Type (_, [_, kT])) (b as Bound i) (Abs (x, xT, t)) = + if null (loose_bnos t) then ((n, kT), (Abs (x, xT, Bound (i + 1)))) else ((n, T), b) + | K_skeleton n T b _ = ((n, T), b); in + (* record_simproc *) -(* Simplifies selections of an record update: - * (1) S (S_update k r) = k (S r) - * (2) S (X_update k r) = S r - * The simproc skips multiple updates at once, eg: - * S (X_update x (Y_update y (S_update k r))) = k (S r) - * But be careful in (2) because of the extendibility of records. - * - If S is a more-selector we have to make sure that the update on component - * X does not affect the selected subrecord. - * - If X is a more-selector we have to make sure that S is not in the updated - * subrecord. - *) + +(* + Simplify selections of an record update: + (1) S (S_update k r) = k (S r) + (2) S (X_update k r) = S r + + The simproc skips multiple updates at once, eg: + S (X_update x (Y_update y (S_update k r))) = k (S r) + + But be careful in (2) because of the extensibility of records. + - If S is a more-selector we have to make sure that the update on component + X does not affect the selected subrecord. + - If X is a more-selector we have to make sure that S is not in the updated + subrecord. +*) val record_simproc = Simplifier.simproc @{theory HOL} "record_simp" ["x"] (fn thy => fn ss => fn t => - (case t of (sel as Const (s, Type (_,[domS,rangeS])))$ - ((upd as Const (u,Type(_,[_,Type (_,[rT,_])]))) $ k $ r)=> - if is_selector thy s then - (case get_updates thy u of SOME u_name => - let - val {sel_upd={updates,...},extfields,...} = RecordsData.get thy; - - fun mk_eq_terms ((upd as Const (u,Type(_,[kT,_]))) $ k $ r) = - (case Symtab.lookup updates u of - NONE => NONE - | SOME u_name - => if u_name = s - then (case mk_eq_terms r of - NONE => - let - val rv = ("r",rT) - val rb = Bound 0 - val (kv,kb) = K_skeleton "k" kT (Bound 1) k; - in SOME (upd$kb$rb,kb$(sel$rb),[kv,rv]) end - | SOME (trm,trm',vars) => - let - val (kv,kb) = K_skeleton "k" kT (Bound (length vars)) k; - in SOME (upd$kb$trm,kb$trm',kv::vars) end) - else if has_field extfields u_name rangeS - orelse has_field extfields s (domain_type kT) - then NONE - else (case mk_eq_terms r of - SOME (trm,trm',vars) - => let - val (kv,kb) = - K_skeleton "k" kT (Bound (length vars)) k; - in SOME (upd$kb$trm,trm',kv::vars) end - | NONE - => let - val rv = ("r",rT) - val rb = Bound 0 - val (kv,kb) = K_skeleton "k" kT (Bound 1) k; - in SOME (upd$kb$rb,sel$rb,[kv,rv]) end)) - | mk_eq_terms r = NONE - in - (case mk_eq_terms (upd$k$r) of - SOME (trm,trm',vars) - => SOME (prove_unfold_defs thy ss domS [] [] - (list_all(vars,(Logic.mk_equals (sel$trm, trm'))))) - | NONE => NONE) - end - | NONE => NONE) - else NONE + (case t of + (sel as Const (s, Type (_, [domS, rangeS]))) $ + ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) => + if is_selector thy s then + (case get_updates thy u of + SOME u_name => + let + val {sel_upd = {updates, ...}, extfields, ...} = RecordsData.get thy; + + fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) = + (case Symtab.lookup updates u of + NONE => NONE + | SOME u_name => + if u_name = s then + (case mk_eq_terms r of + NONE => + let + val rv = ("r", rT); + val rb = Bound 0; + val (kv, kb) = K_skeleton "k" kT (Bound 1) k; + in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end + | SOME (trm, trm', vars) => + let + val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k; + in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end) + else if has_field extfields u_name rangeS orelse + has_field extfields s (domain_type kT) then NONE + else + (case mk_eq_terms r of + SOME (trm, trm', vars) => + let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k + in SOME (upd $ kb $ trm, trm', kv :: vars) end + | NONE => + let + val rv = ("r", rT); + val rb = Bound 0; + val (kv, kb) = K_skeleton "k" kT (Bound 1) k; + in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end)) + | mk_eq_terms r = NONE; + in + (case mk_eq_terms (upd $ k $ r) of + SOME (trm, trm', vars) => + SOME + (prove_unfold_defs thy ss domS [] [] + (list_all (vars, Logic.mk_equals (sel $ trm, trm')))) + | NONE => NONE) + end + | NONE => NONE) + else NONE | _ => NONE)); -fun get_upd_acc_cong_thm upd acc thy simpset = let +fun get_upd_acc_cong_thm upd acc thy simpset = + let val in_tac = IsTupleSupport.istuple_intros_tac thy; val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)] - val prop = concl_of (named_cterm_instantiate insts updacc_cong_triv); - in Goal.prove (ProofContext.init thy) [] [] prop (fn prems => - EVERY [simp_tac simpset 1, - REPEAT_DETERM (in_tac 1), - TRY (resolve_tac [updacc_cong_idI] 1)]) + val prop = concl_of (named_cterm_instantiate insts updacc_cong_triv); + in + Goal.prove (ProofContext.init thy) [] [] prop + (fn prems => + EVERY + [simp_tac simpset 1, + REPEAT_DETERM (in_tac 1), + TRY (resolve_tac [updacc_cong_idI] 1)]) end; + (* record_upd_simproc *) -(* simplify multiple updates: - * (1) "N_update y (M_update g (N_update x (M_update f r))) = + +(*Simplify multiple updates: + (1) "N_update y (M_update g (N_update x (M_update f r))) = (N_update (y o x) (M_update (g o f) r))" - * (2) "r(|M:= M r|) = r" - * In both cases "more" updates complicate matters: for this reason - * we omit considering further updates if doing so would introduce - * both a more update and an update to a field within it. -*) + (2) "r(|M:= M r|) = r" + + In both cases "more" updates complicate matters: for this reason + we omit considering further updates if doing so would introduce + both a more update and an update to a field within it.*) val record_upd_simproc = Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"] (fn thy => fn ss => fn t => let - (* we can use more-updators with other updators as long - as none of the other updators go deeper than any more - updator. min here is the depth of the deepest other - updator, max the depth of the shallowest more updator *) + (*We can use more-updators with other updators as long + as none of the other updators go deeper than any more + updator. min here is the depth of the deepest other + updator, max the depth of the shallowest more updator.*) fun include_depth (dep, true) (min, max) = - if (min <= dep) - then SOME (min, if dep <= max orelse max = ~1 then dep else max) - else NONE + if min <= dep + then SOME (min, if dep <= max orelse max = ~1 then dep else max) + else NONE | include_depth (dep, false) (min, max) = - if (dep <= max orelse max = ~1) - then SOME (if min <= dep then dep else min, max) - else NONE; + if dep <= max orelse max = ~1 + then SOME (if min <= dep then dep else min, max) + else NONE; fun getupdseq (term as (upd as Const (u, T)) $ f $ tm) min max = - (case get_update_details u thy of - SOME (s, dep, ismore) => - (case include_depth (dep, ismore) (min, max) of - SOME (min', max') => let - val (us, bs, _) = getupdseq tm min' max'; + (case get_update_details u thy of + SOME (s, dep, ismore) => + (case include_depth (dep, ismore) (min, max) of + SOME (min', max') => + let val (us, bs, _) = getupdseq tm min' max' in ((upd, s, f) :: us, bs, fastype_of term) end - | NONE => ([], term, HOLogic.unitT)) - | NONE => ([], term, HOLogic.unitT)) + | NONE => ([], term, HOLogic.unitT)) + | NONE => ([], term, HOLogic.unitT)) | getupdseq term _ _ = ([], term, HOLogic.unitT); val (upds, base, baseT) = getupdseq t 0 ~1; fun is_upd_noop s (f as Abs (n, T, Const (s', T') $ tm')) tm = - if s = s' andalso null (loose_bnos tm') - andalso subst_bound (HOLogic.unit, tm') = tm - then (true, Abs (n, T, Const (s', T') $ Bound 1)) - else (false, HOLogic.unit) + if s = s' andalso null (loose_bnos tm') + andalso subst_bound (HOLogic.unit, tm') = tm + then (true, Abs (n, T, Const (s', T') $ Bound 1)) + else (false, HOLogic.unit) | is_upd_noop s f tm = (false, HOLogic.unit); fun get_noop_simps (upd as Const (u, T)) - (f as Abs (n, T', (acc as Const (s, T'')) $ _)) = let - - val ss = get_sel_upd_defs thy; + (f as Abs (n, T', (acc as Const (s, T'')) $ _)) = + let + val ss = get_sel_upd_defs thy; val uathm = get_upd_acc_cong_thm upd acc thy ss; - in [standard (uathm RS updacc_noopE), - standard (uathm RS updacc_noop_compE)] end; - - (* if f is constant then (f o g) = f. we know that K_skeleton - only returns constant abstractions thus when we see an - abstraction we can discard inner updates. *) + in + [standard (uathm RS updacc_noopE), standard (uathm RS updacc_noop_compE)] + end; + + (*If f is constant then (f o g) = f. we know that K_skeleton + only returns constant abstractions thus when we see an + abstraction we can discard inner updates.*) fun add_upd (f as Abs _) fs = [f] | add_upd f fs = (f :: fs); - (* mk_updterm returns - * (orig-term-skeleton, simplified-skeleton, - * variables, duplicate-updates, simp-flag, noop-simps) - * - * where duplicate-updates is a table used to pass upward - * the list of update functions which can be composed - * into an update above them, simp-flag indicates whether - * any simplification was achieved, and noop-simps are - * used for eliminating case (2) defined above - *) - fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term = let - val (lhs, rhs, vars, dups, simp, noops) = + (*mk_updterm returns + (orig-term-skeleton, simplified-skeleton, + variables, duplicate-updates, simp-flag, noop-simps) + + where duplicate-updates is a table used to pass upward + the list of update functions which can be composed + into an update above them, simp-flag indicates whether + any simplification was achieved, and noop-simps are + used for eliminating case (2) defined above*) + fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term = + let + val (lhs, rhs, vars, dups, simp, noops) = mk_updterm upds (Symtab.update (u, ()) above) term; - val (fvar, skelf) = K_skeleton (Long_Name.base_name s) (domain_type T) - (Bound (length vars)) f; - val (isnoop, skelf') = is_upd_noop s f term; - val funT = domain_type T; - fun mk_comp_local (f, f') = - Const ("Fun.comp", funT --> funT --> funT) $ f $ f'; - in if isnoop - then (upd $ skelf' $ lhs, rhs, vars, + val (fvar, skelf) = + K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f; + val (isnoop, skelf') = is_upd_noop s f term; + val funT = domain_type T; + fun mk_comp_local (f, f') = Const ("Fun.comp", funT --> funT --> funT) $ f $ f'; + in + if isnoop then + (upd $ skelf' $ lhs, rhs, vars, Symtab.update (u, []) dups, true, if Symtab.defined noops u then noops else Symtab.update (u, get_noop_simps upd skelf') noops) - else if Symtab.defined above u - then (upd $ skelf $ lhs, rhs, fvar :: vars, + else if Symtab.defined above u then + (upd $ skelf $ lhs, rhs, fvar :: vars, Symtab.map_default (u, []) (add_upd skelf) dups, true, noops) - else case Symtab.lookup dups u of - SOME fs => - (upd $ skelf $ lhs, - upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs, - fvar :: vars, dups, true, noops) - | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs, - fvar :: vars, dups, simp, noops) - end - | mk_updterm [] above term = (Bound 0, Bound 0, [("r", baseT)], - Symtab.empty, false, Symtab.empty) - | mk_updterm us above term = raise TERM ("mk_updterm match", - map (fn (x, y, z) => x) us); - - val (lhs, rhs, vars, dups, simp, noops) - = mk_updterm upds Symtab.empty base; + else + (case Symtab.lookup dups u of + SOME fs => + (upd $ skelf $ lhs, + upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs, + fvar :: vars, dups, true, noops) + | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops)) + end + | mk_updterm [] above term = + (Bound 0, Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty) + | mk_updterm us above term = + raise TERM ("mk_updterm match", map (fn (x, y, z) => x) us); + + val (lhs, rhs, vars, dups, simp, noops) = mk_updterm upds Symtab.empty base; val noops' = flat (map snd (Symtab.dest noops)); in if simp then - SOME (prove_unfold_defs thy ss baseT noops' [record_simproc] - (list_all(vars,(Logic.mk_equals (lhs, rhs))))) + SOME + (prove_unfold_defs thy ss baseT noops' [record_simproc] + (list_all (vars, Logic.mk_equals (lhs, rhs)))) else NONE - end) - -end + end); + +end; (* record_eq_simproc *) -(* looks up the most specific record-equality. - * Note on efficiency: - * Testing equality of records boils down to the test of equality of all components. - * Therefore the complexity is: #components * complexity for single component. - * Especially if a record has a lot of components it may be better to split up - * 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 - * Complexity: #components * #updates #updates - * - *) + +(*Looks up the most specific record-equality. + + Note on efficiency: + Testing equality of records boils down to the test of equality of all components. + Therefore the complexity is: #components * complexity for single component. + Especially if a record has a lot of components it may be better to split up + 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 + Complexity: #components * #updates #updates +*) val record_eq_simproc = Simplifier.simproc @{theory HOL} "record_eq_simp" ["r = s"] (fn thy => fn _ => fn t => (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ => - (case rec_id (~1) T of - "" => NONE - | name => (case get_equalities thy name of - NONE => NONE - | SOME thm => SOME (thm RS Eq_TrueI))) - | _ => NONE)); + (case rec_id ~1 T of + "" => NONE + | name => + (case get_equalities thy name of + NONE => NONE + | SOME thm => SOME (thm RS Eq_TrueI))) + | _ => NONE)); + (* record_split_simproc *) -(* splits quantified occurrences of records, for which P holds. P can peek on the - * subterm starting at the quantified occurrence of the record (including the quantifier) - * P t = 0: do not split - * P t = ~1: completely split - * P t > 0: split up to given bound of record extensions - *) + +(*Split quantified occurrences of records, for which P holds. P can peek on the + subterm starting at the quantified occurrence of the record (including the quantifier): + P t = 0: do not split + P t = ~1: completely split + P t > 0: split up to given bound of record extensions.*) fun record_split_simproc P = Simplifier.simproc @{theory HOL} "record_split_simp" ["x"] (fn thy => fn _ => fn t => - (case t of (Const (quantifier, Type (_, [Type (_, [T, _]), _])))$trm => - if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex" - then (case rec_id (~1) T of - "" => NONE - | name - => let val split = P t - in if split <> 0 then - (case get_splits thy (rec_id split T) of - NONE => NONE - | SOME (all_thm, All_thm, Ex_thm,_) - => SOME (case quantifier of - "all" => all_thm - | "All" => All_thm RS eq_reflection - | "Ex" => Ex_thm RS eq_reflection - | _ => error "record_split_simproc")) - else NONE - end) - else NONE - | _ => NONE)) + (case t of + Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ trm => + if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex" then + (case rec_id ~1 T of + "" => NONE + | name => + let val split = P t in + if split <> 0 then + (case get_splits thy (rec_id split T) of + NONE => NONE + | SOME (all_thm, All_thm, Ex_thm, _) => + SOME + (case quantifier of + "all" => all_thm + | "All" => All_thm RS eq_reflection + | "Ex" => Ex_thm RS eq_reflection + | _ => error "record_split_simproc")) + else NONE + end) + else NONE + | _ => NONE)); val record_ex_sel_eq_simproc = Simplifier.simproc @{theory HOL} "record_ex_sel_eq_simproc" ["Ex t"] (fn thy => fn ss => fn t => - let - fun prove prop = - quick_and_dirty_prove true thy [] prop - (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy) - addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1); - - fun mkeq (lr,Teq,(sel,Tsel),x) i = - if is_selector thy sel then - let val x' = if not (loose_bvar1 (x,0)) - then Free ("x" ^ string_of_int i, range_type Tsel) - else raise TERM ("",[x]); - val sel' = Const (sel,Tsel)$Bound 0; - val (l,r) = if lr then (sel',x') else (x',sel'); - in Const ("op =",Teq)$l$r end - else raise TERM ("",[Const (sel,Tsel)]); - - fun dest_sel_eq (Const ("op =",Teq)$(Const (sel,Tsel)$Bound 0)$X) = - (true,Teq,(sel,Tsel),X) - | dest_sel_eq (Const ("op =",Teq)$X$(Const (sel,Tsel)$Bound 0)) = - (false,Teq,(sel,Tsel),X) - | dest_sel_eq _ = raise TERM ("",[]); - - in - (case t of - (Const ("Ex",Tex)$Abs(s,T,t)) => - (let val eq = mkeq (dest_sel_eq t) 0; - val prop = list_all ([("r",T)], - Logic.mk_equals (Const ("Ex",Tex)$Abs(s,T,eq), - HOLogic.true_const)); - in SOME (prove prop) end - handle TERM _ => NONE) - | _ => NONE) - end) + let + fun prove prop = + quick_and_dirty_prove true thy [] prop + (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy) + addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1); + + fun mkeq (lr, Teq, (sel, Tsel), x) i = + if is_selector thy sel then + let + val x' = + if not (loose_bvar1 (x, 0)) + then Free ("x" ^ string_of_int i, range_type Tsel) + else raise TERM ("", [x]); + val sel' = Const (sel, Tsel) $ Bound 0; + val (l, r) = if lr then (sel', x') else (x', sel'); + in Const ("op =", Teq) $ l $ r end + else raise TERM ("", [Const (sel, Tsel)]); + + fun dest_sel_eq (Const ("op =", Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) = + (true, Teq, (sel, Tsel), X) + | dest_sel_eq (Const ("op =", Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) = + (false, Teq, (sel, Tsel), X) + | dest_sel_eq _ = raise TERM ("", []); + in + (case t of + Const ("Ex", Tex) $ Abs (s, T, t) => + (let + val eq = mkeq (dest_sel_eq t) 0; + val prop = + list_all ([("r", T)], + Logic.mk_equals (Const ("Ex", Tex) $ Abs (s, T, eq), HOLogic.true_const)); + in SOME (prove prop) end + handle TERM _ => NONE) + | _ => NONE) + end); local + val inductive_atomize = thms "induct_atomize"; val inductive_rulify = thms "induct_rulify"; + in + (* record_split_simp_tac *) -(* splits (and simplifies) all records in the goal for which P holds. - * For quantified occurrences of a record - * P can peek on the whole subterm (including the quantifier); for free variables P - * can only peek on the variable itself. - * P t = 0: do not split - * P t = ~1: completely split - * P t > 0: split up to given bound of record extensions - *) + +(*Split (and simplify) all records in the goal for which P holds. + For quantified occurrences of a record + P can peek on the whole subterm (including the quantifier); for free variables P + can only peek on the variable itself. + P t = 0: do not split + P t = ~1: completely split + P t > 0: split up to given bound of record extensions.*) fun record_split_simp_tac thms P i st = let val thy = Thm.theory_of_thm st; @@ -1510,40 +1567,47 @@ val frees = List.filter (is_recT o type_of) (OldTerm.term_frees goal); fun mk_split_free_tac free induct_thm i = - let val cfree = cterm_of thy free; - val (_$(_$r)) = concl_of induct_thm; - val crec = cterm_of thy r; - val thm = cterm_instantiate [(crec,cfree)] induct_thm; - in EVERY [simp_tac (HOL_basic_ss addsimps inductive_atomize) i, - rtac thm i, - simp_tac (HOL_basic_ss addsimps inductive_rulify) i] - end; - - fun split_free_tac P i (free as Free (n,T)) = - (case rec_id (~1) T of - "" => NONE - | name => let val split = P free - in if split <> 0 then - (case get_splits thy (rec_id split T) of - NONE => NONE - | SOME (_,_,_,induct_thm) - => SOME (mk_split_free_tac free induct_thm i)) - else NONE - end) - | split_free_tac _ _ _ = NONE; + let + val cfree = cterm_of thy free; + val _$ (_ $ r) = concl_of induct_thm; + val crec = cterm_of thy r; + val thm = cterm_instantiate [(crec, cfree)] induct_thm; + in + EVERY + [simp_tac (HOL_basic_ss addsimps inductive_atomize) i, + rtac thm i, + simp_tac (HOL_basic_ss addsimps inductive_rulify) i] + end; + + fun split_free_tac P i (free as Free (n, T)) = + (case rec_id ~1 T of + "" => NONE + | name => + let val split = P free in + if split <> 0 then + (case get_splits thy (rec_id split T) of + NONE => NONE + | SOME (_, _, _, induct_thm) => + SOME (mk_split_free_tac free induct_thm i)) + else NONE + end) + | split_free_tac _ _ _ = NONE; val split_frees_tacs = List.mapPartial (split_free_tac P i) frees; val simprocs = if has_rec goal then [record_split_simproc P] else []; - val thms' = K_comp_convs@thms - in st |> ((EVERY split_frees_tacs) - THEN (Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i)) + val thms' = K_comp_convs @ thms; + in + st |> + (EVERY split_frees_tacs THEN + Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i) end handle Empty => Seq.empty; end; (* record_split_tac *) -(* splits all records in the goal, which are quantified by ! or !!. *) + +(*Split all records in the goal, which are quantified by ! or !!.*) fun record_split_tac i st = let val thy = Thm.theory_of_thm st; @@ -1553,18 +1617,20 @@ (s = "all" orelse s = "All") andalso is_recT T | _ => false); - val goal = nth (Thm.prems_of st) (i - 1); + val goal = nth (Thm.prems_of st) (i - 1); (* FIXME SUBGOAL *) fun is_all t = - (case t of (Const (quantifier, _)$_) => - if quantifier = "All" orelse quantifier = "all" then ~1 else 0 - | _ => 0); - - 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 Subscript => Seq.empty; + (case t of + Const (quantifier, _) $ _ => + if quantifier = "All" orelse quantifier = "all" then ~1 else 0 + | _ => 0); + + 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 Subscript => Seq.empty; (* FIXME SUBGOAL *) (* wrapper *) @@ -1593,7 +1659,8 @@ fun cert_typ ctxt raw_T env = let val thy = ProofContext.theory_of ctxt; - val T = Type.no_tvars (Sign.certify_typ thy raw_T) handle TYPE (msg, _, _) => error msg; + val T = Type.no_tvars (Sign.certify_typ thy raw_T) + handle TYPE (msg, _, _) => error msg; val env' = OldTerm.add_typ_tfrees (T, env); in (T, env') end; @@ -1609,156 +1676,155 @@ 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. - *) - +(*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.theory_of_thm st); - val g = nth (prems_of st) (i - 1); + val g = nth (prems_of st) (i - 1); (* FIXME SUBGOAL *) val params = Logic.strip_params g; val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g); val rule' = Thm.lift_rule (Thm.cprem_of 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 (Library.drop (length params, ys)) of + (*ca indicates if rule is a case analysis or induction rule*) + val (x, ca) = + (case rev (Library.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 AList.lookup (op =) (map dest_Free (OldTerm.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' + val rule'' = cterm_instantiate (map (pairself cert) + (case (rev params) of + [] => + (case AList.lookup (op =) (map dest_Free (OldTerm.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; -(* !!x1 ... xn. ... ==> EX x1 ... xn. P x1 ... xn; - instantiates x1 ... xn with parameters x1 ... xn *) +(*!!x1 ... xn. ... ==> EX x1 ... xn. P x1 ... xn; + instantiates x1 ... xn with parameters x1 ... xn*) fun ex_inst_tac i st = let val thy = Thm.theory_of_thm st; - val g = nth (prems_of st) (i - 1); + val g = nth (prems_of st) (i - 1); (* FIXME SUBGOAL *) val params = Logic.strip_params g; val exI' = Thm.lift_rule (Thm.cprem_of st i) exI; - val (_$(_$x)) = Logic.strip_assums_concl (hd (prems_of exI')); + val _ $ (_ $ x) = Logic.strip_assums_concl (hd (prems_of exI')); val cx = cterm_of thy (fst (strip_comb x)); - - in Seq.single (Library.foldl (fn (st,v) => - Seq.hd - (compose_tac (false, cterm_instantiate - [(cx,cterm_of thy (list_abs (params,Bound v)))] exI',1) - i st)) (st,((length params) - 1) downto 0)) + in + Seq.single (Library.foldl (fn (st, v) => + Seq.hd + (compose_tac + (false, + cterm_instantiate [(cx, cterm_of thy (list_abs (params, Bound v)))] exI', 1) i st)) + (st, (length params - 1) downto 0)) end; fun extension_definition full name fields names alphas zeta moreT more vars thy = let val base = Long_Name.base_name; val fieldTs = (map snd fields); - val alphas_zeta = alphas@[zeta]; + val alphas_zeta = alphas @ [zeta]; val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta; val vT = TFree (Name.variant alphas_zeta "'v", HOLogic.typeS); val extT_name = suffix ext_typeN name val extT = Type (extT_name, alphas_zetaTs); - val fields_more = fields@[(full moreN,moreT)]; - val fields_moreTs = fieldTs@[moreT]; + val fields_more = fields @ [(full moreN, moreT)]; + val fields_moreTs = fieldTs @ [moreT]; val bfields_more = map (apfst base) fields_more; - val r = Free (rN,extT) + val r = Free (rN, extT); val len = length fields; val idxms = 0 upto len; - (* before doing anything else, create the tree of new types - that will back the record extension *) - - fun mktreeT [] = raise (TYPE ("mktreeT: empty list", [], [])) + (*before doing anything else, create the tree of new types + that will back the record extension*) + + fun mktreeT [] = raise TYPE ("mktreeT: empty list", [], []) | mktreeT [T] = T | mktreeT xs = - let - val len = length xs; - val half = len div 2; - val left = List.take (xs, half); - val right = List.drop (xs, half); - in - HOLogic.mk_prodT (mktreeT left, mktreeT right) - end; - - fun mktreeV [] = raise (TYPE ("mktreeV: empty list", [], [])) + let + val len = length xs; + val half = len div 2; + val left = List.take (xs, half); + val right = List.drop (xs, half); + in + HOLogic.mk_prodT (mktreeT left, mktreeT right) + end; + + fun mktreeV [] = raise TYPE ("mktreeV: empty list", [], []) | mktreeV [T] = T | mktreeV xs = - let - val len = length xs; - val half = len div 2; - val left = List.take (xs, half); - val right = List.drop (xs, half); - in - IsTupleSupport.mk_cons_tuple (mktreeV left, mktreeV right) - end; + let + val len = length xs; + val half = len div 2; + val left = List.take (xs, half); + val right = List.drop (xs, half); + in + IsTupleSupport.mk_cons_tuple (mktreeV left, mktreeV right) + end; fun mk_istuple ((thy, i), (left, rght)) = - let - val suff = if i = 0 then ext_typeN else inner_typeN ^ (string_of_int i); - val nm = suffix suff (Long_Name.base_name name); - val (isom, cons, thy') = IsTupleSupport.add_istuple_type - (nm, alphas_zeta) (fastype_of left, fastype_of rght) thy; - in - ((thy', i + 1), cons $ left $ rght) - end; - - (* trying to create a 1-element istuple will fail, and - is pointless anyway *) - fun mk_even_istuple ((thy, i), [arg]) = - ((thy, i), arg) + let + val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i; + val nm = suffix suff (Long_Name.base_name name); + val (isom, cons, thy') = + IsTupleSupport.add_istuple_type + (nm, alphas_zeta) (fastype_of left, fastype_of rght) thy; + in + ((thy', i + 1), cons $ left $ rght) + end; + + (*trying to create a 1-element istuple will fail, and + is pointless anyway*) + fun mk_even_istuple ((thy, i), [arg]) = ((thy, i), arg) | mk_even_istuple ((thy, i), args) = - mk_istuple ((thy, i), IsTupleSupport.dest_cons_tuple (mktreeV args)); + mk_istuple ((thy, i), IsTupleSupport.dest_cons_tuple (mktreeV args)); fun build_meta_tree_type i thy vars more = - let - val len = length vars; - in - if len < 1 - then raise (TYPE ("meta_tree_type args too short", [], vars)) - else if len > 16 - then let - fun group16 [] = [] - | group16 xs = Library.take (16, xs) - :: group16 (Library.drop (16, xs)); - val vars' = group16 vars; - val ((thy', i'), composites) = - Library.foldl_map mk_even_istuple ((thy, i), vars'); - in - build_meta_tree_type i' thy' composites more - end - else let - val ((thy', i'), term) - = mk_istuple ((thy, 0), (mktreeV vars, more)); - in - (term, thy') - end - end; + let val len = length vars in + if len < 1 then raise (TYPE ("meta_tree_type args too short", [], vars)) + else if len > 16 then + let + fun group16 [] = [] + | group16 xs = Library.take (16, xs) :: group16 (Library.drop (16, xs)); + val vars' = group16 vars; + val ((thy', i'), composites) = + Library.foldl_map mk_even_istuple ((thy, i), vars'); (* FIXME fold_map !? *) + in + build_meta_tree_type i' thy' composites more + end + else + let val ((thy', i'), term) = mk_istuple ((thy, 0), (mktreeV vars, more)) + in (term, thy') end + end; val _ = timing_msg "record extension preparing definitions"; + (* 1st stage part 1: introduce the tree of new types *) + fun get_meta_tree () = build_meta_tree_type 1 thy vars more; val (ext_body, typ_thy) = timeit_msg "record extension nested type def:" get_meta_tree; + (* prepare declarations and definitions *) (*fields constructor*) - val ext_decl = (mk_extC (name,extT) fields_moreTs); - val ext_spec = list_comb (Const ext_decl,vars@[more]) :== ext_body; + val ext_decl = mk_extC (name, extT) fields_moreTs; + val ext_spec = list_comb (Const ext_decl, vars @ [more]) :== ext_body; fun mk_ext args = list_comb (Const ext_decl, args); + (* 1st stage part 2: define the ext constant *) + fun mk_defs () = typ_thy |> Sign.add_consts_i [Syntax.no_syn (apfst (Binding.name o base) ext_decl)] @@ -1768,32 +1834,31 @@ (* prepare propositions *) val _ = timing_msg "record extension preparing propositions"; - val vars_more = vars@[more]; - val named_vars_more = (names@[full moreN])~~vars_more; - val variants = map (fn (Free (x,_))=>x) vars_more; + val vars_more = vars @ [more]; + val named_vars_more = (names @ [full moreN]) ~~ vars_more; + val variants = map (fn Free (x, _) => x) vars_more; val ext = mk_ext vars_more; - val s = Free (rN, extT); - val w = Free (wN, extT); + val s = Free (rN, extT); + val w = Free (wN, extT); val P = Free (Name.variant variants "P", extT-->HOLogic.boolT); val C = Free (Name.variant variants "C", HOLogic.boolT); val intros_tac = IsTupleSupport.istuple_intros_tac defs_thy; val inject_prop = - let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more; - in - ((HOLogic.mk_conj (HOLogic.eq_const extT $ - mk_ext vars_more$mk_ext vars_more', HOLogic.true_const)) - === - foldr1 HOLogic.mk_conj - (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [HOLogic.true_const])) + let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in + HOLogic.mk_conj (HOLogic.eq_const extT $ + mk_ext vars_more $ mk_ext vars_more', HOLogic.true_const) + === + foldr1 HOLogic.mk_conj + (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [HOLogic.true_const]) 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)) + All (map dest_Free vars_more) + (Trueprop (HOLogic.mk_eq (s, ext)) ==> Trueprop C) ==> Trueprop C; val split_meta_prop = @@ -1809,89 +1874,97 @@ in fn prop => prove stndrd [] prop (K tac) end; fun inject_prf () = - simplify HOL_ss ( - prove_standard [] inject_prop (fn prems => - EVERY [simp_tac (HOL_basic_ss addsimps [ext_def]) 1, - REPEAT_DETERM (resolve_tac [refl_conj_eq] 1 - ORELSE intros_tac 1 - ORELSE resolve_tac [refl] 1)])); + simplify HOL_ss + (prove_standard [] inject_prop + (fn prems => + EVERY + [simp_tac (HOL_basic_ss addsimps [ext_def]) 1, + REPEAT_DETERM (resolve_tac [refl_conj_eq] 1 ORELSE + intros_tac 1 ORELSE + resolve_tac [refl] 1)])); val inject = timeit_msg "record extension inject proof:" inject_prf; - (* We need a surjection property r = (| f = f r, g = g r ... |) - to prove other theorems. We haven't given names to the accessors - f, g etc yet however, so we generate an ext structure with - free variables as all arguments and allow the introduction tactic to - operate on it as far as it can. We then use standard to convert - the free variables into unifiable variables and unify them with - (roughly) the definition of the accessor. *) - fun surject_prf () = let + (*We need a surjection property r = (| f = f r, g = g r ... |) + to prove other theorems. We haven't given names to the accessors + f, g etc yet however, so we generate an ext structure with + free variables as all arguments and allow the introduction tactic to + operate on it as far as it can. We then use standard to convert + the free variables into unifiable variables and unify them with + (roughly) the definition of the accessor.*) + fun surject_prf () = + let val cterm_ext = cterm_of defs_thy ext; - val start = named_cterm_instantiate [("y", cterm_ext)] - surject_assist_idE; - val tactic1 = simp_tac (HOL_basic_ss addsimps [ext_def]) 1 - THEN REPEAT_ALL_NEW intros_tac 1 - val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1); - val [halfway] = Seq.list_of (tactic1 start); - val [surject] = Seq.list_of (tactic2 (standard halfway)); + val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE; + val tactic1 = + simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN + REPEAT_ALL_NEW intros_tac 1; + val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1); + val [halfway] = Seq.list_of (tactic1 start); (* FIXME Seq.lift_of ?? *) + val [surject] = Seq.list_of (tactic2 (standard halfway)); (* FIXME Seq.lift_of ?? *) in surject end; val surject = timeit_msg "record extension surjective proof:" surject_prf; fun split_meta_prf () = - prove_standard [] split_meta_prop (fn prems => - EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1, - etac meta_allE 1, atac 1, - rtac (prop_subst OF [surject]) 1, - REPEAT (etac meta_allE 1), atac 1]); + prove_standard [] split_meta_prop + (fn prems => + EVERY + [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1, + etac meta_allE 1, atac 1, + rtac (prop_subst OF [surject]) 1, + REPEAT (etac meta_allE 1), atac 1]); val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf; fun induct_prf () = - let val (assm, concl) = induct_prop - in prove_standard [assm] concl (fn {prems, ...} => - EVERY [cut_rules_tac [split_meta RS meta_iffD2] 1, - resolve_tac prems 2, - asm_simp_tac HOL_ss 1]) end; + let val (assm, concl) = induct_prop in + prove_standard [assm] concl + (fn {prems, ...} => + EVERY + [cut_rules_tac [split_meta RS meta_iffD2] 1, + resolve_tac prems 2, + asm_simp_tac HOL_ss 1]) + end; val induct = timeit_msg "record extension induct proof:" induct_prf; - val ([inject',induct',surjective',split_meta'], - thm_thy) = + val ([inject', induct', surjective', split_meta'], thm_thy) = defs_thy |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name)) [("ext_inject", inject), ("ext_induct", induct), ("ext_surjective", surject), - ("ext_split", split_meta)] - - in (thm_thy,extT,induct',inject',split_meta',ext_def) - end; - -fun chunks [] [] = [] - | chunks [] xs = [xs] - | chunks (l::ls) xs = Library.take (l,xs)::chunks ls (Library.drop (l,xs)); + ("ext_split", split_meta)]; + + in (thm_thy, extT, induct', inject', split_meta', ext_def) end; + +fun chunks [] [] = [] + | chunks [] xs = [xs] + | chunks (l :: ls) xs = Library.take (l, xs) :: chunks ls (Library.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 -*) + | 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 = - fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT; - + fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT; fun obj_to_meta_all thm = let - fun E thm = case (SOME (spec OF [thm]) handle THM _ => NONE) of - SOME thm' => E thm' - | NONE => thm; + fun E thm = (* FIXME proper name *) + (case (SOME (spec OF [thm]) handle THM _ => NONE) of + SOME thm' => E thm' + | NONE => thm); val th1 = E thm; val th2 = Drule.forall_intr_vars th1; in th2 end; @@ -1902,13 +1975,9 @@ val prop = Thm.prop_of thm; val params = Logic.strip_params prop; val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop); - val ct = cterm_of thy - (HOLogic.mk_Trueprop (HOLogic.list_all (params, concl))); + val ct = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.list_all (params, concl))); val thm' = Seq.hd (REPEAT (rtac allI 1) (Thm.trivial ct)); - in - Thm.implies_elim thm' thm - end; - + in Thm.implies_elim thm' thm end; (* record_definition *) @@ -1922,7 +1991,8 @@ val full = Sign.full_bname_path thy bname; val base = Long_Name.base_name; - val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields); + val (bfields, field_syntax) = + split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields); val parent_fields = List.concat (map #fields parents); val parent_chunks = map (length o #fields) parents; @@ -1961,15 +2031,17 @@ 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 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 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)]; + val all_named_vars_more = all_named_vars @ [(full_moreN, more)]; + (* 1st stage: extension_thy *) - val (extension_thy,extT,ext_induct,ext_inject,ext_split,ext_def) = + + val (extension_thy, extT, ext_induct, ext_inject, ext_split, ext_def) = thy |> Sign.add_path bname |> extension_definition full extN fields names alphas_ext zeta moreT more vars; @@ -1977,26 +2049,25 @@ val _ = timing_msg "record preparing definitions"; 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 = Library.foldl (op ^) ("",extension_names); + 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 = Library.foldl (op ^) ("", extension_names); (* FIXME implode!? *) fun rec_schemeT n = mk_recordT (map #extension (prune n parents)) extT; val rec_schemeT0 = rec_schemeT 0; fun recT n = - let val (c,Ts) = extension - in mk_recordT (map #extension (prune n parents)) (Type (c,subst_last HOLogic.unitT Ts)) - end; + let val (c, Ts) = extension + in mk_recordT (map #extension (prune n parents)) (Type (c, subst_last HOLogic.unitT Ts)) 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 = - List.foldr mk_ext' more (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args'))) + let + val (args', more) = chop_last args; + fun mk_ext' (((name, T), args), more) = mk_ext (name, T) (args @ [more]); + fun build Ts = + List.foldr mk_ext' more (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args'))); in if more = HOLogic.unit then build (map recT (0 upto parent_len)) @@ -2004,7 +2075,7 @@ end; val r_rec0 = mk_rec all_vars_more 0; - val r_rec_unit0 = mk_rec (all_vars@[HOLogic.unit]) 0; + val r_rec_unit0 = mk_rec (all_vars @ [HOLogic.unit]) 0; fun r n = Free (rN, rec_schemeT n) val r0 = r 0; @@ -2012,26 +2083,27 @@ val r_unit0 = r_unit 0; val w = Free (wN, rec_schemeT 0) + (* prepare print translation functions *) + val field_tr's = print_translation (distinct (op =) (maps external_names (full_moreN :: names))); val adv_ext_tr's = - let - val trnames = external_names extN; - in map (gen_record_tr') trnames end; + let val trnames = external_names extN + in map (gen_record_tr') trnames end; val adv_record_type_abbr_tr's = - let val trnames = external_names (hd extension_names); - val lastExt = unsuffix ext_typeN (fst extension); - in map (gen_record_type_abbr_tr' name alphas zeta lastExt rec_schemeT0) trnames - end; + let + val trnames = external_names (hd extension_names); + val lastExt = unsuffix ext_typeN (fst extension); + in map (gen_record_type_abbr_tr' name alphas zeta lastExt rec_schemeT0) trnames end; val adv_record_type_tr's = - let val trnames = if parent_len > 0 then external_names extN else []; - (* avoid conflict with adv_record_type_abbr_tr's *) - in map (gen_record_type_tr') trnames - end; + let + val trnames = if parent_len > 0 then external_names extN else []; + (*avoid conflict with adv_record_type_abbr_tr's*) + in map (gen_record_type_tr') trnames end; (* prepare declarations *) @@ -2046,13 +2118,14 @@ (* prepare definitions *) fun parent_more s = - if null parents then s - else mk_sel s (Long_Name.qualify (#name (List.last parents)) moreN, extT); + if null parents then s + else mk_sel s (Long_Name.qualify (#name (List.last parents)) moreN, extT); fun parent_more_upd v s = - if null parents then v$s - else let val mp = Long_Name.qualify (#name (List.last parents)) moreN; - in mk_upd updateN mp v s end; + if null parents then v $ s + else + let val mp = Long_Name.qualify (#name (List.last parents)) moreN; + in mk_upd updateN mp v s end; (*record (scheme) type abbreviation*) val recordT_specs = @@ -2062,64 +2135,66 @@ val ext_defs = ext_def :: map #extdef parents; val intros_tac = IsTupleSupport.istuple_intros_tac extension_thy; - (* Theorems from the istuple intros. - This is complex enough to deserve a full comment. - By unfolding ext_defs from r_rec0 we create a tree of constructor - calls (many of them Pair, but others as well). The introduction - rules for update_accessor_eq_assist can unify two different ways - on these constructors. If we take the complete result sequence of - running a the introduction tactic, we get one theorem for each upd/acc - pair, from which we can derive the bodies of our selector and - updator and their convs. *) - fun get_access_update_thms () = let - val r_rec0_Vars = let - (* pick variable indices of 1 to avoid possible variable - collisions with existing variables in updacc_eq_triv *) + (*Theorems from the istuple intros. + This is complex enough to deserve a full comment. + By unfolding ext_defs from r_rec0 we create a tree of constructor + calls (many of them Pair, but others as well). The introduction + rules for update_accessor_eq_assist can unify two different ways + on these constructors. If we take the complete result sequence of + running a the introduction tactic, we get one theorem for each upd/acc + pair, from which we can derive the bodies of our selector and + updator and their convs.*) + fun get_access_update_thms () = + let + val r_rec0_Vars = + let + (*pick variable indices of 1 to avoid possible variable + collisions with existing variables in updacc_eq_triv*) fun to_Var (Free (c, T)) = Var ((c, 1), T); in mk_rec (map to_Var all_vars_more) 0 end; val cterm_rec = cterm_of extension_thy r_rec0; val cterm_vrs = cterm_of extension_thy r_rec0_Vars; - val insts = [("v", cterm_rec), ("v'", cterm_vrs)]; - val init_thm = named_cterm_instantiate insts updacc_eq_triv; - val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1; - val tactic = simp_tac (HOL_basic_ss addsimps ext_defs) 1 - THEN REPEAT (intros_tac 1 ORELSE terminal); - val updaccs = Seq.list_of (tactic init_thm); + val insts = [("v", cterm_rec), ("v'", cterm_vrs)]; + val init_thm = named_cterm_instantiate insts updacc_eq_triv; + val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1; + val tactic = + simp_tac (HOL_basic_ss addsimps ext_defs) 1 THEN + REPEAT (intros_tac 1 ORELSE terminal); + val updaccs = Seq.list_of (tactic init_thm); (* FIXME Seq.lift_of *) in (updaccs RL [updacc_accessor_eqE], updaccs RL [updacc_updator_eqE], updaccs RL [updacc_cong_from_eq]) end; val (accessor_thms, updator_thms, upd_acc_cong_assists) = - timeit_msg "record getting tree access/updates:" get_access_update_thms; + timeit_msg "record getting tree access/updates:" get_access_update_thms; fun lastN xs = List.drop (xs, parent_fields_len); (*selectors*) - fun mk_sel_spec ((c,T), thm) = + fun mk_sel_spec ((c, T), thm) = let - val (acc $ arg) = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop - o Envir.beta_eta_contract o concl_of) thm; - val _ = if (arg aconv r_rec0) then () - else raise TERM ("mk_sel_spec: different arg", [arg]); + val acc $ arg = + (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Envir.beta_eta_contract o concl_of) thm; + val _ = + if (arg aconv r_rec0) then () + else raise TERM ("mk_sel_spec: different arg", [arg]); in - Const (mk_selC rec_schemeT0 (c,T)) - :== acc + Const (mk_selC rec_schemeT0 (c, T)) :== acc end; val sel_specs = map mk_sel_spec (fields_more ~~ lastN accessor_thms); + (*updates*) - - fun mk_upd_spec ((c,T), thm) = + fun mk_upd_spec ((c, T), thm) = let - val (upd $ _ $ arg) = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop - o Envir.beta_eta_contract o concl_of) thm; - val _ = if (arg aconv r_rec0) then () - else raise TERM ("mk_sel_spec: different arg", [arg]); - in Const (mk_updC updateN rec_schemeT0 (c,T)) - :== upd - end; + val (upd $ _ $ arg) = + (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Envir.beta_eta_contract o concl_of) thm; + val _ = + if (arg aconv r_rec0) then () + else raise TERM ("mk_sel_spec: different arg", [arg]); + in Const (mk_updC updateN rec_schemeT0 (c, T)) :== upd end; val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms); (*derived operations*) @@ -2133,14 +2208,14 @@ 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 *) fun mk_defs () = extension_thy - |> Sign.add_trfuns - ([],[],field_tr's, []) + |> Sign.add_trfuns ([], [], field_tr's, []) |> Sign.add_advanced_trfuns - ([],[],adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's,[]) + ([], [], adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's, []) |> Sign.parent_path |> Sign.add_tyabbrs_i recordT_specs |> Sign.add_path bname @@ -2153,7 +2228,8 @@ ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) upd_specs) ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) [make_spec, fields_spec, extend_spec, truncate_spec]) - |-> (fn defs as ((sel_defs, upd_defs), derived_defs) => + |-> + (fn defs as ((sel_defs, upd_defs), derived_defs) => fold Code.add_default_eqn sel_defs #> fold Code.add_default_eqn upd_defs #> fold Code.add_default_eqn derived_defs @@ -2162,23 +2238,23 @@ timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:" mk_defs; - (* prepare propositions *) val _ = timing_msg "record preparing propositions"; - val P = Free (Name.variant all_variants "P", rec_schemeT0-->HOLogic.boolT); + val P = Free (Name.variant all_variants "P", rec_schemeT0 --> HOLogic.boolT); val C = Free (Name.variant all_variants "C", HOLogic.boolT); - val P_unit = Free (Name.variant all_variants "P", recT0-->HOLogic.boolT); + val P_unit = Free (Name.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; + 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 (Name.variant all_variants (base c ^ "'"),T-->T); - val n = parent_fields_len + i; - val args' = nth_map n (K (x'$nth all_vars_more n)) all_vars_more - in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end; + fun mk_upd_prop (i, (c, T)) = + let + val x' = Free (Name.variant all_variants (base c ^ "'"), T --> T); + val n = parent_fields_len + i; + val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more + in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end; val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more); (*induct*) @@ -2186,22 +2262,22 @@ 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)); + 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 + 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 (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 (HOLogic.mk_eq (r_unit0, r_rec_unit0)) ==> Trueprop C)) ==> Trueprop C; (*split*) @@ -2211,24 +2287,24 @@ (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0)) end; + (* FIXME eliminate old List.foldr *) + val split_object_prop = - let fun ALL vs t = List.foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) t vs - in (ALL [dest_Free r0] (P $ r0)) === (ALL (map dest_Free all_vars_more) (P $ r_rec0)) - end; - + let fun ALL vs t = List.foldr (fn ((v, T), t) => HOLogic.mk_all (v, T, t)) t vs + 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 = List.foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) t vs - in (EX [dest_Free r0] (P $ r0)) === (EX (map dest_Free all_vars_more) (P $ r_rec0)) - end; + let fun EX vs t = List.foldr (fn ((v, T), t) => HOLogic.mk_exists (v, T, t)) t vs + 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; + 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 *) @@ -2241,40 +2317,43 @@ val ss = get_simpset defs_thy; - fun sel_convs_prf () = map (prove_simp false ss - (sel_defs@accessor_thms)) sel_conv_props; + fun sel_convs_prf () = + map (prove_simp false ss (sel_defs @ accessor_thms)) sel_conv_props; val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf; fun sel_convs_standard_prf () = map standard sel_convs val sel_convs_standard = - timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf; - - fun upd_convs_prf () = map (prove_simp false ss - (upd_defs@updator_thms)) upd_conv_props; + timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf; + + fun upd_convs_prf () = + map (prove_simp false ss (upd_defs @ updator_thms)) upd_conv_props; val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf; fun upd_convs_standard_prf () = map standard upd_convs val upd_convs_standard = - timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf; - - fun get_upd_acc_congs () = let - val symdefs = map symmetric (sel_defs @ upd_defs); - val fold_ss = HOL_basic_ss addsimps symdefs; + timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf; + + fun get_upd_acc_congs () = + let + val symdefs = map symmetric (sel_defs @ upd_defs); + val fold_ss = HOL_basic_ss addsimps symdefs; val ua_congs = map (standard o simplify fold_ss) upd_acc_cong_assists; in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end; val (fold_congs, unfold_congs) = - timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs; + timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs; val parent_induct = if null parents then [] else [#induct (hd (rev parents))]; - fun induct_scheme_prf () = prove_standard [] induct_scheme_prop (fn _ => - (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])); + fun induct_scheme_prf () = + prove_standard [] induct_scheme_prop + (fn _ => + 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_scheme = timeit_msg "record induct_scheme proof:" induct_scheme_prf; fun induct_prf () = - let val (assm, concl) = induct_prop; - in + 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" @{thm unit.induct} 1 @@ -2284,81 +2363,91 @@ fun cases_scheme_prf_opt () = let - val (_$(Pvar$_)) = concl_of induct_scheme; - val ind = cterm_instantiate - [(cterm_of defs_thy Pvar, cterm_of defs_thy - (lambda w (HOLogic.imp$HOLogic.mk_eq(r0,w)$C)))] - induct_scheme; + val _ $ (Pvar $ _) = concl_of induct_scheme; + val ind = + cterm_instantiate + [(cterm_of defs_thy Pvar, cterm_of defs_thy + (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))] + induct_scheme; in standard (ObjectLogic.rulify (mp OF [ind, refl])) end; fun cases_scheme_prf_noopt () = - prove_standard [] cases_scheme_prop (fn _ => - 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]) + prove_standard [] cases_scheme_prop + (fn _ => + 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_scheme_prf = quick_and_dirty_prf cases_scheme_prf_noopt cases_scheme_prf_opt; val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf; fun cases_prf () = - prove_standard [] cases_prop (fn _ => - try_param_tac rN cases_scheme 1 - THEN simp_all_tac HOL_basic_ss [unit_all_eq1]); + prove_standard [] cases_prop + (fn _ => + try_param_tac rN cases_scheme 1 THEN + simp_all_tac HOL_basic_ss [unit_all_eq1]); val cases = timeit_msg "record cases proof:" cases_prf; - fun surjective_prf () = let - val leaf_ss = get_sel_upd_defs defs_thy - addsimps (sel_defs @ (o_assoc :: id_o_apps)); - val init_ss = HOL_basic_ss addsimps ext_defs; + fun surjective_prf () = + let + val leaf_ss = get_sel_upd_defs defs_thy addsimps (sel_defs @ (o_assoc :: id_o_apps)); + val init_ss = HOL_basic_ss addsimps ext_defs; in - prove_standard [] surjective_prop (fn prems => - (EVERY [rtac surject_assist_idE 1, - simp_tac init_ss 1, - REPEAT (intros_tac 1 ORELSE - (rtac surject_assistI 1 THEN - simp_tac leaf_ss 1))])) + prove_standard [] surjective_prop + (fn prems => + EVERY + [rtac surject_assist_idE 1, + simp_tac init_ss 1, + REPEAT (intros_tac 1 ORELSE (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))]) end; val surjective = timeit_msg "record surjective proof:" surjective_prf; fun split_meta_prf () = - prove false [] split_meta_prop (fn prems => - EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1, - etac meta_allE 1, atac 1, - rtac (prop_subst OF [surjective]) 1, - REPEAT (etac meta_allE 1), atac 1]); + prove false [] split_meta_prop + (fn prems => + EVERY + [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1, + etac meta_allE 1, atac 1, + rtac (prop_subst OF [surjective]) 1, + REPEAT (etac meta_allE 1), atac 1]); val split_meta = timeit_msg "record split_meta proof:" split_meta_prf; fun split_meta_standardise () = standard split_meta; - val split_meta_standard = timeit_msg "record split_meta standard:" - split_meta_standardise; + val split_meta_standard = + timeit_msg "record split_meta standard:" split_meta_standardise; fun split_object_prf_opt () = let - val cPI= cterm_of defs_thy (lambda r0 (Trueprop (P$r0))); - val (_$Abs(_,_,P$_)) = fst (Logic.dest_equals (concl_of split_meta_standard)); + val cPI= cterm_of defs_thy (lambda r0 (Trueprop (P $ r0))); + val _ $ Abs (_, _, P $ _) = fst (Logic.dest_equals (concl_of split_meta_standard)); val cP = cterm_of defs_thy P; - val split_meta' = cterm_instantiate [(cP,cPI)] split_meta_standard; - val (l,r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop); + val split_meta' = cterm_instantiate [(cP, cPI)] split_meta_standard; + val (l, r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop); val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l); val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r); - val thl = assume cl (*All r. P r*) (* 1 *) - |> obj_to_meta_all (*!!r. P r*) - |> equal_elim split_meta' (*!!n m more. P (ext n m more)*) - |> meta_to_obj_all (*All n m more. P (ext n m more)*) (* 2*) - |> implies_intr cl (* 1 ==> 2 *) - val thr = assume cr (*All n m more. P (ext n m more)*) - |> obj_to_meta_all (*!!n m more. P (ext n m more)*) - |> equal_elim (symmetric split_meta') (*!!r. P r*) - |> meta_to_obj_all (*All r. P r*) - |> implies_intr cr (* 2 ==> 1 *) + val thl = + assume cl (*All r. P r*) (* 1 *) + |> obj_to_meta_all (*!!r. P r*) + |> equal_elim split_meta' (*!!n m more. P (ext n m more)*) + |> meta_to_obj_all (*All n m more. P (ext n m more)*) (* 2*) + |> implies_intr cl (* 1 ==> 2 *) + val thr = + assume cr (*All n m more. P (ext n m more)*) + |> obj_to_meta_all (*!!n m more. P (ext n m more)*) + |> equal_elim (symmetric split_meta') (*!!r. P r*) + |> meta_to_obj_all (*All r. P r*) + |> implies_intr cr (* 2 ==> 1 *) in standard (thr COMP (thl COMP iffI)) end; fun split_object_prf_noopt () = - prove_standard [] split_object_prop (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]); + prove_standard [] split_object_prop + (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]); val split_object_prf = quick_and_dirty_prf split_object_prf_noopt split_object_prf_opt; val split_object = timeit_msg "record split_object proof:" split_object_prf; @@ -2366,30 +2455,33 @@ fun split_ex_prf () = let - val ss = HOL_basic_ss addsimps [not_ex RS sym, Not_eq_iff]; - val P_nm = fst (dest_Free P); + val ss = HOL_basic_ss addsimps [not_ex RS sym, Not_eq_iff]; + val P_nm = fst (dest_Free P); val not_P = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0))); - val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object; - val so'' = simplify ss so'; + val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object; + val so'' = simplify ss so'; in prove_standard [] split_ex_prop (fn prems => resolve_tac [so''] 1) end; val split_ex = timeit_msg "record split_ex proof:" split_ex_prf; fun equality_tac thms = - let val (s'::s::eqs) = rev thms; - val ss' = ss addsimps (s'::s::sel_convs_standard); - val eqs' = map (simplify ss') eqs; - in simp_tac (HOL_basic_ss addsimps (s'::s::eqs')) 1 end; - - fun equality_prf () = prove_standard [] equality_prop (fn {context, ...} => - fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in - st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1 - THEN res_inst_tac context [((rN, 0), s')] cases_scheme 1 - THEN (Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1)) - (* simp_all_tac ss (sel_convs) would also work but is less efficient *) - end); - val equality = timeit_msg "record equality proof:" equality_prf; + let + val s' :: s :: eqs = rev thms; + val ss' = ss addsimps (s' :: s :: sel_convs_standard); + val eqs' = map (simplify ss') eqs; + in simp_tac (HOL_basic_ss addsimps (s' :: s :: eqs')) 1 end; + + fun equality_prf () = + prove_standard [] equality_prop (fn {context, ...} => + fn st => + let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in + st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1 THEN + res_inst_tac context [((rN, 0), s')] cases_scheme 1 THEN + Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1) + (*simp_all_tac ss (sel_convs) would also work but is less efficient*) + end); + val equality = timeit_msg "record equality proof:" equality_prf; val ((([sel_convs', upd_convs', sel_defs', upd_defs', fold_congs', unfold_congs', @@ -2404,7 +2496,7 @@ ("update_defs", upd_defs), ("fold_congs", fold_congs), ("unfold_congs", unfold_congs), - ("splits", [split_meta_standard,split_object,split_ex]), + ("splits", [split_meta_standard, split_object, split_ex]), ("defs", derived_defs)] ||>> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name)) [("surjective", surjective), @@ -2415,7 +2507,6 @@ (("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 sel_upd_defs = sel_defs' @ upd_defs'; val iffs = [ext_inject] @@ -2432,19 +2523,18 @@ |> add_record_equalities extension_id equality' |> add_extinjects ext_inject |> add_extsplit extension_name ext_split - |> 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]) + |> 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]) |> Sign.parent_path; - in final_thy - end; + in final_thy end; (* add_record *) -(*we do all preparations and error checks here, deferring the real - work to record_definition*) +(*We do all preparations and error checks here, deferring the real + work to record_definition.*) fun gen_add_record prep_typ prep_raw_parent quiet_mode (params, bname) raw_parent raw_fields thy = let val _ = Theory.requires thy "Record" "record definitions"; @@ -2520,8 +2610,9 @@ val errs = err_dup_record @ err_dup_parms @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields @ err_dup_sorts; + + val _ = if null errs then () else error (cat_lines errs); in - if null errs then () else error (cat_lines errs) ; thy |> record_definition (args, bname) parent parents bfields end handle ERROR msg => cat_error msg ("Failed to define record " ^ quote bname);