# HG changeset patch # User wenzelm # Date 1254351816 -7200 # Node ID 7478ea5354169c6182cf3db5d999511ba83cf1bc # Parent 4b85b59a9f665b0876bf06bda69db0b65cce4d25 eliminated dead code, redundant bindings and parameters; use === term operator, which is defined here; handle Type.TYPE_MATCH, not arbitrary exceptions; misc tuning and simplification; diff -r 4b85b59a9f66 -r 7478ea535416 src/HOL/Record.thy --- a/src/HOL/Record.thy Thu Oct 01 00:32:00 2009 +0200 +++ b/src/HOL/Record.thy Thu Oct 01 01:03:36 2009 +0200 @@ -450,10 +450,6 @@ "Q = R \ (P \ Q) = (P \ R)" by simp -lemma meta_all_sameI: - "(\x. PROP P x \ PROP Q x) \ (\x. PROP P x) \ (\x. PROP Q x)" - by simp - lemma istuple_UNIV_I: "\x. x\UNIV \ True" by simp diff -r 4b85b59a9f66 -r 7478ea535416 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Thu Oct 01 00:32:00 2009 +0200 +++ b/src/HOL/Tools/record.ML Thu Oct 01 01:03:36 2009 +0200 @@ -202,22 +202,18 @@ struct val eq_reflection = @{thm eq_reflection}; -val Pair_eq = @{thm Product_Type.prod.inject}; val atomize_all = @{thm HOL.atomize_all}; 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 K_record_comp = @{thm K_record_comp}; val K_comp_convs = [@{thm o_apply}, K_record_comp] -val transitive_thm = @{thm transitive}; val o_assoc = @{thm o_assoc}; val id_apply = @{thm id_apply}; val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}]; val Not_eq_iff = @{thm Not_eq_iff}; val refl_conj_eq = @{thm refl_conj_eq}; -val meta_all_sameI = @{thm meta_all_sameI}; val surject_assistI = @{thm "istuple_surjective_proof_assistI"}; val surject_assist_idE = @{thm "istuple_surjective_proof_assist_idE"}; @@ -250,7 +246,6 @@ val ext_typeN = "_ext_type"; val inner_typeN = "_inner_type"; val extN ="_ext"; -val casesN = "_cases"; val ext_dest = "_sel"; val updateN = "_update"; val updN = "_upd"; @@ -259,10 +254,6 @@ val extendN = "extend"; val truncateN = "truncate"; -(*see typedef.ML*) -val RepN = "Rep_"; -val AbsN = "Abs_"; - (*** utilities ***) @@ -273,24 +264,6 @@ let fun varify (a, S) = TVar ((a, midx + 1), S); in map_type_tfree varify end; -fun domain_type' T = - domain_type T handle Match => T; - -fun range_type' T = - 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)); - -fun trace_thms str thms = - (tracing str; map (trace_thm "") thms); - -fun trace_term str t = - tracing (str ^ Syntax.string_of_term_global Pure.thy t); - (* timing *) @@ -302,7 +275,6 @@ (* syntax *) fun prune n xs = Library.drop (n, xs); -fun prefix_base s = Long_Name.map_base_name (fn bname => s ^ bname); val Trueprop = HOLogic.mk_Trueprop; fun All xs t = Term.list_all_free (xs, t); @@ -311,22 +283,10 @@ infix 0 :== ===; infixr 0 ==>; -val (op $$) = Term.list_comb; -val (op :==) = PrimitiveDefs.mk_defpair; -val (op ===) = Trueprop o HOLogic.mk_eq; -val (op ==>) = Logic.mk_implies; - - -(* morphisms *) - -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_Abs name repT absT = - Const (mk_AbsN name, repT --> absT); +val op $$ = Term.list_comb; +val op :== = PrimitiveDefs.mk_defpair; +val op === = Trueprop o HOLogic.mk_eq; +val op ==> = Logic.mk_implies; (* constructor *) @@ -338,15 +298,6 @@ 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 = - let val Ts = binder_types (fastype_of f) - in Const (mk_casesC (name, T, vT) Ts) $ f end; - - (* selector *) fun mk_selC sT (c, T) = (c, sT --> T); @@ -369,7 +320,7 @@ (* types *) -fun dest_recT (typ as Type (c_ext_type, Ts as (T :: _))) = +fun dest_recT (typ as Type (c_ext_type, Ts as (_ :: _))) = (case try (unsuffix ext_typeN) c_ext_type of NONE => raise TYPE ("Record.dest_recT", [typ], []) | SOME c => ((c, Ts), List.last Ts)) @@ -549,8 +500,6 @@ val get_simpset = get_ss_with_context #simpset; val get_sel_upd_defs = get_ss_with_context #defset; -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 @@ -618,8 +567,6 @@ extfields fieldext; in RecordsData.put data thy end; -val get_extsplit = Symtab.lookup o #extsplit o RecordsData.get; - (* access 'splits' *) @@ -659,7 +606,7 @@ let val ((name, Ts), moreT) = dest_recT T; val recname = - let val (nm :: recn :: rst) = rev (Long_Name.explode name) + let val (nm :: _ :: rst) = rev (Long_Name.explode name) (* FIXME !? *) in Long_Name.implode (rev (nm :: rst)) end; val midx = maxidx_of_typs (moreT :: Ts); val varifyT = varifyT midx; @@ -698,7 +645,7 @@ (* parent records *) -fun add_parents thy NONE parents = parents +fun add_parents _ NONE parents = parents | add_parents thy (SOME (types, name)) parents = let fun err msg = error (msg ^ " parent record " ^ quote name); @@ -787,7 +734,7 @@ | splitargs (_ :: _) [] = raise TERM (msg ^ "expecting more fields", [t]) | splitargs _ _ = ([], []); - fun mk_ext (fargs as (name, arg) :: _) = + fun mk_ext (fargs as (name, _) :: _) = (case get_fieldext thy (Sign.intern_const thy name) of SOME (ext, _) => (case get_extfields thy ext of @@ -816,7 +763,7 @@ | splitargs (_ :: _) [] = raise TERM (msg ^ "expecting more fields", [t]) | splitargs _ _ = ([], []); - fun mk_ext (fargs as (name, arg) :: _) = + fun mk_ext (fargs as (name, _) :: _) = (case get_fieldext thy (Sign.intern_const thy name) of SOME (ext, alphas) => (case get_extfields thy ext of @@ -838,7 +785,7 @@ val more' = mk_ext rest; in list_comb (Syntax.const (suffix sfx ext), alphas' @ [more']) - end handle TYPE_MATCH => + end handle Type.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])) @@ -896,7 +843,7 @@ (case k of Abs (_, _, Abs (_, _, t) $ Bound 0) => if null (loose_bnos t) then t else raise Match - | Abs (x, _, t) => + | Abs (_, _, t) => if null (loose_bnos t) then t else raise Match | _ => raise Match); @@ -1012,7 +959,7 @@ 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) + end handle Type.TYPE_MATCH => default_tr' ctxt tm) else raise Match (*give print translation of specialised record a chance*) | _ => raise Match) else default_tr' ctxt tm @@ -1045,8 +992,7 @@ 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)]) + handle Type.TYPE_MATCH => [("", T)] | Library.UnequalLengths => [("", T)]) | NONE => [("", T)]) | NONE => [("", T)]) | NONE => [("", T)]) @@ -1106,7 +1052,8 @@ then noopt () else opt (); -fun is_sel_upd_pair thy (Const (s, t)) (Const (u, t')) = +(* FIXME non-standard name for partial identity; rename to check_... (??) *) +fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) = (case get_updates thy u of SOME u_name => u_name = s | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')])); @@ -1130,7 +1077,6 @@ 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 @@ -1140,10 +1086,10 @@ 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 prop = lhs === rhs; val othm = Goal.prove (ProofContext.init thy) [] [] prop - (fn prems => + (fn _ => EVERY [simp_tac defset 1, REPEAT_DETERM (intros_tac 1), @@ -1164,10 +1110,10 @@ 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 prop = lhs === rhs; val othm = Goal.prove (ProofContext.init thy) [] [] prop - (fn prems => + (fn _ => EVERY [simp_tac defset 1, REPEAT_DETERM (intros_tac 1), @@ -1177,11 +1123,10 @@ 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 + fun build_swaps_to_eq _ [] swaps = swaps | build_swaps_to_eq upd (u :: us) swaps = let val key = (cname u, cname upd); @@ -1192,7 +1137,7 @@ if cname u = cname upd then newswaps else build_swaps_to_eq upd us newswaps end; - fun swaps_needed [] prev seen swaps = map snd (Symreltab.dest swaps) + fun swaps_needed [] _ _ swaps = map snd (Symreltab.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) @@ -1201,20 +1146,20 @@ val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate; -fun prove_unfold_defs thy ss T ex_simps ex_simprs prop = +fun prove_unfold_defs thy ex_simps ex_simprs prop = 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 (head, args) = strip_comb lhs; + val (lhs, _) = Logic.dest_equals (Logic.strip_assums_concl prop'); + val (_, 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; in Goal.prove (ProofContext.init thy) [] [] prop' - (fn prems => + (fn _ => 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; @@ -1251,55 +1196,52 @@ *) val record_simproc = Simplifier.simproc @{theory HOL} "record_simp" ["x"] - (fn thy => fn ss => fn t => + (fn thy => fn _ => fn t => (case t of - (sel as Const (s, Type (_, [domS, rangeS]))) $ + (sel as Const (s, Type (_, [_, 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) + if is_selector thy s andalso is_some (get_updates thy u) then + 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 _ = NONE; + in + (case mk_eq_terms (upd $ k $ r) of + SOME (trm, trm', vars) => + SOME + (prove_unfold_defs thy [] [] + (list_all (vars, Logic.mk_equals (sel $ trm, trm')))) + | NONE => NONE) + end else NONE | _ => NONE)); @@ -1311,7 +1253,7 @@ val prop = concl_of (named_cterm_instantiate insts updacc_cong_triv); in Goal.prove (ProofContext.init thy) [] [] prop - (fn prems => + (fn _ => EVERY [simp_tac simpset 1, REPEAT_DETERM (in_tac 1), @@ -1331,7 +1273,7 @@ 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 => + (fn thy => fn _ => fn t => let (*We can use more-updators with other updators as long as none of the other updators go deeper than any more @@ -1346,7 +1288,7 @@ 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 = + fun getupdseq (term as (upd as Const (u, _)) $ f $ tm) min max = (case get_update_details u thy of SOME (s, dep, ismore) => (case include_depth (dep, ismore) (min, max) of @@ -1359,15 +1301,14 @@ val (upds, base, baseT) = getupdseq t 0 ~1; - fun is_upd_noop s (f as Abs (n, T, Const (s', T') $ tm')) tm = + fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm = if s = s' andalso null (loose_bnos tm') andalso subst_bound (HOLogic.unit, tm') = tm then (true, Abs (n, T, Const (s', T') $ Bound 1)) else (false, HOLogic.unit) - | is_upd_noop 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'')) $ _)) = + | is_upd_noop _ _ _ = (false, HOLogic.unit); + + fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) = let val ss = get_sel_upd_defs thy; val uathm = get_upd_acc_cong_thm upd acc thy ss; @@ -1417,17 +1358,16 @@ fvar :: vars, dups, true, noops) | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops)) end - | mk_updterm [] above term = + | mk_updterm [] _ _ = (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; + | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _) => x) us); + + val (lhs, rhs, vars, _, 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] + (prove_unfold_defs thy noops' [record_simproc] (list_all (vars, Logic.mk_equals (lhs, rhs)))) else NONE end); @@ -1473,11 +1413,11 @@ Simplifier.simproc @{theory HOL} "record_split_simp" ["x"] (fn thy => fn _ => fn t => (case t of - Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ trm => + Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ => 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 @@ -1568,10 +1508,10 @@ simp_tac (HOL_basic_ss addsimps @{thms induct_rulify}) i] end; - fun split_free_tac P i (free as Free (n, T)) = + fun split_free_tac P i (free as Free (_, 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 @@ -1598,8 +1538,6 @@ (*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; - val has_rec = exists_Const (fn (s, Type (_, [Type (_, [T, _]), _])) => (s = "all" orelse s = "All") andalso is_recT T @@ -1695,40 +1633,16 @@ 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*) -fun ex_inst_tac i st = - let - val thy = Thm.theory_of_thm st; - 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 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)) - end; - -fun extension_definition full name fields names alphas zeta moreT more vars thy = +fun extension_definition name fields 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_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 bfields_more = map (apfst base) fields_more; - 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*) @@ -1739,7 +1653,7 @@ 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') = + val (_, cons, thy') = IsTupleSupport.add_istuple_type (nm, alphas_zeta) (fastype_of left, fastype_of right) thy; in @@ -1763,7 +1677,7 @@ build_meta_tree_type i' thy' composites more end else - let val (term, (thy', i')) = mk_istuple (mktreeV vars, more) (thy, 0) + let val (term, (thy', _)) = mk_istuple (mktreeV vars, more) (thy, 0) in (term, thy') end end; @@ -1795,16 +1709,15 @@ val ([ext_def], defs_thy) = timeit_msg "record extension constructor def:" mk_defs; + (* 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 ext = mk_ext vars_more; 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 = @@ -1819,27 +1732,18 @@ val induct_prop = (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s)); - val cases_prop = - All (map dest_Free vars_more) - (Trueprop (HOLogic.mk_eq (s, ext)) ==> Trueprop C) - ==> Trueprop C; - val split_meta_prop = - let val P = Free (Name.variant variants "P", extT-->Term.propT) in + let val P = Free (Name.variant variants "P", extT --> Term.propT) in Logic.mk_equals (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext)) end; - fun prove stndrd = quick_and_dirty_prove stndrd defs_thy; val prove_standard = quick_and_dirty_prove true defs_thy; - fun prove_simp stndrd simps = - let val tac = simp_all_tac HOL_ss simps - in fn prop => prove stndrd [] prop (K tac) end; fun inject_prf () = simplify HOL_ss (prove_standard [] inject_prop - (fn prems => + (fn _ => EVERY [simp_tac (HOL_basic_ss addsimps [ext_def]) 1, REPEAT_DETERM (resolve_tac [refl_conj_eq] 1 ORELSE @@ -1872,7 +1776,7 @@ fun split_meta_prf () = prove_standard [] split_meta_prop - (fn prems => + (fn _ => EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1, etac meta_allE 1, atac 1, @@ -1909,8 +1813,8 @@ | 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] +fun subst_last _ [] = error "subst_last: list should not be empty" + | subst_last s [_] = [s] | subst_last s (x :: xs) = x :: subst_last s xs; @@ -1965,7 +1869,6 @@ val parent_variants = Name.variant_list [moreN, rN, rN ^ "'", wN] (map base parent_names); val parent_vars = ListPair.map Free (parent_variants, parent_types); val parent_len = length parents; - val parents_idx = (map #name parents) ~~ (0 upto (parent_len - 1)); val fields = map (apfst full) bfields; val names = map fst fields; @@ -1979,13 +1882,10 @@ (map fst bfields); val vars = ListPair.map Free (variants, types); val named_vars = names ~~ vars; - val idxs = 0 upto (len - 1); val idxms = 0 upto len; val all_fields = parent_fields @ fields; - val all_names = parent_names @ names; val all_types = parent_types @ types; - val all_len = parent_fields_len + len; val all_variants = parent_variants @ variants; val all_vars = parent_vars @ vars; val all_named_vars = (parent_names ~~ parent_vars) @ named_vars; @@ -1997,7 +1897,6 @@ val full_moreN = full moreN; val bfields_more = bfields @ [(moreN, moreT)]; val fields_more = fields @ [(full_moreN, moreT)]; - val vars_more = vars @ [more]; val named_vars_more = named_vars @ [(full_moreN, more)]; val all_vars_more = all_vars @ [more]; val all_named_vars_more = all_named_vars @ [(full_moreN, more)]; @@ -2008,7 +1907,7 @@ 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; + |> extension_definition extN fields alphas_ext zeta moreT more vars; val _ = timing_msg "record preparing definitions"; val Type extension_scheme = extT; @@ -2080,16 +1979,6 @@ (* prepare definitions *) - fun parent_more s = - 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; - (*record (scheme) type abbreviation*) val recordT_specs = [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn), @@ -2233,14 +2122,12 @@ (*cases*) val cases_scheme_prop = - (All (map dest_Free all_vars_more) - (Trueprop (HOLogic.mk_eq (r0, r_rec0)) ==> Trueprop C)) - ==> Trueprop C; + (All (map dest_Free all_vars_more) (r0 === r_rec0 ==> Trueprop C)) + ==> Trueprop C; val cases_prop = - (All (map dest_Free all_vars) - (Trueprop (HOLogic.mk_eq (r_unit0, r_rec_unit0)) ==> Trueprop C)) - ==> Trueprop C; + (All (map dest_Free all_vars) (r_unit0 === r_rec_unit0 ==> Trueprop C)) + ==> Trueprop C; (*split*) val split_meta_prop = @@ -2359,7 +2246,7 @@ val init_ss = HOL_basic_ss addsimps ext_defs; in prove_standard [] surjective_prop - (fn prems => + (fn _ => EVERY [rtac surject_assist_idE 1, simp_tac init_ss 1, @@ -2369,7 +2256,7 @@ fun split_meta_prf () = prove false [] split_meta_prop - (fn prems => + (fn _ => EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1, etac meta_allE 1, atac 1, @@ -2423,7 +2310,7 @@ 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) + prove_standard [] split_ex_prop (fn _ => resolve_tac [so''] 1) end; val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;