src/HOL/Decision_Procs/langford.ML
author wenzelm
Tue, 25 May 2010 22:21:31 +0200
changeset 37120 5df087c6ce94
parent 36945 src/HOL/Tools/Qelim/langford.ML@9bec62c10714
child 37744 3daaf23b9ab4
permissions -rw-r--r--
moved ML files where they are actually used; more precise dependencies;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29269
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents: 29265
diff changeset
     1
(*  Title:      HOL/Tools/Qelim/langford.ML
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
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
     5
signature LANGFORD_QE = 
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
24083
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
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 =
f00b993bda0d (restored previous version)
haftmann
parents: 30450
diff changeset
    15
 let 
f00b993bda0d (restored previous version)
haftmann
parents: 30450
diff changeset
    16
  fun h acc ct = 
f00b993bda0d (restored previous version)
haftmann
parents: 30450
diff changeset
    17
   case term_of ct of
32264
0be31453f698 Set.UNIV and Set.empty are mere abbreviations for top and bot
haftmann
parents: 30452
diff changeset
    18
     Const (@{const_name Orderings.bot}, _) => acc
30452
f00b993bda0d (restored previous version)
haftmann
parents: 30450
diff changeset
    19
   | Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct)
f00b993bda0d (restored previous version)
haftmann
parents: 30450
diff changeset
    20
in h [] end;
f00b993bda0d (restored previous version)
haftmann
parents: 30450
diff changeset
    21
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    22
fun prove_finite cT u = 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    23
let val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    24
    fun ins x th =
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 35625
diff changeset
    25
     Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    26
                                     (Thm.cprop_of th), SOME x] th1) th
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    27
in fold ins u th0 end;
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    28
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    29
val simp_rule = Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (HOL_basic_ss addsimps (@{thms "ball_simps"} @ simp_thms))));
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    30
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    31
fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep = 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    32
 case term_of ep of 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    33
  Const("Ex",_)$_ => 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    34
   let 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    35
     val p = Thm.dest_arg ep
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    36
     val ths = simplify (HOL_basic_ss addsimps gather) (instantiate' [] [SOME p] stupid)
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    37
     val (L,U) = 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    38
       let 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    39
         val (x,q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths))
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    40
       in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1)
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    41
       end
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    42
     fun proveneF S =         
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    43
       let val (a,A) = Thm.dest_comb S |>> Thm.dest_arg
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    44
           val cT = ctyp_of_term a
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    45
           val ne = instantiate' [SOME cT] [SOME a, SOME A] 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    46
                    @{thm insert_not_empty}
30452
f00b993bda0d (restored previous version)
haftmann
parents: 30450
diff changeset
    47
           val f = prove_finite cT (dest_set S)
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    48
       in (ne, f) end
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    49
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    50
     val qe = case (term_of L, term_of U) of 
32264
0be31453f698 Set.UNIV and Set.empty are mere abbreviations for top and bot
haftmann
parents: 30452
diff changeset
    51
      (Const (@{const_name Orderings.bot}, _),_) =>  
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    52
        let
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    53
          val (neU,fU) = proveneF U 
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 35625
diff changeset
    54
        in simp_rule (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end
32264
0be31453f698 Set.UNIV and Set.empty are mere abbreviations for top and bot
haftmann
parents: 30452
diff changeset
    55
    | (_,Const (@{const_name Orderings.bot}, _)) =>  
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    56
        let
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    57
          val (neL,fL) = proveneF L
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 35625
diff changeset
    58
        in simp_rule (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    59
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    60
    | (_,_) =>  
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    61
      let 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    62
       val (neL,fL) = proveneF L
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    63
       val (neU,fU) = proveneF U
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 35625
diff changeset
    64
      in simp_rule (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU])) 
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    65
      end
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    66
   in qe end 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    67
 | _ => error "dlo_qe : Not an existential formula";
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    68
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    69
val all_conjuncts = 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    70
 let fun h acc ct = 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    71
  case term_of ct of
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    72
   @{term "op &"}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    73
  | _ => ct::acc
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    74
in h [] end;
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    75
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    76
fun conjuncts ct =
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    77
 case term_of ct of
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    78
  @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    79
| _ => [ct];
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    80
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    81
fun fold1 f = foldr1 (uncurry f);
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    82
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    83
val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ;
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    84
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    85
fun mk_conj_tab th = 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    86
 let fun h acc th = 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    87
   case prop_of th of
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    88
   @{term "Trueprop"}$(@{term "op &"}$p$q) => 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    89
     h (h acc (th RS conjunct2)) (th RS conjunct1)
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    90
  | @{term "Trueprop"}$p => (p,th)::acc
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    91
in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    92
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    93
fun is_conj (@{term "op &"}$_$_) = true
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    94
  | is_conj _ = false;
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    95
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    96
fun prove_conj tab cjs = 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    97
 case cjs of 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    98
   [c] => if is_conj (term_of c) then prove_conj tab (conjuncts c) else tab c
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
    99
 | c::cs => conjI OF [prove_conj tab [c], prove_conj tab cs];
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   100
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   101
fun conj_aci_rule eq = 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   102
 let 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   103
  val (l,r) = Thm.dest_equals eq
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 35625
diff changeset
   104
  fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (term_of c))
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 35625
diff changeset
   105
  fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (term_of c))
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   106
  val ll = Thm.dest_arg l
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   107
  val rr = Thm.dest_arg r
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   108
  
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   109
  val thl  = prove_conj tabl (conjuncts rr) 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   110
                |> Drule.implies_intr_hyps
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   111
  val thr  = prove_conj tabr (conjuncts ll) 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   112
                |> Drule.implies_intr_hyps
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   113
  val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 35625
diff changeset
   114
 in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   115
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 24083
diff changeset
   116
fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   117
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   118
fun is_eqx x eq = case term_of eq of
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   119
   Const("op =",_)$l$r => l aconv term_of x orelse r aconv term_of x
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   120
 | _ => false ;
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   121
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   122
local 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   123
fun proc ct = 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   124
 case term_of ct of
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   125
  Const("Ex",_)$Abs (xn,_,_) => 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   126
   let 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   127
    val e = Thm.dest_fun ct
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   128
    val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   129
    val Pp = Thm.capply @{cterm "Trueprop"} p 
30148
5d04b67a866e eliminated private clones of List.partition;
wenzelm
parents: 29269
diff changeset
   130
    val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   131
   in case eqs of
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   132
      [] => 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   133
        let 
30148
5d04b67a866e eliminated private clones of List.partition;
wenzelm
parents: 29269
diff changeset
   134
         val (dx,ndx) = List.partition (contains x) neqs
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   135
         in case ndx of [] => NONE
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   136
                      | _ =>
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   137
            conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   138
                 (Thm.capply @{cterm Trueprop} (list_conj (ndx @dx))))
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 35625
diff changeset
   139
           |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e 
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   140
           |> Conv.fconv_rule (Conv.arg_conv 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   141
                   (Simplifier.rewrite 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   142
                      (HOL_basic_ss addsimps (simp_thms @ ex_simps))))
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   143
           |> SOME
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   144
          end
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   145
    | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   146
                 (Thm.capply @{cterm Trueprop} (list_conj (eqs@neqs))))
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 35625
diff changeset
   147
           |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e 
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   148
           |> Conv.fconv_rule (Conv.arg_conv 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   149
                   (Simplifier.rewrite 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   150
                (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   151
           |> SOME
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   152
   end
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   153
 | _ => NONE;
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   154
in val reduce_ex_simproc = 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   155
  Simplifier.make_simproc 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   156
  {lhss = [@{cpat "EX x. ?P x"}] , name = "reduce_ex_simproc",
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   157
   proc = K (K proc) , identifier = []}
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   158
end;
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   159
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   160
fun raw_dlo_conv dlo_ss 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   161
          ({qe_bnds, qe_nolb, qe_noub, gst, gs, atoms}:Langford_Data.entry) = 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   162
 let 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   163
  val ss = dlo_ss addsimps @{thms "dnf_simps"} addsimprocs [reduce_ex_simproc]
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   164
  val dnfex_conv = Simplifier.rewrite ss
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   165
   val pcv = Simplifier.rewrite
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   166
               (dlo_ss addsimps (simp_thms @ ex_simps @ all_simps)
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   167
                @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib])
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   168
 in fn p => 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   169
   Qelim.gen_qelim_conv pcv pcv dnfex_conv cons 
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 35625
diff changeset
   170
                  (Thm.add_cterm_frees p [])  (K Thm.reflexive) (K Thm.reflexive)
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   171
                  (K (basic_dloqe () gst qe_bnds qe_nolb qe_noub gs)) p
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   172
 end;
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   173
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   174
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   175
val grab_atom_bop =
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   176
 let
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   177
  fun h bounds tm =
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   178
   (case term_of tm of
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   179
     Const ("op =", T) $ _ $ _ =>
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   180
       if domain_type T = HOLogic.boolT then find_args bounds tm
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   181
       else Thm.dest_fun2 tm
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   182
   | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm)
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   183
   | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm)
24083
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   184
   | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   185
   | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm)
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   186
   | Const ("op &", _) $ _ $ _ => find_args bounds tm
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   187
   | Const ("op |", _) $ _ $ _ => find_args bounds tm
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   188
   | Const ("op -->", _) $ _ $ _ => find_args bounds tm
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   189
   | Const ("==>", _) $ _ $ _ => find_args bounds tm
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   190
   | Const ("==", _) $ _ $ _ => find_args bounds tm
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   191
   | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm)
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   192
   | _ => Thm.dest_fun2 tm)
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   193
  and find_args bounds tm =
24083
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   194
    (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   195
 and find_body bounds b =
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   196
   let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   197
   in h (bounds + 1) b' end;
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   198
in h end;
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   199
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   200
fun dlo_instance ctxt tm =
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   201
  (fst (Langford_Data.get ctxt), 
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   202
   Langford_Data.match ctxt (grab_atom_bop 0 tm));
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   203
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   204
fun dlo_conv ctxt tm =
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   205
  (case dlo_instance ctxt tm of
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   206
    (_, NONE) => raise CTERM ("dlo_conv (langford): no corresponding instance in context!", [tm])
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   207
  | (ss, SOME instance) => raw_dlo_conv ss instance tm);
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   208
24083
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   209
fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   210
 let 
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   211
   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   212
   fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 33035
diff changeset
   213
   val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
24083
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   214
   val p' = fold_rev gen ts p
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 35625
diff changeset
   215
 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
   216
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   217
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   218
fun cfrees ats ct =
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   219
 let 
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   220
  val ins = insert (op aconvc)
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   221
  fun h acc t = 
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   222
   case (term_of t) of
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   223
    b$_$_ => if member (op aconvc) ats (Thm.dest_fun2 t) 
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   224
                then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc) 
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   225
                else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   226
  | _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   227
  | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   228
  | Free _ => if member (op aconvc) ats t then acc else ins t acc
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   229
  | Var _ => if member (op aconvc) ats t then acc else ins t acc
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   230
  | _ => acc
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   231
 in h [] ct end
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   232
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   233
fun dlo_tac ctxt = CSUBGOAL (fn (p, i) =>
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   234
  (case dlo_instance ctxt p of
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   235
    (ss, NONE) => simp_tac ss i
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   236
  | (ss,  SOME instance) =>
35625
9c818cab0dd0 modernized structure Object_Logic;
wenzelm
parents: 35408
diff changeset
   237
      Object_Logic.full_atomize_tac i THEN
24083
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   238
      simp_tac ss i
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   239
      THEN (CONVERSION Thm.eta_long_conversion) i
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   240
      THEN (TRY o generalize_tac (cfrees (#atoms instance))) i
35625
9c818cab0dd0 modernized structure Object_Logic;
wenzelm
parents: 35408
diff changeset
   241
      THEN Object_Logic.full_atomize_tac i
9c818cab0dd0 modernized structure Object_Logic;
wenzelm
parents: 35408
diff changeset
   242
      THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ss instance)) i
24083
4ea3656380b1 find_body goes under meta-quantifier ; tactic generalizes free variables;
chaieb
parents: 23906
diff changeset
   243
      THEN (simp_tac ss i)));  
23906
e61361aa23b2 Quantifier elimination for Dense linear orders after Langford
chaieb
parents:
diff changeset
   244
end;