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