author wenzelm Thu Mar 20 21:07:57 2014 +0100 (2014-03-20) changeset 56231 b98813774a63 parent 56230 3e449273942a child 56232 31e283f606e2
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
 src/HOL/Tools/Function/lexicographic_order.ML file | annotate | diff | revisions src/HOL/Tools/Function/termination.ML file | annotate | diff | revisions src/HOL/Tools/coinduction.ML file | annotate | diff | revisions src/HOL/Topological_Spaces.thy file | annotate | diff | revisions src/Pure/Isar/rule_cases.ML file | annotate | diff | revisions src/Pure/tactical.ML file | annotate | diff | revisions src/Tools/induct.ML file | annotate | diff | revisions src/ZF/Tools/induct_tacs.ML file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Thu Mar 20 19:58:33 2014 +0100
1.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Thu Mar 20 21:07:57 2014 +0100
1.3 @@ -174,7 +174,7 @@
1.4
1.5  (** The Main Function **)
1.6
1.7 -fun lex_order_tac quiet ctxt solve_tac (st: thm) =
1.8 +fun lex_order_tac quiet ctxt solve_tac st = SUBGOAL (fn _ =>
1.9    let
1.10      val thy = Proof_Context.theory_of ctxt
1.11      val ((_ \$ (_ \$ rel)) :: tl) = prems_of st
1.12 @@ -187,26 +187,27 @@
1.13      val table = (* 2: create table *)
1.14        map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
1.15    in
1.16 -    case search_table table of
1.17 -      NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
1.18 -    | SOME order =>
1.19 -      let
1.20 -        val clean_table = map (fn x => map (nth x) order) table
1.21 -        val relation = mk_measures domT (map (nth measure_funs) order)
1.22 -        val _ =
1.23 -          if not quiet then
1.24 -            Pretty.writeln (Pretty.block
1.25 -              [Pretty.str "Found termination order:", Pretty.brk 1,
1.26 -                Pretty.quote (Syntax.pretty_term ctxt relation)])
1.27 -          else ()
1.28 -
1.29 -      in (* 4: proof reconstruction *)
1.30 -        st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
1.31 -        THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
1.32 -        THEN (rtac @{thm "wf_empty"} 1)
1.33 -        THEN EVERY (map prove_row clean_table))
1.34 -      end
1.35 -  end
1.36 +    fn st =>
1.37 +      case search_table table of
1.38 +        NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
1.39 +      | SOME order =>
1.40 +        let
1.41 +          val clean_table = map (fn x => map (nth x) order) table
1.42 +          val relation = mk_measures domT (map (nth measure_funs) order)
1.43 +          val _ =
1.44 +            if not quiet then
1.45 +              Pretty.writeln (Pretty.block
1.46 +                [Pretty.str "Found termination order:", Pretty.brk 1,
1.47 +                  Pretty.quote (Syntax.pretty_term ctxt relation)])
1.48 +            else ()
1.49 +
1.50 +        in (* 4: proof reconstruction *)
1.51 +          st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
1.52 +          THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
1.53 +          THEN (rtac @{thm "wf_empty"} 1)
1.54 +          THEN EVERY (map prove_row clean_table))
1.55 +        end
1.56 +  end) 1 st;
1.57
1.58  fun lexicographic_order_tac quiet ctxt =
1.59    TRY (Function_Common.apply_termination_rule ctxt 1) THEN
```
```     2.1 --- a/src/HOL/Tools/Function/termination.ML	Thu Mar 20 19:58:33 2014 +0100
2.2 +++ b/src/HOL/Tools/Function/termination.ML	Thu Mar 20 21:07:57 2014 +0100
2.3 @@ -272,10 +272,10 @@
2.4
2.5  in
2.6
2.7 -fun wf_union_tac ctxt st =
2.8 +fun wf_union_tac ctxt st = SUBGOAL (fn _ =>
2.9    let
2.10      val thy = Proof_Context.theory_of ctxt
2.11 -    val cert = cterm_of (theory_of_thm st)
2.12 +    val cert = cterm_of thy
2.13      val ((_ \$ (_ \$ rel)) :: ineqs) = prems_of st
2.14
2.15      fun mk_compr ineq =
2.16 @@ -304,8 +304,8 @@
2.17    in
2.18      (PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
2.19       THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
2.20 -     THEN rewrite_goal_tac ctxt Un_aci_simps 1) st  (* eliminate duplicates *)
2.21 -  end
2.22 +     THEN rewrite_goal_tac ctxt Un_aci_simps 1)  (* eliminate duplicates *)
2.23 +  end) 1 st
2.24
2.25  end
2.26
```
```     3.1 --- a/src/HOL/Tools/coinduction.ML	Thu Mar 20 19:58:33 2014 +0100
3.2 +++ b/src/HOL/Tools/coinduction.ML	Thu Mar 20 21:07:57 2014 +0100
3.3 @@ -40,19 +40,20 @@
3.4      (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o etac thin_rl)) i st
3.5    end;
3.6
3.7 -fun coinduction_tac ctxt raw_vars opt_raw_thm prems st =
3.8 +fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _, _) =>
3.9    let
3.10      val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
3.11      fun find_coinduct t =
3.12        Induct.find_coinductP ctxt t @
3.13        (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default [])
3.14 -    val raw_thm = case opt_raw_thm
3.15 -      of SOME raw_thm => raw_thm
3.16 -       | NONE => st |> prems_of |> hd |> Logic.strip_assums_concl |> find_coinduct |> hd;
3.17 +    val raw_thm =
3.18 +      (case opt_raw_thm of
3.19 +        SOME raw_thm => raw_thm
3.20 +      | NONE => goal |> Logic.strip_assums_concl |> find_coinduct |> hd);
3.21      val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1
3.22      val cases = Rule_Cases.get raw_thm |> fst
3.23    in
3.24 -    NO_CASES (HEADGOAL (
3.25 +    HEADGOAL (
3.26        Object_Logic.rulify_tac ctxt THEN'
3.27        Method.insert_tac prems THEN'
3.28        Object_Logic.atomize_prems_tac ctxt THEN'
3.29 @@ -110,10 +111,10 @@
3.30                          unfold_thms_tac ctxt eqs
3.31                        end)) ctxt)))])
3.32          end) ctxt) THEN'
3.33 -      K (prune_params_tac ctxt))) st
3.34 -    |> Seq.maps (fn (_, st) =>
3.35 +      K (prune_params_tac ctxt))
3.36 +    #> Seq.maps (fn st =>
3.37        CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st)
3.38 -  end;
3.39 +  end));
3.40
3.41  local
3.42
```
```     4.1 --- a/src/HOL/Topological_Spaces.thy	Thu Mar 20 19:58:33 2014 +0100
4.2 +++ b/src/HOL/Topological_Spaces.thy	Thu Mar 20 21:07:57 2014 +0100
4.3 @@ -373,7 +373,7 @@
4.4  qed
4.5
4.6  ML {*
4.7 -  fun eventually_elim_tac ctxt thms thm =
4.8 +  fun eventually_elim_tac ctxt thms = SUBGOAL_CASES (fn (_, _, st) =>
4.9      let
4.10        val thy = Proof_Context.theory_of ctxt
4.11        val mp_thms = thms RL [@{thm eventually_rev_mp}]
4.12 @@ -381,11 +381,11 @@
4.13          (@{thm allI} RS @{thm always_eventually})
4.14          |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
4.15          |> fold (fn _ => fn thm => @{thm impI} RS thm) thms
4.16 -      val cases_prop = prop_of (raw_elim_thm RS thm)
4.17 +      val cases_prop = prop_of (raw_elim_thm RS st)
4.18        val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])])
4.19      in
4.20 -      CASES cases (rtac raw_elim_thm 1) thm
4.21 -    end
4.22 +      CASES cases (rtac raw_elim_thm 1)
4.23 +    end) 1
4.24  *}
4.25
4.26  method_setup eventually_elim = {*
```
```     5.1 --- a/src/Pure/Isar/rule_cases.ML	Thu Mar 20 19:58:33 2014 +0100
5.2 +++ b/src/Pure/Isar/rule_cases.ML	Thu Mar 20 21:07:57 2014 +0100
5.3 @@ -12,7 +12,7 @@
5.4    type cases_tactic
5.5    val CASES: cases -> tactic -> cases_tactic
5.6    val NO_CASES: tactic -> cases_tactic
5.7 -  val SUBGOAL_CASES: ((term * int) -> cases_tactic) -> int -> cases_tactic
5.8 +  val SUBGOAL_CASES: ((term * int * thm) -> cases_tactic) -> int -> cases_tactic
5.9    val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
5.10  end
5.11
5.12 @@ -190,7 +190,7 @@
5.13
5.14  fun SUBGOAL_CASES tac i st =
5.15    (case try Logic.nth_prem (i, Thm.prop_of st) of
5.16 -    SOME goal => tac (goal, i) st
5.17 +    SOME goal => tac (goal, i, st) st
5.18    | NONE => Seq.empty);
5.19
5.20  fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
```
```     6.1 --- a/src/Pure/tactical.ML	Thu Mar 20 19:58:33 2014 +0100
6.2 +++ b/src/Pure/tactical.ML	Thu Mar 20 21:07:57 2014 +0100
6.3 @@ -334,15 +334,14 @@
6.4  (*Returns all states that have changed in subgoal i, counted from the LAST
6.5    subgoal.  For stac, for example.*)
6.6  fun CHANGED_GOAL tac i st =
6.7 -    let val np = Thm.nprems_of st
6.8 -        val d = np-i                 (*distance from END*)
6.9 -        val t = Thm.term_of (Thm.cprem_of st i)
6.10 -        fun diff st' =
6.11 -            Thm.nprems_of st' - d <= 0   (*the subgoal no longer exists*)
6.12 -            orelse
6.13 -             not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
6.14 -    in  Seq.filter diff (tac i st)  end
6.15 -    handle General.Subscript => Seq.empty  (*no subgoal i*);
6.16 +  SUBGOAL (fn (t, _) =>
6.17 +    let
6.18 +      val np = Thm.nprems_of st;
6.19 +      val d = np - i;  (*distance from END*)
6.20 +      fun diff st' =
6.21 +        Thm.nprems_of st' - d <= 0 orelse  (*the subgoal no longer exists*)
6.22 +        not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))));
6.23 +    in Seq.filter diff o tac i end) i st;
6.24
6.25  (*Returns all states where some subgoals have been solved.  For
6.26    subgoal-based tactics this means subgoal i has been solved
```
```     7.1 --- a/src/Tools/induct.ML	Thu Mar 20 19:58:33 2014 +0100
7.2 +++ b/src/Tools/induct.ML	Thu Mar 20 21:07:57 2014 +0100
7.3 @@ -741,71 +741,71 @@
7.4  type case_data = (((string * string list) * string list) list * int);
7.5
7.6  fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
7.7 -  let
7.8 -    val thy = Proof_Context.theory_of ctxt;
7.9 -
7.10 -    val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
7.11 -    val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
7.12 -
7.13 -    fun inst_rule (concls, r) =
7.14 -      (if null insts then `Rule_Cases.get r
7.15 -       else (align_left "Rule has fewer conclusions than arguments given"
7.16 -          (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
7.17 -        |> maps (prep_inst ctxt align_right (atomize_term thy))
7.18 -        |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
7.19 -      |> mod_cases thy
7.20 -      |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
7.21 -
7.22 -    val ruleq =
7.23 -      (case opt_rule of
7.24 -        SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
7.25 -      | NONE =>
7.26 -          (get_inductP ctxt facts @
7.27 -            map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
7.28 -          |> map_filter (Rule_Cases.mutual_rule ctxt)
7.29 -          |> tap (trace_rules ctxt inductN o map #2)
7.30 -          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
7.31 -
7.32 -    fun rule_cases ctxt rule cases =
7.33 -      let
7.34 -        val rule' = Rule_Cases.internalize_params rule;
7.35 -        val rule'' = rule' |> simp ? simplified_rule ctxt;
7.36 -        val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
7.37 -        val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
7.38 -      in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') cases' end;
7.39 -  in
7.40 -    (fn i => fn st =>
7.41 -      ruleq
7.42 -      |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
7.43 -      |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
7.44 -        (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
7.45 -          (CONJUNCTS (ALLGOALS
7.46 -            let
7.47 -              val adefs = nth_list atomized_defs (j - 1);
7.48 -              val frees = fold (Term.add_frees o Thm.prop_of) adefs [];
7.49 -              val xs = nth_list arbitrary (j - 1);
7.50 -              val k = nth concls (j - 1) + more_consumes
7.51 -            in
7.52 -              Method.insert_tac (more_facts @ adefs) THEN'
7.53 -                (if simp then
7.54 -                   rotate_tac k (length adefs) THEN'
7.55 -                   arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
7.56 -                 else
7.57 -                   arbitrary_tac defs_ctxt k xs)
7.58 -             end)
7.59 -          THEN' inner_atomize_tac defs_ctxt) j))
7.60 -        THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
7.61 -            guess_instance ctxt (internalize ctxt more_consumes rule) i st'
7.62 -            |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
7.63 -            |> Seq.maps (fn rule' =>
7.64 -              CASES (rule_cases ctxt rule' cases)
7.65 -                (rtac rule' i THEN
7.66 -                  PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
7.67 -    THEN_ALL_NEW_CASES
7.68 -      ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac)
7.69 -        else K all_tac)
7.70 -       THEN_ALL_NEW rulify_tac ctxt)
7.71 -  end;
7.72 +  SUBGOAL_CASES (fn (_, i, st) =>
7.73 +    let
7.74 +      val thy = Proof_Context.theory_of ctxt;
7.75 +
7.76 +      val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
7.77 +      val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
7.78 +
7.79 +      fun inst_rule (concls, r) =
7.80 +        (if null insts then `Rule_Cases.get r
7.81 +         else (align_left "Rule has fewer conclusions than arguments given"
7.82 +            (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
7.83 +          |> maps (prep_inst ctxt align_right (atomize_term thy))
7.84 +          |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
7.85 +        |> mod_cases thy
7.86 +        |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
7.87 +
7.88 +      val ruleq =
7.89 +        (case opt_rule of
7.90 +          SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
7.91 +        | NONE =>
7.92 +            (get_inductP ctxt facts @
7.93 +              map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
7.94 +            |> map_filter (Rule_Cases.mutual_rule ctxt)
7.95 +            |> tap (trace_rules ctxt inductN o map #2)
7.96 +            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
7.97 +
7.98 +      fun rule_cases ctxt rule cases =
7.99 +        let
7.100 +          val rule' = Rule_Cases.internalize_params rule;
7.101 +          val rule'' = rule' |> simp ? simplified_rule ctxt;
7.102 +          val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
7.103 +          val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
7.104 +        in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') cases' end;
7.105 +    in
7.106 +      fn st =>
7.107 +        ruleq
7.108 +        |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
7.109 +        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
7.110 +          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
7.111 +            (CONJUNCTS (ALLGOALS
7.112 +              let
7.113 +                val adefs = nth_list atomized_defs (j - 1);
7.114 +                val frees = fold (Term.add_frees o Thm.prop_of) adefs [];
7.115 +                val xs = nth_list arbitrary (j - 1);
7.116 +                val k = nth concls (j - 1) + more_consumes
7.117 +              in
7.118 +                Method.insert_tac (more_facts @ adefs) THEN'
7.119 +                  (if simp then
7.120 +                     rotate_tac k (length adefs) THEN'
7.121 +                     arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
7.122 +                   else
7.123 +                     arbitrary_tac defs_ctxt k xs)
7.124 +               end)
7.125 +            THEN' inner_atomize_tac defs_ctxt) j))
7.126 +          THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
7.127 +              guess_instance ctxt (internalize ctxt more_consumes rule) i st'
7.128 +              |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
7.129 +              |> Seq.maps (fn rule' =>
7.130 +                CASES (rule_cases ctxt rule' cases)
7.131 +                  (rtac rule' i THEN
7.132 +                    PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))
7.133 +      end)
7.134 +      THEN_ALL_NEW_CASES
7.135 +        ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac) else K all_tac)
7.136 +         THEN_ALL_NEW rulify_tac ctxt);
7.137
7.138  val induct_tac = gen_induct_tac (K I);
7.139
7.140 @@ -832,7 +832,7 @@
7.141
7.142  in
7.143
7.144 -fun coinduct_tac ctxt inst taking opt_rule facts =
7.145 +fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i, st) =>
7.146    let
7.147      val thy = Proof_Context.theory_of ctxt;
7.148
7.149 @@ -849,7 +849,7 @@
7.150            |> tap (trace_rules ctxt coinductN)
7.151            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
7.152    in
7.153 -    SUBGOAL_CASES (fn (goal, i) => fn st =>
7.154 +    fn st =>
7.155        ruleq goal
7.156        |> Seq.maps (Rule_Cases.consume ctxt [] facts)
7.157        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
7.158 @@ -858,8 +858,8 @@
7.159          |> Seq.maps (fn rule' =>
7.160            CASES (Rule_Cases.make_common (thy,
7.161                Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
7.162 -            (Method.insert_tac more_facts i THEN rtac rule' i) st)))
7.163 -  end;
7.164 +            (Method.insert_tac more_facts i THEN rtac rule' i) st))
7.165 +  end);
7.166
7.167  end;
7.168
```
```     8.1 --- a/src/ZF/Tools/induct_tacs.ML	Thu Mar 20 19:58:33 2014 +0100
8.2 +++ b/src/ZF/Tools/induct_tacs.ML	Thu Mar 20 21:07:57 2014 +0100
8.3 @@ -89,7 +89,7 @@
8.4        (2) exhaustion works for VARIABLES in the premises, not general terms
8.5  **)
8.6
8.7 -fun exhaust_induct_tac exh ctxt var i state =
8.8 +fun exhaust_induct_tac exh ctxt var i state = SUBGOAL (fn _ =>
8.9    let
8.10      val thy = Proof_Context.theory_of ctxt
8.11      val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i state
8.12 @@ -102,12 +102,12 @@
8.13               [] => error "induction is not available for this datatype"
8.14             | major::_ => FOLogic.dest_Trueprop major)
8.15    in
8.16 -    eres_inst_tac ctxt [(ixn, var)] rule i state
8.17 +    eres_inst_tac ctxt [(ixn, var)] rule i
8.18    end
8.19    handle Find_tname msg =>
8.20              if exh then (*try boolean case analysis instead*)
8.21 -                case_tac ctxt var i state
8.22 -            else error msg;
8.23 +                case_tac ctxt var i
8.24 +            else error msg) i state;
8.25
8.26  val exhaust_tac = exhaust_induct_tac true;
8.27  val induct_tac = exhaust_induct_tac false;
```