| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Tools/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 93 kB |
|
Quelle record.ML Sprache: SML |
|||||||||
|
(* Title: HOL/Tools/record.ML
Author: Wolfgang Naraschewski, TU Muenchen Author: Markus Wenzel, TU Muenchen Author: Norbert Schirmer, TU Muenchen Author: Norbert Schirmer, Apple, 2022 Author: Thomas Sewell, NICTA Extensible records with structural subtyping. *) signature RECORD = sig val type_abbr: bool Config.T val type_as_fields: bool Config.T val timing: bool Config.T type info = {args: (string * sort) list, parent: (typ list * string) option, fields: (string * typ) list, extension: (string * typ list), ext_induct: thm, ext_inject: thm, ext_surjective: thm, ext_split: thm, ext_def: thm, select_convs: thm list, update_convs: thm list, select_defs: thm list, update_defs: thm lis fold_congs: thm list, unfold_congs: thm list, splits: thm list, defs: thm list, surjective: thm, equality: thm, induct_scheme: thm, induct: thm, cases_scheme: thm, cases: thm, simps: thm list, iffs: thm list} val get_info: theory -> string -> info option val the_info: theory -> string -> info val get_hierarchy: theory -> (string * typ list) -> (string * ((string * sort) * typ) list) list val add_record: {overloaded: bool} -> (string * sort) list * binding -> (typ list * string) option -> (binding * typ * mixfix) list -> theory -> theory 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_parent: theory -> string -> (typ list * string) option val get_extension: theory -> string -> (string * typ list) option val get_extinjects: theory -> thm list val get_simpset: theory -> simpset val simproc: simproc val eq_simproc: simproc val upd_simproc: simproc val split_simproc: (term -> int) -> simproc val ex_sel_eq_simproc: simproc val split_tac: Proof.context -> int -> tactic val split_simp_tac: Proof.context -> thm list -> (term -> int) -> int -> tactic val split_wrapper: string * (Proof.context -> wrapper) val pretty_record: Proof.context -> typ -> Pretty.T val pretty_record_cmd: Proof.context -> string -> Pretty.T val codegen: bool Config.T val sort_updates: bool Config.T val updateN: string val ext_typeN: string val extN: string end; signature ISO_TUPLE_SUPPORT = sig val add_iso_tuple_type: {overloaded: bool} -> binding * (string * sort) list -> typ * typ -> theory -> (term * term) * theory val mk_cons_tuple: term * term -> term val dest_cons_tuple: term -> term * term val iso_tuple_intros_tac: Proof.context -> int -> tactic end; structure Iso_Tuple_Support: ISO_TUPLE_SUPPORT = struct val isoN = "_Tuple_Iso"; val iso_tuple_intro = @{thm isomorphic_tuple_intro}; val iso_tuple_intros = Bires.build_net @{thms isomorphic_tuple.intros}; val tuple_iso_tuple = (\<^const_name>\<open>Record.tuple_iso_tuple\<close>, @{thm tuple_iso structure Iso_Tuple_Thms = Theory_Data ( type T = thm Symtab.table; val empty = Symtab.make [tuple_iso_tuple]; fun merge data = Symtab.merge Thm.eq_thm_prop data; (* FIXME handle Symtab.DUP ?? *) ); fun get_typedef_info tyco vs (({rep_type, Abs_name, ...}, {Rep_inject, Abs_inverse, ... }) : Typedef.info) thy = let val exists_thm = @{thm UNIV_I} |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy (Logic.varifyT_global rep_type)) val proj_constr = Abs_inverse OF [exists_thm]; val absT = Type (tyco, map TFree vs); in thy |> pair (tyco, ((Rep_inject, proj_constr), Const (Abs_name, rep_type --> absT), absT)) end fun do_typedef overloaded raw_tyco repT raw_vs thy = let val ctxt = Proof_Context.init_global thy |> Variable.declare_typ repT; val vs = map (Proof_Context.check_tfree ctxt) raw_vs; in thy |> Named_Target.theory_map_result (apsnd o Typedef.transform_info) (Typedef.add_typedef overloaded (raw_tyco, vs, NoSyn) (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' @{thms UNIV_witness} 1)) |-> (fn (tyco, info) => get_typedef_info tyco vs info) end; fun mk_cons_tuple (t, u) = let val (A, B) = apply2 fastype_of (t, u) in \<^Const>\<open>iso_tuple_cons \<^Type>\<open>prod A B\<close> A B for \<^Const>\<open>tuple_iso_tu fun dest_cons_tuple \<^Const_>\<open>iso_tuple_cons _ _ _ for \<open>Const _\<close> t u\<close> = (t, | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]); fun add_iso_tuple_type overloaded (b, alphas) (leftT, rightT) thy = let val repT = HOLogic.mk_prodT (leftT, rightT); val ((_, ((rep_inject, abs_inverse), absC, absT)), typ_thy) = thy |> do_typedef overloaded b repT alphas ||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*) val typ_ctxt = Proof_Context.init_global typ_thy; (*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 infer_instantiate typ_ctxt [(("abst", 0), Thm.cterm_of typ_ctxt absC)] iso_tuple_intro; val (_, body) = Logic.dest_equals (List.last (Thm.prems_of intro_inst)); val isomT = fastype_of body; val isom_binding = Binding.suffix_name isoN b; val isom_name = Sign.full_name typ_thy isom_binding; val isom = Const (isom_name, isomT); val (isom_def, cdef_thy) = typ_thy |> Sign.declare_const_global ((isom_binding, isomT), NoSyn) |> snd |> Global_Theory.add_def (Binding.concealed (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)) val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro)); val cons = \<^Const>\<open>iso_tuple_cons absT leftT rightT\<close>; val thm_thy = cdef_thy |> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple)) |> Sign.restore_naming thy in ((isom, cons $ isom), thm_thy) end; fun iso_tuple_intros_tac ctxt = Bires.resolve_from_net_tac ctxt iso_tuple_intros THEN' CSUBGOAL (fn (cgoal, i) => let val goal = Thm.term_of cgoal; val isthms = Iso_Tuple_Thms.get (Proof_Context.theory_of ctxt); fun err s t = raise TERM ("iso_tuple_intros_tac: " ^ s, [t]); val goal' = Envir.beta_eta_contract goal; val is = (case goal' of \<^Const_>\<open>Trueprop for \<^Const>\<open>isomorphic_tuple _ _ _ for \<open>Const is\<close>\<clo | _ => err "unexpected goal format" goal'); val isthm = (case Symtab.lookup isthms (#1 is) of SOME isthm => isthm | NONE => err "no thm found for constant" (Const is)); in resolve_tac ctxt [isthm] i end); end; structure Record: RECORD = struct val surject_assistI = @{thm iso_tuple_surjective_proof_assistI}; val surject_assist_idE = @{thm iso_tuple_surjective_proof_assist_idE}; val updacc_accessor_eqE = @{thm update_accessor_accessor_eqE}; val updacc_updator_eqE = @{thm update_accessor_updator_eqE}; val updacc_eq_idI = @{thm iso_tuple_update_accessor_eq_assist_idI}; val updacc_eq_triv = @{thm iso_tuple_update_accessor_eq_assist_triv}; val updacc_foldE = @{thm update_accessor_congruence_foldE}; val updacc_unfoldE = @{thm update_accessor_congruence_unfoldE}; val updacc_noopE = @{thm update_accessor_noopE}; val updacc_noop_compE = @{thm update_accessor_noop_compE}; val updacc_cong_idI = @{thm update_accessor_cong_assist_idI}; val updacc_cong_triv = @{thm update_accessor_cong_assist_triv}; val updacc_cong_from_eq = @{thm iso_tuple_update_accessor_cong_from_eq}; val codegen = Attrib.setup_config_bool \<^binding>\<open>record_codegen\<close> (K true); val sort_updates = Attrib.setup_config_bool \<^binding>\<open>record_sort_updates\<close> ( (** name components **) val rN = "r"; val wN = "w"; val moreN = "more"; val schemeN = "_scheme"; val ext_typeN = "_ext"; val inner_typeN = "_inner"; val extN ="_ext"; val updateN = "_update"; val makeN = "make"; val fields_selN = "fields"; val extendN = "extend"; val truncateN = "truncate"; (*** utilities ***) fun varifyT idx = map_type_tfree (fn (a, S) => TVar ((a, idx), S)); (* timing *) val timing = Attrib.setup_config_bool \<^binding>\<open>record_timing\<close> (K false); fun timeit_msg ctxt s x = if Config.get ctxt timing then (warning s; timeit x) else x (); fun timing_msg ctxt s = if Config.get ctxt timing then warning s else (); (* syntax *) val Trueprop = HOLogic.mk_Trueprop; infix 0 :== ===; infixr 0 ==>; val op :== = Misc_Legacy.mk_defpair; val op === = Trueprop o HOLogic.mk_eq; val op ==> = Logic.mk_implies; (* constructor *) fun mk_ext (name, T) ts = let val Ts = map fastype_of ts in list_comb (Const (suffix extN name, Ts ---> T), ts) end; (* selector *) 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; (* updates *) 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; (* types *) fun dest_recT (typ as Type (c_ext_type, Ts as (_ :: _))) = (case try (unsuffix ext_typeN) c_ext_type of NONE => raise TYPE ("Record.dest_recT", [typ], []) | SOME c => ((c, Ts), List.last Ts)) | dest_recT typ = raise TYPE ("Record.dest_recT", [typ], []); val is_recT = can dest_recT; fun dest_recTs T = let val ((c, Ts), U) = dest_recT T in (c, Ts) :: dest_recTs U 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; fun rec_id i T = let val rTs = dest_recTs T; val rTs' = if i < 0 then rTs else take i rTs; in implode (map #1 rTs') end; (*** extend theory by record definition ***) (** record info **) (* type info and parent_info *) type info = {args: (string * sort) list, parent: (typ list * string) option, fields: (string * typ) list, extension: (string * typ list), ext_induct: thm, ext_inject: thm, ext_surjective: thm, ext_split: thm, ext_def: thm, select_convs: thm list, update_convs: thm list, select_defs: thm list, update_defs: thm list, fold_congs: thm list, (* potentially used in L4.verified *) unfold_congs: thm list, (* potentially used in L4.verified *) splits: thm list, defs: thm list, surjective: thm, equality: thm, induct_scheme: thm, induct: thm, cases_scheme: thm, cases: thm, simps: thm list, iffs: thm list}; fun make_info args parent fields extension ext_induct ext_inject ext_surjective ext_split ext_def select_convs update_convs select_defs update_defs fold_congs unfold_congs splits defs surjective equality induct_scheme induct cases_scheme cases simps iffs : info = {args = args, parent = parent, fields = fields, extension = extension, ext_induct = ext_induct, ext_inject = ext_inject, ext_surjective = ext_surjective, ext_split = ext_split, ext_def = ext_def, select_convs = select_convs, update_convs = update_convs, select_defs = select_defs, update_defs = update_defs, fold_congs = fold_congs, unfold_congs = unfold_congs, splits = splits, defs = defs, surjective = surjective, equality = equality, induct_scheme = induct_scheme, induct = induct, cases_scheme = cases_scheme, cases = cases, simps = simps, iffs = iffs}; type parent_info = {name: string, fields: (string * typ) list, extension: (string * typ list), induct_scheme: thm, ext_def: thm}; fun make_parent_info name fields extension ext_def induct_scheme : parent_info = {name = name, fields = fields, extension = extension, ext_def = ext_def, induct_scheme = induct_scheme}; (* theory data *) type splits = {Pure_all: thm, All: thm, Ex: thm, induct_scheme: thm}; fun eq_splits (arg: splits * splits) = Thm.eq_thm (apply2 #Pure_all arg) andalso Thm.eq_thm (apply2 #All arg) andalso Thm.eq_thm (apply2 #Ex arg) andalso Thm.eq_thm (apply2 #induct_scheme arg); type data = {records: info Symtab.table, sel_upd: {selectors: (int * bool) Symtab.table, updates: string Symtab.table, simpset: simpset, defset: simpset}, equalities: thm Symtab.table, extinjects: thm list, extsplit: thm Symtab.table, (*maps extension name to split rule*) splits: splits Symtab.table, (*\<And>/\<forall>/\<exists>-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_data 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 }: data; structure Data = Theory_Data ( type T = data; val empty = make_data Symtab.empty {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss, defset = HOL_basic_ss} Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty; fun merge ({records = recs1, sel_upd = {selectors = sels1, updates = upds1, simpset = ss1, defset = ds1}, equalities = equalities1, extinjects = extinjects1, extsplit = extsplit1, splits = splits1, extfields = extfields1, fieldext = fieldext1}, {records = recs2, sel_upd = {selectors = sels2, updates = upds2, simpset = ss2, defset = ds2}, equalities = equalities2, extinjects = extinjects2, extsplit = extsplit2, splits = splits2, extfields = extfields2, fieldext = fieldext2}) = make_data (Symtab.merge (K true) (recs1, recs2)) {selectors = Symtab.merge (K true) (sels1, sels2), updates = Symtab.merge (K true) (upds1, upds2), simpset = Simplifier.merge_ss (ss1, ss2), defset = Simplifier.merge_ss (ds1, ds2)} (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2)) (Thm.merge_thms (extinjects1, extinjects2)) (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2)) (Symtab.merge eq_splits (splits1, splits2)) (Symtab.merge (K true) (extfields1, extfields2)) (Symtab.merge (K true) (fieldext1, fieldext2)); ); (* access 'records' *) val get_info = Symtab.lookup o #records o Data.get; fun the_info thy name = (case get_info thy name of SOME info => info | NONE => error ("Unknown record type " ^ quote name)); fun put_record name info = Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fiel make_data (Symtab.update (name, info) records) sel_upd equalities extinjects extsplit splits extfields fieldext); (* access 'sel_upd' *) val get_sel_upd = #sel_upd o Data.get; val is_selector = Symtab.defined o #selectors o get_sel_upd; val get_updates = Symtab.lookup o #updates o get_sel_upd; val get_simpset = #simpset o get_sel_upd; val get_sel_upd_defs = #defset o get_sel_upd; 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 thy = let val ctxt0 = Proof_Context.init_global thy; 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}, equalities, extinjects, extsplit, splits, extfields, fieldext} = Data.get thy; val data = make_data records {selectors = fold Symtab.update_new sels selectors, updates = fold Symtab.update_new upds updates, simpset = simpset_map ctxt0 (Simplifier.add_simps simps) simpset, defset = simpset_map ctxt0 (Simplifier.add_simps defs) defset} equalities extinjects extsplit splits extfields fieldext; in Data.put data thy end; (* access 'equalities' *) fun add_equalities name thm = Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fiel make_data records sel_upd (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext val get_equalities = Symtab.lookup o #equalities o Data.get; (* access 'extinjects' *) fun add_extinjects thm = Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fiel make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) extsplit splits extfields fieldext); val get_extinjects = rev o #extinjects o Data.get; (* access 'extsplit' *) fun add_extsplit name thm = Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fiel make_data records sel_upd equalities extinjects (Symtab.update_new (name, thm) extsplit) splits extfields fieldext); (* access 'splits' *) fun add_splits name thmP = Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fiel make_data records sel_upd equalities extinjects extsplit (Symtab.update_new (name, thmP) splits) extfields fieldext); val get_splits = Symtab.lookup o #splits o Data.get; (* parent/extension of named record *) val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o Data.get) val get_extension = Option.map #extension oo (Symtab.lookup o #records o Data.get); (* access 'extfields' *) fun add_extfields name fields = Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fiel make_data records sel_upd equalities extinjects extsplit splits (Symtab.update_new (name, fields) extfields) fieldext); val get_extfields = Symtab.lookup o #extfields o Data.get; fun get_extT_fields thy T = let val ((name, Ts), moreT) = dest_recT T; val recname = let val (nm :: _ :: rst) = rev (Long_Name.explode name) (* FIXME !? *) in Long_Name.implode (rev (nm :: rst)) end; val varifyT = varifyT (maxidx_of_typs (moreT :: Ts) + 1); val {records, extfields, ...} = Data.get thy; val (fields, (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) (#1 (split_last args) ~~ #1 (split_last Ts)) Vartab.emp val fields' = map (apsnd (Envir.norm_type subst o varifyT)) fields; in (fields', (more, moreT)) end; fun get_recT_fields thy T = let val (root_fields, (root_more, root_moreT)) = get_extT_fields thy T; val (rest_fields, rest_more) = if is_recT root_moreT then get_recT_fields thy root_moreT else ([], (root_more, root_moreT)); in (root_fields @ rest_fields, rest_more) end; (* access 'fieldext' *) fun add_fieldext extname_types fields = Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fiel let val fieldext' = fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext; in make_data records sel_upd equalities extinjects extsplit splits extfields fieldext' en val get_fieldext = Symtab.lookup o #fieldext o Data.get; (* parent records *) local fun add_parents _ NONE = I | add_parents thy (SOME (types, name)) = let fun err msg = error (msg ^ " parent record " ^ quote name); val {args, parent, ...} = (case get_info thy name of SOME info => info | NONE => err "Unknown"); val _ = if length types <> length args then err "Bad number of arguments for" else (); fun bad_inst ((x, S), T) = if Sign.of_sort thy (T, S) then NONE else SOME x val bads = map_filter bad_inst (args ~~ types); val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in"); val inst = args ~~ types; val subst = Term.map_type_tfree (the o AList.lookup (op =) inst); val parent' = Option.map (apfst (map subst)) parent; in cons (name, inst) #> add_parents thy parent' end; in fun get_hierarchy thy (name, types) = add_parents thy (SOME (types, name)) []; fun get_parent_info thy parent = add_parents thy parent [] |> map (fn (name, inst) => let val subst = Term.map_type_tfree (the o AList.lookup (op =) inst); val {fields, extension, induct_scheme, ext_def, ...} = the_info thy name; val fields' = map (apsnd subst) fields; val extension' = apsnd (map subst) extension; in make_parent_info name fields' extension' ext_def induct_scheme end); end; (** concrete syntax for records **) (* parse translations *) local fun split_args (field :: fields) ((name, arg) :: fargs) = if can (unsuffix name) field then let val (args, rest) = split_args fields fargs in (arg :: args, rest) end else raise Fail ("expecting field " ^ quote field ^ " but got " ^ quote name) | split_args [] (fargs as (_ :: _)) = ([], fargs) | split_args (_ :: _) [] = raise Fail "expecting more fields" | split_args _ _ = ([], []); fun field_type_tr ((Const (\<^syntax_const>\<open>_field_type\<close>, _) $ Const (name, _) $ ar (name, arg) | field_type_tr t = raise TERM ("field_type_tr", [t]); fun field_types_tr (Const (\<^syntax_const>\<open>_field_types\<close>, _) $ t $ u) = field_type_tr t :: field_types_tr u | field_types_tr t = [field_type_tr t]; fun record_field_types_tr more ctxt t = let val thy = Proof_Context.theory_of ctxt; fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]); fun mk_ext (fargs as (name, _) :: _) = (case get_fieldext thy (Proof_Context.intern_const ctxt name) of SOME (ext, alphas) => (case get_extfields thy ext of SOME fields => let val (fields', _) = split_last fields; val types = map snd fields'; val (args, rest) = split_args (map fst fields') fargs handle Fail msg => err msg; val argtypes = Syntax.check_typs ctxt (map Syntax_Phases.decode_typ args); val varifyT = varifyT (fold Term.maxidx_typ argtypes ~1 + 1); val vartypes = map varifyT types; val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty handle Type.TYPE_MATCH => err "type is no proper record (extension)"; val alphas' = map (Syntax_Phases.term_of_typ ctxt o Envir.norm_type subst o varifyT) (#1 (split_last alphas)); val more' = mk_ext rest; in list_comb (Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more']) end | NONE => err ("no fields defined for " ^ quote ext)) | NONE => err (quote name ^ " is no proper field")) | mk_ext [] = more; in mk_ext (field_types_tr t) end; fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const \<^type_syntax>\<open>uni | record_type_tr _ ts = raise TERM ("record_type_tr", ts); fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t | record_type_scheme_tr _ ts = raise TERM ("record_type_scheme_tr", ts); fun field_tr ((Const (\<^syntax_const>\<open>_field\<close>, _) $ Const (name, _) $ arg)) = (name, | field_tr t = raise TERM ("field_tr", [t]); fun fields_tr (Const (\<^syntax_const>\<open>_fields\<close>, _) $ t $ u) = field_tr t :: fields_tr | fields_tr t = [field_tr t]; fun record_fields_tr more ctxt t = let val thy = Proof_Context.theory_of ctxt; fun err msg = raise TERM ("Error in record input: " ^ msg, [t]); fun mk_ext (fargs as (name, _) :: _) = (case get_fieldext thy (Proof_Context.intern_const ctxt name) of SOME (ext, _) => (case get_extfields thy ext of SOME fields => let val (args, rest) = split_args (map fst (fst (split_last fields))) fargs handle Fail msg => err msg; val more' = mk_ext rest; in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end | NONE => err ("no fields defined for " ^ quote ext)) | NONE => err (quote name ^ " is no proper field")) | mk_ext [] = more; in mk_ext (fields_tr t) end; fun record_tr ctxt [t] = record_fields_tr (Syntax.const \<^const_syntax>\<open>Unity\<close>) | record_tr _ ts = raise TERM ("record_tr", ts); fun record_scheme_tr ctxt [t, more] = record_fields_tr more ctxt t | record_scheme_tr _ ts = raise TERM ("record_scheme_tr", ts); fun field_update_tr (Const (\<^syntax_const>\<open>_field_update\<close>, _) $ Const (name, _) Syntax.const (suffix updateN name) $ Abs (Name.uu_, dummyT, arg) | field_update_tr t = raise TERM ("field_update_tr", [t]); fun field_updates_tr (Const (\<^syntax_const>\<open>_field_updates\<close>, _) $ t $ u) = field_update_tr t :: field_updates_tr u | field_updates_tr t = [field_update_tr t]; fun record_update_tr [t, u] = fold (curry op $) (field_updates_tr u) t | record_update_tr ts = raise TERM ("record_update_tr", ts); in val _ = Theory.setup (Sign.parse_translation [(\<^syntax_const>\<open>_record_update\<close>, K record_update_tr), (\<^syntax_const>\<open>_record\<close>, record_tr), (\<^syntax_const>\<open>_record_scheme\<close>, record_scheme_tr), (\<^syntax_const>\<open>_record_type\<close>, record_type_tr), (\<^syntax_const>\<open>_record_type_scheme\<close>, record_type_scheme_tr)]); end; (* print translations *) val type_abbr = Attrib.setup_config_bool \<^binding>\<open>record_type_abbr\<close> (K true) val type_as_fields = Attrib.setup_config_bool \<^binding>\<open>record_type_as_fields\<cl local (* FIXME early extern (!??) *) (* FIXME Syntax.free (??) *) fun field_type_tr' (c, t) = Syntax.const \<^syntax_const>\ fun field_types_tr' (t, u) = Syntax.const \<^syntax_const>\ fun record_type_tr' ctxt t = let val thy = Proof_Context.theory_of ctxt; val T = Syntax_Phases.decode_typ t; val varifyT = varifyT (Term.maxidx_of_typ T + 1); fun strip_fields T = (case T of Type (ext, args as _ :: _) => (case try (unsuffix ext_typeN) ext of SOME ext' => (case get_extfields thy ext' of SOME (fields as (x, _) :: _) => (case get_fieldext thy x of SOME (_, alphas) => (let val (f :: fs, _) = split_last fields; val fields' = apfst (Proof_Context.extern_const ctxt) f :: map (apfst Long_Name.base_name) fs; val (args', more) = split_last args; val alphavars = map varifyT (#1 (split_last alphas)); val subst = Type.raw_matches (alphavars, args') Vartab.empty; val fields'' = (map o apsnd) (Envir.norm_type subst o varifyT) fields'; in fields'' @ strip_fields more end handle Type.TYPE_MATCH => [("", T)]) | _ => [("", T)]) | _ => [("", T)]) | _ => [("", T)]) | _ => [("", T)]); val (fields, (_, moreT)) = split_last (strip_fields T); val _ = null fields andalso raise Match; val u = foldr1 field_types_tr' (map (field_type_tr' o apsnd (Syntax_Phases.term_of_typ ctxt)) fields); in if not (Config.get ctxt type_as_fields) orelse null fields then raise Match else if moreT = HOLogic.unitT then Syntax.const \<^syntax_const>\<open>_record_type\<close> $ u else Syntax.const \<^syntax_const>\<open>_record_type_scheme\<close> $ u $ Syntax_Phases.term_of_typ ctxt moreT end; (*try to reconstruct the record name type abbreviation from the (nested) extension types*) fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm = let val T = Syntax_Phases.decode_typ tm; val varifyT = varifyT (maxidx_of_typ T + 1); fun mk_type_abbr subst name args = let val abbrT = Type (name, map (varifyT o TFree) args) in Syntax_Phases.term_of_typ ctxt (Envir.norm_type subst abbrT) end; fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty; in if Config.get ctxt type_abbr then (case last_extT T of SOME (name, _) => if name = last_ext then let val subst = match schemeT T in if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree zeta))) then mk_type_abbr subst abbr alphas else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta]) end handle Type.TYPE_MATCH => record_type_tr' ctxt tm else raise Match (*give print translation of specialised record a chance*) | _ => raise Match) else record_type_tr' ctxt tm end; in fun record_ext_type_tr' name = let val ext_type_name = Lexicon.mark_type (suffix ext_typeN name); fun tr' ctxt ts = record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts)); in (ext_type_name, tr') end; fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name = let val ext_type_name = Lexicon.mark_type (suffix ext_typeN name); fun tr' ctxt ts = record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt (list_comb (Syntax.const ext_type_name, ts)); in (ext_type_name, tr') end; end; local (* FIXME Syntax.free (??) *) fun field_tr' (c, t) = Syntax.const \<^syntax_const>\ fun fields_tr' (t, u) = Syntax.const \<^syntax_const>\ fun record_tr' ctxt t = let val thy = Proof_Context.theory_of ctxt; fun strip_fields t = (case strip_comb t of (Const (ext, _), args as (_ :: _)) => (case try (Lexicon.unmark_const o unsuffix extN) ext of SOME ext' => (case get_extfields thy ext' of SOME fields => (let val (f :: fs, _) = split_last (map fst fields); val fields' = Proof_Context.extern_const ctxt f :: map Long_Name.base_name fs; val (args', more) = split_last args; in (fields' ~~ args') @ strip_fields more end handle ListPair.UnequalLengths => [("", t)]) | NONE => [("", t)]) | NONE => [("", t)]) | _ => [("", t)]); val (fields, (_, more)) = split_last (strip_fields t); val _ = null fields andalso raise Match; val u = foldr1 fields_tr' (map field_tr' fields); in (case more of Const (\<^const_syntax>\<open>Unity\<close>, _) => Syntax.const \<^syntax_const>\<open>_record\<c | _ => Syntax.const \<^syntax_const>\<open>_record_scheme\<close> $ u $ more) end; in fun record_ext_tr' name = let val ext_name = Lexicon.mark_const (name ^ extN); fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts)); in (ext_name, tr') end; end; local fun dest_update ctxt c = (case try Lexicon.unmark_const c of SOME d => try (unsuffix updateN) (Proof_Context.extern_const ctxt d) | NONE => NONE); fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) = (case dest_update ctxt c of SOME name => (case try Syntax_Trans.const_abs_tr' k of SOME t => apfst (cons (Syntax.const \<^syntax_const>\<open>_field_update\<close> $ Syntax.free name $ t) (field_updates_tr' ctxt u) | NONE => ([], tm)) | NONE => ([], tm)) | field_updates_tr' _ tm = ([], tm); fun record_update_tr' ctxt tm = (case field_updates_tr' ctxt tm of ([], _) => raise Match | (ts, u) => Syntax.const \<^syntax_const>\<open>_record_update\<close> $ u $ foldr1 (fn (v, w) => Syntax.const \<^syntax_const>\<open>_field_updates\<close> $ v $ w) (rev ts)); in fun field_update_tr' name = let val update_name = Lexicon.mark_const (name ^ updateN); fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u) | tr' _ _ = raise Match; in (update_name, tr') end; end; (** record simprocs **) fun is_sel_upd_pair thy (Const (s, _)) (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_id f = let val T = range_type (fastype_of f) in HOLogic.mk_comp (\<^Const>\<open>id T\<close>, f) end; fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t | get_upd_funs _ = []; fun get_accupd_simps ctxt term defset = let val thy = Proof_Context.theory_of ctxt; val (acc, [body]) = strip_comb term; val upd_funs = sort_distinct Term_Ord.fast_term_ord (get_upd_funs body); fun get_simp upd = let (* FIXME fresh "f" (!?) *) val T = domain_type (fastype_of upd); val lhs = HOLogic.mk_comp (acc, upd $ Free ("f", T)); val rhs = if is_sel_upd_pair thy acc upd then HOLogic.mk_comp (Free ("f", T), acc) else mk_comp_id acc; val prop = lhs === rhs; val othm = Goal.prove ctxt [] [] prop (fn {context = ctxt', ...} => simp_tac (put_simpset defset ctxt') 1 THEN REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1) THEN TRY (simp_tac (put_simpset HOL_ss ctxt' |> Simplifier.add_simps @{thms id_apply id_o o_id}) 1)); val dest = if is_sel_upd_pair thy acc upd then @{thm o_eq_dest} else @{thm o_eq_id_dest}; in Drule.export_without_context (othm RS dest) end; in map get_simp upd_funs end; fun get_updupd_simp ctxt defset u u' comp = let (* FIXME fresh "f" (!?) *) val f = Free ("f", domain_type (fastype_of u)); val f' = Free ("f'", domain_type (fastype_of u')); val lhs = HOLogic.mk_comp (u $ f, u' $ f'); val rhs = if comp then u $ HOLogic.mk_comp (f, f') else HOLogic.mk_comp (u' $ f', u $ f); val prop = lhs === rhs; val othm = Goal.prove ctxt [] [] prop (fn {context = ctxt', ...} => simp_tac (put_simpset defset ctxt') 1 THEN REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1) THEN TRY (simp_tac (put_simpset HOL_ss ctxt' |> Simplifier.add_simps @{thms id_apply}) 1) val dest = if comp then @{thm o_eq_dest_lhs} else @{thm o_eq_dest}; in Drule.export_without_context (othm RS dest) end; fun gen_get_updupd_simps ctxt upd_funs defset = let fun getswap u u' = get_updupd_simp ctxt defset u u' (dest_Const_name u = dest_Const_nam fun build_swaps_to_eq _ [] swaps = swaps | build_swaps_to_eq upd (u :: us) swaps = let val key = (dest_Const_name u, dest_Const_name upd); val newswaps = if Symreltab.defined swaps key then swaps else Symreltab.insert (K true) (key, getswap u upd) swaps; in if dest_Const_name u = dest_Const_name upd then newswaps else build_swaps_to_eq upd us newswaps end; fun swaps_needed [] _ _ swaps = map snd (Symreltab.dest swaps) | swaps_needed (u :: us) prev seen swaps = if Symtab.defined seen (dest_Const_name u) then swaps_needed us prev seen (build_swaps_to_eq u prev swaps) else swaps_needed us (u :: prev) (Symtab.insert (K true) (dest_Const_name u, ()) seen) swaps; in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end; fun get_updupd_simps ctxt term defset = gen_get_updupd_simps ctxt (get_upd_funs term) defs fun prove_unfold_defs thy upd_funs ex_simps ex_simprs prop = let val ctxt = Proof_Context.init_global thy; val defset = get_sel_upd_defs thy; val prop' = Envir.beta_eta_contract prop; val (lhs, _) = Logic.dest_equals (Logic.strip_assums_concl prop'); val (_, args) = strip_comb lhs; val simps = if null upd_funs then (if length args = 1 then get_accupd_simps else get_updupd_simps) ctxt lhs defset else gen_get_updupd_simps ctxt upd_funs defset in Goal.prove ctxt [] [] prop' (fn {context = ctxt', ...} => let val ctxt0 = put_simpset HOL_basic_ss ctxt' in simp_tac (ctxt0 |> Simplifier.add_simps (simps @ @{thms K_record_comp})) 1 THEN TRY (simp_tac (ctxt0 |> Simplifier.add_simps ex_simps |> fold Simplifier.add_proc ex_simprs) 1) end) end; local 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); in (* simproc *) (* 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. *) fun select_update_proc ctxt ct = let val thy = Proof_Context.theory_of ctxt; val t = Thm.term_of ct; in (case t of (sel as Const (s, Type (_, [_, rangeS]))) $ ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) => if is_selector thy s andalso is_some (get_updates thy u) then let val {sel_upd = {updates, ...}, extfields, ...} = Data.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 _ = NONE; in (case mk_eq_terms (upd $ k $ r) of SOME (trm, trm', vars) => SOME (prove_unfold_defs thy [] [] [] (Logic.list_all (vars, Logic.mk_equals (sel $ trm, trm')))) | NONE => NONE) end else NONE | _ => NONE) end; val simproc = \<^simproc_setup>\<open>select_update ("x::'a::{}") = \<open>K select_update_pr fun get_upd_acc_cong_thm upd acc thy ss = let val ctxt = Proof_Context.init_global thy; val prop = infer_instantiate ctxt [(("upd", 0), Thm.cterm_of ctxt upd), (("ac", 0), Thm.cterm_of ctxt acc)] updacc_cong_triv |> Thm.concl_of; in Goal.prove ctxt [] [] prop (fn {context = ctxt', ...} => simp_tac (put_simpset ss ctxt') 1 THEN REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1) THEN TRY (resolve_tac ctxt' [updacc_cong_idI] 1)) end; fun sorted ord [] = true | sorted ord [x] = true | sorted ord (x::y::xs) = (case ord (x, y) of LESS => sorted ord (y::xs) | EQUAL => sorted ord (y::xs) | GREATER => false) fun insert_unique ord x [] = [x] | insert_unique ord x (y::ys) = (case ord (x, y) of LESS => (x::y::ys) | EQUAL => (x::ys) | GREATER => y :: insert_unique ord x ys) fun insert_unique_hd ord (x::xs) = x :: insert_unique ord x xs | insert_unique_hd ord xs = xs (* upd_simproc *) (*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.*) fun upd_proc ctxt ct = let val thy = Proof_Context.theory_of ctxt; val t = Thm.term_of ct; (*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 | include_depth (dep, false) (min, max) = 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, _)) $ 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' in ((upd, s, f) :: us, bs, fastype_of term) end | NONE => ([], term, HOLogic.unitT)) | NONE => ([], term, HOLogic.unitT)) | getupdseq term _ _ = ([], term, HOLogic.unitT); val (upds, base, baseT) = getupdseq t 0 ~1; val orig_upds = map_index (fn (i, (x, y, z)) => (x, y, z, i)) upds val upd_ord = rev_order o fast_string_ord o apply2 #2 val (upds, commuted) = if not (null orig_upds) andalso Config.get ctxt sort_updates andalso not (sorted upd_ord ori (sort upd_ord orig_upds, true) else (orig_upds, false) fun is_upd_noop s (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) | is_upd_noop _ _ _ = (false, HOLogic.unit); fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) = let val ss = get_sel_upd_defs thy; val uathm = get_upd_acc_cong_thm upd acc thy ss; in [Drule.export_without_context (uathm RS updacc_noopE), Drule.export_without_context (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 _) _ = [f] | add_upd f fs = (f :: fs); (*mk_updterm returns (orig-term-skeleton-update list , 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, i) :: upds) above term = let val (lhs_upds, 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 \<^Type>\<open>fun \<^Type>\<open>fun A _\<close> _\<close> = T; fun mk_comp_local (f, f') = \<^Const>\ in if isnoop then ((upd $ skelf', i)::lhs_upds, 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, i)::lhs_upds, rhs, fvar :: vars, Symtab.map_default (u, []) (add_upd skelf) dups, true, noops) else (case Symtab.lookup dups u of SOME fs => ((upd $ skelf, i)::lhs_upds, upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs, fvar :: vars, dups, true, noops) | NONE => ((upd $ skelf, i)::lhs_upds, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops)) end | mk_updterm [] _ _ = ([], Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty) | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _, _) => x) us); val (lhs_upds, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base; val orig_order_lhs_upds = lhs_upds |> sort (rev_order o int_ord o apply2 snd) val lhs = Bound 0 |> fold (fn (upd, _) => fn s => upd $ s) orig_order_lhs_upds (* Note that the simplifier works bottom up. So all nested updates are already normalised, e.g. sorted. 'commuted' thus means that the outermost update has to be inserted at its place inside the sorted nested updates. The necessary swaps can be expressed via 'upd_funs' by replicating the outer update at the designated position: *) val upd_funs = (if commuted then insert_unique_hd upd_ord orig_upds else orig_upds) |> map #1 val noops' = maps snd (Symtab.dest noops); in if simp orelse commuted then SOME (prove_unfold_defs thy upd_funs noops' [simproc] (Logic.list_all (vars, Logic.mk_equals (lhs, rhs)))) else NONE end; val upd_simproc = \<^simproc_setup>\<open>update ("x::'a::{}") = \<open>K upd_proc\<close>\<clos end; (* eq_simproc *) (*Look 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 (split_simp_tac). e.g. r(|lots of updates|) = x eq_simproc split_simp_tac Complexity: #components * #updates #updates *) fun eq_proc ctxt ct = (case Thm.term_of ct of \<^Const_>\<open>HOL.eq T for _ _\<close> => (case rec_id ~1 T of "" => NONE | name => (case get_equalities (Proof_Context.theory_of ctxt) name of NONE => NONE | SOME thm => SOME (thm RS @{thm Eq_TrueI}))) | _ => NONE); val eq_simproc = \<^simproc_setup>\<open>eq ("r = s") = \<open>K eq_proc\<close>\<close>; (* split_simproc *) (*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 split_simproc P = Simplifier.make_simproc \<^context> {name = "record_split", kind = Simproc, lhss = [\<^term>\<open>x::'a::{}\ proc = fn _ => fn ctxt => fn ct => let fun quantifier T which = (case rec_id ~1 T of "" => NONE | _ => let val split = P (Thm.term_of ct) in if split <> 0 then (case get_splits (Proof_Context.theory_of ctxt) (rec_id split T) of NONE => NONE | SOME thms => SOME (which thms)) else NONE end) in (case Thm.term_of ct of \<^Const_>\<open>Pure.all T for _\<close> => quantifier T #Pure_all | \<^Const_>\<open>All T for _\<close> => quantifier T #All | \<^Const_>\<open>Ex T for _\<close> => quantifier T #Ex | _ => NONE) end, identifier = []}; fun ex_sel_eq_proc ctxt ct = let val thy = Proof_Context.theory_of ctxt; val t = Thm.term_of ct; fun mkeq (lr, T, (sel, Tsel), x) i = if is_selector thy sel then let val x' = if not (Term.is_dependent x) 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>\<open>HOL.eq T for l r\<close> end else raise TERM ("", [Const (sel, Tsel)]); fun dest_sel_eq (\<^Const_>\<open>HOL.eq T\<close> $ (Const (sel, Tsel) $ Bound 0) $ X) = (true, T, (sel, Tsel), X) | dest_sel_eq (\<^Const_>\<open>HOL.eq T\<close> $ X $ (Const (sel, Tsel) $ Bound 0)) = (false, T, (sel, Tsel), X) | dest_sel_eq _ = raise TERM ("", []); in (case t of \<^Const_>\<open>Ex T for \<open>Abs (s, _, t)\<close>\<close> => (let val eq = mkeq (dest_sel_eq t) 0; val prop = Logic.list_all ([("r", T)], Logic.mk_equals (\<^Const>\<open>Ex T for \<open>Abs (s, T, eq)\<close>\<close>, \<^Const>\<open>True\< in SOME (Goal.prove_sorry_global thy [] [] prop (fn {context = ctxt', ...} => simp_tac (put_simpset (get_simpset thy) ctxt' |> Simplifier.add_simps @{thms simp_thms} |> Simplifier.add_proc (split_simproc (K ~1))) 1)) end handle TERM _ => NONE) | _ => NONE) end; val ex_sel_eq_simproc = \<^simproc_setup>\<open>passive ex_sel_eq ("Ex t") = \<open>K ex_sel_e (* split_simp_tac *) (*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 split_simp_tac ctxt thms P = CSUBGOAL (fn (cgoal, i) => let val thy = Proof_Context.theory_of ctxt; val goal = Thm.term_of cgoal; val frees = filter (is_recT o #2) (Term.add_frees goal []); val has_rec = exists_subterm (fn \<^Const_>\<open>Pure.all T\<close> => is_recT T | \<^Const_>\<open>All T\<close> => is_recT T | \<^Const_>\<open>Ex T\<close> => is_recT T | _ => false); fun mk_split_free_tac free induct_thm i = let val _ $ (_ $ Var (r, _)) = Thm.concl_of induct_thm; val thm = infer_instantiate ctxt [(r, Thm.cterm_of ctxt free)] induct_thm; in simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps @{thms induct_atomize}) i resolve_tac ctxt [thm] i THEN simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps @{thms induct_rulify}) i end; val split_frees_tacs = frees |> map_filter (fn (x, T) => (case rec_id ~1 T of "" => NONE | _ => let val free = Free (x, T); val split = P free; in if split <> 0 then (case get_splits thy (rec_id split T) of NONE => NONE | SOME thms => SOME (mk_split_free_tac free (#induct_scheme thms) i)) else NONE end)); val add_simproc = if has_rec goal then Simplifier.add_proc (split_simproc P) else I; val thms' = @{thms o_apply K_record_comp} @ thms; in EVERY split_frees_tacs THEN full_simp_tac (put_simpset (get_simpset thy) ctxt |> Simplifier.add_simps thms' |> add_s end); (* split_tac *) (*Split all records in the goal, which are quantified by !! or ALL.*) fun split_tac ctxt = CSUBGOAL (fn (cgoal, i) => let val goal = Thm.term_of cgoal; val has_rec = exists_subterm (fn \<^Const_>\<open>Pure.all T\<close> => is_recT T | \<^Const_>\<open>All T\<close> => is_recT T | _ => false); fun is_all \<^Const_>\<open>Pure.all _ for _\<close> = ~1 | is_all \<^Const_>\<open>All _ for _\<close> = ~1 | is_all _ = 0; in if has_rec goal then full_simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_proc (split_simproc is_al else no_tac end); (* wrapper *) val split_name = "record_split_tac"; val split_wrapper = (split_name, fn ctxt => fn tac => split_tac ctxt ORELSE' tac); (** theory extender interface **) (* attributes *) val case_names_fields = Rule_Cases.case_names ["fields"]; fun induct_type_global name = [case_names_fields, Induct.induct_type name]; fun cases_type_global name = [case_names_fields, Induct.cases_type name]; (* tactics *) (*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 ctxt s rule = CSUBGOAL (fn (cgoal, i) => let val g = Thm.term_of cgoal; val params = Logic.strip_params g; val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g); val rule' = Thm.lift_rule cgoal rule; val (P, ys) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_assums_concl (Thm.prop_of r (*ca indicates if rule is a case analysis or induction rule*) val (x, ca) = (case rev (drop (length params) ys) of [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (hd (rev (Logic.strip_assums_hyp (hd (Thm.take_prems_of 1 rule')))))))), true) | [x] => (head_of x, false)); val rule'' = infer_instantiate ctxt (map (apsnd (Thm.cterm_of ctxt)) (case rev params of [] => (case AList.lookup (op =) (Term.add_frees g []) s of NONE => error "try_param_tac: no such variable" | SOME T => [(#1 (dest_Var P), if ca then concl else lambda (Free (s, T)) concl), (#1 (dest_Var x), Free (s, T))]) | (_, T) :: _ => [(#1 (dest_Var P), fold_rev Term.abs params (if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))), (#1 (dest_Var x), fold_rev Term.abs params (Bound 0))])) rule'; in compose_tac ctxt (false, rule'', Thm.nprems_of rule) i end); fun extension_definition overloaded name fields alphas zeta moreT more vars thy = let val ctxt = Proof_Context.init_global thy; val base_name = Long_Name.base_name name; val fieldTs = map snd fields; val fields_moreTs = fieldTs @ [moreT]; val alphas_zeta = alphas @ [zeta]; val ext_binding = Binding.name (suffix extN base_name); val ext_name = suffix extN name; val ext_tyco = suffix ext_typeN name; val extT = Type (ext_tyco, map TFree alphas_zeta); val ext_type = fields_moreTs ---> extT; (* the tree of new types that will back the record extension *) val mktreeV = Balanced_Tree.make Iso_Tuple_Support.mk_cons_tuple; fun mk_iso_tuple (left, right) (thy, i) = let val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i; val ((_, cons), thy') = thy |> Iso_Tuple_Support.add_iso_tuple_type overloaded (Binding.suffix_name suff (Binding.name base_name), alphas_zeta) (fastype_of left, fastype_of right); in (cons $ left $ right, (thy', i + 1)) end; (*trying to create a 1-element iso_tuple will fail, and is pointless anyway*) fun mk_even_iso_tuple [arg] = pair arg | mk_even_iso_tuple args = mk_iso_tuple (Iso_Tuple_Support.dest_cons_tuple (mktreeV arg 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 = take 16 xs :: group16 (drop 16 xs); val vars' = group16 vars; val (composites, (thy', i')) = fold_map mk_even_iso_tuple vars' (thy, i); in build_meta_tree_type i' thy' composites more end else let val (term, (thy', _)) = mk_iso_tuple (mktreeV vars, more) (thy, 0) in (term, thy') end end; val _ = timing_msg ctxt "record extension preparing definitions"; (* 1st stage part 1: introduce the tree of new types *) val (ext_body, typ_thy) = timeit_msg ctxt "record extension nested type def:" (fn () => build_meta_tree_type 1 thy vars more); (* prepare declarations and definitions *) (* 1st stage part 2: define the ext constant *) fun mk_ext args = list_comb (Const (ext_name, ext_type), args); val ext_spec = Logic.mk_equals (mk_ext (vars @ [more]), ext_body); val (ext_def, defs_thy) = timeit_msg ctxt "record extension constructor def:" (fn () => typ_thy |> Sign.declare_const_global ((ext_binding, ext_type), NoSyn) |> snd |> Global_Theory.add_def (Thm.def_binding ext_binding, ext_spec)); val defs_ctxt = Proof_Context.init_global defs_thy; (* prepare propositions *) val _ = timing_msg ctxt "record extension preparing propositions"; val vars_more = vars @ [more]; val variants = map (fn Free (x, _) => x) vars_more; val ext = mk_ext vars_more; val s = Free (rN, extT); val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT); val inject_prop = (* FIXME local x x' *) 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', \<^term>\ === foldr1 HOLogic.mk_conj (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [\<^term>\ end; val induct_prop = (fold_rev Logic.all vars_more (Trueprop (P $ ext)), Trueprop (P $ s)); val split_meta_prop = (* FIXME local P *) let val P = Free (singleton (Name.variant_list variants) "P", extT --> propT) in Logic.mk_equals (Logic.all s (P $ s), fold_rev Logic.all vars_more (P $ ext)) end; val inject = timeit_msg ctxt "record extension inject proof:" (fn () => simplify (put_simpset HOL_ss defs_ctxt) (Goal.prove_sorry_global defs_thy [] [] inject_prop (fn {context = ctxt', ...} => simp_tac (put_simpset HOL_basic_ss ctxt' |> Simplifier.add_simp ext_def) 1 THEN REPEAT_DETERM (resolve_tac ctxt' @{thms refl_conj_eq} 1 ORELSE Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1 ORELSE resolve_tac ctxt' [refl] 1)))); (*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 Drule.export_without_context to convert the free variables into unifiable variables and unify them with (roughly) the definition of the accessor.*) val surject = timeit_msg ctxt "record extension surjective proof:" (fn () => let val start = infer_instantiate defs_ctxt [(("y", 0), Thm.cterm_of defs_ctxt ext)] surject_assist_idE val tactic1 = simp_tac (put_simpset HOL_basic_ss defs_ctxt |> Simplifier.add_simp ext_def) 1 THEN REPEAT_ALL_NEW (Iso_Tuple_Support.iso_tuple_intros_tac defs_ctxt) 1; val tactic2 = REPEAT (resolve_tac defs_ctxt [surject_assistI] 1 THEN resolve_tac defs_ctxt [refl] 1); val [halfway] = Seq.list_of (tactic1 start); val [surject] = Seq.list_of (tactic2 (Drule.export_without_context halfway)); in surject end); val split_meta = timeit_msg ctxt "record extension split_meta proof:" (fn () => Goal.prove_sorry_global defs_thy [] [] split_meta_prop (fn {context = ctxt', ...} => EVERY1 [resolve_tac ctxt' @{thms equal_intr_rule}, Goal.norm_hhf_tac ctxt', eresolve_tac ctxt' @{thms meta_allE}, assume_tac ctxt', resolve_tac ctxt' [@{thm prop_subst} OF [surject]], REPEAT o eresolve_tac ctxt' @{thms meta_allE}, assume_tac ctxt'])); val induct = timeit_msg ctxt "record extension induct proof:" (fn () => let val (assm, concl) = induct_prop in Goal.prove_sorry_global defs_thy [] [assm] concl (fn {context = ctxt', prems, ...} => cut_tac (split_meta RS Drule.equal_elim_rule2) 1 THEN resolve_tac ctxt' prems 2 THEN asm_simp_tac (put_simpset HOL_ss ctxt') 1) end); val ([(_, [induct']), (_, [inject']), (_, [surjective']), (_, [split_meta'])], thm_th defs_thy |> Global_Theory.note_thmss "" [((Binding.name "ext_induct", []), [([induct], [])]), ((Binding.name "ext_inject", []), [([inject], [])]), ((Binding.name "ext_surjective", []), [([surject], [])]), ((Binding.name "ext_split", []), [([split_meta], [])])]; in (((ext_name, ext_type), (ext_tyco, alphas_zeta), extT, induct', inject', surjective', split_meta', ext_def), thm_thy) end; fun chunks [] [] = [] | chunks [] xs = [xs] | chunks (l :: ls) xs = take l xs :: chunks ls (drop l xs); fun chop_last [] = error "chop_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 _ [] = error "subst_last: list should not be empty" | subst_last s [_] = [s] | subst_last s (x :: xs) = x :: subst_last s xs; (* mk_recordT *) (*build 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; (* code generation *) fun mk_random_eq tyco vs extN Ts = let (* FIXME local i etc. *) val size = \<^term>\<open>i::natural\<close>; fun termifyT T = HOLogic.mk_prodT (T, \<^typ>\<open>unit \<Rightarrow> term\<close>); val T = Type (tyco, map TFree vs); val Tm = termifyT T; val params = Name.invent_names_global "x" Ts; val lhs = HOLogic.mk_random T size; val tc = HOLogic.mk_return Tm \<^typ>\<open>Random.seed\<close> (HOLogic.mk_valtermify_app extN params T); val rhs = HOLogic.mk_ST (map (fn (v, T') => ((HOLogic.mk_random T' size, \<^typ>\ tc \<^typ>\<open>Random.seed\<close> (SOME Tm, \<^typ>\<open>Random.seed\<close>); in (lhs, rhs) end fun mk_full_exhaustive_eq tyco vs extN Ts = let (* FIXME local i etc. *) val size = \<^term>\<open>i::natural\<close>; fun termifyT T = HOLogic.mk_prodT (T, \<^typ>\<open>unit \<Rightarrow> term\<close>); val T = Type (tyco, map TFree vs); val test_function = Free ("f", termifyT T --> \<^typ>\<open>(bool \<times> term list) option\<close>) val params = Name.invent_names_global "x" Ts; --> -------------------- --> maximum size reached --> -------------------- ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.24Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Eine klare Vorstellung vom Zielzustand |
|
2026-03-28