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