# HG changeset patch # User wenzelm # Date 1438001726 -7200 # Node ID 8d41b16d929336318c2d17175f31357b410b0f76 # Parent c24fa03f4c71b7ceb689c328cf06e230cdb9f5fe updated to infer_instantiate; clarified context; diff -r c24fa03f4c71 -r 8d41b16d9293 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Mon Jul 27 11:30:10 2015 +0200 +++ b/src/HOL/Tools/record.ML Mon Jul 27 14:55:26 2015 +0200 @@ -60,7 +60,6 @@ val mk_cons_tuple: term * term -> term val dest_cons_tuple: term -> term * term val iso_tuple_intros_tac: Proof.context -> int -> tactic - val named_cterm_instantiate: (string * cterm) list -> thm -> thm end; structure Iso_Tuple_Support: ISO_TUPLE_SUPPORT = @@ -73,17 +72,6 @@ val tuple_iso_tuple = (@{const_name Record.tuple_iso_tuple}, @{thm tuple_iso_tuple}); -fun named_cterm_instantiate values thm = (* FIXME eliminate *) - let - fun match name ((name', _), _) = name = name'; - fun getvar name = - (case find_first (match name) (Term.add_vars (Thm.prop_of thm) []) of - SOME var => Thm.global_cterm_of (Thm.theory_of_thm thm) (Var var) - | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])); - in - cterm_instantiate (map (apfst getvar) values) thm - end; - structure Iso_Tuple_Thms = Theory_Data ( type T = thm Symtab.table; @@ -137,11 +125,14 @@ thy |> do_typedef b repT alphas ||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*) + val typ_ctxt = Proof_Context.init_global typ_thy; (*construct a type and body for the isomorphism constant by instantiating the theorem to which the definition will be applied*) val intro_inst = - rep_inject RS named_cterm_instantiate [("abst", Thm.global_cterm_of typ_thy absC)] iso_tuple_intro; + rep_inject RS + infer_instantiate typ_ctxt + [(("abst", 0), Thm.cterm_of typ_ctxt absC)] iso_tuple_intro; val (_, body) = Logic.dest_equals (List.last (Thm.prems_of intro_inst)); val isomT = fastype_of body; val isom_binding = Binding.suffix_name isoN b; @@ -949,8 +940,10 @@ fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t | get_upd_funs _ = []; -fun get_accupd_simps thy term defset = +fun get_accupd_simps ctxt term defset = let + val thy = Proof_Context.theory_of ctxt; + val (acc, [body]) = strip_comb term; val upd_funs = sort_distinct Term_Ord.fast_term_ord (get_upd_funs body); fun get_simp upd = @@ -964,11 +957,11 @@ else mk_comp_id acc; val prop = lhs === rhs; val othm = - Goal.prove (Proof_Context.init_global thy) [] [] prop - (fn {context = ctxt, ...} => - simp_tac (put_simpset defset ctxt) 1 THEN - REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1) THEN - TRY (simp_tac (put_simpset HOL_ss ctxt addsimps @{thms id_apply id_o o_id}) 1)); + Goal.prove ctxt [] [] prop + (fn {context = ctxt', ...} => + simp_tac (put_simpset defset ctxt') 1 THEN + REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1) THEN + TRY (simp_tac (put_simpset HOL_ss ctxt' addsimps @{thms id_apply id_o o_id}) 1)); val dest = if is_sel_upd_pair thy acc upd then @{thm o_eq_dest} @@ -976,7 +969,7 @@ in Drule.export_without_context (othm RS dest) end; in map get_simp upd_funs end; -fun get_updupd_simp thy defset u u' comp = +fun get_updupd_simp ctxt defset u u' comp = let (* FIXME fresh "f" (!?) *) val f = Free ("f", domain_type (fastype_of u)); @@ -988,19 +981,19 @@ else HOLogic.mk_comp (u' $ f', u $ f); val prop = lhs === rhs; val othm = - Goal.prove (Proof_Context.init_global thy) [] [] prop - (fn {context = ctxt, ...} => - simp_tac (put_simpset defset ctxt) 1 THEN - REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1) THEN - TRY (simp_tac (put_simpset HOL_ss ctxt addsimps @{thms id_apply}) 1)); + Goal.prove ctxt [] [] prop + (fn {context = ctxt', ...} => + simp_tac (put_simpset defset ctxt') 1 THEN + REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1) THEN + TRY (simp_tac (put_simpset HOL_ss ctxt' addsimps @{thms id_apply}) 1)); val dest = if comp then @{thm o_eq_dest_lhs} else @{thm o_eq_dest}; in Drule.export_without_context (othm RS dest) end; -fun get_updupd_simps thy term defset = +fun get_updupd_simps ctxt term defset = let val upd_funs = get_upd_funs term; val cname = fst o dest_Const; - fun getswap u u' = get_updupd_simp thy defset u u' (cname u = cname u'); + fun getswap u u' = get_updupd_simp ctxt defset u u' (cname u = cname u'); fun build_swaps_to_eq _ [] swaps = swaps | build_swaps_to_eq upd (u :: us) swaps = let @@ -1019,20 +1012,20 @@ else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps; in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end; -val named_cterm_instantiate = Iso_Tuple_Support.named_cterm_instantiate; - fun prove_unfold_defs thy ex_simps ex_simprs prop = let + val ctxt = Proof_Context.init_global thy; + val defset = get_sel_upd_defs thy; val prop' = Envir.beta_eta_contract prop; val (lhs, _) = Logic.dest_equals (Logic.strip_assums_concl prop'); val (_, args) = strip_comb lhs; - val simps = (if length args = 1 then get_accupd_simps else get_updupd_simps) thy lhs defset; + val simps = (if length args = 1 then get_accupd_simps else get_updupd_simps) ctxt lhs defset; in - Goal.prove (Proof_Context.init_global thy) [] [] prop' - (fn {context = ctxt, ...} => - simp_tac (put_simpset HOL_basic_ss ctxt addsimps (simps @ @{thms K_record_comp})) 1 THEN - TRY (simp_tac (put_simpset HOL_basic_ss ctxt addsimps ex_simps addsimprocs ex_simprs) 1)) + Goal.prove ctxt [] [] prop' + (fn {context = ctxt', ...} => + simp_tac (put_simpset HOL_basic_ss ctxt' addsimps (simps @ @{thms K_record_comp})) 1 THEN + TRY (simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ex_simps addsimprocs ex_simprs) 1)) end; @@ -1120,14 +1113,18 @@ fun get_upd_acc_cong_thm upd acc thy ss = let - val insts = [("upd", Thm.global_cterm_of thy upd), ("ac", Thm.global_cterm_of thy acc)]; - val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv); + val ctxt = Proof_Context.init_global thy; + val prop = + infer_instantiate ctxt + [(("upd", 0), Thm.cterm_of ctxt upd), (("ac", 0), Thm.cterm_of ctxt acc)] + updacc_cong_triv + |> Thm.concl_of; in - Goal.prove (Proof_Context.init_global thy) [] [] prop - (fn {context = ctxt, ...} => - simp_tac (put_simpset ss ctxt) 1 THEN - REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt 1) THEN - TRY (resolve_tac ctxt [updacc_cong_idI] 1)) + Goal.prove ctxt [] [] prop + (fn {context = ctxt', ...} => + simp_tac (put_simpset ss ctxt') 1 THEN + REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac ctxt' 1) THEN + TRY (resolve_tac ctxt' [updacc_cong_idI] 1)) end; @@ -1374,10 +1371,8 @@ fun mk_split_free_tac free induct_thm i = let - val cfree = Thm.cterm_of ctxt free; - val _$ (_ $ r) = Thm.concl_of induct_thm; - val crec = Thm.cterm_of ctxt r; - val thm = cterm_instantiate [(crec, cfree)] induct_thm; + val _ $ (_ $ Var (r, _)) = Thm.concl_of induct_thm; + val thm = infer_instantiate ctxt [(r, Thm.cterm_of ctxt free)] induct_thm; in simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms induct_atomize}) i THEN resolve_tac ctxt [thm] i THEN @@ -1471,16 +1466,20 @@ (hd (rev (Logic.strip_assums_hyp (hd (Thm.prems_of rule')))))))), true) | [x] => (head_of x, false)); val rule'' = - cterm_instantiate - (map (apply2 (Thm.cterm_of ctxt)) + infer_instantiate ctxt + (map (apsnd (Thm.cterm_of ctxt)) (case rev params of [] => (case AList.lookup (op =) (Term.add_frees g []) s of NONE => error "try_param_tac: no such variable" - | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))]) + | SOME T => + [(#1 (dest_Var P), if ca then concl else lambda (Free (s, T)) concl), + (#1 (dest_Var x), Free (s, T))]) | (_, T) :: _ => - [(P, fold_rev Term.abs params (if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))), - (x, fold_rev Term.abs params (Bound 0))])) rule'; + [(#1 (dest_Var P), + fold_rev Term.abs params + (if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))), + (#1 (dest_Var x), fold_rev Term.abs params (Bound 0))])) rule'; in compose_tac ctxt (false, rule'', Thm.nprems_of rule) i end); @@ -1605,8 +1604,8 @@ (roughly) the definition of the accessor.*) val surject = timeit_msg ctxt "record extension surjective proof:" (fn () => let - val cterm_ext = Thm.cterm_of defs_ctxt ext; - val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE; + val start = + infer_instantiate defs_ctxt [(("y", 0), Thm.cterm_of defs_ctxt ext)] surject_assist_idE; val tactic1 = simp_tac (put_simpset HOL_basic_ss defs_ctxt addsimps [ext_def]) 1 THEN REPEAT_ALL_NEW (Iso_Tuple_Support.iso_tuple_intros_tac defs_ctxt) 1; @@ -1793,13 +1792,13 @@ (* definition *) -fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy = +fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy0 = let - val ctxt = Proof_Context.init_global thy; + val ctxt0 = Proof_Context.init_global thy0; val prefix = Binding.name_of binding; - val name = Sign.full_name thy binding; - val full = Sign.full_name_path thy prefix; + val name = Sign.full_name thy0 binding; + val full = Sign.full_name_path thy0 prefix; val bfields = map (fn (x, T, _) => (x, T)) raw_fields; val field_syntax = map #3 raw_fields; @@ -1850,12 +1849,12 @@ val ((ext, (ext_tyco, vs), extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) = - thy + thy0 |> Sign.qualified_path false binding |> extension_definition extension_name fields alphas_ext zeta moreT more vars; val ext_ctxt = Proof_Context.init_global ext_thy; - val _ = timing_msg ctxt "record preparing definitions"; + val _ = timing_msg ext_ctxt "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; @@ -1935,7 +1934,7 @@ pair, from which we can derive the bodies of our selector and updator and their convs.*) val (accessor_thms, updator_thms, upd_acc_cong_assists) = - timeit_msg ctxt "record getting tree access/updates:" (fn () => + timeit_msg ext_ctxt "record getting tree access/updates:" (fn () => let val r_rec0_Vars = let @@ -1944,10 +1943,11 @@ fun to_Var (Free (c, T)) = Var ((c, 1), T); in mk_rec (map to_Var all_vars_more) 0 end; - val cterm_rec = Thm.cterm_of ext_ctxt r_rec0; - val cterm_vrs = Thm.cterm_of ext_ctxt r_rec0_Vars; - val insts = [("v", cterm_rec), ("v'", cterm_vrs)]; - val init_thm = named_cterm_instantiate insts updacc_eq_triv; + val init_thm = + infer_instantiate ext_ctxt + [(("v", 0), Thm.cterm_of ext_ctxt r_rec0), + (("v'", 0), Thm.cterm_of ext_ctxt r_rec0_Vars)] + updacc_eq_triv; val terminal = resolve_tac ext_ctxt [updacc_eq_idI] 1 THEN resolve_tac ext_ctxt [refl] 1; val tactic = @@ -2004,11 +2004,11 @@ (* 2st stage: defs_thy *) val (((sel_defs, upd_defs), derived_defs), defs_thy) = - timeit_msg ctxt "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:" + timeit_msg ext_ctxt "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:" (fn () => ext_thy |> Sign.print_translation print_translation - |> Sign.restore_naming thy + |> Sign.restore_naming thy0 |> Typedecl.abbrev_global (binding, map #1 alphas, NoSyn) recT0 |> snd |> Typedecl.abbrev_global (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0 @@ -2029,7 +2029,7 @@ val defs_ctxt = Proof_Context.init_global defs_thy; (* prepare propositions *) - val _ = timing_msg ctxt "record preparing propositions"; + val _ = timing_msg defs_ctxt "record preparing propositions"; val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> HOLogic.boolT); val C = Free (singleton (Name.variant_list all_variants) "C", HOLogic.boolT); val P_unit = Free (singleton (Name.variant_list all_variants) "P", recT0 --> HOLogic.boolT); @@ -2099,14 +2099,14 @@ addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms); val (sel_convs, upd_convs) = - timeit_msg ctxt "record sel_convs/upd_convs proof:" (fn () => + timeit_msg defs_ctxt "record sel_convs/upd_convs proof:" (fn () => grouped 10 Par_List.map (fn prop => Goal.prove_sorry_global defs_thy [] [] prop (fn _ => ALLGOALS (asm_full_simp_tac sel_upd_ctxt))) (sel_conv_props @ upd_conv_props)) |> chop (length sel_conv_props); - val (fold_congs, unfold_congs) = timeit_msg ctxt "record upd fold/unfold congs:" (fn () => + val (fold_congs, unfold_congs) = timeit_msg defs_ctxt "record upd fold/unfold congs:" (fn () => let val symdefs = map Thm.symmetric (sel_defs @ upd_defs); val fold_ctxt = put_simpset HOL_basic_ss defs_ctxt addsimps symdefs; @@ -2115,7 +2115,7 @@ val parent_induct = Option.map #induct_scheme (try List.last parents); - val induct_scheme = timeit_msg ctxt "record induct_scheme proof:" (fn () => + val induct_scheme = timeit_msg defs_ctxt "record induct_scheme proof:" (fn () => Goal.prove_sorry_global defs_thy [] [] induct_scheme_prop (fn {context = ctxt, ...} => EVERY @@ -2123,14 +2123,14 @@ try_param_tac ctxt rN ext_induct 1, asm_simp_tac (put_simpset HOL_basic_ss ctxt) 1])); - val induct = timeit_msg ctxt "record induct proof:" (fn () => + val induct = timeit_msg defs_ctxt "record induct proof:" (fn () => Goal.prove_sorry_global defs_thy [] [#1 induct_prop] (#2 induct_prop) (fn {context = ctxt, prems, ...} => try_param_tac ctxt rN induct_scheme 1 THEN try_param_tac ctxt "more" @{thm unit.induct} 1 THEN resolve_tac ctxt prems 1)); - val surjective = timeit_msg ctxt "record surjective proof:" (fn () => + val surjective = timeit_msg defs_ctxt "record surjective proof:" (fn () => Goal.prove_sorry_global defs_thy [] [] surjective_prop (fn {context = ctxt, ...} => EVERY @@ -2142,20 +2142,20 @@ simp_tac (put_simpset (get_sel_upd_defs defs_thy) ctxt addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id})) 1))])); - val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" (fn () => + val cases_scheme = timeit_msg defs_ctxt "record cases_scheme proof:" (fn () => Goal.prove_sorry_global defs_thy [] [#1 cases_scheme_prop] (#2 cases_scheme_prop) (fn {context = ctxt, prems, ...} => resolve_tac ctxt prems 1 THEN resolve_tac ctxt [surjective] 1)); - val cases = timeit_msg ctxt "record cases proof:" (fn () => + val cases = timeit_msg defs_ctxt "record cases proof:" (fn () => Goal.prove_sorry_global defs_thy [] [] cases_prop (fn {context = ctxt, ...} => try_param_tac ctxt rN cases_scheme 1 THEN ALLGOALS (asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms unit_all_eq1})))); - val split_meta = timeit_msg ctxt "record split_meta proof:" (fn () => + val split_meta = timeit_msg defs_ctxt "record split_meta proof:" (fn () => Goal.prove_sorry_global defs_thy [] [] split_meta_prop (fn {context = ctxt', ...} => EVERY1 @@ -2164,14 +2164,14 @@ resolve_tac ctxt' [@{thm prop_subst} OF [surjective]], REPEAT o eresolve_tac ctxt' @{thms meta_allE}, assume_tac ctxt'])); - val split_object = timeit_msg ctxt "record split_object proof:" (fn () => + val split_object = timeit_msg defs_ctxt "record split_object proof:" (fn () => Goal.prove_sorry_global defs_thy [] [] split_object_prop (fn {context = ctxt, ...} => resolve_tac ctxt [@{lemma "Trueprop A \ Trueprop B \ A = B" by (rule iffI) unfold}] 1 THEN rewrite_goals_tac ctxt @{thms atomize_all [symmetric]} THEN resolve_tac ctxt [split_meta] 1)); - val split_ex = timeit_msg ctxt "record split_ex proof:" (fn () => + val split_ex = timeit_msg defs_ctxt "record split_ex proof:" (fn () => Goal.prove_sorry_global defs_thy [] [] split_ex_prop (fn {context = ctxt, ...} => simp_tac @@ -2180,7 +2180,7 @@ @{thms not_not Not_eq_iff})) 1 THEN resolve_tac ctxt [split_object] 1)); - val equality = timeit_msg ctxt "record equality proof:" (fn () => + val equality = timeit_msg defs_ctxt "record equality proof:" (fn () => Goal.prove_sorry_global defs_thy [] [] equality_prop (fn {context = ctxt, ...} => asm_full_simp_tac (put_simpset record_ss ctxt addsimps (split_meta :: sel_convs)) 1)); @@ -2237,7 +2237,7 @@ |> add_fieldext (extension_name, snd extension) names |> add_code ext_tyco vs extT ext simps' ext_inject |> add_ctr_sugar (Const ext) cases_scheme' ext_inject sel_convs' - |> Sign.restore_naming thy; + |> Sign.restore_naming thy0; in final_thy end;