diff --git a/src/HOL/Decision_Procs/Approximation.thy b/src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy +++ b/src/HOL/Decision_Procs/Approximation.thy @@ -1,1232 +1,1232 @@ - (* Author: Johannes Hoelzl, TU Muenchen +(* Author: Johannes Hoelzl, TU Muenchen Coercions removed by Dmitriy Traytel *) theory Approximation imports Complex_Main - "HOL-Library.Code_Target_Numeral" Approximation_Bounds + "HOL-Library.Code_Target_Numeral_Float" keywords "approximate" :: diag begin section "Implement floatarith" subsection "Define syntax and semantics" datatype floatarith = Add floatarith floatarith | Minus floatarith | Mult floatarith floatarith | Inverse floatarith | Cos floatarith | Arctan floatarith | Abs floatarith | Max floatarith floatarith | Min floatarith floatarith | Pi | Sqrt floatarith | Exp floatarith | Powr floatarith floatarith | Ln floatarith | Power floatarith nat | Floor floatarith | Var nat | Num float fun interpret_floatarith :: "floatarith \ real list \ real" where "interpret_floatarith (Add a b) vs = (interpret_floatarith a vs) + (interpret_floatarith b vs)" | "interpret_floatarith (Minus a) vs = - (interpret_floatarith a vs)" | "interpret_floatarith (Mult a b) vs = (interpret_floatarith a vs) * (interpret_floatarith b vs)" | "interpret_floatarith (Inverse a) vs = inverse (interpret_floatarith a vs)" | "interpret_floatarith (Cos a) vs = cos (interpret_floatarith a vs)" | "interpret_floatarith (Arctan a) vs = arctan (interpret_floatarith a vs)" | "interpret_floatarith (Min a b) vs = min (interpret_floatarith a vs) (interpret_floatarith b vs)" | "interpret_floatarith (Max a b) vs = max (interpret_floatarith a vs) (interpret_floatarith b vs)" | "interpret_floatarith (Abs a) vs = \interpret_floatarith a vs\" | "interpret_floatarith Pi vs = pi" | "interpret_floatarith (Sqrt a) vs = sqrt (interpret_floatarith a vs)" | "interpret_floatarith (Exp a) vs = exp (interpret_floatarith a vs)" | "interpret_floatarith (Powr a b) vs = interpret_floatarith a vs powr interpret_floatarith b vs" | "interpret_floatarith (Ln a) vs = ln (interpret_floatarith a vs)" | "interpret_floatarith (Power a n) vs = (interpret_floatarith a vs)^n" | "interpret_floatarith (Floor a) vs = floor (interpret_floatarith a vs)" | "interpret_floatarith (Num f) vs = f" | "interpret_floatarith (Var n) vs = vs ! n" lemma interpret_floatarith_divide: "interpret_floatarith (Mult a (Inverse b)) vs = (interpret_floatarith a vs) / (interpret_floatarith b vs)" unfolding divide_inverse interpret_floatarith.simps .. lemma interpret_floatarith_diff: "interpret_floatarith (Add a (Minus b)) vs = (interpret_floatarith a vs) - (interpret_floatarith b vs)" unfolding interpret_floatarith.simps by simp lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 (- 1)))) (Minus a))) vs = sin (interpret_floatarith a vs)" unfolding sin_cos_eq interpret_floatarith.simps interpret_floatarith_divide interpret_floatarith_diff by auto subsection "Implement approximation function" fun lift_bin :: "(float interval) option \ (float interval) option \ (float interval \ float interval \ (float interval) option) \ (float interval) option" where "lift_bin (Some ivl1) (Some ivl2) f = f ivl1 ivl2" | "lift_bin a b f = None" fun lift_bin' :: "(float interval) option \ (float interval) option \ (float interval \ float interval \ float interval) \ (float interval) option" where "lift_bin' (Some ivl1) (Some ivl2) f = Some (f ivl1 ivl2)" | "lift_bin' a b f = None" fun lift_un :: "float interval option \ (float interval \ float interval option) \ float interval option" where "lift_un (Some ivl) f = f ivl" | "lift_un b f = None" lemma lift_un_eq:\ \TODO\ "lift_un x f = Option.bind x f" by (cases x) auto fun lift_un' :: "(float interval) option \ (float interval \ (float interval)) \ (float interval) option" where "lift_un' (Some ivl1) f = Some (f ivl1)" | "lift_un' b f = None" definition bounded_by :: "real list \ (float interval) option list \ bool" where "bounded_by xs vs \ (\ i < length vs. case vs ! i of None \ True | Some ivl \ xs ! i \\<^sub>r ivl)" lemma bounded_byE: assumes "bounded_by xs vs" shows "\ i. i < length vs \ case vs ! i of None \ True | Some ivl \ xs ! i \\<^sub>r ivl" using assms by (auto simp: bounded_by_def) lemma bounded_by_update: assumes "bounded_by xs vs" and bnd: "xs ! i \\<^sub>r ivl" shows "bounded_by xs (vs[i := Some ivl])" using assms by (cases "i < length vs") (auto simp: bounded_by_def nth_list_update split: option.splits) lemma bounded_by_None: "bounded_by xs (replicate (length xs) None)" unfolding bounded_by_def by auto fun approx approx' :: "nat \ floatarith \ (float interval) option list \ (float interval) option" where "approx' prec a bs = (case (approx prec a bs) of Some ivl \ Some (round_interval prec ivl) | None \ None)" | "approx prec (Add a b) bs = lift_bin' (approx' prec a bs) (approx' prec b bs) (plus_float_interval prec)" | "approx prec (Minus a) bs = lift_un' (approx' prec a bs) uminus" | "approx prec (Mult a b) bs = lift_bin' (approx' prec a bs) (approx' prec b bs) (mult_float_interval prec)" | "approx prec (Inverse a) bs = lift_un (approx' prec a bs) (inverse_float_interval prec)" | "approx prec (Cos a) bs = lift_un' (approx' prec a bs) (cos_float_interval prec)" | "approx prec Pi bs = Some (pi_float_interval prec)" | "approx prec (Min a b) bs = lift_bin' (approx' prec a bs) (approx' prec b bs) (min_interval)" | "approx prec (Max a b) bs = lift_bin' (approx' prec a bs) (approx' prec b bs) (max_interval)" | "approx prec (Abs a) bs = lift_un' (approx' prec a bs) (abs_interval)" | "approx prec (Arctan a) bs = lift_un' (approx' prec a bs) (arctan_float_interval prec)" | "approx prec (Sqrt a) bs = lift_un' (approx' prec a bs) (sqrt_float_interval prec)" | "approx prec (Exp a) bs = lift_un' (approx' prec a bs) (exp_float_interval prec)" | "approx prec (Powr a b) bs = lift_bin (approx' prec a bs) (approx' prec b bs) (powr_float_interval prec)" | "approx prec (Ln a) bs = lift_un (approx' prec a bs) (ln_float_interval prec)" | "approx prec (Power a n) bs = lift_un' (approx' prec a bs) (power_float_interval prec n)" | "approx prec (Floor a) bs = lift_un' (approx' prec a bs) (floor_float_interval)" | "approx prec (Num f) bs = Some (interval_of f)" | "approx prec (Var i) bs = (if i < length bs then bs ! i else None)" lemma approx_approx': assumes Pa: "\ivl. approx prec a vs = Some ivl \ interpret_floatarith a xs \\<^sub>r ivl" and approx': "approx' prec a vs = Some ivl" shows "interpret_floatarith a xs \\<^sub>r ivl" proof - obtain ivl' where S: "approx prec a vs = Some ivl'" and ivl_def: "ivl = round_interval prec ivl'" using approx' unfolding approx'.simps by (cases "approx prec a vs") auto show ?thesis by (auto simp: ivl_def intro!: in_round_intervalI Pa[OF S]) qed lemma approx: assumes "bounded_by xs vs" and "approx prec arith vs = Some ivl" shows "interpret_floatarith arith xs \\<^sub>r ivl" using \approx prec arith vs = Some ivl\ using \bounded_by xs vs\[THEN bounded_byE] by (induct arith arbitrary: ivl) (force split: option.splits if_splits intro!: plus_float_intervalI mult_float_intervalI uminus_in_float_intervalI inverse_float_interval_eqI abs_in_float_intervalI min_intervalI max_intervalI cos_float_intervalI arctan_float_intervalI pi_float_interval sqrt_float_intervalI exp_float_intervalI powr_float_interval_eqI ln_float_interval_eqI power_float_intervalI floor_float_intervalI intro: in_round_intervalI)+ datatype form = Bound floatarith floatarith floatarith form | Assign floatarith floatarith form | Less floatarith floatarith | LessEqual floatarith floatarith | AtLeastAtMost floatarith floatarith floatarith | Conj form form | Disj form form fun interpret_form :: "form \ real list \ bool" where "interpret_form (Bound x a b f) vs = (interpret_floatarith x vs \ { interpret_floatarith a vs .. interpret_floatarith b vs } \ interpret_form f vs)" | "interpret_form (Assign x a f) vs = (interpret_floatarith x vs = interpret_floatarith a vs \ interpret_form f vs)" | "interpret_form (Less a b) vs = (interpret_floatarith a vs < interpret_floatarith b vs)" | "interpret_form (LessEqual a b) vs = (interpret_floatarith a vs \ interpret_floatarith b vs)" | "interpret_form (AtLeastAtMost x a b) vs = (interpret_floatarith x vs \ { interpret_floatarith a vs .. interpret_floatarith b vs })" | "interpret_form (Conj f g) vs \ interpret_form f vs \ interpret_form g vs" | "interpret_form (Disj f g) vs \ interpret_form f vs \ interpret_form g vs" fun approx_form' and approx_form :: "nat \ form \ (float interval) option list \ nat list \ bool" where "approx_form' prec f 0 n ivl bs ss = approx_form prec f (bs[n := Some ivl]) ss" | "approx_form' prec f (Suc s) n ivl bs ss = (let (ivl1, ivl2) = split_float_interval ivl in (if approx_form' prec f s n ivl1 bs ss then approx_form' prec f s n ivl2 bs ss else False))" | "approx_form prec (Bound (Var n) a b f) bs ss = (case (approx prec a bs, approx prec b bs) of (Some ivl1, Some ivl2) \ approx_form' prec f (ss ! n) n (sup ivl1 ivl2) bs ss | _ \ False)" | "approx_form prec (Assign (Var n) a f) bs ss = (case (approx prec a bs) of (Some ivl) \ approx_form' prec f (ss ! n) n ivl bs ss | _ \ False)" | "approx_form prec (Less a b) bs ss = (case (approx prec a bs, approx prec b bs) of (Some ivl, Some ivl') \ float_plus_up prec (upper ivl) (-lower ivl') < 0 | _ \ False)" | "approx_form prec (LessEqual a b) bs ss = (case (approx prec a bs, approx prec b bs) of (Some ivl, Some ivl') \ float_plus_up prec (upper ivl) (-lower ivl') \ 0 | _ \ False)" | "approx_form prec (AtLeastAtMost x a b) bs ss = (case (approx prec x bs, approx prec a bs, approx prec b bs) of (Some ivlx, Some ivl, Some ivl') \ float_plus_up prec (upper ivl) (-lower ivlx) \ 0 \ float_plus_up prec (upper ivlx) (-lower ivl') \ 0 | _ \ False)" | "approx_form prec (Conj a b) bs ss \ approx_form prec a bs ss \ approx_form prec b bs ss" | "approx_form prec (Disj a b) bs ss \ approx_form prec a bs ss \ approx_form prec b bs ss" | "approx_form _ _ _ _ = False" lemma lazy_conj: "(if A then B else False) = (A \ B)" by simp lemma approx_form_approx_form': assumes "approx_form' prec f s n ivl bs ss" and "(x::real) \\<^sub>r ivl" obtains ivl' where "x \\<^sub>r ivl'" and "approx_form prec f (bs[n := Some ivl']) ss" using assms proof (induct s arbitrary: ivl) case 0 from this(1)[of ivl] this(2,3) show thesis by auto next case (Suc s) then obtain ivl1 ivl2 where ivl_split: "split_float_interval ivl = (ivl1, ivl2)" by (fastforce dest: split_float_intervalD) from split_float_interval_realD[OF this \x \\<^sub>r ivl\] consider "x \\<^sub>r ivl1" | "x \\<^sub>r ivl2" by atomize_elim then show thesis proof cases case *: 1 from Suc.hyps[OF _ _ *] Suc.prems show ?thesis by (simp add: lazy_conj ivl_split split: prod.splits) next case *: 2 from Suc.hyps[OF _ _ *] Suc.prems show ?thesis by (simp add: lazy_conj ivl_split split: prod.splits) qed qed lemma approx_form_aux: assumes "approx_form prec f vs ss" and "bounded_by xs vs" shows "interpret_form f xs" using assms proof (induct f arbitrary: vs) case (Bound x a b f) then obtain n where x_eq: "x = Var n" by (cases x) auto with Bound.prems obtain ivl1 ivl2 where l_eq: "approx prec a vs = Some ivl1" and u_eq: "approx prec b vs = Some ivl2" and approx_form': "approx_form' prec f (ss ! n) n (sup ivl1 ivl2) vs ss" by (cases "approx prec a vs", simp) (cases "approx prec b vs", auto) have "interpret_form f xs" if "xs ! n \ { interpret_floatarith a xs .. interpret_floatarith b xs }" proof - from approx[OF Bound.prems(2) l_eq] and approx[OF Bound.prems(2) u_eq] that have "xs ! n \\<^sub>r (sup ivl1 ivl2)" by (auto simp: set_of_eq sup_float_def max_def inf_float_def min_def) from approx_form_approx_form'[OF approx_form' this] obtain ivlx where bnds: "xs ! n \\<^sub>r ivlx" and approx_form: "approx_form prec f (vs[n := Some ivlx]) ss" . from \bounded_by xs vs\ bnds have "bounded_by xs (vs[n := Some ivlx])" by (rule bounded_by_update) with Bound.hyps[OF approx_form] show ?thesis by blast qed thus ?case using interpret_form.simps x_eq and interpret_floatarith.simps by simp next case (Assign x a f) then obtain n where x_eq: "x = Var n" by (cases x) auto with Assign.prems obtain ivl where bnd_eq: "approx prec a vs = Some ivl" and x_eq: "x = Var n" and approx_form': "approx_form' prec f (ss ! n) n ivl vs ss" by (cases "approx prec a vs") auto have "interpret_form f xs" if bnds: "xs ! n = interpret_floatarith a xs" proof - from approx[OF Assign.prems(2) bnd_eq] bnds have "xs ! n \\<^sub>r ivl" by auto from approx_form_approx_form'[OF approx_form' this] obtain ivlx where bnds: "xs ! n \\<^sub>r ivlx" and approx_form: "approx_form prec f (vs[n := Some ivlx]) ss" . from \bounded_by xs vs\ bnds have "bounded_by xs (vs[n := Some ivlx])" by (rule bounded_by_update) with Assign.hyps[OF approx_form] show ?thesis by blast qed thus ?case using interpret_form.simps x_eq and interpret_floatarith.simps by simp next case (Less a b) then obtain ivl ivl' where l_eq: "approx prec a vs = Some ivl" and u_eq: "approx prec b vs = Some ivl'" and inequality: "real_of_float (float_plus_up prec (upper ivl) (-lower ivl')) < 0" by (cases "approx prec a vs", auto, cases "approx prec b vs", auto) from le_less_trans[OF float_plus_up inequality] approx[OF Less.prems(2) l_eq] approx[OF Less.prems(2) u_eq] show ?case by (auto simp: set_of_eq) next case (LessEqual a b) then obtain ivl ivl' where l_eq: "approx prec a vs = Some ivl" and u_eq: "approx prec b vs = Some ivl'" and inequality: "real_of_float (float_plus_up prec (upper ivl) (-lower ivl')) \ 0" by (cases "approx prec a vs", auto, cases "approx prec b vs", auto) from order_trans[OF float_plus_up inequality] approx[OF LessEqual.prems(2) l_eq] approx[OF LessEqual.prems(2) u_eq] show ?case by (auto simp: set_of_eq) next case (AtLeastAtMost x a b) then obtain ivlx ivl ivl' where x_eq: "approx prec x vs = Some ivlx" and l_eq: "approx prec a vs = Some ivl" and u_eq: "approx prec b vs = Some ivl'" and inequality: "real_of_float (float_plus_up prec (upper ivl) (-lower ivlx)) \ 0" "real_of_float (float_plus_up prec (upper ivlx) (-lower ivl')) \ 0" by (cases "approx prec x vs", auto, cases "approx prec a vs", auto, cases "approx prec b vs", auto) from order_trans[OF float_plus_up inequality(1)] order_trans[OF float_plus_up inequality(2)] approx[OF AtLeastAtMost.prems(2) l_eq] approx[OF AtLeastAtMost.prems(2) u_eq] approx[OF AtLeastAtMost.prems(2) x_eq] show ?case by (auto simp: set_of_eq) qed auto lemma approx_form: assumes "n = length xs" and "approx_form prec f (replicate n None) ss" shows "interpret_form f xs" using approx_form_aux[OF _ bounded_by_None] assms by auto subsection \Implementing Taylor series expansion\ fun isDERIV :: "nat \ floatarith \ real list \ bool" where "isDERIV x (Add a b) vs = (isDERIV x a vs \ isDERIV x b vs)" | "isDERIV x (Mult a b) vs = (isDERIV x a vs \ isDERIV x b vs)" | "isDERIV x (Minus a) vs = isDERIV x a vs" | "isDERIV x (Inverse a) vs = (isDERIV x a vs \ interpret_floatarith a vs \ 0)" | "isDERIV x (Cos a) vs = isDERIV x a vs" | "isDERIV x (Arctan a) vs = isDERIV x a vs" | "isDERIV x (Min a b) vs = False" | "isDERIV x (Max a b) vs = False" | "isDERIV x (Abs a) vs = False" | "isDERIV x Pi vs = True" | "isDERIV x (Sqrt a) vs = (isDERIV x a vs \ interpret_floatarith a vs > 0)" | "isDERIV x (Exp a) vs = isDERIV x a vs" | "isDERIV x (Powr a b) vs = (isDERIV x a vs \ isDERIV x b vs \ interpret_floatarith a vs > 0)" | "isDERIV x (Ln a) vs = (isDERIV x a vs \ interpret_floatarith a vs > 0)" | "isDERIV x (Floor a) vs = (isDERIV x a vs \ interpret_floatarith a vs \ \)" | "isDERIV x (Power a 0) vs = True" | "isDERIV x (Power a (Suc n)) vs = isDERIV x a vs" | "isDERIV x (Num f) vs = True" | "isDERIV x (Var n) vs = True" fun DERIV_floatarith :: "nat \ floatarith \ floatarith" where "DERIV_floatarith x (Add a b) = Add (DERIV_floatarith x a) (DERIV_floatarith x b)" | "DERIV_floatarith x (Mult a b) = Add (Mult a (DERIV_floatarith x b)) (Mult (DERIV_floatarith x a) b)" | "DERIV_floatarith x (Minus a) = Minus (DERIV_floatarith x a)" | "DERIV_floatarith x (Inverse a) = Minus (Mult (DERIV_floatarith x a) (Inverse (Power a 2)))" | "DERIV_floatarith x (Cos a) = Minus (Mult (Cos (Add (Mult Pi (Num (Float 1 (- 1)))) (Minus a))) (DERIV_floatarith x a))" | "DERIV_floatarith x (Arctan a) = Mult (Inverse (Add (Num 1) (Power a 2))) (DERIV_floatarith x a)" | "DERIV_floatarith x (Min a b) = Num 0" | "DERIV_floatarith x (Max a b) = Num 0" | "DERIV_floatarith x (Abs a) = Num 0" | "DERIV_floatarith x Pi = Num 0" | "DERIV_floatarith x (Sqrt a) = (Mult (Inverse (Mult (Sqrt a) (Num 2))) (DERIV_floatarith x a))" | "DERIV_floatarith x (Exp a) = Mult (Exp a) (DERIV_floatarith x a)" | "DERIV_floatarith x (Powr a b) = Mult (Powr a b) (Add (Mult (DERIV_floatarith x b) (Ln a)) (Mult (Mult (DERIV_floatarith x a) b) (Inverse a)))" | "DERIV_floatarith x (Ln a) = Mult (Inverse a) (DERIV_floatarith x a)" | "DERIV_floatarith x (Power a 0) = Num 0" | "DERIV_floatarith x (Power a (Suc n)) = Mult (Num (Float (int (Suc n)) 0)) (Mult (Power a n) (DERIV_floatarith x a))" | "DERIV_floatarith x (Floor a) = Num 0" | "DERIV_floatarith x (Num f) = Num 0" | "DERIV_floatarith x (Var n) = (if x = n then Num 1 else Num 0)" lemma has_real_derivative_powr': fixes f g :: "real \ real" assumes "(f has_real_derivative f') (at x)" assumes "(g has_real_derivative g') (at x)" assumes "f x > 0" defines "h \ \x. f x powr g x * (g' * ln (f x) + f' * g x / f x)" shows "((\x. f x powr g x) has_real_derivative h x) (at x)" proof (subst DERIV_cong_ev[OF refl _ refl]) from assms have "isCont f x" by (simp add: DERIV_continuous) hence "f \x\ f x" by (simp add: continuous_at) with \f x > 0\ have "eventually (\x. f x > 0) (nhds x)" by (auto simp: tendsto_at_iff_tendsto_nhds dest: order_tendstoD) thus "eventually (\x. f x powr g x = exp (g x * ln (f x))) (nhds x)" by eventually_elim (simp add: powr_def) next from assms show "((\x. exp (g x * ln (f x))) has_real_derivative h x) (at x)" by (auto intro!: derivative_eq_intros simp: h_def powr_def) qed lemma DERIV_floatarith: assumes "n < length vs" assumes isDERIV: "isDERIV n f (vs[n := x])" shows "DERIV (\ x'. interpret_floatarith f (vs[n := x'])) x :> interpret_floatarith (DERIV_floatarith n f) (vs[n := x])" (is "DERIV (?i f) x :> _") using isDERIV proof (induct f arbitrary: x) case (Inverse a) thus ?case by (auto intro!: derivative_eq_intros simp add: algebra_simps power2_eq_square) next case (Cos a) thus ?case by (auto intro!: derivative_eq_intros simp del: interpret_floatarith.simps(5) simp add: interpret_floatarith_sin interpret_floatarith.simps(5)[of a]) next case (Power a n) thus ?case by (cases n) (auto intro!: derivative_eq_intros simp del: power_Suc) next case (Floor a) thus ?case by (auto intro!: derivative_eq_intros DERIV_isCont floor_has_real_derivative) next case (Ln a) thus ?case by (auto intro!: derivative_eq_intros simp add: divide_inverse) next case (Var i) thus ?case using \n < length vs\ by auto next case (Powr a b) note [derivative_intros] = has_real_derivative_powr' from Powr show ?case by (auto intro!: derivative_eq_intros simp: field_simps) qed (auto intro!: derivative_eq_intros) declare approx.simps[simp del] fun isDERIV_approx :: "nat \ nat \ floatarith \ (float interval) option list \ bool" where "isDERIV_approx prec x (Add a b) vs = (isDERIV_approx prec x a vs \ isDERIV_approx prec x b vs)" | "isDERIV_approx prec x (Mult a b) vs = (isDERIV_approx prec x a vs \ isDERIV_approx prec x b vs)" | "isDERIV_approx prec x (Minus a) vs = isDERIV_approx prec x a vs" | "isDERIV_approx prec x (Inverse a) vs = (isDERIV_approx prec x a vs \ (case approx prec a vs of Some ivl \ 0 < lower ivl \ upper ivl < 0 | None \ False))" | "isDERIV_approx prec x (Cos a) vs = isDERIV_approx prec x a vs" | "isDERIV_approx prec x (Arctan a) vs = isDERIV_approx prec x a vs" | "isDERIV_approx prec x (Min a b) vs = False" | "isDERIV_approx prec x (Max a b) vs = False" | "isDERIV_approx prec x (Abs a) vs = False" | "isDERIV_approx prec x Pi vs = True" | "isDERIV_approx prec x (Sqrt a) vs = (isDERIV_approx prec x a vs \ (case approx prec a vs of Some ivl \ 0 < lower ivl | None \ False))" | "isDERIV_approx prec x (Exp a) vs = isDERIV_approx prec x a vs" | "isDERIV_approx prec x (Powr a b) vs = (isDERIV_approx prec x a vs \ isDERIV_approx prec x b vs \ (case approx prec a vs of Some ivl \ 0 < lower ivl | None \ False))" | "isDERIV_approx prec x (Ln a) vs = (isDERIV_approx prec x a vs \ (case approx prec a vs of Some ivl \ 0 < lower ivl | None \ False))" | "isDERIV_approx prec x (Power a 0) vs = True" | "isDERIV_approx prec x (Floor a) vs = (isDERIV_approx prec x a vs \ (case approx prec a vs of Some ivl \ lower ivl > floor (upper ivl) \ upper ivl < ceiling (lower ivl) | None \ False))" | "isDERIV_approx prec x (Power a (Suc n)) vs = isDERIV_approx prec x a vs" | "isDERIV_approx prec x (Num f) vs = True" | "isDERIV_approx prec x (Var n) vs = True" lemma isDERIV_approx: assumes "bounded_by xs vs" and isDERIV_approx: "isDERIV_approx prec x f vs" shows "isDERIV x f xs" using isDERIV_approx proof (induct f) case (Inverse a) then obtain ivl where approx_Some: "approx prec a vs = Some ivl" and *: "0 < lower ivl \ upper ivl < 0" by (cases "approx prec a vs") auto with approx[OF \bounded_by xs vs\ approx_Some] have "interpret_floatarith a xs \ 0" by (auto simp: set_of_eq) thus ?case using Inverse by auto next case (Ln a) then obtain ivl where approx_Some: "approx prec a vs = Some ivl" and *: "0 < lower ivl" by (cases "approx prec a vs") auto with approx[OF \bounded_by xs vs\ approx_Some] have "0 < interpret_floatarith a xs" by (auto simp: set_of_eq) thus ?case using Ln by auto next case (Sqrt a) then obtain ivl where approx_Some: "approx prec a vs = Some ivl" and *: "0 < lower ivl" by (cases "approx prec a vs") auto with approx[OF \bounded_by xs vs\ approx_Some] have "0 < interpret_floatarith a xs" by (auto simp: set_of_eq) thus ?case using Sqrt by auto next case (Power a n) thus ?case by (cases n) auto next case (Powr a b) from Powr obtain ivl1 where a: "approx prec a vs = Some ivl1" and pos: "0 < lower ivl1" by (cases "approx prec a vs") auto with approx[OF \bounded_by xs vs\ a] have "0 < interpret_floatarith a xs" by (auto simp: set_of_eq) with Powr show ?case by auto next case (Floor a) then obtain ivl where approx_Some: "approx prec a vs = Some ivl" and "real_of_int \real_of_float (upper ivl)\ < real_of_float (lower ivl)" "real_of_float (upper ivl) < real_of_int \real_of_float (lower ivl)\" and "isDERIV x a xs" by (cases "approx prec a vs") auto with approx[OF \bounded_by xs vs\ approx_Some] le_floor_iff show ?case by (force elim!: Ints_cases simp: set_of_eq) qed auto lemma bounded_by_update_var: assumes "bounded_by xs vs" and "vs ! i = Some ivl" and bnd: "x \\<^sub>r ivl" shows "bounded_by (xs[i := x]) vs" using assms using nth_list_update by (cases "i < length xs") (force simp: bounded_by_def split: option.splits)+ lemma isDERIV_approx': assumes "bounded_by xs vs" and vs_x: "vs ! x = Some ivl" and X_in: "X \\<^sub>r ivl" and approx: "isDERIV_approx prec x f vs" shows "isDERIV x f (xs[x := X])" proof - from bounded_by_update_var[OF \bounded_by xs vs\ vs_x X_in] approx show ?thesis by (rule isDERIV_approx) qed lemma DERIV_approx: assumes "n < length xs" and bnd: "bounded_by xs vs" and isD: "isDERIV_approx prec n f vs" and app: "approx prec (DERIV_floatarith n f) vs = Some ivl" (is "approx _ ?D _ = _") shows "\(x::real). x \\<^sub>r ivl \ DERIV (\ x. interpret_floatarith f (xs[n := x])) (xs!n) :> x" (is "\ x. _ \ DERIV (?i f) _ :> _") proof (rule exI[of _ "?i ?D (xs!n)"], rule conjI) let "?i f" = "\x. interpret_floatarith f (xs[n := x])" from approx[OF bnd app] show "?i ?D (xs!n) \\<^sub>r ivl" using \n < length xs\ by auto from DERIV_floatarith[OF \n < length xs\, of f "xs!n"] isDERIV_approx[OF bnd isD] show "DERIV (?i f) (xs!n) :> (?i ?D (xs!n))" by simp qed lemma lift_bin_aux: assumes lift_bin_Some: "lift_bin a b f = Some ivl" obtains ivl1 ivl2 where "a = Some ivl1" and "b = Some ivl2" and "f ivl1 ivl2 = Some ivl" using assms by (cases a, simp, cases b, simp, auto) fun approx_tse where "approx_tse prec n 0 c k f bs = approx prec f bs" | "approx_tse prec n (Suc s) c k f bs = (if isDERIV_approx prec n f bs then lift_bin (approx prec f (bs[n := Some (interval_of c)])) (approx_tse prec n s c (Suc k) (DERIV_floatarith n f) bs) (\ivl1 ivl2. approx prec (Add (Var 0) (Mult (Inverse (Num (Float (int k) 0))) (Mult (Add (Var (Suc (Suc 0))) (Minus (Num c))) (Var (Suc 0))))) [Some ivl1, Some ivl2, bs!n]) else approx prec f bs)" lemma bounded_by_Cons: assumes bnd: "bounded_by xs vs" and x: "x \\<^sub>r ivl" shows "bounded_by (x#xs) ((Some ivl)#vs)" proof - have "case ((Some ivl)#vs) ! i of Some ivl \ (x#xs)!i \\<^sub>r ivl | None \ True" if *: "i < length ((Some ivl)#vs)" for i proof (cases i) case 0 with x show ?thesis by auto next case (Suc i) with * have "i < length vs" by auto from bnd[THEN bounded_byE, OF this] show ?thesis unfolding Suc nth_Cons_Suc . qed thus ?thesis by (auto simp add: bounded_by_def) qed lemma approx_tse_generic: assumes "bounded_by xs vs" and bnd_c: "bounded_by (xs[x := c]) vs" and "x < length vs" and "x < length xs" and bnd_x: "vs ! x = Some ivlx" and ate: "approx_tse prec x s c k f vs = Some ivl" shows "\ n. (\ m < n. \ (z::real) \ set_of (real_interval ivlx). DERIV (\ y. interpret_floatarith ((DERIV_floatarith x ^^ m) f) (xs[x := y])) z :> (interpret_floatarith ((DERIV_floatarith x ^^ (Suc m)) f) (xs[x := z]))) \ (\ (t::real) \ set_of (real_interval ivlx). (\ i = 0.. j \ {k.. j \ {k..\<^sub>r ivl)" (is "\ n. ?taylor f k ivl n") using ate proof (induct s arbitrary: k f ivl) case 0 { fix t::real assume "t \\<^sub>r ivlx" note bounded_by_update_var[OF \bounded_by xs vs\ bnd_x this] from approx[OF this 0[unfolded approx_tse.simps]] have "(interpret_floatarith f (xs[x := t])) \\<^sub>r ivl" by (auto simp add: algebra_simps) } thus ?case by (auto intro!: exI[of _ 0]) next case (Suc s) show ?case proof (cases "isDERIV_approx prec x f vs") case False note ap = Suc.prems[unfolded approx_tse.simps if_not_P[OF False]] { fix t::real assume "t \\<^sub>r ivlx" note bounded_by_update_var[OF \bounded_by xs vs\ bnd_x this] from approx[OF this ap] have "(interpret_floatarith f (xs[x := t])) \\<^sub>r ivl" by (auto simp add: algebra_simps) } thus ?thesis by (auto intro!: exI[of _ 0]) next case True with Suc.prems obtain ivl1 ivl2 where a: "approx prec f (vs[x := Some (interval_of c)]) = Some ivl1" and ate: "approx_tse prec x s c (Suc k) (DERIV_floatarith x f) vs = Some ivl2" and final: "approx prec (Add (Var 0) (Mult (Inverse (Num (Float (int k) 0))) (Mult (Add (Var (Suc (Suc 0))) (Minus (Num c))) (Var (Suc 0))))) [Some ivl1, Some ivl2, vs!x] = Some ivl" by (auto elim!: lift_bin_aux) from bnd_c \x < length xs\ have bnd: "bounded_by (xs[x:=c]) (vs[x:= Some (interval_of c)])" by (auto intro!: bounded_by_update) from approx[OF this a] have f_c: "interpret_floatarith ((DERIV_floatarith x ^^ 0) f) (xs[x := c]) \\<^sub>r ivl1" (is "?f 0 (real_of_float c) \ _") by auto have funpow_Suc[symmetric]: "(f ^^ Suc n) x = (f ^^ n) (f x)" for f :: "'a \ 'a" and n :: nat and x :: 'a by (induct n) auto from Suc.hyps[OF ate, unfolded this] obtain n where DERIV_hyp: "\m z. \ m < n ; (z::real) \\<^sub>r ivlx \ \ DERIV (?f (Suc m)) z :> ?f (Suc (Suc m)) z" and hyp: "\t \ set_of (real_interval ivlx). (\ i = 0.. j \ {Suc k.. j \ {Suc k..\<^sub>r ivl2" (is "\ t \ _. ?X (Suc k) f n t \ _") by blast have DERIV: "DERIV (?f m) z :> ?f (Suc m) z" if "m < Suc n" and bnd_z: "z \\<^sub>r ivlx" for m and z::real proof (cases m) case 0 with DERIV_floatarith[OF \x < length xs\ isDERIV_approx'[OF \bounded_by xs vs\ bnd_x bnd_z True]] show ?thesis by simp next case (Suc m') hence "m' < n" using \m < Suc n\ by auto from DERIV_hyp[OF this bnd_z] show ?thesis using Suc by simp qed have "\k i. k < i \ {k ..< i} = insert k {Suc k ..< i}" by auto hence prod_head_Suc: "\k i. \{k ..< k + Suc i} = k * \{Suc k ..< Suc k + i}" by auto have sum_move0: "\k F. sum F {0.. k. F (Suc k)) {0..\<^sub>r ivlx" hence "bounded_by [xs!x] [vs!x]" using \bounded_by xs vs\[THEN bounded_byE, OF \x < length vs\] by (cases "vs!x", auto simp add: bounded_by_def) with hyp[THEN bspec, OF t] f_c have "bounded_by [?f 0 c, ?X (Suc k) f n t, xs!x] [Some ivl1, Some ivl2, vs!x]" by (auto intro!: bounded_by_Cons) from approx[OF this final, unfolded atLeastAtMost_iff[symmetric]] have "?X (Suc k) f n t * (xs!x - real_of_float c) * inverse k + ?f 0 c \\<^sub>r ivl" by (auto simp add: algebra_simps) also have "?X (Suc k) f n t * (xs!x - real_of_float c) * inverse (real k) + ?f 0 c = (\ i = 0.. j \ {k.. j \ {k..\<^sub>r ivl" . } thus ?thesis using DERIV by blast qed qed lemma prod_fact: "real (\ {1..<1 + k}) = fact (k :: nat)" by (simp add: fact_prod atLeastLessThanSuc_atLeastAtMost) lemma approx_tse: assumes "bounded_by xs vs" and bnd_x: "vs ! x = Some ivlx" and bnd_c: "real_of_float c \\<^sub>r ivlx" and "x < length vs" and "x < length xs" and ate: "approx_tse prec x s c 1 f vs = Some ivl" shows "interpret_floatarith f xs \\<^sub>r ivl" proof - define F where [abs_def]: "F n z = interpret_floatarith ((DERIV_floatarith x ^^ n) f) (xs[x := z])" for n z hence F0: "F 0 = (\ z. interpret_floatarith f (xs[x := z]))" by auto hence "bounded_by (xs[x := c]) vs" and "x < length vs" "x < length xs" using \bounded_by xs vs\ bnd_x bnd_c \x < length vs\ \x < length xs\ by (auto intro!: bounded_by_update_var) from approx_tse_generic[OF \bounded_by xs vs\ this bnd_x ate] obtain n where DERIV: "\ m z. m < n \ real_of_float (lower ivlx) \ z \ z \ real_of_float (upper ivlx) \ DERIV (F m) z :> F (Suc m) z" and hyp: "\ (t::real). t \\<^sub>r ivlx \ (\ j = 0..\<^sub>r ivl" (is "\ t. _ \ ?taylor t \ _") unfolding F_def atLeastAtMost_iff[symmetric] prod_fact by (auto simp: set_of_eq Ball_def) have bnd_xs: "xs ! x \\<^sub>r ivlx" using \bounded_by xs vs\[THEN bounded_byE, OF \x < length vs\] bnd_x by auto show ?thesis proof (cases n) case 0 thus ?thesis using hyp[OF bnd_xs] unfolding F_def by auto next case (Suc n') show ?thesis proof (cases "xs ! x = c") case True from True[symmetric] hyp[OF bnd_xs] Suc show ?thesis unfolding F_def Suc sum.atLeast_Suc_lessThan[OF zero_less_Suc] sum.shift_bounds_Suc_ivl by auto next case False have "lower ivlx \ real_of_float c" "real_of_float c \ upper ivlx" "lower ivlx \ xs!x" "xs!x \ upper ivlx" using Suc bnd_c \bounded_by xs vs\[THEN bounded_byE, OF \x < length vs\] bnd_x by (auto simp: set_of_eq) from Taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False] obtain t::real where t_bnd: "if xs ! x < c then xs ! x < t \ t < c else c < t \ t < xs ! x" and fl_eq: "interpret_floatarith f (xs[x := xs ! x]) = (\m = 0..\<^sub>r ivlx" by (cases "xs ! x < c") (auto simp: set_of_eq) have "interpret_floatarith f (xs[x := xs ! x]) = ?taylor t" unfolding fl_eq Suc by (auto simp add: algebra_simps divide_inverse) also have "\ \\<^sub>r ivl" using * by (rule hyp) finally show ?thesis by simp qed qed qed fun approx_tse_form' where "approx_tse_form' prec t f 0 ivl cmp = (case approx_tse prec 0 t (mid ivl) 1 f [Some ivl] of Some ivl \ cmp ivl | None \ False)" | "approx_tse_form' prec t f (Suc s) ivl cmp = (let (ivl1, ivl2) = split_float_interval ivl in (if approx_tse_form' prec t f s ivl1 cmp then approx_tse_form' prec t f s ivl2 cmp else False))" lemma approx_tse_form': fixes x :: real assumes "approx_tse_form' prec t f s ivl cmp" and "x \\<^sub>r ivl" shows "\ivl' ivly. x \\<^sub>r ivl' \ ivl' \ ivl \ cmp ivly \ approx_tse prec 0 t (mid ivl') 1 f [Some ivl'] = Some ivly" using assms proof (induct s arbitrary: ivl) case 0 then obtain ivly where *: "approx_tse prec 0 t (mid ivl) 1 f [Some ivl] = Some ivly" and **: "cmp ivly" by (auto elim!: case_optionE) with 0 show ?case by auto next case (Suc s) let ?ivl1 = "fst (split_float_interval ivl)" let ?ivl2 = "snd (split_float_interval ivl)" from Suc.prems have l: "approx_tse_form' prec t f s ?ivl1 cmp" and u: "approx_tse_form' prec t f s ?ivl2 cmp" by (auto simp add: Let_def lazy_conj) have subintervals: "?ivl1 \ ivl" "?ivl2 \ ivl" using mid_le by (auto simp: less_eq_interval_def split_float_interval_bounds) from split_float_interval_realD[OF _ \x \\<^sub>r ivl\] consider "x \\<^sub>r ?ivl1" | "x \\<^sub>r ?ivl2" by (auto simp: prod_eq_iff) then show ?case proof cases case 1 from Suc.hyps[OF l this] obtain ivl' ivly where "x \\<^sub>r ivl' \ ivl' \ fst (split_float_interval ivl) \ cmp ivly \ approx_tse prec 0 t (mid ivl') 1 f [Some ivl'] = Some ivly" by blast then show ?thesis using subintervals by (auto) next case 2 from Suc.hyps[OF u this] obtain ivl' ivly where "x \\<^sub>r ivl' \ ivl' \ snd (split_float_interval ivl) \ cmp ivly \ approx_tse prec 0 t (mid ivl') 1 f [Some ivl'] = Some ivly" by blast then show ?thesis using subintervals by (auto) qed qed lemma approx_tse_form'_less: fixes x :: real assumes tse: "approx_tse_form' prec t (Add a (Minus b)) s ivl (\ ivl. 0 < lower ivl)" and x: "x \\<^sub>r ivl" shows "interpret_floatarith b [x] < interpret_floatarith a [x]" proof - from approx_tse_form'[OF tse x] obtain ivl' ivly where x': "x \\<^sub>r ivl'" and "ivl' \ ivl" and "0 < lower ivly" and tse: "approx_tse prec 0 t (mid ivl') 1 (Add a (Minus b)) [Some ivl'] = Some ivly" by blast hence "bounded_by [x] [Some ivl']" by (auto simp add: bounded_by_def) from approx_tse[OF this _ _ _ _ tse, of ivl'] x' mid_le have "lower ivly \ interpret_floatarith a [x] - interpret_floatarith b [x]" by (auto simp: set_of_eq) from order_less_le_trans[OF _ this, of 0] \0 < lower ivly\ show ?thesis by auto qed lemma approx_tse_form'_le: fixes x :: real assumes tse: "approx_tse_form' prec t (Add a (Minus b)) s ivl (\ ivl. 0 \ lower ivl)" and x: "x \\<^sub>r ivl" shows "interpret_floatarith b [x] \ interpret_floatarith a [x]" proof - from approx_tse_form'[OF tse x] obtain ivl' ivly where x': "x \\<^sub>r ivl'" and "ivl' \ ivl" and "0 \ lower ivly" and tse: "approx_tse prec 0 t (mid ivl') 1 (Add a (Minus b)) [Some (ivl')] = Some ivly" by blast hence "bounded_by [x] [Some ivl']" by (auto simp add: bounded_by_def) from approx_tse[OF this _ _ _ _ tse, of ivl'] x' mid_le have "lower ivly \ interpret_floatarith a [x] - interpret_floatarith b [x]" by (auto simp: set_of_eq) from order_trans[OF _ this, of 0] \0 \ lower ivly\ show ?thesis by auto qed fun approx_tse_concl where "approx_tse_concl prec t (Less lf rt) s ivl ivl' \ approx_tse_form' prec t (Add rt (Minus lf)) s (sup ivl ivl') (\ ivl. 0 < lower ivl)" | "approx_tse_concl prec t (LessEqual lf rt) s ivl ivl' \ approx_tse_form' prec t (Add rt (Minus lf)) s (sup ivl ivl') (\ ivl. 0 \ lower ivl)" | "approx_tse_concl prec t (AtLeastAtMost x lf rt) s ivl ivl' \ (if approx_tse_form' prec t (Add x (Minus lf)) s (sup ivl ivl') (\ ivl. 0 \ lower ivl) then approx_tse_form' prec t (Add rt (Minus x)) s (sup ivl ivl') (\ ivl. 0 \ lower ivl) else False)" | "approx_tse_concl prec t (Conj f g) s ivl ivl' \ approx_tse_concl prec t f s ivl ivl' \ approx_tse_concl prec t g s ivl ivl'" | "approx_tse_concl prec t (Disj f g) s ivl ivl' \ approx_tse_concl prec t f s ivl ivl' \ approx_tse_concl prec t g s ivl ivl'" | "approx_tse_concl _ _ _ _ _ _ \ False" definition "approx_tse_form prec t s f = (case f of Bound x a b f \ x = Var 0 \ (case (approx prec a [None], approx prec b [None]) of (Some ivl, Some ivl') \ approx_tse_concl prec t f s ivl ivl' | _ \ False) | _ \ False)" lemma approx_tse_form: assumes "approx_tse_form prec t s f" shows "interpret_form f [x]" proof (cases f) case f_def: (Bound i a b f') with assms obtain ivl ivl' where a: "approx prec a [None] = Some ivl" and b: "approx prec b [None] = Some ivl'" unfolding approx_tse_form_def by (auto elim!: case_optionE) from f_def assms have "i = Var 0" unfolding approx_tse_form_def by auto hence i: "interpret_floatarith i [x] = x" by auto { let ?f = "\z. interpret_floatarith z [x]" assume "?f i \ { ?f a .. ?f b }" with approx[OF _ a, of "[x]"] approx[OF _ b, of "[x]"] have bnd: "x \\<^sub>r sup ivl ivl'" unfolding bounded_by_def i by (auto simp: set_of_eq sup_float_def inf_float_def min_def max_def) have "interpret_form f' [x]" using assms[unfolded f_def] proof (induct f') case (Less lf rt) with a b have "approx_tse_form' prec t (Add rt (Minus lf)) s (sup ivl ivl') (\ ivl. 0 < lower ivl)" unfolding approx_tse_form_def by auto from approx_tse_form'_less[OF this bnd] show ?case using Less by auto next case (LessEqual lf rt) with f_def a b assms have "approx_tse_form' prec t (Add rt (Minus lf)) s (sup ivl ivl') (\ ivl. 0 \ lower ivl)" unfolding approx_tse_form_def by auto from approx_tse_form'_le[OF this bnd] show ?case using LessEqual by auto next case (AtLeastAtMost x lf rt) with f_def a b assms have "approx_tse_form' prec t (Add rt (Minus x)) s (sup ivl ivl') (\ ivl. 0 \ lower ivl)" and "approx_tse_form' prec t (Add x (Minus lf)) s (sup ivl ivl') (\ ivl. 0 \ lower ivl)" unfolding approx_tse_form_def lazy_conj by (auto split: if_split_asm) from approx_tse_form'_le[OF this(1) bnd] approx_tse_form'_le[OF this(2) bnd] show ?case using AtLeastAtMost by auto qed (auto simp: f_def approx_tse_form_def elim!: case_optionE) } thus ?thesis unfolding f_def by auto qed (insert assms, auto simp add: approx_tse_form_def) text \\<^term>\approx_form_eval\ is only used for the {\tt value}-command.\ fun approx_form_eval :: "nat \ form \ (float interval) option list \ (float interval) option list" where "approx_form_eval prec (Bound (Var n) a b f) bs = (case (approx prec a bs, approx prec b bs) of (Some ivl1, Some ivl2) \ approx_form_eval prec f (bs[n := Some (sup ivl1 ivl2)]) | _ \ bs)" | "approx_form_eval prec (Assign (Var n) a f) bs = (case (approx prec a bs) of (Some ivl) \ approx_form_eval prec f (bs[n := Some ivl]) | _ \ bs)" | "approx_form_eval prec (Less a b) bs = bs @ [approx prec a bs, approx prec b bs]" | "approx_form_eval prec (LessEqual a b) bs = bs @ [approx prec a bs, approx prec b bs]" | "approx_form_eval prec (AtLeastAtMost x a b) bs = bs @ [approx prec x bs, approx prec a bs, approx prec b bs]" | "approx_form_eval _ _ bs = bs" subsection \Implement proof method \texttt{approximation}\ ML \ val _ = \ \Trusting the oracle \@{oracle_name "holds_by_evaluation"} signature APPROXIMATION_COMPUTATION = sig val approx_bool: Proof.context -> term -> term val approx_arith: Proof.context -> term -> term val approx_form_eval: Proof.context -> term -> term val approx_conv: Proof.context -> conv end structure Approximation_Computation : APPROXIMATION_COMPUTATION = struct fun approx_conv ctxt ct = @{computation_check terms: Trueprop "0 :: nat" "1 :: nat" "2 :: nat" "3 :: nat" Suc "(+)::nat\nat\nat" "(-)::nat\nat\nat" "(*)::nat\nat\nat" "0 :: int" "1 :: int" "2 :: int" "3 :: int" "-1 :: int" "(+)::int\int\int" "(-)::int\int\int" "(*)::int\int\int" "uminus::int\int" "replicate :: _ \ (float interval) option \ _" "interval_of::float\float interval" approx' approx_form approx_tse_form approx_form_eval datatypes: bool int nat integer "nat list" float "(float interval) option list" floatarith form } ctxt ct fun term_of_bool true = \<^term>\True\ | term_of_bool false = \<^term>\False\; val mk_int = HOLogic.mk_number \<^typ>\int\ o @{code integer_of_int}; fun term_of_float (@{code Float} (k, l)) = \<^term>\Float\ $ mk_int k $ mk_int l; fun term_of_float_interval x = @{term "Interval::_\float interval"} $ HOLogic.mk_prod (apply2 term_of_float (@{code lowerF} x, @{code upperF} x)) fun term_of_float_interval_option NONE = \<^term>\None :: (float interval) option\ | term_of_float_interval_option (SOME ff) = \<^term>\Some :: float interval \ _\ $ (term_of_float_interval ff); val term_of_float_interval_option_list = HOLogic.mk_list \<^typ>\(float interval) option\ o map term_of_float_interval_option; val approx_bool = @{computation bool} (fn _ => fn x => case x of SOME b => term_of_bool b | NONE => error "Computation approx_bool failed.") val approx_arith = @{computation "float interval option"} (fn _ => fn x => case x of SOME ffo => term_of_float_interval_option ffo | NONE => error "Computation approx_arith failed.") val approx_form_eval = @{computation "float interval option list"} (fn _ => fn x => case x of SOME ffos => term_of_float_interval_option_list ffos | NONE => error "Computation approx_form_eval failed.") end \ lemma intervalE: "a \ x \ x \ b \ \ x \ { a .. b } \ P\ \ P" by auto lemma meta_eqE: "x \ a \ \ x = a \ P\ \ P" by auto named_theorems approximation_preproc lemma approximation_preproc_floatarith[approximation_preproc]: "0 = real_of_float 0" "1 = real_of_float 1" "0 = Float 0 0" "1 = Float 1 0" "numeral a = Float (numeral a) 0" "numeral a = real_of_float (numeral a)" "x - y = x + - y" "x / y = x * inverse y" "ceiling x = - floor (- x)" "log x y = ln y * inverse (ln x)" "sin x = cos (pi / 2 - x)" "tan x = sin x / cos x" by (simp_all add: inverse_eq_divide ceiling_def log_def sin_cos_eq tan_def real_of_float_eq) lemma approximation_preproc_int[approximation_preproc]: "real_of_int 0 = real_of_float 0" "real_of_int 1 = real_of_float 1" "real_of_int (i + j) = real_of_int i + real_of_int j" "real_of_int (- i) = - real_of_int i" "real_of_int (i - j) = real_of_int i - real_of_int j" "real_of_int (i * j) = real_of_int i * real_of_int j" "real_of_int (i div j) = real_of_int (floor (real_of_int i / real_of_int j))" "real_of_int (min i j) = min (real_of_int i) (real_of_int j)" "real_of_int (max i j) = max (real_of_int i) (real_of_int j)" "real_of_int (abs i) = abs (real_of_int i)" "real_of_int (i ^ n) = (real_of_int i) ^ n" "real_of_int (numeral a) = real_of_float (numeral a)" "i mod j = i - i div j * j" "i = j \ real_of_int i = real_of_int j" "i \ j \ real_of_int i \ real_of_int j" "i < j \ real_of_int i < real_of_int j" "i \ {j .. k} \ real_of_int i \ {real_of_int j .. real_of_int k}" by (simp_all add: floor_divide_of_int_eq minus_div_mult_eq_mod [symmetric]) lemma approximation_preproc_nat[approximation_preproc]: "real 0 = real_of_float 0" "real 1 = real_of_float 1" "real (i + j) = real i + real j" "real (i - j) = max (real i - real j) 0" "real (i * j) = real i * real j" "real (i div j) = real_of_int (floor (real i / real j))" "real (min i j) = min (real i) (real j)" "real (max i j) = max (real i) (real j)" "real (i ^ n) = (real i) ^ n" "real (numeral a) = real_of_float (numeral a)" "i mod j = i - i div j * j" "n = m \ real n = real m" "n \ m \ real n \ real m" "n < m \ real n < real m" "n \ {m .. l} \ real n \ {real m .. real l}" by (simp_all add: real_div_nat_eq_floor_of_divide minus_div_mult_eq_mod [symmetric]) ML_file \approximation.ML\ method_setup approximation = \ let val free = Args.context -- Args.term >> (fn (_, Free (n, _)) => n | (ctxt, t) => error ("Bad free variable: " ^ Syntax.string_of_term ctxt t)); in Scan.lift Parse.nat -- Scan.optional (Scan.lift (Args.$$$ "splitting" |-- Args.colon) |-- Parse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift Parse.nat)) [] -- Scan.option (Scan.lift (Args.$$$ "taylor" |-- Args.colon) |-- (free |-- Scan.lift (Args.$$$ "=") |-- Scan.lift Parse.nat)) >> (fn ((prec, splitting), taylor) => fn ctxt => SIMPLE_METHOD' (Approximation.approximation_tac prec splitting taylor ctxt)) end \ "real number approximation" section "Quickcheck Generator" lemma approximation_preproc_push_neg[approximation_preproc]: fixes a b::real shows "\ (a < b) \ b \ a" "\ (a \ b) \ b < a" "\ (a = b) \ b < a \ a < b" "\ (p \ q) \ \ p \ \ q" "\ (p \ q) \ \ p \ \ q" "\ \ q \ q" by auto ML_file \approximation_generator.ML\ setup "Approximation_Generator.setup" section "Avoid pollution of name space" bundle floatarith_notation begin notation Add ("Add") notation Minus ("Minus") notation Mult ("Mult") notation Inverse ("Inverse") notation Cos ("Cos") notation Arctan ("Arctan") notation Abs ("Abs") notation Max ("Max") notation Min ("Min") notation Pi ("Pi") notation Sqrt ("Sqrt") notation Exp ("Exp") notation Powr ("Powr") notation Ln ("Ln") notation Power ("Power") notation Floor ("Floor") notation Var ("Var") notation Num ("Num") end bundle no_floatarith_notation begin no_notation Add ("Add") no_notation Minus ("Minus") no_notation Mult ("Mult") no_notation Inverse ("Inverse") no_notation Cos ("Cos") no_notation Arctan ("Arctan") no_notation Abs ("Abs") no_notation Max ("Max") no_notation Min ("Min") no_notation Pi ("Pi") no_notation Sqrt ("Sqrt") no_notation Exp ("Exp") no_notation Powr ("Powr") no_notation Ln ("Ln") no_notation Power ("Power") no_notation Floor ("Floor") no_notation Var ("Var") no_notation Num ("Num") end hide_const (open) Add Minus Mult Inverse Cos Arctan Abs Max Min Pi Sqrt Exp Powr Ln Power Floor Var Num end diff --git a/src/HOL/Library/Code_Target_Numeral_Float.thy b/src/HOL/Library/Code_Target_Numeral_Float.thy new file mode 100644 --- /dev/null +++ b/src/HOL/Library/Code_Target_Numeral_Float.thy @@ -0,0 +1,16 @@ +(* Title: HOL/Library/Code_Target_Numeral_Float.thy + Author: Florian Haftmann, TU Muenchen +*) + +section \Preprocessor setup for floats implemented by target language numerals\ + +theory Code_Target_Numeral_Float +imports Float Code_Target_Numeral +begin + +lemma numeral_float_computation_unfold [code_computation_unfold]: + \numeral k = Float (int_of_integer (Code_Numeral.positive k)) 0\ + \- numeral k = Float (int_of_integer (Code_Numeral.negative k)) 0\ + by (simp_all add: Float.compute_float_numeral Float.compute_float_neg_numeral) + +end diff --git a/src/HOL/ROOT b/src/HOL/ROOT --- a/src/HOL/ROOT +++ b/src/HOL/ROOT @@ -1,1208 +1,1209 @@ chapter HOL session HOL (main) = Pure + description " Classical Higher-order Logic. " options [strict_facts] sessions Tools theories Main (global) Complex_Main (global) document_theories Tools.Code_Generator document_files "root.bib" "root.tex" session "HOL-Examples" in Examples = HOL + description " Notable Examples in Isabelle/HOL. " sessions "HOL-Library" theories Adhoc_Overloading_Examples Ackermann Cantor Coherent Commands Drinker Groebner_Examples Iff_Oracle Induction_Schema Knaster_Tarski "ML" Peirce Records Seq document_files "root.bib" "root.tex" session "HOL-Proofs" (timing) in Proofs = Pure + description " HOL-Main with explicit proof terms. " options [quick_and_dirty = false, record_proofs = 2, parallel_limit = 500] sessions "HOL-Library" theories "HOL-Library.Realizers" session "HOL-Library" (main timing) in Library = HOL + description " Classical Higher-order Logic -- batteries included. " theories Library (*conflicting type class instantiations and dependent applications*) Finite_Lattice List_Lexorder List_Lenlexorder Prefix_Order Product_Lexorder Product_Order Subseq_Order (*conflicting syntax*) Datatype_Records (*data refinements and dependent applications*) AList_Mapping Code_Binary_Nat Code_Prolog Code_Real_Approx_By_Float Code_Target_Numeral + Code_Target_Numeral_Float DAList DAList_Multiset RBT_Mapping RBT_Set (*printing modifications*) OptionalSugar (*prototypic tools*) Predicate_Compile_Quickcheck (*legacy tools*) Old_Datatype Old_Recdef Realizers Refute document_files "root.bib" "root.tex" session "HOL-Analysis" (main timing) in Analysis = HOL + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] sessions "HOL-Library" "HOL-Combinatorics" "HOL-Computational_Algebra" theories Analysis document_files "root.tex" "root.bib" session "HOL-Complex_Analysis" (main timing) in Complex_Analysis = "HOL-Analysis" + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] theories Complex_Analysis document_files "root.tex" "root.bib" session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" + theories Approximations Metric_Arith_Examples session "HOL-Homology" (timing) in Homology = "HOL-Analysis" + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] sessions "HOL-Algebra" theories Homology document_files "root.tex" session "HOL-Combinatorics" (main timing) in "Combinatorics" = "HOL" + sessions "HOL-Library" theories Combinatorics Guide document_files "root.tex" session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" + theories Computational_Algebra (*conflicting type class instantiations and dependent applications*) Field_as_Ring session "HOL-Real_Asymp" in Real_Asymp = HOL + sessions "HOL-Decision_Procs" theories Real_Asymp Real_Asymp_Approx Real_Asymp_Examples session "HOL-Real_Asymp-Manual" in "Real_Asymp/Manual" = "HOL-Real_Asymp" + theories Real_Asymp_Doc document_files (in "~~/src/Doc") "iman.sty" "extra.sty" "isar.sty" document_files "root.tex" "style.sty" session "HOL-Hahn_Banach" in Hahn_Banach = HOL + description " Author: Gertrud Bauer, TU Munich The Hahn-Banach theorem for real vector spaces. This is the proof of the Hahn-Banach theorem for real vectorspaces, following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach theorem is one of the fundamental theorems of functional analysis. It is a conclusion of Zorn's lemma. Two different formaulations of the theorem are presented, one for general real vectorspaces and its application to normed vectorspaces. The theorem says, that every continous linearform, defined on arbitrary subspaces (not only one-dimensional subspaces), can be extended to a continous linearform on the whole vectorspace. " sessions "HOL-Analysis" theories Hahn_Banach document_files "root.bib" "root.tex" session "HOL-Induct" in Induct = HOL + description " Examples of (Co)Inductive Definitions. Comb proves the Church-Rosser theorem for combinators (see http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz). Mutil is the famous Mutilated Chess Board problem (see http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz). PropLog proves the completeness of a formalization of propositional logic (see http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz). Exp demonstrates the use of iterated inductive definitions to reason about mutually recursive relations. " sessions "HOL-Library" theories [quick_and_dirty] Common_Patterns theories Nested_Datatype QuoDataType QuoNestedDataType Term SList ABexp Infinitely_Branching_Tree Ordinals Sigma_Algebra Comb PropLog Com document_files "root.tex" session "HOL-IMP" (timing) in IMP = "HOL-Library" + options [document_variants = document] theories BExp ASM Finite_Reachable Denotational Compiler2 Poly_Types Sec_Typing Sec_TypingT Def_Init_Big Def_Init_Small Fold Live Live_True Hoare_Examples Hoare_Sound_Complete VCG Hoare_Total VCG_Total_EX VCG_Total_EX2 Collecting1 Collecting_Examples Abs_Int_Tests Abs_Int1_parity Abs_Int1_const Abs_Int3 Procs_Dyn_Vars_Dyn Procs_Stat_Vars_Dyn Procs_Stat_Vars_Stat C_like OO document_files "root.bib" "root.tex" session "HOL-IMPP" in IMPP = HOL + description \ Author: David von Oheimb Copyright 1999 TUM IMPP -- An imperative language with procedures. This is an extension of IMP with local variables and mutually recursive procedures. For documentation see "Hoare Logic for Mutual Recursion and Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html). \ theories EvenOdd session "HOL-Data_Structures" (timing) in Data_Structures = HOL + options [document_variants = document] sessions "HOL-Number_Theory" theories [document = false] Less_False theories Sorting Balance Tree_Map Interval_Tree AVL_Map AVL_Bal_Set AVL_Bal2_Set Height_Balanced_Tree RBT_Set2 RBT_Map Tree23_Map Tree23_of_List Tree234_Map Brother12_Map AA_Map Set2_Join_RBT Array_Braun Trie_Fun Trie_Map Tries_Binary Queue_2Lists Heaps Leftist_Heap Binomial_Heap Selection document_files "root.tex" "root.bib" session "HOL-Import" in Import = HOL + theories HOL_Light_Maps theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import session "HOL-Number_Theory" (main timing) in Number_Theory = "HOL-Computational_Algebra" + description " Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity. " sessions "HOL-Algebra" theories Number_Theory document_files "root.tex" session "HOL-Hoare" in Hoare = HOL + description " Verification of imperative programs (verification conditions are generated automatically from pre/post conditions and loop invariants). " theories Examples ExamplesAbort ExamplesTC Pointers0 Pointer_Examples Pointer_ExamplesAbort SchorrWaite Separation document_files "root.bib" "root.tex" session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL + description " Verification of shared-variable imperative programs a la Owicki-Gries. (verification conditions are generated automatically). " theories Hoare_Parallel document_files "root.bib" "root.tex" session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" + sessions "HOL-Number_Theory" "HOL-Data_Structures" "HOL-Examples" theories Generate Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures Code_Lazy_Test Code_Test_PolyML Code_Test_Scala theories [condition = ISABELLE_GHC] Code_Test_GHC theories [condition = ISABELLE_MLTON] Code_Test_MLton theories [condition = ISABELLE_OCAMLFIND] Code_Test_OCaml theories [condition = ISABELLE_SMLNJ] Code_Test_SMLNJ session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" + description " Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Testing Metis and Sledgehammer. " sessions "HOL-Decision_Procs" theories Abstraction Big_O Binary_Tree Clausification Message Proxies Tarski Trans_Closure Sets session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL + description " Author: Jasmin Blanchette, TU Muenchen Copyright 2009 " options [kodkod_scala] sessions "HOL-Library" theories [quick_and_dirty] Nitpick_Examples session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" + description " Author: Clemens Ballarin, started 24 September 1999, and many others The Isabelle Algebraic Library. " sessions "HOL-Cardinals" "HOL-Combinatorics" theories (* Orders and Lattices *) Galois_Connection (* Knaster-Tarski theorem and Galois connections *) (* Groups *) FiniteProduct (* Product operator for commutative groups *) Sylow (* Sylow's theorem *) Bij (* Automorphism Groups *) Multiplicative_Group Zassenhaus (* The Zassenhaus lemma *) (* Rings *) Divisibility (* Rings *) IntRing (* Ideals and residue classes *) UnivPoly (* Polynomials *) (* Main theory *) Algebra document_files "root.bib" "root.tex" session "HOL-Auth" (timing) in Auth = HOL + description " A new approach to verifying authentication protocols. " sessions "HOL-Library" directories "Smartcard" "Guard" theories Auth_Shared Auth_Public "Smartcard/Auth_Smartcard" "Guard/Auth_Guard_Shared" "Guard/Auth_Guard_Public" document_files "root.tex" session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" + description " Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge Verifying security protocols using Chandy and Misra's UNITY formalism. " directories "Simple" "Comp" theories (*Basic meta-theory*) UNITY_Main (*Simple examples: no composition*) "Simple/Deadlock" "Simple/Common" "Simple/Network" "Simple/Token" "Simple/Channel" "Simple/Lift" "Simple/Mutex" "Simple/Reach" "Simple/Reachability" (*Verifying security protocols using UNITY*) "Simple/NSP_Bad" (*Example of composition*) "Comp/Handshake" (*Universal properties examples*) "Comp/Counter" "Comp/Counterc" "Comp/Priority" "Comp/TimerArray" "Comp/Progress" "Comp/Alloc" "Comp/AllocImpl" "Comp/Client" (*obsolete*) ELT document_files "root.tex" session "HOL-Unix" in Unix = HOL + options [print_mode = "no_brackets,no_type_brackets"] sessions "HOL-Library" theories Unix document_files "root.bib" "root.tex" session "HOL-ZF" in ZF = HOL + sessions "HOL-Library" theories MainZF Games document_files "root.tex" session "HOL-Imperative_HOL" (timing) in Imperative_HOL = HOL + options [print_mode = "iff,no_brackets"] sessions "HOL-Library" directories "ex" theories Imperative_HOL_ex document_files "root.bib" "root.tex" session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" + description " Various decision procedures, typically involving reflection. " directories "ex" theories Decision_Procs session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + sessions "HOL-Examples" theories Hilbert_Classical Proof_Terms XML_Data session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" + description " Examples for program extraction in Higher-Order Logic. " options [quick_and_dirty = false] sessions "HOL-Computational_Algebra" theories Greatest_Common_Divisor Warshall Higman_Extraction Pigeonhole Euclid document_files "root.bib" "root.tex" session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" + description \ Lambda Calculus in de Bruijn's Notation. This session defines lambda-calculus terms with de Bruijn indixes and proves confluence of beta, eta and beta+eta. The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html). \ options [print_mode = "no_brackets", quick_and_dirty = false] sessions "HOL-Library" theories Eta StrongNorm Standardization WeakNorm document_files "root.bib" "root.tex" session "HOL-Prolog" in Prolog = HOL + description " Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) A bare-bones implementation of Lambda-Prolog. This is a simple exploratory implementation of Lambda-Prolog in HOL, including some minimal examples (in Test.thy) and a more typical example of a little functional language and its type system. " theories Test Type session "HOL-MicroJava" (timing) in MicroJava = HOL + description " Formalization of a fragment of Java, together with a corresponding virtual machine and a specification of its bytecode verifier and a lightweight bytecode verifier, including proofs of type-safety. " sessions "HOL-Library" "HOL-Eisbach" directories "BV" "Comp" "DFA" "J" "JVM" theories MicroJava document_files "introduction.tex" "root.bib" "root.tex" session "HOL-NanoJava" in NanoJava = HOL + description " Hoare Logic for a tiny fragment of Java. " theories Example document_files "root.bib" "root.tex" session "HOL-Bali" (timing) in Bali = HOL + sessions "HOL-Library" theories AxExample AxSound AxCompl Trans TypeSafe document_files "root.tex" session "HOL-IOA" in IOA = HOL + description \ Author: Tobias Nipkow and Konrad Slind and Olaf Müller Copyright 1994--1996 TU Muenchen The meta-theory of I/O-Automata in HOL. This formalization has been significantly changed and extended, see HOLCF/IOA. There are also the proofs of two communication protocols which formerly have been here. @inproceedings{Nipkow-Slind-IOA, author={Tobias Nipkow and Konrad Slind}, title={{I/O} Automata in {Isabelle/HOL}}, booktitle={Proc.\ TYPES Workshop 1994}, publisher=Springer, series=LNCS, note={To appear}} ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz and @inproceedings{Mueller-Nipkow, author={Olaf M\"uller and Tobias Nipkow}, title={Combining Model Checking and Deduction for {I/O}-Automata}, booktitle={Proc.\ TACAS Workshop}, organization={Aarhus University, BRICS report}, year=1995} ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz \ theories Solve session "HOL-Lattice" in Lattice = HOL + description " Author: Markus Wenzel, TU Muenchen Basic theory of lattices and orders. " theories CompleteLattice document_files "root.tex" session "HOL-ex" (timing) in ex = "HOL-Number_Theory" + description " Miscellaneous examples for Higher-Order Logic. " theories Antiquote Argo_Examples Arith_Examples Ballot BinEx Birthday_Paradox Bit_Lists Bubblesort CTL Cartouche_Examples Case_Product Chinese Classical Code_Binary_Nat_examples Code_Lazy_Demo Code_Timing Coercion_Examples Computations Conditional_Parametricity_Examples Cubic_Quartic Datatype_Record_Examples Dedekind_Real Erdoes_Szekeres Eval_Examples Executable_Relation Execute_Choice Functions Function_Growth Gauge_Integration Guess HarmonicSeries Hebrew Hex_Bin_Examples IArray_Examples Intuitionistic Join_Theory Lagrange List_to_Set_Comprehension_Examples LocaleTest2 MergeSort MonoidGroup Multiquote NatSum Normalization_by_Evaluation PER Parallel_Example Peano_Axioms Perm_Fragments PresburgerEx Primrec Pythagoras Quicksort Radix_Sort Reflection_Examples Refute_Examples Residue_Ring Rewrite_Examples SOS SOS_Cert Serbian Set_Comprehension_Pointfree_Examples Set_Theory Simproc_Tests Simps_Case_Conv_Examples Sketch_and_Explore Sorting_Algorithms_Examples Specifications_with_bundle_mixins Sqrt Sqrt_Script Sudoku Sum_of_Powers Tarski Termination ThreeDivides Transfer_Debug Transfer_Int_Nat Transitive_Closure_Table_Ex Tree23 Triangular_Numbers Unification While_Combinator_Example veriT_Preprocessing theories [skip_proofs = false] SAT_Examples Meson_Test session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" + description " Miscellaneous Isabelle/Isar examples. " options [quick_and_dirty] sessions "HOL-Hoare" theories Structured_Statements Basic_Logic Expr_Compiler Fibonacci Group Group_Context Group_Notepad Hoare_Ex Mutilated_Checkerboard Puzzle Summation document_files "root.bib" "root.tex" session "HOL-Eisbach" in Eisbach = HOL + description \ The Eisbach proof method language and "match" method. \ sessions FOL "HOL-Analysis" theories Eisbach Tests Examples Examples_FOL Example_Metric session "HOL-SET_Protocol" (timing) in SET_Protocol = HOL + description " Verification of the SET Protocol. " sessions "HOL-Library" theories SET_Protocol document_files "root.tex" session "HOL-Matrix_LP" in Matrix_LP = HOL + description " Two-dimensional matrices and linear programming. " sessions "HOL-Library" directories "Compute_Oracle" theories Cplex document_files "root.tex" session "HOL-TLA" in TLA = HOL + description " Lamport's Temporal Logic of Actions. " theories TLA session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" + theories Inc session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" + theories DBuffer session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" + theories MemoryImplementation session "HOL-TPTP" in TPTP = HOL + description " Author: Jasmin Blanchette, TU Muenchen Author: Nik Sultana, University of Cambridge Copyright 2011 TPTP-related extensions. " sessions "HOL-Library" theories ATP_Theory_Export MaSh_Eval TPTP_Interpret THF_Arith TPTP_Proof_Reconstruction theories ATP_Problem_Import session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" + sessions "HOL-Combinatorics" theories Probability document_files "root.tex" session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" + theories Dining_Cryptographers Koepf_Duermuth_Countermeasure Measure_Not_CCC session "HOL-Nominal" in Nominal = HOL + sessions "HOL-Library" theories Nominal session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" + theories Class3 CK_Machine Compile Contexts Crary CR_Takahashi CR Fsub Height Lambda_mu Lam_Funs LocalWeakening Pattern SN SOS Standardization Support Type_Preservation Weakening W theories [quick_and_dirty] VC_Condition session "HOL-Cardinals" (timing) in Cardinals = HOL + description " Ordinals and Cardinals, Full Theories. " theories Cardinals Bounded_Set document_files "intro.tex" "root.tex" "root.bib" session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" + description " (Co)datatype Examples. " directories "Derivation_Trees" theories Compat Lambda_Term Process TreeFsetI "Derivation_Trees/Gram_Lang" "Derivation_Trees/Parallel_Composition" Koenig Lift_BNF Milner_Tofte Stream_Processor Cyclic_List Free_Idempotent_Monoid Regex_ACI Regex_ACIDZ TLList FAE_Sequence Misc_Codatatype Misc_Datatype Misc_Primcorec Misc_Primrec Datatype_Simproc_Tests session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" + description " Corecursion Examples. " directories "Tests" theories LFilter Paper_Examples Stream_Processor "Tests/Simple_Nesting" "Tests/Iterate_GPV" theories [quick_and_dirty] "Tests/GPV_Bare_Bones" "Tests/Merge_D" "Tests/Merge_Poly" "Tests/Misc_Mono" "Tests/Misc_Poly" "Tests/Small_Concrete" "Tests/Stream_Friends" "Tests/TLList_Friends" "Tests/Type_Class" session "HOL-Statespace" in Statespace = HOL + theories [skip_proofs = false] StateSpaceEx document_files "root.tex" session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" + description " Nonstandard analysis. " theories Nonstandard_Analysis document_files "root.tex" session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" + theories NSPrimes session "HOL-Mirabelle" in Mirabelle = HOL + theories Mirabelle_Test session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" + options [timeout = 60] theories Ex session "HOL-SMT_Examples" (timing) in SMT_Examples = HOL + options [quick_and_dirty] sessions "HOL-Library" theories Boogie SMT_Examples SMT_Word_Examples SMT_Tests SMT_Tests_Verit SMT_Examples_Verit session "HOL-SPARK" in "SPARK" = HOL + sessions "HOL-Library" theories SPARK session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" + directories "Gcd" "Liseq" "RIPEMD-160" "Sqrt" theories "Gcd/Greatest_Common_Divisor" "Liseq/Longest_Increasing_Subsequence" "RIPEMD-160/F" "RIPEMD-160/Hash" "RIPEMD-160/K_L" "RIPEMD-160/K_R" "RIPEMD-160/R_L" "RIPEMD-160/Round" "RIPEMD-160/R_R" "RIPEMD-160/S_L" "RIPEMD-160/S_R" "Sqrt/Sqrt" export_files (in ".") "*:**.prv" session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" + options [show_question_marks = false] sessions "HOL-Library" "HOL-SPARK-Examples" theories Example_Verification VC_Principles Reference Complex_Types document_theories "HOL-SPARK-Examples.Greatest_Common_Divisor" document_files "complex_types.ads" "complex_types_app.adb" "complex_types_app.ads" "Gcd.adb" "Gcd.ads" "intro.tex" "loop_invariant.adb" "loop_invariant.ads" "root.bib" "root.tex" "Simple_Gcd.adb" "Simple_Gcd.ads" session "HOL-Mutabelle" in Mutabelle = HOL + sessions "HOL-Library" theories MutabelleExtra session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = HOL + sessions "HOL-Library" theories Quickcheck_Examples Quickcheck_Lattice_Examples Completeness Quickcheck_Interfaces Quickcheck_Nesting_Example theories [condition = ISABELLE_GHC] Hotel_Example Quickcheck_Narrowing_Examples session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" + description " Author: Cezary Kaliszyk and Christian Urban " theories DList Quotient_FSet Quotient_Int Quotient_Message Lift_FSet Lift_Set Lift_Fun Quotient_Rat Lift_DList Int_Pow Lifting_Code_Dt_Test session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = HOL + sessions "HOL-Library" theories Examples Predicate_Compile_Tests Predicate_Compile_Quickcheck_Examples Specialisation_Examples IMP_1 IMP_2 (* FIXME since 21-Jul-2011 Hotel_Example_Small_Generator *) IMP_3 IMP_4 theories [condition = ISABELLE_SWIPL] Code_Prolog_Examples Context_Free_Grammar_Example Hotel_Example_Prolog Lambda_Example List_Examples theories [condition = ISABELLE_SWIPL, quick_and_dirty] Reg_Exp_Example session "HOL-Types_To_Sets" in Types_To_Sets = HOL + description " Experimental extension of Higher-Order Logic to allow translation of types to sets. " directories "Examples" theories Types_To_Sets "Examples/Prerequisites" "Examples/Finite" "Examples/T2_Spaces" "Examples/Unoverload_Def" "Examples/Linear_Algebra_On" session HOLCF (main timing) in HOLCF = HOL + description " Author: Franz Regensburger Author: Brian Huffman HOLCF -- a semantic extension of HOL by the LCF logic. " sessions "HOL-Library" theories HOLCF (global) document_files "root.tex" session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF + theories Domain_ex Fixrec_ex New_Domain document_files "root.tex" session "HOLCF-Library" in "HOLCF/Library" = HOLCF + theories HOLCF_Library HOL_Cpo session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF + description " IMP -- A WHILE-language and its Semantics. This is the HOLCF-based denotational semantics of a simple WHILE-language. " sessions "HOL-IMP" theories HoareEx document_files "isaverbatimwrite.sty" "root.tex" "root.bib" session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" + description " Miscellaneous examples for HOLCF. " theories Dnat Dagstuhl Focus_ex Fix2 Hoare Concurrency_Monad Loop Powerdomain_ex Domain_Proofs Letrec Pattern_Match session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" + description \ FOCUS: a theory of stream-processing functions Isabelle/HOLCF. For introductions to FOCUS, see "The Design of Distributed Systems - An Introduction to FOCUS" http://www4.in.tum.de/publ/html.php?e=2 "Specification and Refinement of a Buffer of Length One" http://www4.in.tum.de/publ/html.php?e=15 "Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321 \ theories Fstreams FOCUS Buffer_adm session IOA (timing) in "HOLCF/IOA" = HOLCF + description " Author: Olaf Müller Copyright 1997 TU München A formalization of I/O automata in HOLCF. The distribution contains simulation relations, temporal logic, and an abstraction theory. Everything is based upon a domain-theoretic model of finite and infinite sequences. " theories Abstraction session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA + description " Author: Olaf Müller The Alternating Bit Protocol performed in I/O-Automata: combining IOA with Model Checking. Theory Correctness contains the proof of the abstraction from unbounded channels to finite ones. File Check.ML contains a simple ModelChecker prototype checking Spec against the finite version of the ABP-protocol. " theories Correctness Spec session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA + description " Author: Tobias Nipkow & Konrad Slind A network transmission protocol, performed in the I/O automata formalization by Olaf Müller. " theories Overview Correctness session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA + description " Author: Olaf Müller Memory storage case study. " theories Correctness session "IOA-ex" in "HOLCF/IOA/ex" = IOA + description " Author: Olaf Müller " theories TrivEx TrivEx2