src/HOL/Decision_Procs/ferrante_rackoff.ML
author wenzelm
Sat, 10 Jun 2017 21:48:02 +0200
changeset 66061 880db47fed30
parent 61075 f6b0d827240e
child 69597 ff784d5a5bfb
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37744
3daaf23b9ab4 tuned titles
haftmann
parents: 37120
diff changeset
     1
(* Title:      HOL/Decision_Procs/ferrante_rackoff.ML
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     2
   Author:     Amine Chaieb, TU Muenchen
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     3
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     4
Ferrante and Rackoff's algorithm for quantifier elimination in dense
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     5
linear orders.  Proof-synthesis and tactic.
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     6
*)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     7
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
     8
signature FERRANTE_RACKOFF =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
     9
sig
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    10
  val dlo_conv: Proof.context -> conv
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    11
  val dlo_tac: Proof.context -> int -> tactic
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    12
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    13
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    14
structure FerranteRackoff: FERRANTE_RACKOFF =
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    15
struct
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    16
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    17
open Ferrante_Rackoff_Data;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    18
open Conv;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    19
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    20
type entry = {minf: thm list, pinf: thm list, nmi: thm list, npi: thm list,
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    21
   ld: thm list, qe: thm, atoms : cterm list} *
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    22
  {isolate_conv: cterm list -> cterm -> thm,
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    23
                 whatis : cterm -> cterm -> ord,
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    24
                 simpset : simpset};
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    25
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    26
fun get_p1 th =
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    27
  funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59058
diff changeset
    28
    (funpow 2 Thm.dest_arg (Thm.cprop_of th)) |> Thm.dest_arg
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    29
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46497
diff changeset
    30
fun ferrack_conv ctxt
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    31
   (entr as ({minf = minf, pinf = pinf, nmi = nmi, npi = npi,
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    32
              ld = ld, qe = qe, atoms = atoms},
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    33
             {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    34
let
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59058
diff changeset
    35
 fun uset (vars as (x::vs)) p = case Thm.term_of p of
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
    36
   Const(@{const_name HOL.conj}, _)$ _ $ _ =>
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    37
     let
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    38
       val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    39
       val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    40
     in (lS@rS, Drule.binop_cong_rule b lth rth) end
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
    41
 |  Const(@{const_name HOL.disj}, _)$ _ $ _ =>
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    42
     let
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    43
       val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    44
       val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    45
     in (lS@rS, Drule.binop_cong_rule b lth rth) end
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    46
 | _ =>
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    47
    let
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    48
      val th = icv vars p
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    49
      val p' = Thm.rhs_of th
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    50
      val c = wi x p'
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    51
      val S = (if member (op =) [Lt, Le, Eq] c then single o Thm.dest_arg
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    52
               else if member (op =) [Gt, Ge] c then single o Thm.dest_arg1
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    53
               else if c = NEq then single o Thm.dest_arg o Thm.dest_arg
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    54
               else K []) p'
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    55
    in (S,th) end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    56
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    57
 val ((p1_v,p2_v),(mp1_v,mp2_v)) =
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    58
   funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59058
diff changeset
    59
     (funpow 4 Thm.dest_arg (Thm.cprop_of (hd minf)))
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 56245
diff changeset
    60
   |> Thm.dest_binop |> apply2 Thm.dest_binop |> apfst (apply2 Thm.dest_fun)
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59970
diff changeset
    61
   |> apply2 (apply2 (dest_Var o Thm.term_of))
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    62
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    63
 fun myfwd (th1, th2, th3, th4, th5) p1 p2
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    64
      [(th_1,th_2,th_3,th_4,th_5), (th_1',th_2',th_3',th_4',th_5')] =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    65
  let
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    66
   val (mp1, mp2) = (get_p1 th_1, get_p1 th_1')
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    67
   val (pp1, pp2) = (get_p1 th_2, get_p1 th_2')
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    68
   fun fw mi th th' th'' =
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    69
     let
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    70
      val th0 = if mi then
43333
2bdec7f430d3 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents: 40314
diff changeset
    71
           Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
2bdec7f430d3 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents: 40314
diff changeset
    72
        else Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36862
diff changeset
    73
     in Thm.implies_elim (Thm.implies_elim th0 th') th'' end
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    74
  in (fw true th1 th_1 th_1', fw false th2 th_2 th_2',
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    75
      fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5')
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    76
  end
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59970
diff changeset
    77
 val U_v = dest_Var (Thm.term_of (Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 (Thm.cprop_of qe)))))
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    78
 fun main vs p =
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    79
  let
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59058
diff changeset
    80
   val ((xn,ce),(x,fm)) = (case Thm.term_of p of
38558
32ad17fe2b9c tuned quotes
haftmann
parents: 38549
diff changeset
    81
                   Const(@{const_name Ex},_)$Abs(xn,xT,_) =>
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    82
                        Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    83
                 | _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
59586
ddf6deaadfe8 clarified signature;
wenzelm
parents: 59582
diff changeset
    84
   val cT = Thm.ctyp_of_cterm x
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    85
   val (u,nth) = uset (x::vs) fm |>> distinct (op aconvc)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    86
   val nthx = Thm.abstract_rule xn x nth
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    87
   val q = Thm.rhs_of nth
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    88
   val qx = Thm.rhs_of nthx
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    89
   val enth = Drule.arg_cong_rule ce nthx
60801
7664e0916eec tuned signature;
wenzelm
parents: 60642
diff changeset
    90
   val [th0,th1] = map (Thm.instantiate' [SOME cT] []) @{thms "finite.intros"}
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    91
   fun ins x th =
60801
7664e0916eec tuned signature;
wenzelm
parents: 60642
diff changeset
    92
      Thm.implies_elim (Thm.instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    93
                                       (Thm.cprop_of th), SOME x] th1) th
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    94
   val fU = fold ins u th0
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    95
   val cU = funpow 2 Thm.dest_arg (Thm.cprop_of fU)
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
    96
   local
60801
7664e0916eec tuned signature;
wenzelm
parents: 60642
diff changeset
    97
     val insI1 = Thm.instantiate' [SOME cT] [] @{thm "insertI1"}
7664e0916eec tuned signature;
wenzelm
parents: 60642
diff changeset
    98
     val insI2 = Thm.instantiate' [SOME cT] [] @{thm "insertI2"}
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
    99
   in
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   100
    fun provein x S =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59058
diff changeset
   101
     case Thm.term_of S of
32264
0be31453f698 Set.UNIV and Set.empty are mere abbreviations for top and bot
haftmann
parents: 32149
diff changeset
   102
        Const(@{const_name Orderings.bot}, _) => raise CTERM ("provein : not a member!", [S])
30304
d8e4cd2ac2a1 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents: 24584
diff changeset
   103
      | Const(@{const_name insert}, _) $ y $_ =>
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   104
         let val (cy,S') = Thm.dest_binop S
60801
7664e0916eec tuned signature;
wenzelm
parents: 60642
diff changeset
   105
         in if Thm.term_of x aconv y then Thm.instantiate' [] [SOME x, SOME S'] insI1
7664e0916eec tuned signature;
wenzelm
parents: 60642
diff changeset
   106
         else Thm.implies_elim (Thm.instantiate' [] [SOME x, SOME S', SOME cy] insI2)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   107
                           (provein x S')
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   108
         end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   109
   end
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59058
diff changeset
   110
   val tabU = fold (fn t => fn tab => Termtab.update (Thm.term_of t, provein t cU) tab)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   111
                   u Termtab.empty
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59058
diff changeset
   112
   val U = the o Termtab.lookup tabU o Thm.term_of
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   113
   val [minf_conj, minf_disj, minf_eq, minf_neq, minf_lt,
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   114
        minf_le, minf_gt, minf_ge, minf_P] = minf
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   115
   val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt,
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   116
        pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   117
   val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt,
43333
2bdec7f430d3 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents: 40314
diff changeset
   118
        nmi_le, nmi_gt, nmi_ge, nmi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) nmi
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   119
   val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt,
43333
2bdec7f430d3 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents: 40314
diff changeset
   120
        npi_le, npi_gt, npi_ge, npi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) npi
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   121
   val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt,
43333
2bdec7f430d3 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents: 40314
diff changeset
   122
        ld_le, ld_gt, ld_ge, ld_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) ld
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   123
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   124
   fun decomp_mpinf fm =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59058
diff changeset
   125
     case Thm.term_of fm of
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   126
       Const(@{const_name HOL.conj},_)$_$_ =>
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   127
        let val (p,q) = Thm.dest_binop fm
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   128
        in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
46497
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45654
diff changeset
   129
                         (Thm.lambda x p) (Thm.lambda x q))
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   130
        end
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   131
     | Const(@{const_name HOL.disj},_)$_$_ =>
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   132
        let val (p,q) = Thm.dest_binop fm
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   133
        in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
46497
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45654
diff changeset
   134
                         (Thm.lambda x p) (Thm.lambda x q))
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   135
        end
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   136
     | _ =>
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   137
        (let val c = wi x fm
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   138
             val t = (if c=Nox then I
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   139
                      else if member (op =) [Lt, Le, Eq] c then Thm.dest_arg
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   140
                      else if member (op =) [Gt, Ge] c then Thm.dest_arg1
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   141
                      else if c = NEq then (Thm.dest_arg o Thm.dest_arg)
40314
b5ec88d9ac03 replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents: 38864
diff changeset
   142
                      else raise Fail "decomp_mpinf: Impossible case!!") fm
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   143
             val [mi_th, pi_th, nmi_th, npi_th, ld_th] =
60801
7664e0916eec tuned signature;
wenzelm
parents: 60642
diff changeset
   144
               if c = Nox then map (Thm.instantiate' [] [SOME fm])
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   145
                                    [minf_P, pinf_P, nmi_P, npi_P, ld_P]
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   146
               else
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   147
                let val [mi_th,pi_th,nmi_th,npi_th,ld_th] =
60801
7664e0916eec tuned signature;
wenzelm
parents: 60642
diff changeset
   148
                 map (Thm.instantiate' [] [SOME t])
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   149
                 (case c of Lt => [minf_lt, pinf_lt, nmi_lt, npi_lt, ld_lt]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   150
                          | Le => [minf_le, pinf_le, nmi_le, npi_le, ld_le]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   151
                          | Gt => [minf_gt, pinf_gt, nmi_gt, npi_gt, ld_gt]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   152
                          | Ge => [minf_ge, pinf_ge, nmi_ge, npi_ge, ld_ge]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   153
                          | Eq => [minf_eq, pinf_eq, nmi_eq, npi_eq, ld_eq]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   154
                          | NEq => [minf_neq, pinf_neq, nmi_neq, npi_neq, ld_neq])
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   155
                    val tU = U t
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36862
diff changeset
   156
                    fun Ufw th = Thm.implies_elim th tU
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   157
                 in [mi_th, pi_th, Ufw nmi_th, Ufw npi_th, Ufw ld_th]
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   158
                 end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   159
         in ([], K (mi_th, pi_th, nmi_th, npi_th, ld_th)) end)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   160
   val (minf_th, pinf_th, nmi_th, npi_th, ld_th) = divide_and_conquer decomp_mpinf q
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   161
   val qe_th = Drule.implies_elim_list
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   162
                  ((fconv_rule (Thm.beta_conversion true))
60801
7664e0916eec tuned signature;
wenzelm
parents: 60642
diff changeset
   163
                   (Thm.instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th])
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   164
                        qe))
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   165
                  [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   166
    val bex_conv =
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46497
diff changeset
   167
      Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms bex_simps(1-5)})
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36862
diff changeset
   168
    val result_th = fconv_rule (arg_conv bex_conv) (Thm.transitive enth qe_th)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   169
   in result_th
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   170
   end
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   171
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   172
in main
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   173
end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   174
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   175
val grab_atom_bop =
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   176
 let
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   177
  fun h bounds tm =
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59058
diff changeset
   178
   (case Thm.term_of tm of
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38795
diff changeset
   179
     Const (@{const_name HOL.eq}, T) $ _ $ _ =>
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   180
       if domain_type T = HOLogic.boolT then find_args bounds tm
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   181
       else Thm.dest_fun2 tm
38558
32ad17fe2b9c tuned quotes
haftmann
parents: 38549
diff changeset
   182
   | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
32ad17fe2b9c tuned quotes
haftmann
parents: 38549
diff changeset
   183
   | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
32ad17fe2b9c tuned quotes
haftmann
parents: 38549
diff changeset
   184
   | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   185
   | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   186
   | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
38786
e46e7a9cb622 formerly unnamed infix impliciation now named HOL.implies
haftmann
parents: 38558
diff changeset
   187
   | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 54742
diff changeset
   188
   | Const (@{const_name Pure.imp}, _) $ _ $ _ => find_args bounds tm
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 54742
diff changeset
   189
   | Const (@{const_name Pure.eq}, _) $ _ $ _ => find_args bounds tm
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 54742
diff changeset
   190
   | Const (@{const_name Pure.all}, _) $ _ => find_body bounds (Thm.dest_arg tm)
38558
32ad17fe2b9c tuned quotes
haftmann
parents: 38549
diff changeset
   191
   | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   192
   | _ => Thm.dest_fun2 tm)
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   193
  and find_args bounds tm =
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   194
           (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   195
 and find_body bounds b =
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   196
   let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   197
   in h (bounds + 1) b' end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   198
in h end;
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   199
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46497
diff changeset
   200
fun raw_ferrack_qe_conv ctxt (thy, {isolate_conv, whatis, simpset = ss}) tm =
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   201
 let
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   202
   val ss' =
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46497
diff changeset
   203
     merge_ss (simpset_of
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46497
diff changeset
   204
      (put_simpset HOL_basic_ss ctxt addsimps
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46497
diff changeset
   205
        @{thms simp_thms ex_simps all_simps not_all all_not_ex ex_disj_distrib}), ss);
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46497
diff changeset
   206
   val pcv = Simplifier.rewrite (put_simpset ss' ctxt);
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46497
diff changeset
   207
   val postcv = Simplifier.rewrite (put_simpset ss ctxt);
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46497
diff changeset
   208
   val nnf = K (nnf_conv ctxt then_conv postcv)
61075
f6b0d827240e tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60818
diff changeset
   209
   val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (Drule.cterm_add_frees tm [])
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   210
                  (isolate_conv ctxt) nnf
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46497
diff changeset
   211
                  (fn vs => ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt,
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46497
diff changeset
   212
                                               whatis = whatis, simpset = ss}) vs
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   213
                   then_conv postcv)
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46497
diff changeset
   214
 in (Simplifier.rewrite (put_simpset ss ctxt) then_conv qe_conv) tm end;
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   215
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   216
fun dlo_instance ctxt tm =
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   217
  Ferrante_Rackoff_Data.match ctxt (grab_atom_bop 0 tm);
23486
4a6506fade73 Thm.add_cterm_frees;
wenzelm
parents: 23466
diff changeset
   218
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   219
fun dlo_conv ctxt tm =
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   220
  (case dlo_instance ctxt tm of
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   221
    NONE => raise CTERM ("ferrackqe_conv: no corresponding instance in context!", [tm])
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   222
  | SOME instance => raw_ferrack_qe_conv ctxt instance tm);
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   223
23567
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   224
fun dlo_tac ctxt = CSUBGOAL (fn (p, i) =>
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   225
  (case dlo_instance ctxt p of
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   226
    NONE => no_tac
28c6a0118818 export dlo_conv;
wenzelm
parents: 23524
diff changeset
   227
  | SOME instance =>
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 51717
diff changeset
   228
      Object_Logic.full_atomize_tac ctxt i THEN
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46497
diff changeset
   229
      simp_tac (put_simpset (#simpset (snd instance)) ctxt) i THEN  (* FIXME already part of raw_ferrack_qe_conv? *)
59970
e9f73d87d904 proper context for Object_Logic operations;
wenzelm
parents: 59586
diff changeset
   230
      CONVERSION (Object_Logic.judgment_conv ctxt (raw_ferrack_qe_conv ctxt instance)) i THEN
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46497
diff changeset
   231
      simp_tac ctxt i));  (* FIXME really? *)
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   232
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
diff changeset
   233
end;