# HG changeset patch # User wenzelm # Date 1255803359 -7200 # Node ID 84d105ad5adb9c2c8cf902dc016c05ab4b17b4f2 # Parent 2a1aaa2d9e64be2463690fb43f6b50137c02707a simplified tactics; use proper SUBGOAL/CSUBGOAL; diff -r 2a1aaa2d9e64 -r 84d105ad5adb src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Sat Oct 17 19:04:35 2009 +0200 +++ b/src/HOL/Tools/record.ML Sat Oct 17 20:15:59 2009 +0200 @@ -56,7 +56,7 @@ 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 istuple_intros_tac: int -> tactic val named_cterm_instantiate: (string * cterm) list -> thm -> thm end; @@ -157,26 +157,26 @@ ((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, i) => - let - val goal' = Envir.beta_eta_contract goal; - val is = - (case goal' of - Const (@{const_name Trueprop}, _) $ - (Const (@{const_name isomorphic_tuple}, _) $ Const is) => is - | _ => err "unexpected goal format" goal'); - val isthm = - (case Symtab.lookup isthms (#1 is) of - SOME isthm => isthm - | NONE => err "no thm found for constant" (Const is)); - in rtac isthm i end); - in - resolve_from_net_tac istuple_intros THEN' use_istuple_thm_tac - end; +val istuple_intros_tac = resolve_from_net_tac istuple_intros THEN' + CSUBGOAL (fn (cgoal, i) => + let + val thy = Thm.theory_of_cterm cgoal; + val goal = Thm.term_of cgoal; + + val isthms = IsTupleThms.get thy; + fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]); + + val goal' = Envir.beta_eta_contract goal; + val is = + (case goal' of + Const (@{const_name Trueprop}, _) $ + (Const (@{const_name isomorphic_tuple}, _) $ Const is) => is + | _ => err "unexpected goal format" goal'); + val isthm = + (case Symtab.lookup isthms (#1 is) of + SOME isthm => isthm + | NONE => err "no thm found for constant" (Const is)); + in rtac isthm i end); end; @@ -305,8 +305,7 @@ | SOME c => ((c, Ts), List.last Ts)) | dest_recT typ = raise TYPE ("Record.dest_recT", [typ], []); -fun is_recT T = - (case try dest_recT T of NONE => false | SOME _ => true); +val is_recT = can dest_recT; fun dest_recTs T = let val ((c, Ts), U) = dest_recT T @@ -1052,7 +1051,7 @@ fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t | get_upd_funs _ = []; -fun get_accupd_simps thy term defset intros_tac = +fun get_accupd_simps thy term defset = let val (acc, [body]) = strip_comb term; val upd_funs = sort_distinct TermOrd.fast_term_ord (get_upd_funs body); @@ -1068,10 +1067,9 @@ val othm = Goal.prove (ProofContext.init thy) [] [] prop (fn _ => - EVERY - [simp_tac defset 1, - REPEAT_DETERM (intros_tac 1), - TRY (simp_tac (HOL_ss addsimps id_o_apps) 1)]); + simp_tac defset 1 THEN + REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN + TRY (simp_tac (HOL_ss addsimps id_o_apps) 1)); val dest = if is_sel_upd_pair thy acc upd then o_eq_dest @@ -1079,7 +1077,7 @@ in Drule.standard (othm RS dest) end; in map get_simp upd_funs end; -fun get_updupd_simp thy defset intros_tac u u' comp = +fun get_updupd_simp thy defset u u' comp = let val f = Free ("f", domain_type (fastype_of u)); val f' = Free ("f'", domain_type (fastype_of u')); @@ -1092,18 +1090,17 @@ val othm = Goal.prove (ProofContext.init thy) [] [] prop (fn _ => - EVERY - [simp_tac defset 1, - REPEAT_DETERM (intros_tac 1), - TRY (simp_tac (HOL_ss addsimps [id_apply]) 1)]); + simp_tac defset 1 THEN + REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN + TRY (simp_tac (HOL_ss addsimps [id_apply]) 1)); val dest = if comp then o_eq_dest_lhs else o_eq_dest; in Drule.standard (othm RS dest) end; -fun get_updupd_simps thy term defset intros_tac = +fun get_updupd_simps thy 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 intros_tac u u' (cname u = cname u'); + fun getswap u u' = get_updupd_simp thy defset u u' (cname u = cname u'); fun build_swaps_to_eq _ [] swaps = swaps | build_swaps_to_eq upd (u :: us) swaps = let @@ -1127,14 +1124,10 @@ 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, _) = 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; + val simps = (if length args = 1 then get_accupd_simps else get_updupd_simps) thy lhs defset; in Goal.prove (ProofContext.init thy) [] [] prop' (fn _ => @@ -1225,17 +1218,14 @@ 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); + val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)]; + val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv); in Goal.prove (ProofContext.init thy) [] [] prop (fn _ => - EVERY - [simp_tac simpset 1, - REPEAT_DETERM (in_tac 1), - TRY (resolve_tac [updacc_cong_idI] 1)]) + simp_tac simpset 1 THEN + REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN + TRY (resolve_tac [updacc_cong_idI] 1)) end; @@ -1462,18 +1452,18 @@ 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 = +fun record_split_simp_tac thms P = CSUBGOAL (fn (cgoal, i) => let - val thy = Thm.theory_of_thm st; + val thy = Thm.theory_of_cterm cgoal; + + val goal = term_of cgoal; + val frees = filter (is_recT o #2) (Term.add_frees goal []); val has_rec = exists_Const (fn (s, Type (_, [Type (_, [T, _]), _])) => (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T | _ => false); - val goal = nth (Thm.prems_of st) (i - 1); (* FIXME SUBGOAL *) - val frees = 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; @@ -1481,61 +1471,58 @@ val crec = cterm_of thy r; val thm = cterm_instantiate [(crec, cfree)] induct_thm; in - EVERY - [simp_tac (HOL_basic_ss addsimps @{thms induct_atomize}) i, - rtac thm i, - simp_tac (HOL_basic_ss addsimps @{thms induct_rulify}) i] + simp_tac (HOL_basic_ss addsimps @{thms induct_atomize}) i THEN + rtac thm i THEN + simp_tac (HOL_basic_ss addsimps @{thms induct_rulify}) i end; - fun split_free_tac P i (free as Free (_, T)) = - (case rec_id ~1 T of - "" => NONE - | _ => - 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 = map_filter (split_free_tac P i) frees; + val split_frees_tacs = + frees |> map_filter (fn (x, T) => + (case rec_id ~1 T of + "" => NONE + | _ => + let + val free = Free (x, T); + val split = P free; + in + if split <> 0 then + (case get_splits thy (rec_id split T) of + NONE => NONE + | SOME (_, _, _, induct_thm) => + SOME (mk_split_free_tac free induct_thm i)) + else NONE + end)); 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) - end handle Empty => Seq.empty; + EVERY split_frees_tacs THEN + Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i + end); (* record_split_tac *) (*Split all records in the goal, which are quantified by ! or !!.*) -fun record_split_tac i st = +val record_split_tac = CSUBGOAL (fn (cgoal, i) => let + val goal = term_of cgoal; + val has_rec = exists_Const (fn (s, Type (_, [Type (_, [T, _]), _])) => (s = "all" orelse s = "All") andalso is_recT T | _ => false); - 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; (* FIXME SUBGOAL *) + Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i + else no_tac + end); (* wrapper *) @@ -1585,13 +1572,14 @@ (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 = +fun try_param_tac s rule = CSUBGOAL (fn (cgoal, i) => let - val cert = cterm_of (Thm.theory_of_thm st); - val g = nth (prems_of st) (i - 1); (* FIXME SUBGOAL *) + val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal); + + val g = Thm.term_of cgoal; val params = Logic.strip_params g; val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g); - val rule' = Thm.lift_rule (Thm.cprem_of st i) rule; + val rule' = Thm.lift_rule cgoal 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*) @@ -1601,15 +1589,15 @@ (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 rev params of [] => - (case AList.lookup (op =) (map dest_Free (OldTerm.term_frees (prop_of st))) s of + (case AList.lookup (op =) (Term.add_frees g []) 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; + in compose_tac (false, rule'', nprems_of rule) i end); fun extension_definition name fields alphas zeta moreT more vars thy = @@ -1697,7 +1685,6 @@ val ext = mk_ext vars_more; val s = Free (rN, extT); val P = Free (Name.variant variants "P", extT --> 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 @@ -1723,11 +1710,11 @@ simplify HOL_ss (prove_standard [] inject_prop (fn _ => - 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)])); + simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN + REPEAT_DETERM + (rtac refl_conj_eq 1 ORELSE + IsTupleSupport.istuple_intros_tac 1 ORELSE + rtac refl 1))); val inject = timeit_msg "record extension inject proof:" inject_prf; @@ -1744,7 +1731,7 @@ 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; + REPEAT_ALL_NEW IsTupleSupport.istuple_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 (Drule.standard halfway)); @@ -1756,21 +1743,20 @@ fun split_meta_prf () = prove_standard [] split_meta_prop (fn _ => - 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]); + EVERY1 + [rtac equal_intr_rule, Goal.norm_hhf_tac, + etac meta_allE, atac, + rtac (prop_subst OF [surject]), + REPEAT o etac meta_allE, atac]); 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 Drule.equal_elim_rule2] 1, - resolve_tac prems 2, - asm_simp_tac HOL_ss 1]) + cut_rules_tac [split_meta RS Drule.equal_elim_rule2] 1 THEN + resolve_tac prems 2 THEN + asm_simp_tac HOL_ss 1) end; val induct = timeit_msg "record extension induct proof:" induct_prf; @@ -1967,7 +1953,6 @@ (Binding.name bname, alphas, recT0, Syntax.NoSyn)]; 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. @@ -1994,7 +1979,7 @@ 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); + REPEAT (IsTupleSupport.istuple_intros_tac 1 ORELSE terminal); val updaccs = Seq.list_of (tactic init_thm); in (updaccs RL [updacc_accessor_eqE], @@ -2175,8 +2160,7 @@ prove_standard [] induct_scheme_prop (fn _ => EVERY - [if null parent_induct - then all_tac else try_param_tac rN (hd parent_induct) 1, + [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; @@ -2203,13 +2187,13 @@ 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]); + EVERY1 + [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]), + try_param_tac rN induct_scheme, + rtac impI, + REPEAT o etac allE, + etac mp, + rtac refl]); 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; @@ -2230,18 +2214,20 @@ 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))]) + REPEAT + (IsTupleSupport.istuple_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 _ => - 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]); + EVERY1 + [rtac equal_intr_rule, Goal.norm_hhf_tac, + etac meta_allE, atac, + rtac (prop_subst OF [surjective]), + REPEAT o etac meta_allE, atac]); val split_meta = timeit_msg "record split_meta proof:" split_meta_prf; fun split_meta_standardise () = Drule.standard split_meta; val split_meta_standard = @@ -2273,10 +2259,10 @@ 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]); + EVERY1 + [rtac iffI, + REPEAT o rtac allI, etac allE, atac, + rtac allI, rtac induct_scheme, REPEAT o etac allE, atac]); 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;