1(*  Title:      Subgoal_Methods.thy
2    Author:     Daniel Matichuk, NICTA/UNSW
3
4Methods for managing subgoals collectively.
5*)
6
7(*
8 * Copyright 2014, NICTA
9 *
10 * This software may be distributed and modified according to the terms of
11 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
12 * See "LICENSE_BSD2.txt" for details.
13 *
14 * @TAG(NICTA_BSD)
15 *)
16
17theory Subgoal_Methods
18imports Main
19begin
20ML \<open>
21signature SUBGOAL_METHODS =
22sig
23  val fold_subgoals: Proof.context -> bool -> thm -> thm
24  val unfold_subgoals_tac: Proof.context -> tactic
25  val distinct_subgoals: Proof.context -> thm -> thm
26end;
27
28structure Subgoal_Methods: SUBGOAL_METHODS =
29struct
30
31fun max_common_prefix eq (ls :: lss) =
32      let
33        val ls' = tag_list 0 ls;
34        fun all_prefix (i,a) =
35          forall (fn ls' => if length ls' > i then eq (a, nth ls' i) else false) lss
36        val ls'' = take_prefix all_prefix ls'
37      in map snd ls'' end
38  | max_common_prefix _ [] = [];
39
40fun push_outer_params ctxt th =
41  let
42    val ctxt' = ctxt
43      |> Simplifier.empty_simpset
44      |> Simplifier.add_simp Drule.norm_hhf_eq;
45  in
46    Conv.fconv_rule
47      (Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE)) ctxt') th
48  end;
49
50fun fix_schematics ctxt raw_st =
51  let
52    val ((schematic_types, [st']), ctxt1) = Variable.importT [raw_st] ctxt;
53    val ((_, inst), ctxt2) =
54      Variable.import_inst true [Thm.prop_of st'] ctxt1;
55
56    val schematic_terms = map (apsnd (Thm.cterm_of ctxt2)) inst;
57    val schematics = (schematic_types, schematic_terms);
58
59  in (Thm.instantiate schematics st', ctxt2) end
60
61val strip_params = Term.strip_all_vars;
62val strip_prems = Logic.strip_imp_prems o Term.strip_all_body;
63val strip_concl = Logic.strip_imp_concl o Term.strip_all_body;
64
65
66
67fun fold_subgoals ctxt prefix raw_st =
68  if Thm.nprems_of raw_st < 2 then raw_st
69  else
70    let
71      val (st, inner_ctxt) = fix_schematics ctxt raw_st;
72
73      val subgoals = Thm.prems_of st;
74      val paramss = map strip_params subgoals;
75      val common_params = max_common_prefix (eq_snd (op =)) paramss;
76
77      fun strip_shift subgoal =
78        let
79          val params = strip_params subgoal;
80          val diff = length common_params - length params;
81          val prems = strip_prems subgoal;
82        in map (Term.incr_boundvars diff) prems end;
83
84      val premss = map (strip_shift) subgoals;
85
86      val common_prems = max_common_prefix (op aconv) premss;
87
88      val common_params = if prefix then common_params else [];
89      val common_prems = if prefix then common_prems else [];
90
91      fun mk_concl subgoal =
92        let
93          val params = Term.strip_all_vars subgoal;
94          val local_params = drop (length common_params) params;
95          val prems = strip_prems subgoal;
96          val local_prems = drop (length common_prems) prems;
97          val concl = strip_concl subgoal;
98        in Logic.list_all (local_params, Logic.list_implies (local_prems, concl)) end;
99
100      val goal =
101        Logic.list_all (common_params,
102          (Logic.list_implies (common_prems,Logic.mk_conjunction_list (map mk_concl subgoals))));
103
104      val chyp = Thm.cterm_of inner_ctxt goal;
105
106      val (common_params',inner_ctxt') =
107        Variable.add_fixes (map fst common_params) inner_ctxt
108        |>> map2 (fn (_, T) => fn x => Thm.cterm_of inner_ctxt (Free (x, T))) common_params;
109
110      fun try_dest rule =
111        try (fn () => (@{thm conjunctionD1} OF [rule], @{thm conjunctionD2} OF [rule])) ();
112
113      fun solve_headgoal rule =
114        let
115          val rule' = rule
116            |> Drule.forall_intr_list common_params'
117            |> push_outer_params inner_ctxt';
118        in
119          (fn st => Thm.implies_elim st rule')
120        end;
121
122      fun solve_subgoals rule' st =
123        (case try_dest rule' of
124          SOME (this, rest) => solve_subgoals rest (solve_headgoal this st)
125        | NONE => solve_headgoal rule' st);
126
127      val rule = Drule.forall_elim_list common_params' (Thm.assume chyp);
128    in
129      st
130      |> push_outer_params inner_ctxt
131      |> solve_subgoals rule
132      |> Thm.implies_intr chyp
133      |> singleton (Variable.export inner_ctxt' ctxt)
134    end;
135
136fun distinct_subgoals ctxt raw_st =
137  let
138    val (st, inner_ctxt) = fix_schematics ctxt raw_st;
139    val subgoals = Drule.cprems_of st;
140    val atomize = Conv.fconv_rule (Object_Logic.atomize_prems inner_ctxt);
141
142    val rules =
143      map (atomize o Raw_Simplifier.norm_hhf inner_ctxt o Thm.assume) subgoals
144      |> sort (int_ord o apply2 Thm.nprems_of);
145
146    val st' = st
147      |> ALLGOALS (fn i =>
148        Object_Logic.atomize_prems_tac inner_ctxt i THEN solve_tac inner_ctxt rules i)
149      |> Seq.hd;
150
151    val subgoals' = subgoals
152      |> inter (op aconvc) (Thm.chyps_of st')
153      |> distinct (op aconvc);
154  in
155    Drule.implies_intr_list subgoals' st'
156    |> singleton (Variable.export inner_ctxt ctxt)
157  end;
158
159(* Variant of filter_prems_tac that recovers premise order *)
160fun filter_prems_tac' ctxt pred =
161  let
162    fun Then NONE tac = SOME tac
163      | Then (SOME tac) tac' = SOME (tac THEN' tac');
164    fun thins H (tac, n, i) =
165      (if pred H then (tac, n + 1, i)
166       else (Then tac (rotate_tac n THEN' eresolve_tac ctxt [thin_rl]), 0, i + n));
167  in
168    SUBGOAL (fn (goal, i) =>
169      let val Hs = Logic.strip_assums_hyp goal in
170        (case fold thins Hs (NONE, 0, 0) of
171          (NONE, _, _) => no_tac
172        | (SOME tac, _, n) => tac i THEN rotate_tac (~ n) i)
173      end)
174  end;
175
176fun trim_prems_tac ctxt rules =
177let
178  fun matches (prem,rule) =
179  let
180    val ((_,prem'),ctxt') = Variable.focus NONE prem ctxt;
181    val rule_prop = Thm.prop_of rule;
182  in Unify.matches_list (Context.Proof ctxt') [rule_prop] [prem'] end;
183
184in filter_prems_tac' ctxt (not o member matches rules) end;
185
186val adhoc_conjunction_tac = REPEAT_ALL_NEW
187  (SUBGOAL (fn (goal, i) =>
188    if can Logic.dest_conjunction (Logic.strip_imp_concl goal)
189    then resolve0_tac [Conjunction.conjunctionI] i
190    else no_tac));
191
192fun unfold_subgoals_tac ctxt =
193  TRY (adhoc_conjunction_tac 1)
194  THEN (PRIMITIVE (Raw_Simplifier.norm_hhf ctxt));
195
196val _ =
197  Theory.setup
198   (Method.setup @{binding fold_subgoals}
199      (Scan.lift (Args.mode "prefix") >> (fn prefix => fn ctxt =>
200         SIMPLE_METHOD (PRIMITIVE (fold_subgoals ctxt prefix))))
201      "lift all subgoals over common premises/params" #>
202    Method.setup @{binding unfold_subgoals}
203      (Scan.succeed (fn ctxt => SIMPLE_METHOD (unfold_subgoals_tac ctxt)))
204      "recover subgoals after folding" #>
205    Method.setup @{binding distinct_subgoals}
206      (Scan.succeed (fn ctxt => SIMPLE_METHOD (PRIMITIVE (distinct_subgoals ctxt))))
207     "trim all subgoals to be (logically) distinct" #>
208    Method.setup @{binding trim}
209      (Attrib.thms >> (fn thms => fn ctxt =>
210         SIMPLE_METHOD (HEADGOAL (trim_prems_tac ctxt thms))))
211     "trim all premises that match the given rules");
212
213end;
214\<close>
215
216end
217