src/HOL/Tools/SMT/conj_disj_perm.ML
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (18 months ago)
changeset 67091 1393c2340eec
parent 60752 b48830b670a1
child 67149 e61557884799
permissions -rw-r--r--
more symbols;
     1 (*  Title:      HOL/Tools/SMT/conj_disj_perm.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Tactic to prove equivalence of permutations of conjunctions and disjunctions.
     5 *)
     6 
     7 signature CONJ_DISJ_PERM =
     8 sig
     9   val conj_disj_perm_tac: Proof.context -> int -> tactic
    10 end
    11 
    12 structure Conj_Disj_Perm: CONJ_DISJ_PERM =
    13 struct
    14 
    15 fun with_assumption ct f =
    16   let val ct' = Thm.apply @{cterm HOL.Trueprop} ct
    17   in Thm.implies_intr ct' (f (Thm.assume ct')) end
    18 
    19 fun eq_from_impls thm1 thm2 = thm2 INCR_COMP (thm1 INCR_COMP @{thm iffI})
    20 
    21 fun add_lit thm = Termtab.update (HOLogic.dest_Trueprop (Thm.prop_of thm), thm)
    22 
    23 val ndisj1_rule = @{lemma "\<not>(P \<or> Q) \<Longrightarrow> \<not>P" by auto}
    24 val ndisj2_rule = @{lemma "\<not>(P \<or> Q) \<Longrightarrow> \<not>Q" by auto}
    25 
    26 fun explode_thm thm =
    27   (case HOLogic.dest_Trueprop (Thm.prop_of thm) of
    28     @{const HOL.conj} $ _ $ _ => explode_conj_thm @{thm conjunct1} @{thm conjunct2} thm
    29   | @{const HOL.Not} $ (@{const HOL.disj} $ _ $ _) => explode_conj_thm ndisj1_rule ndisj2_rule thm
    30   | @{const HOL.Not} $ (@{const HOL.Not} $ _) => explode_thm (thm RS @{thm notnotD})
    31   | _ => add_lit thm)
    32 
    33 and explode_conj_thm rule1 rule2 thm lits =
    34   explode_thm (thm RS rule1) (explode_thm (thm RS rule2) (add_lit thm lits))
    35 
    36 val not_false_rule = @{lemma "\<not>False" by auto}
    37 fun explode thm = explode_thm thm (add_lit not_false_rule (add_lit @{thm TrueI} Termtab.empty))
    38 
    39 fun find_dual_lit lits (@{const HOL.Not} $ t, thm) = Termtab.lookup lits t |> Option.map (pair thm)
    40   | find_dual_lit _ _ = NONE
    41 
    42 fun find_dual_lits lits = Termtab.get_first (find_dual_lit lits) lits
    43 
    44 val not_not_rule = @{lemma "P \<Longrightarrow> \<not>\<not>P" by auto}
    45 val ndisj_rule = @{lemma "\<not>P \<Longrightarrow> \<not>Q \<Longrightarrow> \<not>(P \<or> Q)" by auto}
    46 
    47 fun join lits t =
    48   (case Termtab.lookup lits t of
    49     SOME thm => thm
    50   | NONE => join_term lits t)
    51 
    52 and join_term lits (@{const HOL.conj} $ t $ u) = @{thm conjI} OF (map (join lits) [t, u])
    53   | join_term lits (@{const HOL.Not} $ (@{const HOL.disj} $ t $ u)) =
    54       ndisj_rule OF (map (join lits o HOLogic.mk_not) [t, u])
    55   | join_term lits (@{const HOL.Not} $ (@{const HOL.Not} $ t)) = join lits t RS not_not_rule
    56   | join_term _ t = raise TERM ("join_term", [t])
    57 
    58 fun prove_conj_disj_imp ct cu = with_assumption ct (fn thm => join (explode thm) (Thm.term_of cu))
    59 
    60 fun 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 
    66 val not_not_false_rule = @{lemma "\<not>\<not>False \<Longrightarrow> P" by auto}
    67 val not_true_rule = @{lemma "\<not>True \<Longrightarrow> P" by auto}
    68 
    69 fun prove_any_imp ct =
    70   (case Thm.term_of ct of
    71     @{const HOL.False} => @{thm FalseE}
    72   | @{const HOL.Not} $ (@{const HOL.Not} $ @{const HOL.False}) => not_not_false_rule
    73   | @{const HOL.Not} $ @{const HOL.True} => not_true_rule
    74   | _ => raise CTERM ("prove_any_imp", [ct]))
    75 
    76 fun prove_contradiction_imp ct =
    77   with_assumption ct (fn thm =>
    78     let val lits = explode thm
    79     in
    80       (case Termtab.lookup lits @{const HOL.False} of
    81         SOME thm' => thm' RS @{thm FalseE}
    82       | NONE =>
    83           (case Termtab.lookup lits (@{const HOL.Not} $ @{const HOL.True}) 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 
    91 fun 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 
    97 val contrapos_rule = @{lemma "(\<not>P) = (\<not>Q) \<Longrightarrow> P = Q" by auto}
    98 fun contrapos prove cp = contrapos_rule OF [prove (apply2 (Thm.apply @{cterm HOL.Not}) cp)]
    99 
   100 datatype kind = True | False | Conj | Disj | Other
   101 
   102 fun choose t _ _ _ @{const HOL.True} = t
   103   | choose _ f _ _ @{const HOL.False} = f
   104   | choose _ _ c _ (@{const HOL.conj} $ _ $ _) = c
   105   | choose _ _ _ d (@{const HOL.disj} $ _ $ _) = d
   106   | choose _ _ _ _ _ = Other
   107 
   108 fun kind_of (@{const HOL.Not} $ t) = choose False True Disj Conj t
   109   | kind_of t = choose True False Conj Disj t
   110 
   111 fun 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 
   121 fun conj_disj_perm_tac ctxt = CSUBGOAL (fn (ct, i) => 
   122   (case Thm.term_of ct of
   123     @{const HOL.Trueprop} $ (@{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 
   127 end