--- 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);