1(*
2 * Copyright 2015, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 *)
10
11theory ProvePart
12imports Main
13begin
14
15text {* Introduces a (sort-of) tactic for proving part of a goal by automatic
16methods. The split between the proven and unproven part goes down into conjunction,
17implication etc. The unproven parts are left in (roughly) their original form. *}
18
19text {*
20The first part is to take a goal and split it into two conjuncts,
21e.g. "a \<and> (\<forall>x. b \<and> c x)
22    = (((P1 \<longrightarrow> a) \<and> (\<forall>x. (P2 \<longrightarrow> b) \<and> (P3 \<longrightarrow> c x)))
23        \<and> ((\<not> P1 \<longrightarrow> a) \<and> (\<forall>x. (\<not> P2 \<longrightarrow> b) \<and> (\<not> P3 \<longrightarrow> c x)))"
24
25The first conjunct is then attacked by some automatic method.
26
27The final part is to eliminate any goals remaining after that
28automatic method by setting the Pi to False. The remaining Pi
29(whose goal fragments were solved) are set to True. If the
30resulting goals cannot be solved by setting to False, or if
31no Pi are actually set to true, the process fails.
32*}
33
34lemma logic_to_conj_thm_workers:
35  "A = (A' \<and> A'') \<Longrightarrow> B = (B' \<and> B'')
36    \<Longrightarrow> (A \<and> B) = ((A' \<and> B') \<and> (A'' \<and> B''))"
37  "B = (B' \<and> B'')
38    \<Longrightarrow> (A \<or> B) = ((A \<or> B') \<and> (A \<or> B''))"
39  "\<lbrakk> \<And>x. P x = (P' x \<and> P'' x) \<rbrakk>
40    \<Longrightarrow> (\<forall>x. P x) = ((\<forall>x. P' x) \<and> (\<forall>x. P'' x))"
41  "\<lbrakk> \<And>x. P x = (P' x \<and> P'' x) \<rbrakk>
42    \<Longrightarrow> (\<forall>x \<in> S. P x) = ((\<forall>x \<in> S. P' x) \<and> (\<forall>x \<in> S. P'' x))"
43  "B = (B' \<and> B'')
44    \<Longrightarrow> (A \<longrightarrow> B) = ((A \<longrightarrow> B') \<and> (A \<longrightarrow> B''))"
45  by auto
46
47ML {*
48structure Split_To_Conj = struct
49
50fun abs_name (Abs (s, _, _)) = s
51  | abs_name _ = "x"
52
53fun all_type (Const (@{const_name "All"}, T) $ _)
54    = domain_type (domain_type T)
55  | all_type (Const (@{const_name "Ball"}, T) $ _ $ _)
56    = domain_type (domain_type (range_type T))
57  | all_type t = raise TERM ("all_type", [t])
58
59fun split_thm prefix ctxt t = let
60    val ok = not (String.isPrefix "Q" prefix orelse String.isPrefix "R" prefix)
61    val _ = ok orelse error ("split_thm: prefix has prefix Q/R: " ^ prefix)
62    fun params (@{term "(\<and>)"} $ x $ y) Ts = params x Ts @ params y Ts
63      | params (@{term "(\<or>)"} $ _ $ y) Ts = (Ts, SOME @{typ bool}) :: params y Ts
64      | params (all as (Const (@{const_name "All"}, _) $ t)) Ts
65        = params (betapply (t, Bound 0)) (all_type all :: Ts)
66      | params (ball as (Const (@{const_name "Ball"}, T) $ _ $ t)) Ts
67        = (Ts, SOME (domain_type T)) :: params (betapply (t, Bound 0)) (all_type ball :: Ts)
68      | params (@{term "(\<longrightarrow>)"} $ _ $ t) Ts = (Ts, SOME @{typ bool}) :: params t Ts
69      | params _ Ts = [(Ts, NONE)]
70    val ps = params t []
71    val Ps = Variable.variant_frees ctxt [t]
72        (replicate (length ps) (prefix, @{typ bool}))
73        |> map Free
74    val Qs = Variable.variant_frees ctxt [t]
75        (map (fn (ps, T) => case T of NONE => ("Q", ps ---> @{typ bool})
76                | SOME T => ("R", ps ---> T)) ps)
77        |> map Free
78    val Qs = map (fn (Q, (ps, _)) => Term.list_comb (Q, map Bound (0 upto (length ps - 1))))
79        (Qs ~~ ps)
80    fun assemble_bits (@{term "(\<and>)"} $ x $ y) Ps = let
81        val (x, Ps) = assemble_bits x Ps
82        val (y, Ps) = assemble_bits y Ps
83      in (@{term "(\<and>)"} $ x $ y, Ps) end
84      | assemble_bits (@{term "(\<or>)"} $ _ $ y) Ps = let
85        val x = hd Ps
86        val (y, Ps) = assemble_bits y (tl Ps)
87      in (@{term "(\<or>)"} $ x $ y, Ps) end
88      | assemble_bits (all as (Const (@{const_name "All"}, T) $ t)) Ps = let
89        val nm = abs_name t
90        val (t, Ps) = assemble_bits (betapply (t, Bound 0)) Ps
91      in (Const (@{const_name "All"}, T) $ Abs (nm, all_type all, t), Ps) end
92      | assemble_bits (ball as (Const (@{const_name "Ball"}, T) $ _ $ t)) Ps = let
93        val nm = abs_name t
94        val S = hd Ps
95        val (t, Ps) = assemble_bits (betapply (t, Bound 0)) (tl Ps)
96      in (Const (@{const_name "Ball"}, T) $ S $ Abs (nm, all_type ball, t), Ps) end
97      | assemble_bits (@{term "(\<longrightarrow>)"} $ _ $ y) Ps = let
98        val x = hd Ps
99        val (y, Ps) = assemble_bits y (tl Ps)
100      in (@{term "(\<longrightarrow>)"} $ x $ y, Ps) end
101      | assemble_bits _ Ps = (hd Ps, tl Ps)
102    val bits_lhs = assemble_bits t Qs |> fst
103    fun imp tf (P, Q) = if String.isPrefix "R" (fst (dest_Free (head_of Q))) then Q
104        else HOLogic.mk_imp (if tf then P else HOLogic.mk_not P, Q)
105    val bits_true = assemble_bits t (map (imp true) (Ps ~~ Qs)) |> fst
106    val bits_false = assemble_bits t (map (imp false) (Ps ~~ Qs)) |> fst
107    val concl = HOLogic.mk_eq (bits_lhs, HOLogic.mk_conj (bits_true, bits_false))
108      |> HOLogic.mk_Trueprop
109  in (Goal.prove ctxt (map (fst o dest_Free o head_of) Qs) [] concl
110    (K (REPEAT_ALL_NEW (resolve_tac ctxt
111        @{thms logic_to_conj_thm_workers cases_simp[symmetric]}) 1)),
112        map dest_Free Ps)
113  end
114
115fun get_split_tac prefix ctxt tac = SUBGOAL (fn (t, i) =>
116  let
117    val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl t)
118    val (thm, Ps) = split_thm prefix ctxt concl
119  in (resolve0_tac [ @{thm iffD2} ] THEN' resolve0_tac [thm] THEN' tac Ps) end i)
120
121end
122*}
123
124text {* Testing. *}
125
126ML {*
127Split_To_Conj.split_thm "P" @{context}
128  @{term "x & y & (\<forall>t \<in> UNIV. \<forall>n. True \<longrightarrow> z t n)"}
129*}
130
131ML {*
132structure Partial_Prove = struct
133
134fun inst_frees_tac _ Ps ct = REPEAT_DETERM o SUBGOAL (fn (t, _) =>
135  fn thm => case Term.add_frees t [] |> filter (member (=) Ps)
136  of [] => Seq.empty
137  | (f :: _) => let
138    val idx = Thm.maxidx_of thm + 1
139    val var = ((fst f, idx), snd f)
140  in thm |> Thm.generalize ([], [fst f]) idx
141    |> Thm.instantiate ([], [(var, ct)])
142    |> Seq.single
143  end)
144
145fun cleanup_tac ctxt Ps
146    = inst_frees_tac ctxt Ps @{cterm False}
147      THEN' asm_full_simp_tac ctxt
148
149fun finish_tac ctxt Ps = inst_frees_tac ctxt Ps @{cterm True}
150    THEN' CONVERSION (Conv.params_conv ~1 (fn ctxt =>
151            (Conv.concl_conv ~1 (Simplifier.rewrite (put_simpset HOL_ss ctxt)))
152        ) ctxt)
153
154fun test_start_partial_prove ctxt i t = let
155    val j = Thm.nprems_of t - i
156  in Split_To_Conj.get_split_tac ("P_" ^ string_of_int j ^ "_") ctxt
157        (K (K all_tac)) i t
158  end
159
160fun test_end_partial_prove ctxt t = let
161    fun match_P (s, T) = case space_explode "_" s of
162        ["P", n, _] => try (fn () => ((s, T), the (Int.fromString n))) ()
163      | _ => NONE
164    val Ps = Term.add_frees (Thm.concl_of t) [] |> map_filter match_P
165    fun getmax ((x, n) :: xs) max maxes = if n > max then getmax xs n [x]
166      else getmax xs max maxes
167      | getmax [] max maxes = (max, maxes)
168    val (j, Ps) = getmax Ps 0 []
169    val i = Thm.nprems_of t - j
170  in REPEAT_DETERM (FIRSTGOAL (fn k => if k < i then cleanup_tac ctxt Ps k else no_tac))
171    THEN finish_tac ctxt Ps i end t
172
173fun partial_prove tactic ctxt i
174    = Split_To_Conj.get_split_tac ("P_" ^ string_of_int i ^ "_") ctxt
175      (fn Ps => fn i => tactic i THEN finish_tac ctxt Ps i) i
176
177fun method (ctxtg, []) = (fn ctxt => Method.SIMPLE_METHOD (test_start_partial_prove ctxt 1),
178    (ctxtg, []))
179  | method args = error "Partial_Prove: still working on that"
180
181fun fin_method () = Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (test_end_partial_prove ctxt))
182
183end
184*}
185
186method_setup partial_prove = {* Partial_Prove.method *}
187  "partially prove a compound goal by some automatic method"
188
189method_setup finish_partial_prove = {* Partial_Prove.fin_method () *}
190  "partially prove a compound goal by some automatic method"
191
192end
193