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