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