src/HOL/Library/positivstellensatz.ML
changeset 58628 fd3c96a8ca60
parent 52049 156e12d5cb92
child 59058 a78612c67ec0
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Oct 08 09:09:12 2014 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Oct 08 10:03:46 2014 +0200
     1.3 @@ -2,8 +2,8 @@
     1.4      Author:     Amine Chaieb, University of Cambridge
     1.5  
     1.6  A generic arithmetic prover based on Positivstellensatz certificates
     1.7 ---- also implements Fourrier-Motzkin elimination as a special case
     1.8 -Fourrier-Motzkin elimination.
     1.9 +--- also implements Fourier-Motzkin elimination as a special case
    1.10 +Fourier-Motzkin elimination.
    1.11  *)
    1.12  
    1.13  (* A functor for finite mappings based on Tables *)
    1.14 @@ -360,7 +360,8 @@
    1.15         absconv1,absconv2,prover) =
    1.16    let
    1.17      val pre_ss = put_simpset HOL_basic_ss ctxt addsimps
    1.18 -      @{thms simp_thms ex_simps all_simps not_all not_ex ex_disj_distrib all_conj_distrib if_bool_eq_disj}
    1.19 +      @{thms simp_thms ex_simps all_simps not_all not_ex ex_disj_distrib
    1.20 +          all_conj_distrib if_bool_eq_disj}
    1.21      val prenex_ss = put_simpset HOL_basic_ss ctxt addsimps prenex_simps
    1.22      val skolemize_ss = put_simpset HOL_basic_ss ctxt addsimps [choice_iff]
    1.23      val presimp_conv = Simplifier.rewrite pre_ss
    1.24 @@ -439,7 +440,9 @@
    1.25        let
    1.26          val (p,q) = Thm.dest_binop (concl th)
    1.27          val c = concl th1
    1.28 -        val _ = if c aconvc (concl th2) then () else error "disj_cases : conclusions not alpha convertible"
    1.29 +        val _ =
    1.30 +          if c aconvc (concl th2) then ()
    1.31 +          else error "disj_cases : conclusions not alpha convertible"
    1.32        in Thm.implies_elim (Thm.implies_elim
    1.33            (Thm.implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
    1.34            (Thm.implies_intr (Thm.apply @{cterm Trueprop} p) th1))
    1.35 @@ -463,8 +466,12 @@
    1.36              in overall cert_choice dun (th1::th2::oths) end
    1.37            else if is_disj ct then
    1.38              let
    1.39 -              val (th1, cert1) = overall (Left::cert_choice) dun (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
    1.40 -              val (th2, cert2) = overall (Right::cert_choice) dun (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
    1.41 +              val (th1, cert1) =
    1.42 +                overall (Left::cert_choice) dun
    1.43 +                  (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
    1.44 +              val (th2, cert2) =
    1.45 +                overall (Right::cert_choice) dun
    1.46 +                  (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
    1.47              in (disj_cases th th1 th2, Branch (cert1, cert2)) end
    1.48            else overall cert_choice (th::dun) oths
    1.49          end
    1.50 @@ -495,7 +502,8 @@
    1.51        let
    1.52          fun h (acc, t) =
    1.53            case (term_of t) of
    1.54 -            Const(@{const_name Ex},_)$Abs(_,_,_) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
    1.55 +            Const(@{const_name Ex},_)$Abs(_,_,_) =>
    1.56 +              h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
    1.57            | _ => (acc,t)
    1.58        in fn t => h ([],t)
    1.59        end
    1.60 @@ -505,7 +513,10 @@
    1.61        | Var ((s,_),_) => s
    1.62        | _ => "x"
    1.63  
    1.64 -    fun mk_forall x th = Drule.arg_cong_rule (instantiate_cterm' [SOME (ctyp_of_term x)] [] @{cpat "All :: (?'a => bool) => _" }) (Thm.abstract_rule (name_of x) x th)
    1.65 +    fun mk_forall x th =
    1.66 +      Drule.arg_cong_rule
    1.67 +        (instantiate_cterm' [SOME (ctyp_of_term x)] [] @{cpat "All :: (?'a => bool) => _" })
    1.68 +        (Thm.abstract_rule (name_of x) x th)
    1.69  
    1.70      val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
    1.71  
    1.72 @@ -527,13 +538,16 @@
    1.73        | _ => raise THM ("choose",0,[th, th'])
    1.74  
    1.75      fun simple_choose v th =
    1.76 -      choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
    1.77 +      choose v
    1.78 +        (Thm.assume
    1.79 +          ((Thm.apply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
    1.80  
    1.81      val strip_forall =
    1.82        let
    1.83          fun h (acc, t) =
    1.84            case (term_of t) of
    1.85 -            Const(@{const_name All},_)$Abs(_,_,_) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
    1.86 +            Const(@{const_name All},_)$Abs(_,_,_) =>
    1.87 +              h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
    1.88            | _ => (acc,t)
    1.89        in fn t => h ([],t)
    1.90        end
    1.91 @@ -560,7 +574,9 @@
    1.92              val (avs,ibod) = strip_forall bod
    1.93              val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod))
    1.94              val (th2, certs) = overall [] [] [specl avs (Thm.assume (Thm.rhs_of th1))]
    1.95 -            val th3 = fold simple_choose evs (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply @{cterm Trueprop} bod))) th2)
    1.96 +            val th3 =
    1.97 +              fold simple_choose evs
    1.98 +                (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply @{cterm Trueprop} bod))) th2)
    1.99            in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs)
   1.100            end
   1.101        in (Thm.implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)