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