# HG changeset patch # User wenzelm # Date 1266260467 -3600 # Node ID a68e4972fd31142eb734778e505e489849e6ac07 # Parent d137efecf79369e599323c4312bb883bdc617b9e formal markup of constants; misc tuning; diff -r d137efecf793 -r a68e4972fd31 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Mon Feb 15 19:16:45 2010 +0100 +++ b/src/HOL/Tools/record.ML Mon Feb 15 20:01:07 2010 +0100 @@ -156,7 +156,8 @@ ((isom, cons $ isom), thm_thy) end; -val iso_tuple_intros_tac = resolve_from_net_tac iso_tuple_intros THEN' +val iso_tuple_intros_tac = + resolve_from_net_tac iso_tuple_intros THEN' CSUBGOAL (fn (cgoal, i) => let val thy = Thm.theory_of_cterm cgoal; @@ -197,21 +198,21 @@ val refl_conj_eq = @{thm refl_conj_eq}; -val surject_assistI = @{thm "iso_tuple_surjective_proof_assistI"}; -val surject_assist_idE = @{thm "iso_tuple_surjective_proof_assist_idE"}; - -val updacc_accessor_eqE = @{thm "update_accessor_accessor_eqE"}; -val updacc_updator_eqE = @{thm "update_accessor_updator_eqE"}; -val updacc_eq_idI = @{thm "iso_tuple_update_accessor_eq_assist_idI"}; -val updacc_eq_triv = @{thm "iso_tuple_update_accessor_eq_assist_triv"}; - -val updacc_foldE = @{thm "update_accessor_congruence_foldE"}; -val updacc_unfoldE = @{thm "update_accessor_congruence_unfoldE"}; -val updacc_noopE = @{thm "update_accessor_noopE"}; -val updacc_noop_compE = @{thm "update_accessor_noop_compE"}; -val updacc_cong_idI = @{thm "update_accessor_cong_assist_idI"}; -val updacc_cong_triv = @{thm "update_accessor_cong_assist_triv"}; -val updacc_cong_from_eq = @{thm "iso_tuple_update_accessor_cong_from_eq"}; +val surject_assistI = @{thm iso_tuple_surjective_proof_assistI}; +val surject_assist_idE = @{thm iso_tuple_surjective_proof_assist_idE}; + +val updacc_accessor_eqE = @{thm update_accessor_accessor_eqE}; +val updacc_updator_eqE = @{thm update_accessor_updator_eqE}; +val updacc_eq_idI = @{thm iso_tuple_update_accessor_eq_assist_idI}; +val updacc_eq_triv = @{thm iso_tuple_update_accessor_eq_assist_triv}; + +val updacc_foldE = @{thm update_accessor_congruence_foldE}; +val updacc_unfoldE = @{thm update_accessor_congruence_unfoldE}; +val updacc_noopE = @{thm update_accessor_noopE}; +val updacc_noop_compE = @{thm update_accessor_noop_compE}; +val updacc_cong_idI = @{thm update_accessor_cong_assist_idI}; +val updacc_cong_triv = @{thm update_accessor_cong_assist_triv}; +val updacc_cong_from_eq = @{thm iso_tuple_update_accessor_cong_from_eq}; val o_eq_dest = @{thm o_eq_dest}; val o_eq_id_dest = @{thm o_eq_id_dest}; @@ -590,7 +591,7 @@ 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; + val flds' = map (apsnd (Envir.norm_type subst o varifyT)) flds; in (flds', (more, moreT)) end; fun get_recT_fields thy T = @@ -674,12 +675,14 @@ fun record_update_tr [t, u] = - fold (curry op $) (gen_fields_tr "_updates" "_update" updateN u) t + fold (curry op $) + (gen_fields_tr @{syntax_const "_updates"} @{syntax_const "_update"} updateN u) t | record_update_tr ts = raise TERM ("record_update_tr", ts); fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts | update_name_tr (Const (x, T) :: ts) = Const (suffix updateN x, T) $$ ts - | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) = + | update_name_tr (((c as Const (@{syntax_const "_constrain"}, _)) $ t $ ty) :: ts) = + (* FIXME @{type_syntax} *) (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy")) $$ ts | update_name_tr ts = raise TERM ("update_name_tr", ts); @@ -719,7 +722,7 @@ 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])) + | NONE => raise TERM (msg ^ name ^ " is no proper field", [t])) | mk_ext [] = more; in mk_ext fieldargs end; @@ -784,27 +787,31 @@ gen_ext_type_tr sep mark sfx more ctxt t | gen_adv_record_type_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts); -val adv_record_tr = gen_adv_record_tr "_fields" "_field" extN HOLogic.unit; - -val adv_record_scheme_tr = gen_adv_record_scheme_tr "_fields" "_field" extN; +val adv_record_tr = + gen_adv_record_tr @{syntax_const "_fields"} @{syntax_const "_field"} extN HOLogic.unit; + +val adv_record_scheme_tr = + gen_adv_record_scheme_tr @{syntax_const "_fields"} @{syntax_const "_field"} extN; val adv_record_type_tr = - gen_adv_record_type_tr "_field_types" "_field_type" ext_typeN + gen_adv_record_type_tr + @{syntax_const "_field_types"} @{syntax_const "_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 + @{syntax_const "_field_types"} @{syntax_const "_field_type"} ext_typeN; val parse_translation = - [("_record_update", record_update_tr), - ("_update_name", update_name_tr)]; + [(@{syntax_const "_record_update"}, record_update_tr), + (@{syntax_const "_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)]; + [(@{syntax_const "_record"}, adv_record_tr), + (@{syntax_const "_record_scheme"}, adv_record_scheme_tr), + (@{syntax_const "_record_type"}, adv_record_type_tr), + (@{syntax_const "_record_type_scheme"}, adv_record_type_scheme_tr)]; (* print translations *) @@ -821,11 +828,6 @@ | Abs (_, _, 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 => @@ -835,11 +837,11 @@ | gen_field_upds_tr' _ _ tm = ([], tm); fun record_update_tr' tm = - let val (ts, u) = gen_field_upds_tr' "_update" updateN tm in + let val (ts, u) = gen_field_upds_tr' @{syntax_const "_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) + Syntax.const @{syntax_const "_record_update"} $ u $ + foldr1 (fn (v, w) => Syntax.const @{syntax_const "_updates"} $ v $ w) (rev ts) end; fun gen_field_tr' sfx tr' name = @@ -880,9 +882,10 @@ fun gen_record_tr' name = let val name_sfx = suffix extN name; - val unit = (fn Const (@{const_syntax "Product_Type.Unity"}, _) => true | _ => false); + val unit = fn Const (@{const_syntax Product_Type.Unity}, _) => true | _ => false; fun tr' ctxt ts = - record_tr' "_fields" "_field" "_record" "_record_scheme" unit ctxt + record_tr' @{syntax_const "_fields"} @{syntax_const "_field"} + @{syntax_const "_record"} @{syntax_const "_record_scheme"} unit ctxt (list_comb (Syntax.const name_sfx, ts)); in (name_sfx, tr') end; @@ -901,6 +904,7 @@ (*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*) + (* FIXME !??? *) (*WORKAROUND: If a record type occurs in an error message of type inference there may be some internal frees donoted by ??: @@ -967,7 +971,8 @@ 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.TYPE_MATCH => [("", T)] | Library.UnequalLengths => [("", T)]) + handle Type.TYPE_MATCH => [("", T)] + | Library.UnequalLengths => [("", T)]) | NONE => [("", T)]) | NONE => [("", T)]) | NONE => [("", T)]) @@ -989,8 +994,9 @@ 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)) + record_type_tr' @{syntax_const "_field_types"} @{syntax_const "_field_type"} + @{syntax_const "_record_type"} @{syntax_const "_record_type_scheme"} + ctxt (list_comb (Syntax.const name_sfx, ts)); in (name_sfx, tr') end; @@ -998,7 +1004,8 @@ let val name_sfx = suffix ext_typeN name; val default_tr' = - record_type_tr' "_field_types" "_field_type" "_record_type" "_record_type_scheme"; + record_type_tr' @{syntax_const "_field_types"} @{syntax_const "_field_type"} + @{syntax_const "_record_type"} @{syntax_const "_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)); @@ -1040,11 +1047,11 @@ val B = range_type X; val C = range_type (fastype_of f); val T = (B --> C) --> (A --> B) --> A --> C; - in Const ("Fun.comp", T) $ f $ g end; + in Const (@{const_name Fun.comp}, T) $ f $ g end; fun mk_comp_id f = let val T = range_type (fastype_of f) - in mk_comp (Const ("Fun.id", T --> T)) f end; + in mk_comp (Const (@{const_name Fun.id}, T --> T)) f end; fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t | get_upd_funs _ = []; @@ -1055,6 +1062,7 @@ val upd_funs = sort_distinct TermOrd.fast_term_ord (get_upd_funs body); fun get_simp upd = let + (* FIXME fresh "f" (!?) *) val T = domain_type (fastype_of upd); val lhs = mk_comp acc (upd $ Free ("f", T)); val rhs = @@ -1077,6 +1085,7 @@ fun get_updupd_simp thy defset u u' comp = let + (* FIXME fresh "f" (!?) *) val f = Free ("f", domain_type (fastype_of u)); val f' = Free ("f'", domain_type (fastype_of u')); val lhs = mk_comp (u $ f) (u' $ f'); @@ -1306,7 +1315,8 @@ 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'; + fun mk_comp_local (f, f') = + Const (@{const_name Fun.comp}, funT --> funT --> funT) $ f $ f'; in if isnoop then (upd $ skelf' $ lhs, rhs, vars, @@ -1359,7 +1369,7 @@ 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 t of Const (@{const_name "op ="}, Type (_, [T, _])) $ _ $ _ => (case rec_id ~1 T of "" => NONE | name => @@ -1381,7 +1391,10 @@ (fn thy => fn _ => fn t => (case t of Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ => - if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex" then + if quantifier = @{const_name All} orelse + quantifier = @{const_name all} orelse + quantifier = @{const_name Ex} + then (case rec_id ~1 T of "" => NONE | _ => @@ -1392,9 +1405,9 @@ | 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 + @{const_name all} => all_thm + | @{const_name All} => All_thm RS eq_reflection + | @{const_name Ex} => Ex_thm RS eq_reflection | _ => error "record_split_simproc")) else NONE end) @@ -1419,22 +1432,23 @@ 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 + in Const (@{const_name "op ="}, Teq) $ l $ r end else raise TERM ("", [Const (sel, Tsel)]); - fun dest_sel_eq (Const ("op =", Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) = + fun dest_sel_eq (Const (@{const_name "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)) = + | dest_sel_eq (Const (@{const_name "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) => + Const (@{const_name 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)); + val eq = mkeq (dest_sel_eq t) 0; + val prop = + list_all ([("r", T)], + Logic.mk_equals + (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), HOLogic.true_const)); in SOME (prove prop) end handle TERM _ => NONE) | _ => NONE) @@ -1459,7 +1473,8 @@ val has_rec = exists_Const (fn (s, Type (_, [Type (_, [T, _]), _])) => - (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T + (s = @{const_name all} orelse s = @{const_name All} orelse s = @{const_name Ex}) andalso + is_recT T | _ => false); fun mk_split_free_tac free induct_thm i = @@ -1508,13 +1523,13 @@ val has_rec = exists_Const (fn (s, Type (_, [Type (_, [T, _]), _])) => - (s = "all" orelse s = "All") andalso is_recT T + (s = @{const_name All} orelse s = @{const_name all}) andalso is_recT T | _ => false); fun is_all t = (case t of Const (quantifier, _) $ _ => - if quantifier = "All" orelse quantifier = "all" then ~1 else 0 + if quantifier = @{const_name All} orelse quantifier = @{const_name all} then ~1 else 0 | _ => 0); in if has_rec goal then @@ -1945,6 +1960,7 @@ val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0); val truncate_decl = (truncateN, rec_schemeT0 --> recT0); + (* prepare definitions *) (*record (scheme) type abbreviation*) @@ -1955,7 +1971,6 @@ val ext_defs = ext_def :: map #extdef parents; (*Theorems from the iso_tuple 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