src/HOL/Library/positivstellensatz.ML
 changeset 44454 6f28f96a09bf parent 44058 ae85c5d64913 child 45654 cf10bde35973
```     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Mon Aug 22 16:49:45 2011 -0700
1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Mon Aug 22 17:22:49 2011 -0700
1.3 @@ -204,10 +204,12 @@
1.4      @{lemma "((P & (Q | R)) = ((P&Q) | (P&R)))" and "((Q | R) & P) = ((Q&P) | (R&P))" and
1.5        "(P & Q) = (Q & P)" and "((P | Q) = (Q | P))" by blast+};
1.6
1.7 +(*
1.8  val nnfD_simps =
1.9    @{lemma "((~(P & Q)) = (~P | ~Q))" and "((~(P | Q)) = (~P & ~Q) )" and
1.10      "((P --> Q) = (~P | Q) )" and "((P = Q) = ((P & Q) | (~P & ~ Q)))" and
1.11      "((~(P = Q)) = ((P & ~ Q) | (~P & Q)) )" and "((~ ~(P)) = P)" by blast+};
1.12 +*)
1.13
1.14  val choice_iff = @{lemma "(ALL x. EX y. P x y) = (EX f. ALL x. P x (f x))" by metis};
1.15  val prenex_simps =
1.16 @@ -293,16 +295,18 @@
1.17   | _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd)
1.18   fun is_ratconst t = can dest_ratconst t
1.19
1.20 +(*
1.21  fun find_term p t = if p t then t else
1.22   case t of
1.23    a\$b => (find_term p a handle TERM _ => find_term p b)
1.24   | Abs (_,_,t') => find_term p t'
1.25   | _ => raise TERM ("find_term",[t]);
1.26 +*)
1.27
1.28  fun find_cterm p t = if p t then t else
1.29   case term_of t of
1.30 -  a\$b => (find_cterm p (Thm.dest_fun t) handle CTERM _ => find_cterm p (Thm.dest_arg t))
1.31 - | Abs (_,_,t') => find_cterm p (Thm.dest_abs NONE t |> snd)
1.32 +  _\$_ => (find_cterm p (Thm.dest_fun t) handle CTERM _ => find_cterm p (Thm.dest_arg t))
1.33 + | Abs (_,_,_) => find_cterm p (Thm.dest_abs NONE t |> snd)
1.34   | _ => raise CTERM ("find_cterm",[t]);
1.35
1.36      (* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*)
1.37 @@ -477,7 +481,7 @@
1.38   val strip_exists =
1.39    let fun h (acc, t) =
1.40     case (term_of t) of
1.41 -    Const(@{const_name Ex},_)\$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
1.42 +    Const(@{const_name Ex},_)\$Abs(_,_,_) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
1.43    | _ => (acc,t)
1.44    in fn t => h ([],t)
1.45    end
1.46 @@ -512,7 +516,7 @@
1.47   val strip_forall =
1.48    let fun h (acc, t) =
1.49     case (term_of t) of
1.50 -    Const(@{const_name All},_)\$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
1.51 +    Const(@{const_name All},_)\$Abs(_,_,_) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
1.52    | _ => (acc,t)
1.53    in fn t => h ([],t)
1.54    end
1.55 @@ -725,7 +729,7 @@
1.56  fun gen_prover_real_arith ctxt prover =
1.57   let
1.58    fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS