1(* Title: HOL/Tools/SMT/conj_disj_perm.ML 2 Author: Sascha Boehme, TU Muenchen 3 4Tactic to prove equivalence of permutations of conjunctions and disjunctions. 5*) 6 7signature CONJ_DISJ_PERM = 8sig 9 val conj_disj_perm_tac: Proof.context -> int -> tactic 10end 11 12structure Conj_Disj_Perm: CONJ_DISJ_PERM = 13struct 14 15fun with_assumption ct f = 16 let val ct' = Thm.apply \<^cterm>\<open>HOL.Trueprop\<close> ct 17 in Thm.implies_intr ct' (f (Thm.assume ct')) end 18 19fun eq_from_impls thm1 thm2 = thm2 INCR_COMP (thm1 INCR_COMP @{thm iffI}) 20 21fun add_lit thm = Termtab.update (HOLogic.dest_Trueprop (Thm.prop_of thm), thm) 22 23val ndisj1_rule = @{lemma "\<not>(P \<or> Q) \<Longrightarrow> \<not>P" by auto} 24val ndisj2_rule = @{lemma "\<not>(P \<or> Q) \<Longrightarrow> \<not>Q" by auto} 25 26fun explode_thm thm = 27 (case HOLogic.dest_Trueprop (Thm.prop_of thm) of 28 \<^const>\<open>HOL.conj\<close> $ _ $ _ => explode_conj_thm @{thm conjunct1} @{thm conjunct2} thm 29 | \<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.disj\<close> $ _ $ _) => explode_conj_thm ndisj1_rule ndisj2_rule thm 30 | \<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.Not\<close> $ _) => explode_thm (thm RS @{thm notnotD}) 31 | _ => add_lit thm) 32 33and explode_conj_thm rule1 rule2 thm lits = 34 explode_thm (thm RS rule1) (explode_thm (thm RS rule2) (add_lit thm lits)) 35 36val not_false_rule = @{lemma "\<not>False" by auto} 37fun explode thm = explode_thm thm (add_lit not_false_rule (add_lit @{thm TrueI} Termtab.empty)) 38 39fun find_dual_lit lits (\<^const>\<open>HOL.Not\<close> $ t, thm) = Termtab.lookup lits t |> Option.map (pair thm) 40 | find_dual_lit _ _ = NONE 41 42fun find_dual_lits lits = Termtab.get_first (find_dual_lit lits) lits 43 44val not_not_rule = @{lemma "P \<Longrightarrow> \<not>\<not>P" by auto} 45val ndisj_rule = @{lemma "\<not>P \<Longrightarrow> \<not>Q \<Longrightarrow> \<not>(P \<or> Q)" by auto} 46 47fun join lits t = 48 (case Termtab.lookup lits t of 49 SOME thm => thm 50 | NONE => join_term lits t) 51 52and join_term lits (\<^const>\<open>HOL.conj\<close> $ t $ u) = @{thm conjI} OF (map (join lits) [t, u]) 53 | join_term lits (\<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.disj\<close> $ t $ u)) = 54 ndisj_rule OF (map (join lits o HOLogic.mk_not) [t, u]) 55 | join_term lits (\<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.Not\<close> $ t)) = join lits t RS not_not_rule 56 | join_term _ t = raise TERM ("join_term", [t]) 57 58fun prove_conj_disj_imp ct cu = with_assumption ct (fn thm => join (explode thm) (Thm.term_of cu)) 59 60fun prove_conj_disj_eq (clhs, crhs) = 61 let 62 val thm1 = prove_conj_disj_imp clhs crhs 63 val thm2 = prove_conj_disj_imp crhs clhs 64 in eq_from_impls thm1 thm2 end 65 66val not_not_false_rule = @{lemma "\<not>\<not>False \<Longrightarrow> P" by auto} 67val not_true_rule = @{lemma "\<not>True \<Longrightarrow> P" by auto} 68 69fun prove_any_imp ct = 70 (case Thm.term_of ct of 71 \<^const>\<open>HOL.False\<close> => @{thm FalseE} 72 | \<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.Not\<close> $ \<^const>\<open>HOL.False\<close>) => not_not_false_rule 73 | \<^const>\<open>HOL.Not\<close> $ \<^const>\<open>HOL.True\<close> => not_true_rule 74 | _ => raise CTERM ("prove_any_imp", [ct])) 75 76fun prove_contradiction_imp ct = 77 with_assumption ct (fn thm => 78 let val lits = explode thm 79 in 80 (case Termtab.lookup lits \<^const>\<open>HOL.False\<close> of 81 SOME thm' => thm' RS @{thm FalseE} 82 | NONE => 83 (case Termtab.lookup lits (\<^const>\<open>HOL.Not\<close> $ \<^const>\<open>HOL.True\<close>) of 84 SOME thm' => thm' RS not_true_rule 85 | NONE => 86 (case find_dual_lits lits of 87 SOME (not_lit_thm, lit_thm) => @{thm notE} OF [not_lit_thm, lit_thm] 88 | NONE => raise CTERM ("prove_contradiction", [ct])))) 89 end) 90 91fun prove_contradiction_eq to_right (clhs, crhs) = 92 let 93 val thm1 = if to_right then prove_contradiction_imp clhs else prove_any_imp clhs 94 val thm2 = if to_right then prove_any_imp crhs else prove_contradiction_imp crhs 95 in eq_from_impls thm1 thm2 end 96 97val contrapos_rule = @{lemma "(\<not>P) = (\<not>Q) \<Longrightarrow> P = Q" by auto} 98fun contrapos prove cp = contrapos_rule OF [prove (apply2 (Thm.apply \<^cterm>\<open>HOL.Not\<close>) cp)] 99 100datatype kind = True | False | Conj | Disj | Other 101 102fun choose t _ _ _ \<^const>\<open>HOL.True\<close> = t 103 | choose _ f _ _ \<^const>\<open>HOL.False\<close> = f 104 | choose _ _ c _ (\<^const>\<open>HOL.conj\<close> $ _ $ _) = c 105 | choose _ _ _ d (\<^const>\<open>HOL.disj\<close> $ _ $ _) = d 106 | choose _ _ _ _ _ = Other 107 108fun kind_of (\<^const>\<open>HOL.Not\<close> $ t) = choose False True Disj Conj t 109 | kind_of t = choose True False Conj Disj t 110 111fun prove_conj_disj_perm ct cp = 112 (case apply2 (kind_of o Thm.term_of) cp of 113 (Conj, Conj) => prove_conj_disj_eq cp 114 | (Disj, Disj) => contrapos prove_conj_disj_eq cp 115 | (Conj, False) => prove_contradiction_eq true cp 116 | (False, Conj) => prove_contradiction_eq false cp 117 | (Disj, True) => contrapos (prove_contradiction_eq true) cp 118 | (True, Disj) => contrapos (prove_contradiction_eq false) cp 119 | _ => raise CTERM ("prove_conj_disj_perm", [ct])) 120 121fun conj_disj_perm_tac ctxt = CSUBGOAL (fn (ct, i) => 122 (case Thm.term_of ct of 123 \<^const>\<open>HOL.Trueprop\<close> $ (@{const HOL.eq(bool)} $ _ $ _) => 124 resolve_tac ctxt [prove_conj_disj_perm ct (Thm.dest_binop (Thm.dest_arg ct))] i 125 | _ => no_tac)) 126 127end; 128