proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
authorwenzelm
Sat Apr 16 20:49:48 2011 +0200 (2011-04-16)
changeset 423683b8498ac2314
parent 42367 577d85fb5862
child 42369 167e8ba0f4b1
proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
tuned;
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/Import/shuffler.ML
src/HOL/Library/reflection.ML
src/HOL/Statespace/distinct_tree_prover.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Datatype/datatype_aux.ML
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Apr 16 20:30:44 2011 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Apr 16 20:49:48 2011 +0200
     1.3 @@ -3007,25 +3007,23 @@
     1.4  structure FRParTac = 
     1.5  struct
     1.6  
     1.7 -fun frpar_tac T ps ctxt i = 
     1.8 - Object_Logic.full_atomize_tac i
     1.9 - THEN (fn st =>
    1.10 +fun frpar_tac T ps ctxt = 
    1.11 + Object_Logic.full_atomize_tac
    1.12 + THEN' CSUBGOAL (fn (g, i) =>
    1.13    let
    1.14 -    val g = nth (cprems_of st) (i - 1)
    1.15      val thy = Proof_Context.theory_of ctxt
    1.16      val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps
    1.17 -    val th = frpar_oracle (T, fs,ps, (* Pattern.eta_long [] *)g)
    1.18 -  in rtac (th RS iffD2) i st end);
    1.19 +    val th = frpar_oracle (T, fs, ps, (* Pattern.eta_long [] *) g)
    1.20 +  in rtac (th RS iffD2) i end);
    1.21  
    1.22 -fun frpar2_tac T ps ctxt i = 
    1.23 - Object_Logic.full_atomize_tac i
    1.24 - THEN (fn st =>
    1.25 +fun frpar2_tac T ps ctxt = 
    1.26 + Object_Logic.full_atomize_tac
    1.27 + THEN' CSUBGOAL (fn (g, i) =>
    1.28    let
    1.29 -    val g = nth (cprems_of st) (i - 1)
    1.30      val thy = Proof_Context.theory_of ctxt
    1.31      val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps
    1.32 -    val th = frpar_oracle2 (T, fs,ps, (* Pattern.eta_long [] *)g)
    1.33 -  in rtac (th RS iffD2) i st end);
    1.34 +    val th = frpar_oracle2 (T, fs, ps, (* Pattern.eta_long [] *) g)
    1.35 +  in rtac (th RS iffD2) i end);
    1.36  
    1.37  end;
    1.38  
     2.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Sat Apr 16 20:30:44 2011 +0200
     2.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat Apr 16 20:49:48 2011 +0200
     2.3 @@ -66,9 +66,8 @@
     2.4  fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
     2.5  
     2.6  
     2.7 -fun linz_tac ctxt q i = Object_Logic.atomize_prems_tac i THEN (fn st =>
     2.8 +fun linz_tac ctxt q = Object_Logic.atomize_prems_tac THEN' SUBGOAL (fn (g, i) =>
     2.9    let
    2.10 -    val g = nth (prems_of st) (i - 1)
    2.11      val thy = Proof_Context.theory_of ctxt
    2.12      (* Transform the term*)
    2.13      val (t,np,nh) = prepare_for_linz q g
    2.14 @@ -117,9 +116,7 @@
    2.15              assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
    2.16      end
    2.17        | _ => (pre_thm, assm_tac i)
    2.18 -  in (rtac (((mp_step nh) o (spec_step np)) th) i
    2.19 -      THEN tac) st
    2.20 -  end handle Subscript => no_tac st);
    2.21 +  in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);
    2.22  
    2.23  val setup =
    2.24    Method.setup @{binding cooper}
     3.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Sat Apr 16 20:30:44 2011 +0200
     3.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Sat Apr 16 20:49:48 2011 +0200
     3.3 @@ -87,13 +87,12 @@
     3.4  fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
     3.5  
     3.6  
     3.7 -fun mir_tac ctxt q i = 
     3.8 -    Object_Logic.atomize_prems_tac i
     3.9 -        THEN simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i
    3.10 -        THEN REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i)
    3.11 -        THEN (fn st =>
    3.12 +fun mir_tac ctxt q = 
    3.13 +    Object_Logic.atomize_prems_tac
    3.14 +        THEN' simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms)
    3.15 +        THEN' (REPEAT_DETERM o split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
    3.16 +        THEN' SUBGOAL (fn (g, i) =>
    3.17    let
    3.18 -    val g = nth (prems_of st) (i - 1)
    3.19      val thy = Proof_Context.theory_of ctxt
    3.20      (* Transform the term*)
    3.21      val (t,np,nh) = prepare_for_mir thy q g
    3.22 @@ -145,9 +144,7 @@
    3.23              assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
    3.24      end
    3.25        | _ => (pre_thm, assm_tac i)
    3.26 -  in (rtac (((mp_step nh) o (spec_step np)) th) i 
    3.27 -      THEN tac) st
    3.28 -  end handle Subscript => no_tac st);
    3.29 +  in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);
    3.30  
    3.31  val setup =
    3.32    Method.setup @{binding mir}
     4.1 --- a/src/HOL/Import/shuffler.ML	Sat Apr 16 20:30:44 2011 +0200
     4.2 +++ b/src/HOL/Import/shuffler.ML	Sat Apr 16 20:49:48 2011 +0200
     4.3 @@ -606,21 +606,18 @@
     4.4          filter (match_consts ignored t) all_thms
     4.5      end
     4.6  
     4.7 -fun gen_shuffle_tac ctxt search thms i st =
     4.8 +fun gen_shuffle_tac ctxt search thms = SUBGOAL (fn (t, i) =>
     4.9      let
    4.10          val thy = Proof_Context.theory_of ctxt
    4.11 -        val _ = message ("Shuffling " ^ (string_of_thm st))
    4.12 -        val t = nth (prems_of st) (i - 1)
    4.13          val set = set_prop thy t
    4.14          fun process_tac thms st =
    4.15              case set thms of
    4.16                  SOME (_,th) => Seq.of_list (compose (th,i,st))
    4.17                | NONE => Seq.empty
    4.18      in
    4.19 -        (process_tac thms APPEND (if search
    4.20 -                                  then process_tac (find_potential thy t)
    4.21 -                                  else no_tac)) st
    4.22 -    end
    4.23 +        process_tac thms APPEND
    4.24 +          (if search then process_tac (find_potential thy t) else no_tac)
    4.25 +    end)
    4.26  
    4.27  fun shuffle_tac ctxt thms =
    4.28    gen_shuffle_tac ctxt false (map (pair "") thms);
     5.1 --- a/src/HOL/Library/reflection.ML	Sat Apr 16 20:30:44 2011 +0200
     5.2 +++ b/src/HOL/Library/reflection.ML	Sat Apr 16 20:49:48 2011 +0200
     5.3 @@ -298,23 +298,19 @@
     5.4               (simplify (HOL_basic_ss addsimps [rth]) th)
     5.5    end
     5.6  
     5.7 -fun genreify_tac ctxt eqs to i = (fn st =>
     5.8 +fun genreify_tac ctxt eqs to = SUBGOAL (fn (goal, i) =>
     5.9    let
    5.10 -    fun P () = HOLogic.dest_Trueprop (nth (prems_of st) (i - 1))
    5.11 -    val t = (case to of NONE => P () | SOME x => x)
    5.12 -    val th = (genreif ctxt eqs t) RS ssubst
    5.13 -  in rtac th i st
    5.14 -  end);
    5.15 +    val t = (case to of NONE => HOLogic.dest_Trueprop goal | SOME x => x)
    5.16 +    val th = genreif ctxt eqs t RS ssubst
    5.17 +  in rtac th i end);
    5.18  
    5.19      (* Reflection calls reification and uses the correctness *)
    5.20          (* theorem assumed to be the dead of the list *)
    5.21 -fun gen_reflection_tac ctxt conv corr_thms raw_eqs to i = (fn st =>
    5.22 +fun gen_reflection_tac ctxt conv corr_thms raw_eqs to = SUBGOAL (fn (goal, i) =>
    5.23    let
    5.24 -    val P = HOLogic.dest_Trueprop (nth (prems_of st) (i - 1));
    5.25 -    val t = the_default P to;
    5.26 -    val th = genreflect ctxt conv corr_thms raw_eqs t
    5.27 -      RS ssubst;
    5.28 -  in (rtac th i THEN TRY(rtac TrueI i)) st end);
    5.29 +    val t = (case to of NONE => HOLogic.dest_Trueprop goal | SOME x => x)
    5.30 +    val th = genreflect ctxt conv corr_thms raw_eqs t RS ssubst
    5.31 +  in rtac th i THEN TRY (rtac TrueI i) end);  (* FIXME THEN_ALL_NEW !? *)
    5.32  
    5.33  fun reflection_tac ctxt = gen_reflection_tac ctxt Codegen.evaluation_conv;
    5.34    (*FIXME why Codegen.evaluation_conv?  very specific...*)
     6.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Sat Apr 16 20:30:44 2011 +0200
     6.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Sat Apr 16 20:49:48 2011 +0200
     6.3 @@ -13,7 +13,7 @@
     6.4    val distinctTreeProver : thm -> Direction list -> Direction list -> thm
     6.5    val neq_x_y : Proof.context -> term -> term -> string -> thm option   
     6.6    val distinctFieldSolver : string list -> solver
     6.7 -  val distinctTree_tac : string list -> Proof.context -> term * int -> tactic
     6.8 +  val distinctTree_tac : string list -> Proof.context -> int -> tactic
     6.9    val distinct_implProver : thm -> cterm -> thm
    6.10    val subtractProver : term -> cterm -> thm -> thm
    6.11    val distinct_simproc : string list -> simproc
    6.12 @@ -343,17 +343,19 @@
    6.13    in SOME thm  
    6.14    end handle Option => NONE)
    6.15  
    6.16 -fun distinctTree_tac names ctxt 
    6.17 -      (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ x $ y)), i) =
    6.18 -  (case get_fst_success (neq_x_y ctxt x y) names of
    6.19 -     SOME neq => rtac neq i
    6.20 -   | NONE => no_tac)
    6.21 -  | distinctTree_tac _ _ _ = no_tac;
    6.22 +fun distinctTree_tac names ctxt = SUBGOAL (fn (goal, i) =>
    6.23 +    (case goal of
    6.24 +      Const (@{const_name Trueprop}, _) $
    6.25 +          (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ x $ y)) =>
    6.26 +        (case get_fst_success (neq_x_y ctxt x y) names of
    6.27 +          SOME neq => rtac neq i
    6.28 +        | NONE => no_tac)
    6.29 +    | _ => no_tac))
    6.30  
    6.31  fun distinctFieldSolver names = mk_solver' "distinctFieldSolver"
    6.32       (fn ss => case try Simplifier.the_context ss of
    6.33 -                 SOME ctxt => SUBGOAL (distinctTree_tac names ctxt)
    6.34 -                | NONE => fn i => no_tac)
    6.35 +                 SOME ctxt => distinctTree_tac names ctxt
    6.36 +               | NONE => K no_tac)
    6.37  
    6.38  fun distinct_simproc names =
    6.39    Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
     7.1 --- a/src/HOL/Statespace/state_space.ML	Sat Apr 16 20:30:44 2011 +0200
     7.2 +++ b/src/HOL/Statespace/state_space.ML	Sat Apr 16 20:49:48 2011 +0200
     7.3 @@ -39,8 +39,7 @@
     7.4  
     7.5      val neq_x_y : Proof.context -> term -> term -> thm option
     7.6      val distinctNameSolver : Simplifier.solver
     7.7 -    val distinctTree_tac :
     7.8 -       Proof.context -> term * int -> Tactical.tactic
     7.9 +    val distinctTree_tac : Proof.context -> int -> tactic
    7.10      val distinct_simproc : Simplifier.simproc
    7.11  
    7.12  
    7.13 @@ -221,18 +220,20 @@
    7.14    in SOME thm
    7.15    end handle Option => NONE)
    7.16  
    7.17 -fun distinctTree_tac ctxt
    7.18 -      (Const (@{const_name Trueprop},_) $
    7.19 -        (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ (x as Free _)$ (y as Free _))), i) =
    7.20 -  (case (neq_x_y ctxt x y) of
    7.21 -     SOME neq => rtac neq i
    7.22 -   | NONE => no_tac)
    7.23 -  | distinctTree_tac _ _ = no_tac;
    7.24 +fun distinctTree_tac ctxt = SUBGOAL (fn (goal, i) =>
    7.25 +  (case goal of
    7.26 +    Const (@{const_name Trueprop}, _) $
    7.27 +      (Const (@{const_name Not}, _) $
    7.28 +        (Const (@{const_name HOL.eq}, _) $ (x as Free _) $ (y as Free _))) =>
    7.29 +      (case neq_x_y ctxt x y of
    7.30 +        SOME neq => rtac neq i
    7.31 +      | NONE => no_tac)
    7.32 +  | _ => no_tac));
    7.33  
    7.34  val distinctNameSolver = mk_solver' "distinctNameSolver"
    7.35       (fn ss => case try Simplifier.the_context ss of
    7.36 -                 SOME ctxt => SUBGOAL (distinctTree_tac ctxt)
    7.37 -                | NONE => fn i => no_tac)
    7.38 +                 SOME ctxt => distinctTree_tac ctxt
    7.39 +                | NONE => K no_tac)
    7.40  
    7.41  val distinct_simproc =
    7.42    Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
    7.43 @@ -249,16 +250,14 @@
    7.44  fun interprete_parent name dist_thm_name parent_expr thy =
    7.45    let
    7.46  
    7.47 -    fun solve_tac ctxt (_,i) st =
    7.48 +    fun solve_tac ctxt = CSUBGOAL (fn (goal, i) =>
    7.49        let
    7.50          val distinct_thm = Proof_Context.get_thm ctxt dist_thm_name;
    7.51 -        val goal = nth (cprems_of st) (i - 1);
    7.52          val rule = DistinctTreeProver.distinct_implProver distinct_thm goal;
    7.53 -      in EVERY [rtac rule i] st
    7.54 -      end
    7.55 +      in rtac rule i end);
    7.56  
    7.57 -    fun tac ctxt = EVERY [Locale.intro_locales_tac true ctxt [],
    7.58 -                          ALLGOALS (SUBGOAL (solve_tac ctxt))]
    7.59 +    fun tac ctxt =
    7.60 +      Locale.intro_locales_tac true ctxt [] THEN ALLGOALS (solve_tac ctxt);
    7.61  
    7.62    in thy
    7.63       |> prove_interpretation_in tac (name,parent_expr)
     8.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Sat Apr 16 20:30:44 2011 +0200
     8.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Sat Apr 16 20:49:48 2011 +0200
     8.3 @@ -128,44 +128,49 @@
     8.4  
     8.5  (* instantiate induction rule *)
     8.6  
     8.7 -fun indtac indrule indnames i st =
     8.8 +fun indtac indrule indnames = CSUBGOAL (fn (cgoal, i) =>
     8.9    let
    8.10 +    val cert = cterm_of (Thm.theory_of_cterm cgoal);
    8.11 +    val goal = term_of cgoal;
    8.12      val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule));
    8.13 -    val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop
    8.14 -      (Logic.strip_imp_concl (nth (prems_of st) (i - 1))));
    8.15 -    val getP = if can HOLogic.dest_imp (hd ts) then
    8.16 -      (apfst SOME) o HOLogic.dest_imp else pair NONE;
    8.17 -    val flt = if null indnames then I else
    8.18 -      filter (fn Free (s, _) => member (op =) indnames s | _ => false);
    8.19 -    fun abstr (t1, t2) = (case t1 of
    8.20 -        NONE => (case flt (OldTerm.term_frees t2) of
    8.21 +    val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop (Logic.strip_imp_concl goal));
    8.22 +    val getP =
    8.23 +      if can HOLogic.dest_imp (hd ts)
    8.24 +      then apfst SOME o HOLogic.dest_imp
    8.25 +      else pair NONE;
    8.26 +    val flt =
    8.27 +      if null indnames then I
    8.28 +      else filter (fn Free (s, _) => member (op =) indnames s | _ => false);
    8.29 +    fun abstr (t1, t2) =
    8.30 +      (case t1 of
    8.31 +        NONE =>
    8.32 +          (case flt (OldTerm.term_frees t2) of
    8.33              [Free (s, T)] => SOME (absfree (s, T, t2))
    8.34            | _ => NONE)
    8.35        | SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2))))
    8.36 -    val cert = cterm_of (Thm.theory_of_thm st);
    8.37 -    val insts = map_filter (fn (t, u) => case abstr (getP u) of
    8.38 +    val insts = map_filter (fn (t, u) =>
    8.39 +      case abstr (getP u) of
    8.40          NONE => NONE
    8.41        | SOME u' => SOME (t |> getP |> snd |> head_of |> cert, cert u')) (ts ~~ ts');
    8.42      val indrule' = cterm_instantiate insts indrule
    8.43 -  in
    8.44 -    rtac indrule' i st
    8.45 -  end;
    8.46 +  in rtac indrule' i end);
    8.47 +
    8.48  
    8.49  (* perform exhaustive case analysis on last parameter of subgoal i *)
    8.50  
    8.51 -fun exh_tac exh_thm_of i state =
    8.52 +fun exh_tac exh_thm_of = CSUBGOAL (fn (cgoal, i) =>
    8.53    let
    8.54 -    val thy = Thm.theory_of_thm state;
    8.55 -    val prem = nth (prems_of state) (i - 1);
    8.56 -    val params = Logic.strip_params prem;
    8.57 +    val thy = Thm.theory_of_cterm cgoal;
    8.58 +    val goal = term_of cgoal;
    8.59 +    val params = Logic.strip_params goal;
    8.60      val (_, Type (tname, _)) = hd (rev params);
    8.61 -    val exhaustion = Thm.lift_rule (Thm.cprem_of state i) (exh_thm_of tname);
    8.62 +    val exhaustion = Thm.lift_rule cgoal (exh_thm_of tname);
    8.63      val prem' = hd (prems_of exhaustion);
    8.64      val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
    8.65 -    val exhaustion' = cterm_instantiate [(cterm_of thy (head_of lhs),
    8.66 -      cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))] exhaustion
    8.67 -  in compose_tac (false, exhaustion', nprems_of exhaustion) i state
    8.68 -  end;
    8.69 +    val exhaustion' =
    8.70 +      cterm_instantiate [(cterm_of thy (head_of lhs),
    8.71 +        cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))] exhaustion
    8.72 +  in compose_tac (false, exhaustion', nprems_of exhaustion) i end);
    8.73  
    8.74  
    8.75  (********************** Internal description of datatypes *********************)