author wenzelm Wed, 08 Oct 2014 10:03:46 +0200 changeset 58628 fd3c96a8ca60 parent 58626 6c473ed0ac70 child 58629 a6a6cd499d4e
tuned spelling; tuned whitespace;
```--- a/src/HOL/Library/positivstellensatz.ML	Wed Oct 08 09:09:12 2014 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Wed Oct 08 10:03:46 2014 +0200
@@ -2,8 +2,8 @@
Author:     Amine Chaieb, University of Cambridge

A generic arithmetic prover based on Positivstellensatz certificates
---- also implements Fourrier-Motzkin elimination as a special case
-Fourrier-Motzkin elimination.
+--- also implements Fourier-Motzkin elimination as a special case
+Fourier-Motzkin elimination.
*)

(* A functor for finite mappings based on Tables *)
@@ -360,7 +360,8 @@
absconv1,absconv2,prover) =
let
val pre_ss = put_simpset HOL_basic_ss ctxt addsimps
-      @{thms simp_thms ex_simps all_simps not_all not_ex ex_disj_distrib all_conj_distrib if_bool_eq_disj}
+      @{thms simp_thms ex_simps all_simps not_all not_ex ex_disj_distrib
+          all_conj_distrib if_bool_eq_disj}
val prenex_ss = put_simpset HOL_basic_ss ctxt addsimps prenex_simps
val skolemize_ss = put_simpset HOL_basic_ss ctxt addsimps [choice_iff]
val presimp_conv = Simplifier.rewrite pre_ss
@@ -439,7 +440,9 @@
let
val (p,q) = Thm.dest_binop (concl th)
val c = concl th1
-        val _ = if c aconvc (concl th2) then () else error "disj_cases : conclusions not alpha convertible"
+        val _ =
+          if c aconvc (concl th2) then ()
+          else error "disj_cases : conclusions not alpha convertible"
in Thm.implies_elim (Thm.implies_elim
(Thm.implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
(Thm.implies_intr (Thm.apply @{cterm Trueprop} p) th1))
@@ -463,8 +466,12 @@
in overall cert_choice dun (th1::th2::oths) end
else if is_disj ct then
let
-              val (th1, cert1) = overall (Left::cert_choice) dun (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
-              val (th2, cert2) = overall (Right::cert_choice) dun (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
+              val (th1, cert1) =
+                overall (Left::cert_choice) dun
+                  (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
+              val (th2, cert2) =
+                overall (Right::cert_choice) dun
+                  (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
in (disj_cases th th1 th2, Branch (cert1, cert2)) end
else overall cert_choice (th::dun) oths
end
@@ -495,7 +502,8 @@
let
fun h (acc, t) =
case (term_of t) of
-            Const(@{const_name Ex},_)\$Abs(_,_,_) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+            Const(@{const_name Ex},_)\$Abs(_,_,_) =>
+              h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
end
@@ -505,7 +513,10 @@
| Var ((s,_),_) => s
| _ => "x"

-    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)
+    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)

val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));

@@ -527,13 +538,16 @@
| _ => raise THM ("choose",0,[th, th'])

fun simple_choose v th =
-      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
+      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

val strip_forall =
let
fun h (acc, t) =
case (term_of t) of
-            Const(@{const_name All},_)\$Abs(_,_,_) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+            Const(@{const_name All},_)\$Abs(_,_,_) =>
+              h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
end
@@ -560,7 +574,9 @@
val (avs,ibod) = strip_forall bod
val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod))
val (th2, certs) = overall [] [] [specl avs (Thm.assume (Thm.rhs_of th1))]
-            val th3 = fold simple_choose evs (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply @{cterm Trueprop} bod))) th2)
+            val th3 =
+              fold simple_choose evs
+                (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply @{cterm Trueprop} bod))) th2)
in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs)
end
in (Thm.implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)```