src/HOL/Decision_Procs/langford.ML
author wenzelm
Sun, 02 Mar 2014 22:37:55 +0100
changeset 55847 c38ad094e5bf
parent 55846 b56fda32bf24
child 55848 1bfe72d14630
permissions -rw-r--r--
silence warning due to addsimps @{thms dnf_simps}: duplicate not_not rule via simp_thms and nnf_simps;
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
55506
46f3e31c5a87 removed dead code;
wenzelm
parents: 54742
diff changeset
     5
signature LANGFORD_QE =
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
55506
46f3e31c5a87 removed dead code;
wenzelm
parents: 54742
diff changeset
    11
structure LangfordQE: LANGFORD_QE =
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 =
687240115804 tuned whitespace;
wenzelm
parents: 55506
diff changeset
    17
      (case term_of ct of
687240115804 tuned whitespace;
wenzelm
parents: 55506
diff changeset
    18
        Const (@{const_name Orderings.bot}, _) => acc
687240115804 tuned whitespace;
wenzelm
parents: 55506
diff changeset
    19
      | Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct));
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
55846
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
    24
    val [th0, th1] = map (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
687240115804 tuned whitespace;
wenzelm
parents: 55506
diff changeset
    27
        (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) (Thm.cprop_of th), SOME x] th1) th
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 =
55846
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
    36
  (case term_of ep of
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
    37
    Const (@{const_name Ex}, _) $ _ =>
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)
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
    42
            (instantiate' [] [SOME p] stupid)
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
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
    49
            val cT = ctyp_of_term a
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
    50
            val ne = instantiate' [SOME cT] [SOME a, SOME A] @{thm insert_not_empty}
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 =
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
    55
          (case (term_of L, term_of U) of
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
    56
            (Const (@{const_name Orderings.bot}, _),_) =>
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
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
    59
          | (_, Const (@{const_name Orderings.bot}, _)) =>
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 =
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
    73
      (case term_of ct of
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
    74
        @{term HOL.conj} $ _ $ _ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
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 =
55846
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
    79
  (case term_of ct of
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
    80
    @{term HOL.conj} $ _ $ _ => Thm.dest_arg1 ct :: conjuncts (Thm.dest_arg ct)
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 =
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
    86
  fold1 (fn c => fn c' => Thm.apply (Thm.apply @{cterm HOL.conj} 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 =
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
    91
      (case prop_of th of
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
    92
        @{term "Trueprop"} $ (@{term HOL.conj} $ p $ q) =>
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
    93
          h (h acc (th RS conjunct2)) (th RS conjunct1)
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
    94
      | @{term "Trueprop"} $ p => (p, th) :: acc)
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
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
    97
fun is_conj (@{term HOL.conj}$_$_) = 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] =>
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   103
      if is_conj (term_of c)
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
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   111
    fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (term_of c))
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   112
    fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (term_of c))
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
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   117
    val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
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 =
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   121
  member (op aconv) (Misc_Legacy.term_frees (term_of ct)) (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 =
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   124
  (case term_of eq of
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   125
    Const (@{const_name HOL.eq}, _) $ l $ r =>
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   126
      l aconv term_of x orelse r aconv term_of x
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 =
55846
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   132
  (case term_of ct of
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   133
    Const (@{const_name Ex}, _) $ Abs (xn, _, _) =>
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)
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   137
        val Pp = Thm.apply @{cterm Trueprop} p
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
              | _ =>
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   148
                conj_aci_rule (Thm.mk_binop @{cterm "op \<equiv> :: prop => _"} Pp
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   149
                  (Thm.apply @{cterm Trueprop} (list_conj (ndx @ dx))))
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
        | _ =>
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   159
            conj_aci_rule (Thm.mk_binop @{cterm "op \<equiv> :: prop => _"} Pp
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   160
              (Thm.apply @{cterm Trueprop} (list_conj (eqs @ neqs))))
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 =
55506
46f3e31c5a87 removed dead code;
wenzelm
parents: 54742
diff changeset
   173
  Simplifier.make_simproc
55846
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   174
    {lhss = [@{cpat "\<exists>x. ?P x"}],
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   175
     name = "reduce_ex_simproc",
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   176
     proc = K proc,
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   177
     identifier = []};
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   178
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   179
end;
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   180
55506
46f3e31c5a87 removed dead code;
wenzelm
parents: 54742
diff changeset
   181
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
   182
  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
   183
    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
   184
      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
   185
        addsimps @{thms dnf_simps} addsimprocs [reduce_ex_simproc]
55846
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   186
    val dnfex_conv = Simplifier.rewrite ctxt'
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   187
    val pcv =
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   188
      Simplifier.rewrite
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   189
        (put_simpset dlo_ss ctxt
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   190
          addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   191
  in
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   192
    fn p =>
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   193
      Qelim.gen_qelim_conv pcv pcv dnfex_conv cons
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   194
        (Thm.add_cterm_frees p []) (K Thm.reflexive) (K Thm.reflexive)
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   195
        (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   196
  end;
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   197
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   198
val grab_atom_bop =
55846
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   199
  let
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   200
    fun h bounds tm =
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   201
      (case term_of tm of
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   202
        Const (@{const_name HOL.eq}, T) $ _ $ _ =>
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   203
          if domain_type T = HOLogic.boolT then find_args bounds tm
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   204
          else Thm.dest_fun2 tm
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   205
      | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   206
      | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   207
      | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   208
      | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   209
      | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   210
      | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   211
      | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   212
      | Const ("==>", _) $ _ $ _ => find_args bounds tm
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   213
      | Const ("==", _) $ _ $ _ => find_args bounds tm
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   214
      | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   215
      | _ => Thm.dest_fun2 tm)
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   216
    and find_args bounds tm =
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   217
      (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   218
    and find_body bounds b =
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   219
      let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   220
      in h (bounds + 1) b' end;
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   221
  in h end;
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_instance ctxt tm =
55846
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   224
  (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
   225
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   226
fun dlo_conv ctxt tm =
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   227
  (case dlo_instance ctxt tm of
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   228
    (_, 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
   229
  | (ss, SOME instance) => raw_dlo_conv ctxt ss instance tm);
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   230
55506
46f3e31c5a87 removed dead code;
wenzelm
parents: 54742
diff changeset
   231
fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
55846
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   232
  let
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   233
    fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   234
    fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   235
    val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   236
    val p' = fold_rev gen ts p
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   237
  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
   238
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   239
fun cfrees ats ct =
55846
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   240
  let
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   241
    val ins = insert (op aconvc)
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   242
    fun h acc t =
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   243
      (case (term_of t) of
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   244
        _ $ _ $ _ =>
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   245
          if member (op aconvc) ats (Thm.dest_fun2 t)
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   246
          then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc)
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   247
          else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   248
      | _ $ _ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   249
      | Abs _ => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   250
      | Free _ => if member (op aconvc) ats t then acc else ins t acc
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   251
      | Var _ => if member (op aconvc) ats t then acc else ins t acc
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   252
      | _ => acc)
b56fda32bf24 tuned whitespace;
wenzelm
parents: 55792
diff changeset
   253
  in h [] ct end
24083
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   254
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   255
fun dlo_tac ctxt = CSUBGOAL (fn (p, i) =>
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   256
  (case dlo_instance ctxt p of
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46497
diff changeset
   257
    (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
   258
  | (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
   259
      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
   260
      simp_tac (put_simpset ss ctxt) i
24083
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   261
      THEN (CONVERSION Thm.eta_long_conversion) i
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   262
      THEN (TRY o generalize_tac (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
   263
      THEN Object_Logic.full_atomize_tac ctxt i
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46497
diff changeset
   264
      THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ctxt ss instance)) i
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46497
diff changeset
   265
      THEN (simp_tac (put_simpset ss ctxt) i)));
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   266
end;