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