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