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