gen_qelim_conv now reduces the universal quatifier to the existential one; Now also deals with Ex f for eta-contracted f;
authorchaieb
Sun Jun 17 13:39:45 2007 +0200 (2007-06-17)
changeset 23410f44d7233a54b
parent 23409 1e0b49793464
child 23411 c524900454f3
gen_qelim_conv now reduces the universal quatifier to the existential one; Now also deals with Ex f for eta-contracted f;
src/HOL/Tools/Presburger/qelim.ML
     1.1 --- a/src/HOL/Tools/Presburger/qelim.ML	Sun Jun 17 13:39:39 2007 +0200
     1.2 +++ b/src/HOL/Tools/Presburger/qelim.ML	Sun Jun 17 13:39:45 2007 +0200
     1.3 @@ -8,9 +8,9 @@
     1.4  
     1.5  signature QELIM =
     1.6   sig
     1.7 - val standard_qelim_conv: (cterm list -> cterm -> thm) ->
     1.8 + val standard_qelim_conv: Proof.context -> (cterm list -> cterm -> thm) ->
     1.9     (cterm list -> Conv.conv) -> (cterm list -> cterm -> thm) -> cterm -> thm
    1.10 - val gen_qelim_conv: Conv.conv -> Conv.conv -> Conv.conv ->
    1.11 + val gen_qelim_conv: Proof.context -> Conv.conv -> Conv.conv -> Conv.conv ->
    1.12     (cterm -> 'a -> 'a) -> 'a -> ('a -> cterm -> thm) ->
    1.13     ('a -> Conv.conv) -> ('a -> cterm -> thm) -> Conv.conv
    1.14  
    1.15 @@ -20,29 +20,40 @@
    1.16  struct
    1.17  open Conv;
    1.18  
    1.19 -val is_refl = op aconv o Logic.dest_equals o Thm.prop_of;
    1.20 -
    1.21 -fun gen_qelim_conv precv postcv simpex_conv ins env atcv ncv qcv  = 
    1.22 - let fun conv p =
    1.23 -  case (term_of p) of 
    1.24 -   Const(s,T)$_$_ => if domain_type T = HOLogic.boolT 
    1.25 -                        andalso s mem ["op &","op |","op -->","op ="]
    1.26 -                    then binop_conv conv p else atcv env p
    1.27 - | Const("Not",_)$_ => arg_conv conv p
    1.28 - | Const("Ex",_)$Abs(s,_,_) => 
    1.29 -   let 
    1.30 -    val (e,p0) = Thm.dest_comb p
    1.31 -    val (x,p') = Thm.dest_abs (SOME s) p0
    1.32 -    val th = Thm.abstract_rule s x 
    1.33 -                  (((gen_qelim_conv precv postcv simpex_conv ins (ins x env) atcv ncv qcv) 
    1.34 -                      then_conv (ncv (ins x env))) p')
    1.35 -                  |> Drule.arg_cong_rule e
    1.36 -    val th' = simpex_conv (Thm.rhs_of th)
    1.37 -    val (l,r) = Thm.dest_equals (cprop_of th')
    1.38 -   in if is_refl th' then Thm.transitive th (qcv env (Thm.rhs_of th))
    1.39 -      else Thm.transitive (Thm.transitive th th') (conv r) end
    1.40 - | _ => atcv env p
    1.41 - in precv then_conv conv then_conv postcv end;
    1.42 +local
    1.43 + val all_not_ex = mk_meta_eq @{thm "all_not_ex"}
    1.44 +in
    1.45 +fun gen_qelim_conv ctxt precv postcv simpex_conv ins env atcv ncv qcv  = 
    1.46 + let 
    1.47 +  val thy = ProofContext.theory_of ctxt
    1.48 +  fun conv env p =
    1.49 +   case (term_of p) of 
    1.50 +    Const(s,T)$_$_ => if domain_type T = HOLogic.boolT 
    1.51 +                         andalso s mem ["op &","op |","op -->","op ="]
    1.52 +                     then binop_conv (conv env) p else atcv env p
    1.53 +  | Const("Not",_)$_ => arg_conv (conv env) p
    1.54 +  | Const("Ex",_)$Abs(s,_,_) => 
    1.55 +    let 
    1.56 +     val (e,p0) = Thm.dest_comb p
    1.57 +     val (x,p') = Thm.dest_abs (SOME s) p0
    1.58 +     val env' = ins x env
    1.59 +     val th = Thm.abstract_rule s x ((conv env' then_conv ncv env') p')
    1.60 +                   |> Drule.arg_cong_rule e
    1.61 +     val th' = simpex_conv (Thm.rhs_of th)
    1.62 +     val (l,r) = Thm.dest_equals (cprop_of th')
    1.63 +    in if is_refl th' then Thm.transitive th (qcv env (Thm.rhs_of th))
    1.64 +       else Thm.transitive (Thm.transitive th th') (conv env r) end
    1.65 +  | Const("Ex",_)$ _ => (eta_conv thy then_conv conv env) p 
    1.66 +  | Const("All",_)$_ => 
    1.67 +    let 
    1.68 +     val p = Thm.dest_arg p
    1.69 +     val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
    1.70 +     val th = instantiate' [SOME T] [SOME p] all_not_ex 
    1.71 +    in transitive th (conv env (Thm.rhs_of th)) 
    1.72 +    end
    1.73 +  | _ => atcv env p
    1.74 + in precv then_conv (conv env) then_conv postcv end
    1.75 +end;
    1.76  
    1.77  fun cterm_frees ct = 
    1.78   let fun h acc t = 
    1.79 @@ -53,12 +64,13 @@
    1.80    | _ => acc
    1.81   in h [] ct end;
    1.82  
    1.83 -val standard_qelim_conv = 
    1.84 - let val pcv = Simplifier.rewrite 
    1.85 -                 (HOL_basic_ss addsimps (simp_thms @ (List.take(ex_simps,4)) 
    1.86 -                     @ [not_all,ex_disj_distrib]))
    1.87 - in fn atcv => fn ncv => fn qcv => fn p => 
    1.88 -       gen_qelim_conv pcv pcv pcv (curry (op ::)) (cterm_frees p) atcv ncv qcv p 
    1.89 - end;
    1.90 +local
    1.91 +val pcv = Simplifier.rewrite 
    1.92 +                 (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps) 
    1.93 +                     @ [@{thm "all_not_ex"}, not_all,ex_disj_distrib])
    1.94 +in 
    1.95 +fun standard_qelim_conv ctxt atcv ncv qcv p = 
    1.96 +    gen_qelim_conv ctxt pcv pcv pcv cons (cterm_frees p) atcv ncv qcv p 
    1.97 +end;
    1.98  
    1.99  end;