src/HOL/Decision_Procs/langford.ML
author nipkow
Tue Feb 23 16:25:08 2016 +0100 (2016-02-23)
changeset 62390 842917225d56
parent 61144 5e94dfead1c2
child 62391 1658fc9b2618
permissions -rw-r--r--
more canonical names
haftmann@37744
     1
(*  Title:      HOL/Decision_Procs/langford.ML
wenzelm@29269
     2
    Author:     Amine Chaieb, TU Muenchen
wenzelm@29269
     3
*)
wenzelm@29269
     4
wenzelm@55848
     5
signature LANGFORD =
chaieb@23906
     6
sig
chaieb@23906
     7
  val dlo_tac : Proof.context -> int -> tactic
chaieb@23906
     8
  val dlo_conv : Proof.context -> cterm -> thm
chaieb@23906
     9
end
chaieb@23906
    10
wenzelm@55848
    11
structure Langford: LANGFORD =
chaieb@23906
    12
struct
chaieb@23906
    13
haftmann@30452
    14
val dest_set =
wenzelm@55792
    15
  let
wenzelm@55792
    16
    fun h acc ct =
wenzelm@59582
    17
      (case Thm.term_of ct of
wenzelm@55792
    18
        Const (@{const_name Orderings.bot}, _) => acc
wenzelm@55792
    19
      | Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct));
wenzelm@55792
    20
  in h [] end;
haftmann@30452
    21
wenzelm@55506
    22
fun prove_finite cT u =
wenzelm@55792
    23
  let
wenzelm@60801
    24
    val [th0, th1] = map (Thm.instantiate' [SOME cT] []) @{thms finite.intros}
chaieb@23906
    25
    fun ins x th =
wenzelm@55792
    26
      Thm.implies_elim
wenzelm@60801
    27
        (Thm.instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) (Thm.cprop_of th), SOME x] th1) th
wenzelm@55792
    28
  in fold ins u th0 end;
chaieb@23906
    29
wenzelm@51717
    30
fun simp_rule ctxt =
wenzelm@45654
    31
  Conv.fconv_rule
wenzelm@51717
    32
    (Conv.arg_conv
wenzelm@51717
    33
      (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms ball_simps simp_thms})));
chaieb@23906
    34
wenzelm@55506
    35
fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep =
wenzelm@59582
    36
  (case Thm.term_of ep of
wenzelm@55846
    37
    Const (@{const_name Ex}, _) $ _ =>
wenzelm@55846
    38
      let
wenzelm@55846
    39
        val p = Thm.dest_arg ep
wenzelm@55846
    40
        val ths =
wenzelm@55846
    41
          simplify (put_simpset HOL_basic_ss ctxt addsimps gather)
wenzelm@60801
    42
            (Thm.instantiate' [] [SOME p] stupid)
wenzelm@55846
    43
        val (L, U) =
wenzelm@55846
    44
          let val (_, q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths))
wenzelm@55846
    45
          in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1) end
wenzelm@55846
    46
        fun proveneF S =
wenzelm@55846
    47
          let
wenzelm@55846
    48
            val (a, A) = Thm.dest_comb S |>> Thm.dest_arg
wenzelm@59586
    49
            val cT = Thm.ctyp_of_cterm a
wenzelm@60801
    50
            val ne = Thm.instantiate' [SOME cT] [SOME a, SOME A] @{thm insert_not_empty}
wenzelm@55846
    51
            val f = prove_finite cT (dest_set S)
wenzelm@55846
    52
         in (ne, f) end
chaieb@23906
    53
wenzelm@55846
    54
        val qe =
wenzelm@59582
    55
          (case (Thm.term_of L, Thm.term_of U) of
wenzelm@55846
    56
            (Const (@{const_name Orderings.bot}, _),_) =>
wenzelm@55846
    57
              let val (neU, fU) = proveneF U
wenzelm@55846
    58
              in simp_rule ctxt (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end
wenzelm@55846
    59
          | (_, Const (@{const_name Orderings.bot}, _)) =>
wenzelm@55846
    60
              let val (neL,fL) = proveneF L
wenzelm@55846
    61
              in simp_rule ctxt (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end
wenzelm@55846
    62
          | _ =>
wenzelm@55846
    63
              let
wenzelm@55846
    64
                val (neL, fL) = proveneF L
wenzelm@55846
    65
                val (neU, fU) = proveneF U
wenzelm@55846
    66
              in simp_rule ctxt (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU])) end)
wenzelm@55846
    67
      in qe end
wenzelm@55846
    68
  | _ => error "dlo_qe : Not an existential formula");
chaieb@23906
    69
wenzelm@55506
    70
val all_conjuncts =
wenzelm@55846
    71
  let
wenzelm@55846
    72
    fun h acc ct =
wenzelm@59582
    73
      (case Thm.term_of ct of
wenzelm@55846
    74
        @{term HOL.conj} $ _ $ _ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
wenzelm@55846
    75
      | _ => ct :: acc)
wenzelm@55846
    76
  in h [] end;
chaieb@23906
    77
chaieb@23906
    78
fun conjuncts ct =
wenzelm@59582
    79
  (case Thm.term_of ct of
wenzelm@55846
    80
    @{term HOL.conj} $ _ $ _ => Thm.dest_arg1 ct :: conjuncts (Thm.dest_arg ct)
wenzelm@55846
    81
  | _ => [ct]);
chaieb@23906
    82
wenzelm@55846
    83
fun fold1 f = foldr1 (uncurry f);  (* FIXME !? *)
chaieb@23906
    84
wenzelm@55846
    85
val list_conj =
wenzelm@55846
    86
  fold1 (fn c => fn c' => Thm.apply (Thm.apply @{cterm HOL.conj} c) c');
chaieb@23906
    87
wenzelm@55506
    88
fun mk_conj_tab th =
wenzelm@55846
    89
  let
wenzelm@55846
    90
    fun h acc th =
wenzelm@59582
    91
      (case Thm.prop_of th of
wenzelm@55846
    92
        @{term "Trueprop"} $ (@{term HOL.conj} $ p $ q) =>
wenzelm@55846
    93
          h (h acc (th RS conjunct2)) (th RS conjunct1)
wenzelm@55846
    94
      | @{term "Trueprop"} $ p => (p, th) :: acc)
wenzelm@55846
    95
  in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
chaieb@23906
    96
haftmann@38795
    97
fun is_conj (@{term HOL.conj}$_$_) = true
chaieb@23906
    98
  | is_conj _ = false;
chaieb@23906
    99
wenzelm@55506
   100
fun prove_conj tab cjs =
wenzelm@55846
   101
  (case cjs of
wenzelm@55846
   102
    [c] =>
wenzelm@59582
   103
      if is_conj (Thm.term_of c)
wenzelm@55846
   104
      then prove_conj tab (conjuncts c)
wenzelm@55846
   105
      else tab c
wenzelm@55846
   106
  | c :: cs => conjI OF [prove_conj tab [c], prove_conj tab cs]);
chaieb@23906
   107
wenzelm@55506
   108
fun conj_aci_rule eq =
wenzelm@55846
   109
  let
wenzelm@55846
   110
    val (l, r) = Thm.dest_equals eq
wenzelm@59582
   111
    fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (Thm.term_of c))
wenzelm@59582
   112
    fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (Thm.term_of c))
wenzelm@55846
   113
    val ll = Thm.dest_arg l
wenzelm@55846
   114
    val rr = Thm.dest_arg r
wenzelm@55846
   115
    val thl  = prove_conj tabl (conjuncts rr) |> Drule.implies_intr_hyps
wenzelm@55846
   116
    val thr  = prove_conj tabr (conjuncts ll) |> Drule.implies_intr_hyps
wenzelm@60801
   117
    val eqI = Thm.instantiate' [] [SOME ll, SOME rr] @{thm iffI}
wenzelm@55846
   118
  in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
wenzelm@55506
   119
wenzelm@55846
   120
fun contains x ct =
wenzelm@59582
   121
  member (op aconv) (Misc_Legacy.term_frees (Thm.term_of ct)) (Thm.term_of x);
chaieb@23906
   122
wenzelm@55846
   123
fun is_eqx x eq =
wenzelm@59582
   124
  (case Thm.term_of eq of
wenzelm@55846
   125
    Const (@{const_name HOL.eq}, _) $ l $ r =>
wenzelm@59582
   126
      l aconv Thm.term_of x orelse r aconv Thm.term_of x
wenzelm@55846
   127
  | _ => false);
chaieb@23906
   128
wenzelm@55506
   129
local
wenzelm@55846
   130
wenzelm@55506
   131
fun proc ctxt ct =
wenzelm@59582
   132
  (case Thm.term_of ct of
wenzelm@55846
   133
    Const (@{const_name Ex}, _) $ Abs (xn, _, _) =>
wenzelm@55846
   134
      let
wenzelm@55846
   135
        val e = Thm.dest_fun ct
wenzelm@55846
   136
        val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
wenzelm@55846
   137
        val Pp = Thm.apply @{cterm Trueprop} p
wenzelm@55846
   138
        val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
wenzelm@55846
   139
      in
wenzelm@55846
   140
        (case eqs of
wenzelm@55846
   141
          [] =>
wenzelm@55846
   142
            let
wenzelm@55846
   143
              val (dx, ndx) = List.partition (contains x) neqs
wenzelm@55846
   144
            in
wenzelm@55846
   145
              case ndx of
wenzelm@55846
   146
                [] => NONE
wenzelm@55846
   147
              | _ =>
wenzelm@55846
   148
                conj_aci_rule (Thm.mk_binop @{cterm "op \<equiv> :: prop => _"} Pp
wenzelm@55846
   149
                  (Thm.apply @{cterm Trueprop} (list_conj (ndx @ dx))))
wenzelm@55846
   150
                |> Thm.abstract_rule xn x
wenzelm@55846
   151
                |> Drule.arg_cong_rule e
wenzelm@55846
   152
                |> Conv.fconv_rule
wenzelm@55846
   153
                  (Conv.arg_conv
wenzelm@55846
   154
                    (Simplifier.rewrite
wenzelm@55846
   155
                      (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
wenzelm@55846
   156
                |> SOME
wenzelm@55846
   157
            end
wenzelm@55846
   158
        | _ =>
wenzelm@55846
   159
            conj_aci_rule (Thm.mk_binop @{cterm "op \<equiv> :: prop => _"} Pp
wenzelm@55846
   160
              (Thm.apply @{cterm Trueprop} (list_conj (eqs @ neqs))))
wenzelm@55846
   161
            |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
wenzelm@55846
   162
            |> Conv.fconv_rule
wenzelm@55846
   163
                (Conv.arg_conv
wenzelm@55846
   164
                  (Simplifier.rewrite
wenzelm@55846
   165
                    (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
wenzelm@55846
   166
            |> SOME)
wenzelm@55846
   167
      end
wenzelm@55846
   168
  | _ => NONE);
wenzelm@55846
   169
wenzelm@55846
   170
in
wenzelm@55846
   171
wenzelm@55846
   172
val reduce_ex_simproc =
wenzelm@61144
   173
  Simplifier.make_simproc @{context} "reduce_ex_simproc"
wenzelm@61144
   174
    {lhss = [@{term "\<exists>x. P x"}], proc = K proc, identifier = []};
wenzelm@55846
   175
chaieb@23906
   176
end;
chaieb@23906
   177
wenzelm@55506
   178
fun raw_dlo_conv ctxt dlo_ss ({qe_bnds, qe_nolb, qe_noub, gst, gs, ...}: Langford_Data.entry) =
wenzelm@55846
   179
  let
wenzelm@55847
   180
    val ctxt' =
wenzelm@55847
   181
      Context_Position.set_visible false (put_simpset dlo_ss ctxt)
wenzelm@55847
   182
        addsimps @{thms dnf_simps} addsimprocs [reduce_ex_simproc]
wenzelm@55846
   183
    val dnfex_conv = Simplifier.rewrite ctxt'
wenzelm@55846
   184
    val pcv =
wenzelm@55846
   185
      Simplifier.rewrite
wenzelm@55846
   186
        (put_simpset dlo_ss ctxt
wenzelm@55846
   187
          addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})
wenzelm@55846
   188
  in
wenzelm@55846
   189
    fn p =>
wenzelm@61075
   190
      Qelim.gen_qelim_conv ctxt pcv pcv dnfex_conv cons
wenzelm@60818
   191
        (Drule.cterm_add_frees p []) (K Thm.reflexive) (K Thm.reflexive)
wenzelm@55846
   192
        (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
wenzelm@55846
   193
  end;
chaieb@23906
   194
chaieb@23906
   195
val grab_atom_bop =
wenzelm@55846
   196
  let
wenzelm@55846
   197
    fun h bounds tm =
wenzelm@59582
   198
      (case Thm.term_of tm of
wenzelm@55846
   199
        Const (@{const_name HOL.eq}, T) $ _ $ _ =>
wenzelm@55846
   200
          if domain_type T = HOLogic.boolT then find_args bounds tm
wenzelm@55846
   201
          else Thm.dest_fun2 tm
wenzelm@55846
   202
      | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
wenzelm@55846
   203
      | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
wenzelm@56245
   204
      | Const (@{const_name Pure.all}, _) $ _ => find_body bounds (Thm.dest_arg tm)
wenzelm@55846
   205
      | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
wenzelm@55846
   206
      | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
wenzelm@55846
   207
      | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
wenzelm@55846
   208
      | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
wenzelm@56245
   209
      | Const (@{const_name Pure.imp}, _) $ _ $ _ => find_args bounds tm
wenzelm@56245
   210
      | Const (@{const_name Pure.eq}, _) $ _ $ _ => find_args bounds tm
wenzelm@55846
   211
      | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
wenzelm@55846
   212
      | _ => Thm.dest_fun2 tm)
wenzelm@55846
   213
    and find_args bounds tm =
wenzelm@55846
   214
      (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
wenzelm@55846
   215
    and find_body bounds b =
wenzelm@55846
   216
      let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
wenzelm@55846
   217
      in h (bounds + 1) b' end;
wenzelm@55846
   218
  in h end;
chaieb@23906
   219
chaieb@23906
   220
fun dlo_instance ctxt tm =
wenzelm@55846
   221
  (fst (Langford_Data.get ctxt), Langford_Data.match ctxt (grab_atom_bop 0 tm));
chaieb@23906
   222
chaieb@23906
   223
fun dlo_conv ctxt tm =
chaieb@23906
   224
  (case dlo_instance ctxt tm of
chaieb@23906
   225
    (_, NONE) => raise CTERM ("dlo_conv (langford): no corresponding instance in context!", [tm])
wenzelm@51717
   226
  | (ss, SOME instance) => raw_dlo_conv ctxt ss instance tm);
chaieb@23906
   227
wenzelm@61075
   228
fun generalize_tac ctxt f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
wenzelm@55846
   229
  let
wenzelm@61075
   230
    fun all x t =
wenzelm@61075
   231
      Thm.apply (Thm.cterm_of ctxt (Logic.all_const (Thm.typ_of_cterm x))) (Thm.lambda x t)
wenzelm@61075
   232
    val ts = sort (fn (a, b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
wenzelm@61075
   233
    val p' = fold_rev all ts p
wenzelm@55846
   234
  in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
chaieb@24083
   235
chaieb@24083
   236
fun cfrees ats ct =
wenzelm@55846
   237
  let
wenzelm@55846
   238
    val ins = insert (op aconvc)
wenzelm@55846
   239
    fun h acc t =
wenzelm@59582
   240
      (case Thm.term_of t of
wenzelm@55846
   241
        _ $ _ $ _ =>
wenzelm@55846
   242
          if member (op aconvc) ats (Thm.dest_fun2 t)
wenzelm@55846
   243
          then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc)
wenzelm@55846
   244
          else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
wenzelm@55846
   245
      | _ $ _ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
wenzelm@55846
   246
      | Abs _ => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
wenzelm@55846
   247
      | Free _ => if member (op aconvc) ats t then acc else ins t acc
wenzelm@55846
   248
      | Var _ => if member (op aconvc) ats t then acc else ins t acc
wenzelm@55846
   249
      | _ => acc)
wenzelm@55846
   250
  in h [] ct end
chaieb@24083
   251
chaieb@23906
   252
fun dlo_tac ctxt = CSUBGOAL (fn (p, i) =>
chaieb@23906
   253
  (case dlo_instance ctxt p of
wenzelm@51717
   254
    (ss, NONE) => simp_tac (put_simpset ss ctxt) i
wenzelm@51717
   255
  | (ss, SOME instance) =>
wenzelm@54742
   256
      Object_Logic.full_atomize_tac ctxt i THEN
wenzelm@51717
   257
      simp_tac (put_simpset ss ctxt) i
chaieb@24083
   258
      THEN (CONVERSION Thm.eta_long_conversion) i
wenzelm@61075
   259
      THEN (TRY o generalize_tac ctxt (cfrees (#atoms instance))) i
wenzelm@54742
   260
      THEN Object_Logic.full_atomize_tac ctxt i
wenzelm@59970
   261
      THEN CONVERSION (Object_Logic.judgment_conv ctxt (raw_dlo_conv ctxt ss instance)) i
wenzelm@51717
   262
      THEN (simp_tac (put_simpset ss ctxt) i)));
chaieb@23906
   263
end;