# HG changeset patch # User wenzelm # Date 1302979788 -7200 # Node ID 3b8498ac231412d67cf0a8f5093ba25d56d88ea6 # Parent 577d85fb58622f5dbb04b03903f4aca9e378422a proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way; tuned; diff -r 577d85fb5862 -r 3b8498ac2314 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sat Apr 16 20:30:44 2011 +0200 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sat Apr 16 20:49:48 2011 +0200 @@ -3007,25 +3007,23 @@ structure FRParTac = struct -fun frpar_tac T ps ctxt i = - Object_Logic.full_atomize_tac i - THEN (fn st => +fun frpar_tac T ps ctxt = + Object_Logic.full_atomize_tac + THEN' CSUBGOAL (fn (g, i) => let - val g = nth (cprems_of st) (i - 1) val thy = Proof_Context.theory_of ctxt val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps - val th = frpar_oracle (T, fs,ps, (* Pattern.eta_long [] *)g) - in rtac (th RS iffD2) i st end); + val th = frpar_oracle (T, fs, ps, (* Pattern.eta_long [] *) g) + in rtac (th RS iffD2) i end); -fun frpar2_tac T ps ctxt i = - Object_Logic.full_atomize_tac i - THEN (fn st => +fun frpar2_tac T ps ctxt = + Object_Logic.full_atomize_tac + THEN' CSUBGOAL (fn (g, i) => let - val g = nth (cprems_of st) (i - 1) val thy = Proof_Context.theory_of ctxt val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps - val th = frpar_oracle2 (T, fs,ps, (* Pattern.eta_long [] *)g) - in rtac (th RS iffD2) i st end); + val th = frpar_oracle2 (T, fs, ps, (* Pattern.eta_long [] *) g) + in rtac (th RS iffD2) i end); end; diff -r 577d85fb5862 -r 3b8498ac2314 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Sat Apr 16 20:30:44 2011 +0200 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Sat Apr 16 20:49:48 2011 +0200 @@ -66,9 +66,8 @@ fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp; -fun linz_tac ctxt q i = Object_Logic.atomize_prems_tac i THEN (fn st => +fun linz_tac ctxt q = Object_Logic.atomize_prems_tac THEN' SUBGOAL (fn (g, i) => let - val g = nth (prems_of st) (i - 1) val thy = Proof_Context.theory_of ctxt (* Transform the term*) val (t,np,nh) = prepare_for_linz q g @@ -117,9 +116,7 @@ assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)) end | _ => (pre_thm, assm_tac i) - in (rtac (((mp_step nh) o (spec_step np)) th) i - THEN tac) st - end handle Subscript => no_tac st); + in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end); val setup = Method.setup @{binding cooper} diff -r 577d85fb5862 -r 3b8498ac2314 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Sat Apr 16 20:30:44 2011 +0200 +++ b/src/HOL/Decision_Procs/mir_tac.ML Sat Apr 16 20:49:48 2011 +0200 @@ -87,13 +87,12 @@ fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp; -fun mir_tac ctxt q i = - Object_Logic.atomize_prems_tac i - THEN simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i - THEN REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i) - THEN (fn st => +fun mir_tac ctxt q = + Object_Logic.atomize_prems_tac + THEN' simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) + THEN' (REPEAT_DETERM o split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]) + THEN' SUBGOAL (fn (g, i) => let - val g = nth (prems_of st) (i - 1) val thy = Proof_Context.theory_of ctxt (* Transform the term*) val (t,np,nh) = prepare_for_mir thy q g @@ -145,9 +144,7 @@ assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))) end | _ => (pre_thm, assm_tac i) - in (rtac (((mp_step nh) o (spec_step np)) th) i - THEN tac) st - end handle Subscript => no_tac st); + in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end); val setup = Method.setup @{binding mir} diff -r 577d85fb5862 -r 3b8498ac2314 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Sat Apr 16 20:30:44 2011 +0200 +++ b/src/HOL/Import/shuffler.ML Sat Apr 16 20:49:48 2011 +0200 @@ -606,21 +606,18 @@ filter (match_consts ignored t) all_thms end -fun gen_shuffle_tac ctxt search thms i st = +fun gen_shuffle_tac ctxt search thms = SUBGOAL (fn (t, i) => let val thy = Proof_Context.theory_of ctxt - val _ = message ("Shuffling " ^ (string_of_thm st)) - val t = nth (prems_of st) (i - 1) val set = set_prop thy t fun process_tac thms st = case set thms of SOME (_,th) => Seq.of_list (compose (th,i,st)) | NONE => Seq.empty in - (process_tac thms APPEND (if search - then process_tac (find_potential thy t) - else no_tac)) st - end + process_tac thms APPEND + (if search then process_tac (find_potential thy t) else no_tac) + end) fun shuffle_tac ctxt thms = gen_shuffle_tac ctxt false (map (pair "") thms); diff -r 577d85fb5862 -r 3b8498ac2314 src/HOL/Library/reflection.ML --- a/src/HOL/Library/reflection.ML Sat Apr 16 20:30:44 2011 +0200 +++ b/src/HOL/Library/reflection.ML Sat Apr 16 20:49:48 2011 +0200 @@ -298,23 +298,19 @@ (simplify (HOL_basic_ss addsimps [rth]) th) end -fun genreify_tac ctxt eqs to i = (fn st => +fun genreify_tac ctxt eqs to = SUBGOAL (fn (goal, i) => let - fun P () = HOLogic.dest_Trueprop (nth (prems_of st) (i - 1)) - val t = (case to of NONE => P () | SOME x => x) - val th = (genreif ctxt eqs t) RS ssubst - in rtac th i st - end); + val t = (case to of NONE => HOLogic.dest_Trueprop goal | SOME x => x) + val th = genreif ctxt eqs t RS ssubst + in rtac th i end); (* Reflection calls reification and uses the correctness *) (* theorem assumed to be the dead of the list *) -fun gen_reflection_tac ctxt conv corr_thms raw_eqs to i = (fn st => +fun gen_reflection_tac ctxt conv corr_thms raw_eqs to = SUBGOAL (fn (goal, i) => let - val P = HOLogic.dest_Trueprop (nth (prems_of st) (i - 1)); - val t = the_default P to; - val th = genreflect ctxt conv corr_thms raw_eqs t - RS ssubst; - in (rtac th i THEN TRY(rtac TrueI i)) st end); + val t = (case to of NONE => HOLogic.dest_Trueprop goal | SOME x => x) + val th = genreflect ctxt conv corr_thms raw_eqs t RS ssubst + in rtac th i THEN TRY (rtac TrueI i) end); (* FIXME THEN_ALL_NEW !? *) fun reflection_tac ctxt = gen_reflection_tac ctxt Codegen.evaluation_conv; (*FIXME why Codegen.evaluation_conv? very specific...*) diff -r 577d85fb5862 -r 3b8498ac2314 src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Sat Apr 16 20:30:44 2011 +0200 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Sat Apr 16 20:49:48 2011 +0200 @@ -13,7 +13,7 @@ val distinctTreeProver : thm -> Direction list -> Direction list -> thm val neq_x_y : Proof.context -> term -> term -> string -> thm option val distinctFieldSolver : string list -> solver - val distinctTree_tac : string list -> Proof.context -> term * int -> tactic + val distinctTree_tac : string list -> Proof.context -> int -> tactic val distinct_implProver : thm -> cterm -> thm val subtractProver : term -> cterm -> thm -> thm val distinct_simproc : string list -> simproc @@ -343,17 +343,19 @@ in SOME thm end handle Option => NONE) -fun distinctTree_tac names ctxt - (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ x $ y)), i) = - (case get_fst_success (neq_x_y ctxt x y) names of - SOME neq => rtac neq i - | NONE => no_tac) - | distinctTree_tac _ _ _ = no_tac; +fun distinctTree_tac names ctxt = SUBGOAL (fn (goal, i) => + (case goal of + Const (@{const_name Trueprop}, _) $ + (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ x $ y)) => + (case get_fst_success (neq_x_y ctxt x y) names of + SOME neq => rtac neq i + | NONE => no_tac) + | _ => no_tac)) fun distinctFieldSolver names = mk_solver' "distinctFieldSolver" (fn ss => case try Simplifier.the_context ss of - SOME ctxt => SUBGOAL (distinctTree_tac names ctxt) - | NONE => fn i => no_tac) + SOME ctxt => distinctTree_tac names ctxt + | NONE => K no_tac) fun distinct_simproc names = Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"] diff -r 577d85fb5862 -r 3b8498ac2314 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Sat Apr 16 20:30:44 2011 +0200 +++ b/src/HOL/Statespace/state_space.ML Sat Apr 16 20:49:48 2011 +0200 @@ -39,8 +39,7 @@ val neq_x_y : Proof.context -> term -> term -> thm option val distinctNameSolver : Simplifier.solver - val distinctTree_tac : - Proof.context -> term * int -> Tactical.tactic + val distinctTree_tac : Proof.context -> int -> tactic val distinct_simproc : Simplifier.simproc @@ -221,18 +220,20 @@ in SOME thm end handle Option => NONE) -fun distinctTree_tac ctxt - (Const (@{const_name Trueprop},_) $ - (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ (x as Free _)$ (y as Free _))), i) = - (case (neq_x_y ctxt x y) of - SOME neq => rtac neq i - | NONE => no_tac) - | distinctTree_tac _ _ = no_tac; +fun distinctTree_tac ctxt = SUBGOAL (fn (goal, i) => + (case goal of + Const (@{const_name Trueprop}, _) $ + (Const (@{const_name Not}, _) $ + (Const (@{const_name HOL.eq}, _) $ (x as Free _) $ (y as Free _))) => + (case neq_x_y ctxt x y of + SOME neq => rtac neq i + | NONE => no_tac) + | _ => no_tac)); val distinctNameSolver = mk_solver' "distinctNameSolver" (fn ss => case try Simplifier.the_context ss of - SOME ctxt => SUBGOAL (distinctTree_tac ctxt) - | NONE => fn i => no_tac) + SOME ctxt => distinctTree_tac ctxt + | NONE => K no_tac) val distinct_simproc = Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"] @@ -249,16 +250,14 @@ fun interprete_parent name dist_thm_name parent_expr thy = let - fun solve_tac ctxt (_,i) st = + fun solve_tac ctxt = CSUBGOAL (fn (goal, i) => let val distinct_thm = Proof_Context.get_thm ctxt dist_thm_name; - val goal = nth (cprems_of st) (i - 1); val rule = DistinctTreeProver.distinct_implProver distinct_thm goal; - in EVERY [rtac rule i] st - end + in rtac rule i end); - fun tac ctxt = EVERY [Locale.intro_locales_tac true ctxt [], - ALLGOALS (SUBGOAL (solve_tac ctxt))] + fun tac ctxt = + Locale.intro_locales_tac true ctxt [] THEN ALLGOALS (solve_tac ctxt); in thy |> prove_interpretation_in tac (name,parent_expr) diff -r 577d85fb5862 -r 3b8498ac2314 src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Sat Apr 16 20:30:44 2011 +0200 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Sat Apr 16 20:49:48 2011 +0200 @@ -128,44 +128,49 @@ (* instantiate induction rule *) -fun indtac indrule indnames i st = +fun indtac indrule indnames = CSUBGOAL (fn (cgoal, i) => let + val cert = cterm_of (Thm.theory_of_cterm cgoal); + val goal = term_of cgoal; val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule)); - val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop - (Logic.strip_imp_concl (nth (prems_of st) (i - 1)))); - val getP = if can HOLogic.dest_imp (hd ts) then - (apfst SOME) o HOLogic.dest_imp else pair NONE; - val flt = if null indnames then I else - filter (fn Free (s, _) => member (op =) indnames s | _ => false); - fun abstr (t1, t2) = (case t1 of - NONE => (case flt (OldTerm.term_frees t2) of + val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop (Logic.strip_imp_concl goal)); + val getP = + if can HOLogic.dest_imp (hd ts) + then apfst SOME o HOLogic.dest_imp + else pair NONE; + val flt = + if null indnames then I + else filter (fn Free (s, _) => member (op =) indnames s | _ => false); + fun abstr (t1, t2) = + (case t1 of + NONE => + (case flt (OldTerm.term_frees t2) of [Free (s, T)] => SOME (absfree (s, T, t2)) | _ => NONE) | SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2)))) - val cert = cterm_of (Thm.theory_of_thm st); - val insts = map_filter (fn (t, u) => case abstr (getP u) of + val insts = map_filter (fn (t, u) => + case abstr (getP u) of NONE => NONE | SOME u' => SOME (t |> getP |> snd |> head_of |> cert, cert u')) (ts ~~ ts'); val indrule' = cterm_instantiate insts indrule - in - rtac indrule' i st - end; + in rtac indrule' i end); + (* perform exhaustive case analysis on last parameter of subgoal i *) -fun exh_tac exh_thm_of i state = +fun exh_tac exh_thm_of = CSUBGOAL (fn (cgoal, i) => let - val thy = Thm.theory_of_thm state; - val prem = nth (prems_of state) (i - 1); - val params = Logic.strip_params prem; + val thy = Thm.theory_of_cterm cgoal; + val goal = term_of cgoal; + val params = Logic.strip_params goal; val (_, Type (tname, _)) = hd (rev params); - val exhaustion = Thm.lift_rule (Thm.cprem_of state i) (exh_thm_of tname); + val exhaustion = Thm.lift_rule cgoal (exh_thm_of tname); val prem' = hd (prems_of exhaustion); val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem')); - val exhaustion' = cterm_instantiate [(cterm_of thy (head_of lhs), - cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))] exhaustion - in compose_tac (false, exhaustion', nprems_of exhaustion) i state - end; + val exhaustion' = + cterm_instantiate [(cterm_of thy (head_of lhs), + cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))] exhaustion + in compose_tac (false, exhaustion', nprems_of exhaustion) i end); (********************** Internal description of datatypes *********************)