diff --git a/thys/Gauss_Jordan/Code_Rational.thy b/thys/Gauss_Jordan/Code_Rational.thy --- a/thys/Gauss_Jordan/Code_Rational.thy +++ b/thys/Gauss_Jordan/Code_Rational.thy @@ -1,139 +1,138 @@ (* Title: Code_Rational.thy Author: Jose Divasón Author: Jesús Aransay *) section\Code Generation for rational numbers in Haskell\ theory Code_Rational imports (*VERY IMPORTANT! When code is exported, the order of the imports is very important. In this case, I have to import here the following three theories. They allow the computation of the Gauss-Jordan algorithm in Haskell*) - Code_Real_Approx_By_Float_Haskell + "HOL-Library.Code_Real_Approx_By_Float" Code_Generation_IArrays (*These theories are necessary for the serialisation:*) - HOL.Rat "HOL-Library.Code_Target_Int" begin subsection\Serializations\ text\The following \code_printing code_module\ module is the usual way to import libraries in Haskell. In this case, we rebind some functions from Data.Ratio. See @{url "https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-June/msg00007.html"}\ code_printing code_module Rational \ (Haskell) \module Rational(fract, numerator, denominator) where import qualified Data.Ratio import Data.Ratio(numerator, denominator) fract (a, b) = a Data.Ratio.% b\ context includes integer.lifting begin lift_definition Frct_integer :: "integer \ integer => rat" is "Frct :: int \ int => rat" . end consts Foo::rat code_datatype Foo context includes integer.lifting begin lemma [code]: "Frct a = Frct_integer ((of_int (fst a)), (of_int (snd a)))" by (transfer, simp) lemma [code]: "Rat.of_int a = Frct_integer (of_int a, 1)" by transfer (auto simp: Fract_of_int_eq Rat.of_int_def) definition numerator :: "rat => int" where "numerator x = fst (quotient_of x)" definition denominator :: "rat => int" where "denominator x = snd (quotient_of x)" lift_definition numerator_integer :: "rat => integer" is "numerator" . lift_definition denominator_integer :: "rat => integer" is "denominator" . lemma [code]: "inverse x = Frct_integer (denominator_integer x, numerator_integer x)" apply (cases x) apply transfer apply (auto simp: inverse_eq_divide numerator_def denominator_def quotient_of_Fract One_rat_def) done lemma quotient_of_num_den: "quotient_of x = ((numerator x), (denominator x))" unfolding numerator_def denominator_def by simp lemma [code]: "quotient_of x = (int_of_integer (numerator_integer x), int_of_integer(denominator_integer x))" by (transfer, simp add: quotient_of_num_den) end code_printing type_constructor rat \ (Haskell) "Prelude.Rational" | class_instance rat :: "HOL.equal" => (Haskell) - | constant "0 :: rat" \ (Haskell) "(Prelude.toRational (0::Integer))" | constant "1 :: rat" \ (Haskell) "(Prelude.toRational (1::Integer))" | constant "Frct_integer" \ (Haskell) "Rational.fract (_)" | constant "numerator_integer" \ (Haskell) "Rational.numerator (_)" | constant "denominator_integer" \ (Haskell) "Rational.denominator (_)" | constant "HOL.equal :: rat \ rat \ bool" \ (Haskell) "(_) == (_)" | constant "(<) :: rat => rat => bool" \ (Haskell) "_ < _" | constant "(\) :: rat => rat => bool" \ (Haskell) "_ <= _" | constant "(+) :: rat \ rat \ rat" \ (Haskell) "(_) + (_)" | constant "(-) :: rat \ rat \ rat" \ (Haskell) "(_) - (_)" | constant "(*) :: rat \ rat \ rat" \ (Haskell) "(_) * (_)" | constant "(/) :: rat \ rat \ rat" \ (Haskell) " (_) '/ (_)" | constant "uminus :: rat => rat" \ (Haskell) "Prelude.negate" (* definition "test1 = (3::rat)" definition "test2 = (3/9::rat)" definition "test3 = (3/8 + 8/7::rat)" definition "test4 = (3/8 - 8/7::rat)" definition "test5 = (3/8 * 8/7::rat)" definition "test6 = (3/8 / 8/7::rat)" definition "test7 = (34 < (53 :: rat))" definition "test8 = (34 <= (53 :: rat))" definition "test9 = (inverse (8/5::rat))" definition "test10 = quotient_of (8/3::rat)" export_code test1 test2 test3 test4 test5 test6 test7 test8 test9 test10 in Haskell module_name "Rational_Haskell" file "haskell" *) end diff --git a/thys/Gauss_Jordan/Code_Real_Approx_By_Float_Haskell.thy b/thys/Gauss_Jordan/Code_Real_Approx_By_Float_Haskell.thy deleted file mode 100644 --- a/thys/Gauss_Jordan/Code_Real_Approx_By_Float_Haskell.thy +++ /dev/null @@ -1,62 +0,0 @@ -(* - Title: Code_Real_Approx_By_Float_Haskell.thy - Author: Jose Divasón - Author: Jesús Aransay -*) - -section\Serialization of real numbers in Haskell\ - -theory Code_Real_Approx_By_Float_Haskell -imports "HOL-Library.Code_Real_Approx_By_Float" -begin - -text\\textbf{WARNING} This theory implements mathematical reals by machine -reals in Haskell, in a similar way to the work done in the theory \Code_Real_Approx_By_Float_Haskell\. -This is inconsistent.\ - -subsection\Implementation of real numbers in Haskell\ - -code_printing - type_constructor real \ (Haskell) "Prelude.Double" (*Double precission*) - | constant "0 :: real" \ (Haskell) "0.0" - | constant "1 :: real" \ (Haskell) "1.0" - | constant "Code_Real_Approx_By_Float.real_of_integer" \ (Haskell) "Prelude.fromIntegral (_)" - | class_instance real :: "HOL.equal" => (Haskell) - (*This is necessary. See the tutorial on code generation, page 29*) - | constant "HOL.equal :: real \ real \ bool" \ - (Haskell) "(_) == (_)" - | constant "(<) :: real => real => bool" \ - (Haskell) "_ < _" - | constant "(\) :: real => real => bool" \ - (Haskell) "_ <= _" - | constant "(+) :: real \ real \ real" \ - (Haskell) "(_) + (_)" - | constant "(-) :: real \ real \ real" \ - (Haskell) "(_) - (_)" - | constant "(*) :: real \ real \ real" \ - (Haskell) "(_) * (_)" - | constant "(/) :: real \ real \ real" \ - (Haskell) " (_) '/ (_)" - | constant "uminus :: real => real" \ - (Haskell) "Prelude.negate" - | constant "sqrt :: real => real" \ - (Haskell) "Prelude.sqrt" - | constant Code_Real_Approx_By_Float.exp_real \ - (Haskell) "Prelude.exp" - | constant ln \ - (Haskell) "Prelude.log" - | constant cos \ - (Haskell) "Prelude.cos" - | constant sin \ - (Haskell) "Prelude.sin" - | constant tan \ - (Haskell) "Prelude.tan" - | constant pi \ - (Haskell) "Prelude.pi" - | constant arctan \ - (Haskell) "Prelude.atan" - | constant arccos \ - (Haskell) "Prelude.acos" - | constant arcsin \ - (Haskell) "Prelude.asin" - -end diff --git a/thys/MDP-Algorithms/code/Code_DP.thy b/thys/MDP-Algorithms/code/Code_DP.thy --- a/thys/MDP-Algorithms/code/Code_DP.thy +++ b/thys/MDP-Algorithms/code/Code_DP.thy @@ -1,526 +1,525 @@ (* Author: Maximilian Schäffeler *) theory Code_DP imports Value_Iteration Policy_Iteration Modified_Policy_Iteration Splitting_Methods - -"HOL-Library.Code_Target_Numeral" -"Gauss_Jordan.Code_Generation_IArrays" + "HOL-Library.Code_Target_Numeral" + "Gauss_Jordan.Code_Generation_IArrays" begin section \Code Generation for MDP Algorithms\ subsection \Least Argmax\ lemma least_list: assumes "sorted xs" "\x \ set xs. P x" shows "(LEAST x \ set xs. P x) = the (find P xs)" using assms proof (induction xs) case (Cons a xs) thus ?case proof (cases "P a") case False have "(LEAST x \ set (a # xs). P x) = (LEAST x \ set xs. P x)" using False Cons(2) by simp metis thus ?thesis using False Cons by simp qed (auto intro: Least_equality) qed auto definition "least_enum P = the (find P (sorted_list_of_set (UNIV :: ('b:: {finite, linorder}) set)))" lemma least_enum_eq: "\x. P x \ least_enum P = (LEAST x. P x)" by (auto simp: least_list[symmetric] least_enum_def) definition "least_max_arg_max_list f init xs = foldl (\(am, m) x. if f x > m then (x, f x) else (am, m)) init xs" lemma snd_least_max_arg_max_list: "snd (least_max_arg_max_list f (n, f n) xs) = (MAX x \ insert n (set xs). f x)" unfolding least_max_arg_max_list_def proof (induction xs arbitrary: n) case (Cons a xs) then show ?case by (cases "xs = []") (fastforce simp: max.assoc[symmetric])+ qed auto lemma least_max_arg_max_list_snd_fst: "snd (least_max_arg_max_list f (x, f x) xs) = f (fst (least_max_arg_max_list f (x, f x) xs))" by (induction xs arbitrary: x) (auto simp: least_max_arg_max_list_def) lemma fst_least_max_arg_max_list: fixes f :: "_ \ _ :: linorder" assumes "sorted (n#xs)" shows "fst (least_max_arg_max_list f (n, f n) xs) = (LEAST x. is_arg_max f (\x. x \ insert n (set xs)) x)" unfolding least_max_arg_max_list_def using assms proof (induction xs arbitrary: n) case Nil then show ?case by (auto simp: is_arg_max_def intro!: Least_equality[symmetric]) next case (Cons a xs) hence "sorted (a#xs)" by auto then show ?case proof (cases "f a > f n") case True then show ?thesis by (fastforce simp: is_arg_max_def Cons.IH[OF \sorted (a#xs)\] intro!: cong[of Least, OF refl]) next case False have "(LEAST b. is_arg_max f (\x. x \ insert n (set (a # xs))) b) = (LEAST b. is_arg_max f (\x. x \ (set (n # xs))) b)" proof (cases "is_arg_max f (\x. x \ set (n #a# xs)) a") case True hence "(LEAST b. is_arg_max f (\x. x \ (set (n#a # xs))) b) = n" using Cons False by (fastforce simp: is_arg_max_linorder intro!: Least_equality) thus ?thesis using False True Cons by (fastforce simp: is_arg_max_linorder intro!: Least_equality[symmetric]) next case False thus ?thesis by (fastforce simp: not_less is_arg_max_linorder intro!: cong[of Least, OF refl]) qed thus ?thesis using False Cons by (auto simp add: Cons.IH[OF \sorted (a#xs)\]) qed qed definition "least_arg_max_enum f X = ( let xs = sorted_list_of_set (X :: (_ :: {finite, linorder}) set) in fst (least_max_arg_max_list f (hd xs, f (hd xs)) (tl xs)))" definition "least_max_arg_max_enum f X = ( let xs = sorted_list_of_set (X :: (_ :: {finite, linorder}) set) in (least_max_arg_max_list f (hd xs, f (hd xs)) (tl xs)))" lemma least_arg_max_enum_correct: assumes "X \ {}" shows " (least_arg_max_enum (f :: _ \ (_ :: linorder)) X) = (LEAST x. is_arg_max f (\x. x \ X) x)" proof - have *: "xs \ [] \ (x = hd xs \ x \ set (tl xs)) \ x \ set xs" for x xs using list.set_sel list.exhaust_sel set_ConsD by metis thus ?thesis unfolding least_arg_max_enum_def using assms by (auto simp: Let_def fst_least_max_arg_max_list *) qed lemma least_max_arg_max_enum_correct1: assumes "X \ {}" shows "fst (least_max_arg_max_enum (f :: _ \ (_ :: linorder)) X) = (LEAST x. is_arg_max f (\x. x \ X) x)" proof - have *: "xs \ [] \ (x = hd xs \ x \ set (tl xs)) \ x \ set xs" for x xs using list.set_sel list.exhaust_sel set_ConsD by metis thus ?thesis using assms by (auto simp: least_max_arg_max_enum_def Let_def fst_least_max_arg_max_list *) qed lemma least_max_arg_max_enum_correct2: assumes "X \ {}" shows "snd (least_max_arg_max_enum (f :: _ \ (_ :: linorder)) X) = (MAX x \ X. f x)" proof - have *: "xs \ [] \ insert (hd xs) (set (tl xs)) = set xs" for xs using list.exhaust_sel list.simps(15) by metis show ?thesis using assms by (auto simp: least_max_arg_max_enum_def Let_def snd_least_max_arg_max_list *) qed subsection \Functions as Vectors\ typedef ('a, 'b) Fun = "UNIV :: ('a \ 'b) set" by blast setup_lifting type_definition_Fun lift_definition to_Fun :: "('a \ 'b) \ ('a, 'b) Fun" is id. definition "fun_to_vec (v :: ('a::finite, 'b) Fun) = vec_lambda (Rep_Fun v)" lift_definition vec_to_fun :: "'b^'a \ ('a, 'b) Fun" is vec_nth. lemma Fun_inverse[simp]: "Rep_Fun (Abs_Fun f) = f" using Abs_Fun_inverse by auto lift_definition zero_Fun :: "('a, 'b::zero) Fun" is 0. code_datatype vec_to_fun lemmas vec_to_fun.rep_eq[code] instantiation Fun :: (enum, equal) equal begin definition "equal_Fun (f :: ('a::enum, 'b::equal) Fun) g = (Rep_Fun f = Rep_Fun g)" instance by standard (auto simp: equal_Fun_def Rep_Fun_inject) end subsection \Bounded Functions as Vectors\ lemma Bfun_inverse_fin[simp]: "apply_bfun (Bfun (f :: 'c :: finite \ _)) = f" using finite by (fastforce intro!: Bfun_inverse simp: bfun_def) definition "bfun_to_vec (v :: ('a::finite) \\<^sub>b ('b::metric_space)) = vec_lambda v" definition "vec_to_bfun v = Bfun (vec_nth v)" code_datatype vec_to_bfun lemma apply_bfun_vec_to_bfun[code]: "apply_bfun (vec_to_bfun f) x = f $ x" by (auto simp: vec_to_bfun_def) lemma [code]: "0 = vec_to_bfun 0" by (auto simp: vec_to_bfun_def) subsection \IArrays with Lengths in the Type\ typedef ('s :: mod_type, 'a) iarray_type = "{arr :: 'a iarray. IArray.length arr = CARD('s)}" using someI_ex[OF Ex_list_of_length] by (auto intro!: exI[of _ "IArray (SOME xs. length xs = CARD('s))"]) setup_lifting type_definition_iarray_type lift_definition fun_to_iarray_t :: "('s::{mod_type} \ 'a) \ ('s, 'a) iarray_type" is "\f. IArray.of_fun (\s. f (from_nat s)) (CARD('s))" by auto lift_definition iarray_t_sub :: "('s::mod_type, 'a) iarray_type \ 's \ 'a" is "\v x. IArray.sub v (to_nat x)". lift_definition iarray_to_vec :: "('s, 'a) iarray_type \ 'a^'s::{mod_type, finite}" is "\v. (\ s. IArray.sub v (to_nat s))". lift_definition vec_to_iarray :: "'a^'s::{mod_type, finite} \ ('s, 'a) iarray_type" is "\v. IArray.of_fun (\s. v $ ((from_nat s) :: 's)) (CARD('s))" by auto lemma length_iarray_type [simp]: "length (IArray.list_of (Rep_iarray_type (v:: ('s::{mod_type}, 'a) iarray_type))) = CARD('s)" using Rep_iarray_type by auto lemma iarray_t_eq_iff: "(v = w) = (\x. iarray_t_sub v x = iarray_t_sub w x)" unfolding iarray_t_sub.rep_eq IArray.sub_def by (metis Rep_iarray_type_inject iarray_exhaust2 length_iarray_type list_eq_iff_nth_eq to_nat_from_nat_id) lemma iarray_to_vec_inv: "iarray_to_vec (vec_to_iarray v) = v" by (auto simp: to_nat_less_card iarray_to_vec.rep_eq vec_to_iarray.rep_eq vec_eq_iff) lemma vec_to_iarray_inv: "vec_to_iarray (iarray_to_vec v) = v" by (auto simp: to_nat_less_card iarray_to_vec.rep_eq vec_to_iarray.rep_eq iarray_t_eq_iff iarray_t_sub.rep_eq) code_datatype iarray_to_vec lemma vec_nth_iarray_to_vec[code]: "vec_nth (iarray_to_vec v) x = iarray_t_sub v x" by (auto simp: iarray_to_vec.rep_eq iarray_t_sub.rep_eq) lemma vec_lambda_iarray_t[code]: "vec_lambda v = iarray_to_vec (fun_to_iarray_t v)" by (auto simp: iarray_to_vec.rep_eq fun_to_iarray_t.rep_eq to_nat_less_card) lemma zero_iarray[code]: "0 = iarray_to_vec (fun_to_iarray_t 0)" by (auto simp: iarray_to_vec.rep_eq fun_to_iarray_t.rep_eq to_nat_less_card vec_eq_iff) subsection \Value Iteration\ locale vi_code = MDP_ord A K r l for A :: "'s::mod_type \ ('a::{finite, wellorder}) set" and K :: "('s::{finite, mod_type} \ 'a::{finite, wellorder}) \ 's pmf" and r l begin definition "vi_test (v::'s\\<^sub>b real) v' eps = 2 * l * dist v v'" partial_function (tailrec) value_iteration_partial where [code]: "value_iteration_partial eps v = (let v' = \\<^sub>b v in (if 2 * l * dist v v' < eps * (1 - l) then v' else (value_iteration_partial eps v')))" lemma vi_eq_partial: "eps > 0 \ value_iteration_partial eps v = value_iteration eps v" proof (induction eps v rule: value_iteration.induct) case (1 eps v) then show ?case by (auto simp: Let_def value_iteration.simps value_iteration_partial.simps) qed definition "L_det d = L (mk_dec_det d)" lemma code_L_det [code]: "L_det d (vec_to_bfun v) = vec_to_bfun (\ s. L\<^sub>a (d s) (vec_nth v) s)" by (auto simp: L_det_def vec_to_bfun_def L_eq_L\<^sub>a_det) lemma code_\\<^sub>b [code]: "\\<^sub>b (vec_to_bfun v) = vec_to_bfun (\ s. (MAX a \ A s. r (s, a) + l * measure_pmf.expectation (K (s, a)) (vec_nth v)))" by (auto simp: vec_to_bfun_def \\<^sub>b_fin_eq_det A_ne cSup_eq_Max) lemma code_value_iteration[code]: "value_iteration eps (vec_to_bfun v) = (if eps \ 0 then \\<^sub>b (vec_to_bfun v) else value_iteration_partial eps (vec_to_bfun v))" by (simp add: value_iteration.simps vi_eq_partial) lift_definition find_policy_impl :: "('s \\<^sub>b real) \ ('s, 'a) Fun" is "\v. find_policy' v". lemma code_find_policy_impl: "find_policy_impl v = vec_to_fun (\ s. (LEAST x. x \ opt_acts v s))" by (auto simp: vec_to_fun_def find_policy_impl_def find_policy'_def Abs_Fun_inject) lemma code_find_policy_impl_opt[code]: "find_policy_impl v = vec_to_fun (\ s. least_arg_max_enum (\a. L\<^sub>a a v s) (A s))" by (auto simp: is_opt_act_def code_find_policy_impl least_arg_max_enum_correct[OF A_ne]) lemma code_vi_policy'[code]: "vi_policy' eps v = Rep_Fun (find_policy_impl (value_iteration eps v))" unfolding vi_policy'_def find_policy_impl_def by auto subsection \Policy Iteration\ partial_function (tailrec) policy_iteration_partial where [code]: "policy_iteration_partial d = (let d' = policy_step d in if d = d' then d else policy_iteration_partial d')" lemma pi_eq_partial: "d \ D\<^sub>D \ policy_iteration_partial d = policy_iteration d" proof (induction d rule: policy_iteration.induct) case (1 d) then show ?case by (auto simp: Let_def is_dec_det_pi policy_step_def policy_iteration_partial.simps) qed definition "P_mat d = (\ i j. pmf (K (i, Rep_Fun d i)) j)" definition "r_vec' d = (\ i. r(i, Rep_Fun d i))" lift_definition policy_eval' :: "('s::{mod_type, finite}, 'a) Fun \ ('s \\<^sub>b real)" is "policy_eval". lemma mat_eq_blinfun: "mat 1 - l *\<^sub>R (P_mat (vec_to_fun d)) = blinfun_to_matrix (id_blinfun - l *\<^sub>R \

\<^sub>1 (mk_dec_det (vec_nth d)))" unfolding blinfun_to_matrix_diff blinfun_to_matrix_id blinfun_to_matrix_scaleR unfolding blinfun_to_matrix_def P_mat_def \

\<^sub>1.rep_eq K_st_def push_exp_def matrix_def axis_def vec_to_fun_def by (auto simp: if_distrib mk_dec_det_def integral_measure_pmf[of UNIV] pmf_expectation_bind[of UNIV] pmf_bind cong: if_cong) lemma \\<^sub>b_vec: "policy_eval' (vec_to_fun d) = vec_to_bfun (matrix_inv (mat 1 - l *\<^sub>R (P_mat (vec_to_fun d))) *v (r_vec' (vec_to_fun d)))" proof - let ?d = "Rep_Fun (vec_to_fun d)" have "vec_to_bfun (matrix_inv (mat 1 - l *\<^sub>R (P_mat (vec_to_fun d))) *v (r_vec' (vec_to_fun d))) = matrix_to_blinfun (matrix_inv (mat 1 - l *\<^sub>R (P_mat (vec_to_fun d)))) (vec_to_bfun (r_vec' (vec_to_fun d)))" by (auto simp: matrix_to_blinfun_mult vec_to_bfun_def r_vec'_def) also have "\ = matrix_to_blinfun (matrix_inv (blinfun_to_matrix (id_blinfun - l *\<^sub>R \

\<^sub>1 (mk_dec_det ?d)))) (r_dec\<^sub>b (mk_dec_det ?d))" unfolding mat_eq_blinfun by (auto simp: r_vec'_def vec_to_bfun_def vec_lambda_inverse r_dec\<^sub>b_def vec_to_fun_def) also have "\ = inv\<^sub>L (id_blinfun - l *\<^sub>R \

\<^sub>1 (mk_dec_det ?d)) (r_dec\<^sub>b (mk_dec_det ?d))" by (auto simp: blinfun_to_matrix_inverse(2)[symmetric] invertible\<^sub>L_inf_sum matrix_to_blinfun_inv) finally have "vec_to_bfun (matrix_inv (mat 1 - l *\<^sub>R (P_mat (vec_to_fun d))) *v (r_vec' (vec_to_fun d))) = inv\<^sub>L (id_blinfun - l *\<^sub>R \

\<^sub>1 (mk_dec_det ?d)) (r_dec\<^sub>b (mk_dec_det ?d))". thus ?thesis by (auto simp: \_stationary policy_eval'.rep_eq policy_eval_def inv\<^sub>L_inf_sum blincomp_scaleR_right) qed lemma \\<^sub>b_vec_opt[code]: "policy_eval' (vec_to_fun d) = vec_to_bfun (Matrix_To_IArray.iarray_to_vec (Matrix_To_IArray.vec_to_iarray ((fst (Gauss_Jordan_PA ((mat 1 - l *\<^sub>R (P_mat (vec_to_fun d)))))) *v (r_vec' (vec_to_fun d)))))" using \\<^sub>b_vec by (auto simp: mat_eq_blinfun matrix_inv_Gauss_Jordan_PA blinfun_to_matrix_inverse(1) invertible\<^sub>L_inf_sum iarray_to_vec_vec_to_iarray) lift_definition policy_improvement' :: "('s, 'a) Fun \ ('s \\<^sub>b real) \ ('s, 'a) Fun" is policy_improvement. lemma [code]: "policy_improvement' (vec_to_fun d) v = vec_to_fun (\ s. (if is_arg_max (\a. L\<^sub>a a v s) (\a. a \ A s) (d $ s) then d $ s else LEAST x. is_arg_max (\a. L\<^sub>a a v s) (\a. a \ A s) x))" by (auto simp: is_opt_act_def policy_improvement'_def vec_to_fun_def vec_lambda_inverse policy_improvement_def Abs_Fun_inject) lift_definition policy_step' :: "('s, 'a) Fun \ ('s, 'a) Fun" is policy_step. lemma [code]: "policy_step' d = policy_improvement' d (policy_eval' d)" by (auto simp: policy_step'_def policy_step_def policy_improvement'_def policy_eval'_def apply_bfun_inverse) lift_definition policy_iteration_partial' :: "('s, 'a) Fun \ ('s, 'a) Fun" is policy_iteration_partial. lemma [code]: "policy_iteration_partial' d = (let d' = policy_step' d in if d = d' then d else policy_iteration_partial' d')" by (auto simp: policy_iteration_partial'.rep_eq policy_step'.rep_eq Let_def policy_iteration_partial.simps Rep_Fun_inject[symmetric]) lift_definition policy_iteration' :: "('s, 'a) Fun \ ('s, 'a) Fun" is policy_iteration. lemma code_policy_iteration'[code]: "policy_iteration' d = (if Rep_Fun d \ D\<^sub>D then d else (policy_iteration_partial' d))" by transfer (auto simp: pi_eq_partial) lemma code_policy_iteration[code]: "policy_iteration d = Rep_Fun (policy_iteration' (vec_to_fun (vec_lambda d)))" by (auto simp add: vec_lambda_inverse policy_iteration'.rep_eq vec_to_fun_def) subsection \Gauss-Seidel Iteration\ partial_function (tailrec) gs_iteration_partial where [code]: "gs_iteration_partial eps v = ( let v' = (GS_rec_fun\<^sub>b v) in (if 2 * l * dist v v' < eps * (1 - l) then v' else gs_iteration_partial eps v'))" lemma gs_iteration_partial_eq: "eps > 0 \ gs_iteration_partial eps v = gs_iteration eps v" by (induction eps v rule: gs_iteration.induct) (auto simp: gs_iteration_partial.simps Let_def gs_iteration.simps) lemma gs_iteration_code_opt[code]: "gs_iteration eps v = (if eps \ 0 then GS_rec_fun\<^sub>b v else gs_iteration_partial eps v)" by (auto simp: gs_iteration_partial_eq gs_iteration.simps) definition "vec_upd v i x = (\ j. if i = j then x else v $ j)" lemma GS_rec_eq_fold: "GS_rec v = foldl (\v s. (vec_upd v s (GS_iter_max v s))) v (sorted_list_of_set UNIV)" proof - have "vec_lambda (foldl (\v s. v(s := GS_rec_iter v s)) (($) v) xs) = foldl (\v s. vec_upd v s (GS_iter_max v s)) v xs" for xs proof (induction xs arbitrary: v) case (Cons a xs) show ?case by (auto simp: vec_upd_def[of v] Cons[symmetric] eq_commute GS_rec_iter_eq_iter_max cong: if_cong) qed auto thus ?thesis unfolding GS_rec_def GS_rec_fun_code' by auto qed lemma GS_rec_fun_code''''[code]: "GS_rec_fun\<^sub>b (vec_to_bfun v) = vec_to_bfun (foldl (\v s. (vec_upd v s (GS_iter_max v s))) v (sorted_list_of_set UNIV))" by (auto simp add: GS_rec_eq_fold[symmetric] GS_rec_eq_elem GS_rec_fun\<^sub>b.rep_eq vec_to_bfun_def) lemma GS_iter_max_code [code]: "GS_iter_max v s = (MAX a \ A s. GS_iter a v s)" using A_ne by (auto simp: GS_iter_max_def cSup_eq_Max) lift_definition opt_policy_gs'' :: "('s \\<^sub>b real) \ ('s, 'a) Fun" is opt_policy_gs. declare opt_policy_gs''.rep_eq[symmetric, code] lemma GS_rec_am_code'_prod: "GS_rec_am_code' v d = (\s'. ( let (v', d') = foldl (\(v,d) s. (v(s := (GS_iter_max (vec_lambda v) s)), d(s := GS_iter_arg_max (vec_lambda v) s))) (vec_nth v, d) (sorted_list_of_set UNIV) in (v' s', d' s')))" proof - have 1: "(\x. (f x, g x))(y := (z, w)) = (\x. ((f(y := z)) x, (g(y := w)) x))" for f g y z w by auto have 2: "(($) f)(a := y) = ($) (vec_lambda ((vec_nth f)(a := y)))" for f a y by auto have "foldl (\vd s. vd(s := (GS_iter_max (\ s. fst (vd s)) s, GS_iter_arg_max (\ s. fst (vd s)) s))) (\s. (v $ s, d s)) xs = (\s'. let (v', d') = foldl (\(v, d) s. (v(s := GS_iter_max (vec_lambda v) s), d(s := GS_iter_arg_max (vec_lambda v) s))) (($) v, d) xs in (v' s', d' s'))" for xs proof (induction xs arbitrary: v d) case Nil then show ?case by auto next case (Cons a xs) show ?case by (simp add: 1 Cons.IH[of "(vec_lambda ((($) v)(a := GS_iter_max v a)))", unfolded 2[symmetric]] del: fun_upd_apply) qed thus ?thesis unfolding GS_rec_am_code'_def by blast qed lemma code_GS_rec_am_arr_opt[code]: "opt_policy_gs'' (vec_to_bfun v) = vec_to_fun ((snd (foldl (\(v, d) s. let (am, m) = least_max_arg_max_enum (\a. r (s, a) + l * (\s' \ UNIV. pmf (K (s,a)) s' * v $ s')) (A s) in (vec_upd v s m, vec_upd d s am)) (v, (\ s. (least_enum (\a. a \ A s)))) (sorted_list_of_set UNIV))))" proof - have 1: "opt_policy_gs'' v' = Abs_Fun (opt_policy_gs v')" for v' by (simp add: opt_policy_gs''.abs_eq) have 2: "opt_policy_gs (vec_to_bfun v) = opt_policy_gs' d v" for v d by (metis Bfun_inverse_fin opt_policy_gs_eq' vec_lambda_eta vec_to_bfun_def) have 3: "opt_policy_gs' d v = (\s. snd (GS_rec_am_code v d s))" for d by (simp add: GS_rec_am_code_eq) have 4: "GS_rec_am_code v d = (\s'. let (v', d') = foldl (\(v, d) s. (v(s := GS_iter_max (vec_lambda v) s), d(s := GS_iter_arg_max (vec_lambda v) s))) (($) v, d) (sorted_list_of_set UNIV) in (v' s', d' s'))" for d s v using GS_rec_am_code' GS_rec_am_code'_prod by presburger have 5: "foldl (\(v, d) s. (v(s := GS_iter_max (vec_lambda v) s), d(s := GS_iter_arg_max (vec_lambda v) s))) (($) v, ($) d) xs = (let (v', d') = foldl (\(v, d) s. (vec_upd v s (GS_iter_max v s), vec_upd d s (GS_iter_arg_max v s))) (v, d) xs in (vec_nth v', vec_nth d'))" for d v xs proof (induction xs arbitrary: d v) case Nil then show ?case by auto next case (Cons a xs) show ?case unfolding vec_lambda_inverse Let_def using Cons[symmetric, unfolded Let_def] by simp (auto simp: vec_lambda_inverse vec_upd_def Let_def eq_commute cong: if_cong) qed have 6: "opt_policy_gs'' (vec_to_bfun v) = vec_to_fun (snd (foldl (\(v, d) s. (vec_upd v s (GS_iter_max v s), vec_upd d s (GS_iter_arg_max v s))) (v, d) (sorted_list_of_set UNIV)))" for d unfolding 1 unfolding 2[of _ "Rep_Fun (vec_to_fun d)"] unfolding 3 unfolding 4 using 5 by (auto simp: Let_def case_prod_beta vec_to_fun_def) show ?thesis unfolding Let_def case_prod_beta unfolding least_max_arg_max_enum_correct1[OF A_ne] using least_max_arg_max_enum_correct2[OF A_ne] unfolding least_max_arg_max_enum_correct2[OF A_ne] using 6 fin_actions A_ne unfolding GS_iter_max_def GS_iter_def GS_iter_arg_max_def by (auto simp: cSup_eq_Max split_beta') qed subsection \Modified Policy Iteration\ sublocale MDP_MPI A K r l "\X. Least (\x. x \ X)" using MDP_act_axioms MDP_reward_axioms by unfold_locales auto definition "d0 s = (LEAST a. a \ A s)" lift_definition d0' :: "('s, 'a) Fun" is d0. lemma d0_dec_det: "is_dec_det d0" using A_ne unfolding d0_def is_dec_det_def by simp lemma v0_code[code]: "v0_mpi\<^sub>b = vec_to_bfun (\ s. r_min / (1 - l))" by (auto simp: v0_mpi\<^sub>b_def v0_mpi_def vec_to_bfun_def ) lemma d0'_code[code]: "d0' = vec_to_fun (\ s. (LEAST a. a \ A s))" by (auto simp: d0'.rep_eq d0_def Rep_Fun_inject[symmetric] vec_to_fun_def) lemma step_value_code[code]: "L_pow v d m = (L_det d ^^ Suc m) v" unfolding L_pow_def L_det_def by auto partial_function (tailrec) mpi_partial where [code]: "mpi_partial eps d v m = (let d' = policy_improvement d v in ( if 2 * l * dist v (\\<^sub>b v) < eps * (1 - l) then (d', v) else mpi_partial eps d' (L_pow v d' (m 0 v)) (\n. m (Suc n))))" lemma mpi_partial_eq_algo: assumes "eps > 0" "d \ D\<^sub>D" "v \ \\<^sub>b v" shows "mpi_partial eps d v m = mpi_algo eps d v m" proof - have "mpi_algo_dom eps (d,v,m)" using assms termination_mpi_algo by blast thus ?thesis by (induction rule: mpi_algo.pinduct) (auto simp: Let_def mpi_algo.psimps mpi_partial.simps) qed lift_definition mpi_partial' :: "real \ ('s, 'a) Fun \ ('s \\<^sub>b real) \ (nat \ ('s \\<^sub>b real) \ nat) \ ('s, 'a) Fun \ ('s \\<^sub>b real)" is mpi_partial. lemma mpi_partial'_code[code]: "mpi_partial' eps d v m = (let d' = policy_improvement' d v in ( if 2 * l * dist v (\\<^sub>b v) < eps * (1 - l) then (d', v) else mpi_partial' eps d' (L_pow v (Rep_Fun d') (m 0 v)) (\n. m (Suc n))))" by (auto simp: mpi_partial'_def mpi_partial.simps Let_def policy_improvement'_def) lemma r_min_code[code_unfold]: "r_min = (MIN s. MIN a. r(s,a))" by (auto simp: cInf_eq_Min) lemma mpi_user_code[code]: "mpi_user eps m = (if eps \ 0 then undefined else let (d, v) = mpi_partial' eps d0' v0_mpi\<^sub>b m in (Rep_Fun d, v))" unfolding mpi_user_def case_prod_beta mpi_partial'_def using mpi_partial_eq_algo A_ne v0_mpi\<^sub>b_le_\\<^sub>b d0_dec_det by (auto simp: d0'.rep_eq d0_def[symmetric]) end subsection \Auxiliary Equations\ lemma [code_unfold]: "dist (f::'a::finite \\<^sub>b 'b::metric_space) g = (MAX a. dist (apply_bfun f a) (g a))" by (auto simp: dist_bfun_def cSup_eq_Max) lemma member_code[code del]: "x \ List.coset xs \ \ List.member xs x" by (auto simp: in_set_member) lemma [code]: "iarray_to_vec v + iarray_to_vec u = (Matrix_To_IArray.iarray_to_vec (Rep_iarray_type v + Rep_iarray_type u))" by (metis (no_types, lifting) Matrix_To_IArray.vec_to_iarray_def iarray_to_vec_vec_to_iarray vec_to_iarray.rep_eq vec_to_iarray_inv vec_to_iarray_plus) lemma [code]: "iarray_to_vec v - iarray_to_vec u = (Matrix_To_IArray.iarray_to_vec (Rep_iarray_type v - Rep_iarray_type u))" unfolding minus_iarray_def Matrix_To_IArray.iarray_to_vec_def iarray_to_vec_def by (auto simp: vec_eq_iff to_nat_less_card) lemma matrix_to_iarray_minus[code_unfold]: "matrix_to_iarray (A - B) = matrix_to_iarray A - matrix_to_iarray B" unfolding matrix_to_iarray_def o_def minus_iarray_def Matrix_To_IArray.vec_to_iarray_def by simp declare matrix_to_iarray_fst_Gauss_Jordan_PA[code_unfold] end \ No newline at end of file diff --git a/thys/MDP-Algorithms/code/Code_Real_Approx_By_Float_Fix.thy b/thys/MDP-Algorithms/code/Code_Real_Approx_By_Float_Fix.thy deleted file mode 100644 --- a/thys/MDP-Algorithms/code/Code_Real_Approx_By_Float_Fix.thy +++ /dev/null @@ -1,59 +0,0 @@ -theory Code_Real_Approx_By_Float_Fix - imports - "HOL-Library.Code_Real_Approx_By_Float" - "Gauss_Jordan.Code_Real_Approx_By_Float_Haskell" -begin -(*<*) -section \Fix for Floating Point Approximation using Haskell\ - -code_printing - type_constructor real \ (Haskell) "Prelude.Double" (*Double precision*) - | constant "0 :: real" \ (Haskell) "0.0" - | constant "1 :: real" \ (Haskell) "1.0" - | constant "Code_Real_Approx_By_Float.real_of_integer" \ (Haskell) "Prelude.fromIntegral (_)" - | class_instance real :: "HOL.equal" => (Haskell) - (*This is necessary. See the tutorial on code generation, page 29*) - | constant "HOL.equal :: real \ real \ bool" \ - (Haskell) "_ == _" - | constant "(<) :: real => real => bool" \ - (Haskell) "_ < _" - | constant "(\) :: real => real => bool" \ - (Haskell) "_ <= _" - | constant "(+) :: real \ real \ real" \ - (Haskell) "_ + _" - | constant "(-) :: real \ real \ real" \ - (Haskell) "_ - _" - | constant "(*) :: real \ real \ real" \ - (Haskell) "_ * _" - | constant "(/) :: real \ real \ real" \ - (Haskell) "_ '/ _" - | constant "uminus :: real => real" \ - (Haskell) "Prelude.negate" - | constant "sqrt :: real => real" \ - (Haskell) "Prelude.sqrt" - | constant Code_Real_Approx_By_Float.exp_real \ - (Haskell) "Prelude.exp" - | constant ln \ - (Haskell) "Prelude.log" - | constant cos \ - (Haskell) "Prelude.cos" - | constant sin \ - (Haskell) "Prelude.sin" - | constant tan \ - (Haskell) "Prelude.tan" - | constant pi \ - (Haskell) "Prelude.pi" - | constant arctan \ - (Haskell) "Prelude.atan" - | constant arccos \ - (Haskell) "Prelude.acos" - | constant arcsin \ - (Haskell) "Prelude.asin" - -code_printing - constant Realfract \ (Haskell) - "(Prelude.fromIntegral (integer'_of'_int _) '/ Prelude.fromIntegral (integer'_of'_int _))" - -code_printing - constant Realfract \ (SML) "(Real.fromInt (IntInf.toInt (integer'_of'_int _))) '// Real.fromInt (IntInf.toInt (integer'_of'_int _))" -(*>*) -end \ No newline at end of file diff --git a/thys/MDP-Algorithms/examples/Code_Inventory.thy b/thys/MDP-Algorithms/examples/Code_Inventory.thy --- a/thys/MDP-Algorithms/examples/Code_Inventory.thy +++ b/thys/MDP-Algorithms/examples/Code_Inventory.thy @@ -1,197 +1,197 @@ (* Author: Maximilian Schäffeler *) theory Code_Inventory imports Code_Mod (* Remove for precise results, approximates real numbers by floats, UNSOUND! *) - Code_Real_Approx_By_Float_Fix + "HOL-Library.Code_Real_Approx_By_Float" begin section \Inventory Management Example\ lemma [code abstype]: "embed_pmf (pmf P) = P" by (metis (no_types, lifting) td_pmf_embed_pmf type_definition_def) lemmas [code_abbrev del] = pmf_integral_code_unfold lemma [code_unfold]: "measure_pmf.expectation P (f :: 'a :: enum \ real) = (\x \ UNIV. pmf P x * f x)" by (metis (no_types, lifting) UNIV_I finite_class.finite_UNIV integral_measure_pmf real_scaleR_def sum.cong) lemma [code]: "pmf (return_pmf x) = (\y. indicat_real {y} x) " by auto lemma [code]: "pmf (bind_pmf N f) = (\i :: 'a. measure_pmf.expectation N (\(x :: 'b ::enum). pmf (f x) i))" using Probability_Mass_Function.pmf_bind by fast lemma pmf_finite_le: "finite (X :: ('a::finite) set) \ sum (pmf p) X \ 1" by (subst sum_pmf_eq_1[symmetric, of UNIV p]) (auto intro: sum_mono2) lemma mod_less_diff: assumes "0 < (x::'s::{mod_type})" "x \ y" shows "y - x < y" proof - have "0 \ Rep y - Rep x" using assms mono_Rep unfolding mono_def by auto have 1: "Rep y - Rep x = Rep (y - x)" unfolding mod_type_class.diff_def Rep_Abs_mod using Rep_ge_0 by (auto intro!: mod_pos_pos_trivial[OF \0 \ Rep y - Rep x\ order.strict_trans1[OF _ Rep_less_n, of _ y], symmetric]) have "Rep y - Rep x < Rep y" using assms(1) strict_mono_Rep Rep_ge_0 le_less not_less by (fastforce simp: strict_mono_def) hence "Rep (y - x) < Rep y" unfolding 1 by blast thus ?thesis by (metis not_less_iff_gr_or_eq strict_mono_Rep strict_mono_def) qed locale inventory = fixes fixed_cost :: real and var_cost :: "'s::{mod_type, finite} \ real" and inv_cost :: "'s \ real" and demand_prob :: "'s pmf" and revenue :: "'s \ real" and discount :: "real" begin definition "order_cost u = (if u = 0 then 0 else fixed_cost + var_cost u)" definition "prob_ge_inv u = 1 - (\jj exp_rev (s + a) - order_cost a - inv_cost (s + a))" lift_definition transition :: "('s \ 's) \ 's pmf" is "\(s, a) s'. (if CARD('s) \ Rep s + Rep a then (if s' = 0 then 1 else 0) else (if s + a < s' then 0 else if s' = 0 then prob_ge_inv (s+a) else pmf demand_prob (s + a - s'))) " proof (safe, goal_cases) case (1 a b x) then show ?case unfolding prob_ge_inv_def using pmf_finite_le by auto next case (2 a b) then show ?case proof (cases "int CARD('s) \ Rep a + Rep b") next case False hence "(\\<^sup>+ x. ennreal (if int CARD('s) \ Rep a + Rep b then if x = 0 then 1 else 0 else if a + b < x then 0 else if x = 0 then prob_ge_inv (a + b) else pmf demand_prob (a + b - x)) \count_space UNIV) = (\x \ UNIV. (if a + b < x then 0 else if x = 0 then prob_ge_inv (a + b) else pmf demand_prob (a + b - x)))" using pmf_nonneg prob_ge_inv_def pmf_finite_le by (auto simp: nn_integral_count_space_finite intro!: sum_ennreal) also have "\ =(\x \ UNIV. (if x = 0 then prob_ge_inv (a + b) else if a + b < x then 0 else pmf demand_prob (a + b - x)))" by (auto intro!: sum.cong ennreal_cong simp add: leD least_mod_type) also have "\ = prob_ge_inv (a + b) + (\x \ UNIV-{0}. (if a + b < x then 0 else pmf demand_prob (a + b - x)))" by (auto simp: sum.remove[of UNIV 0]) also have "\ = prob_ge_inv (a + b) + (\x\{0<..}. (if a + b < x then 0 else pmf demand_prob (a + b - x)))" by (auto simp add: greaterThan_def le_neq_trans least_mod_type intro!: cong[of "sum _"] ennreal_cong) also have "\ = prob_ge_inv (a + b) + (\x\{0<..a+b}. (pmf demand_prob (a + b - x)))" unfolding atMost_def greaterThan_def greaterThanAtMost_def by (auto simp: Collect_neg_eq[symmetric] not_less sum.If_cases) also have "\ = 1 - (\j<(a + b). pmf demand_prob j) + (\x\{0<..a+b}. pmf demand_prob (a + b - x))" unfolding prob_ge_inv_def by auto also have "\ = 1 - (\j<(a + b). pmf demand_prob j) + (\x\{..x\{0<..a+b}. pmf demand_prob (a + b - x)) = (\x\{.. 0 < a + b - x" for x by (metis add.left_neutral diff_add_cancel least_mod_type less_le) moreover have "x < a + b \ a + b - x \ a + b" for x by (metis diff_0_right least_mod_type less_le mod_less_diff not_less) ultimately have "x < a + b \ \xa. x = a + b - xa \ 0 < xa \ xa \ a + b" for x by (auto simp: algebra_simps intro: exI[of _ "a + b - x"]) thus "(-) (a + b) ` {0<..a + b} = {.. = 1" by auto finally show ?thesis. qed (simp add: nn_integral_count_space_finite) qed definition "A_inv (s::'s) = {a::'s. Rep s + Rep a < CARD('s)}" end definition "var_cost_lin (c::real) n = c * Rep n" definition "inv_cost_lin (c::real) n = c * Rep n" definition "revenue_lin (c::real) n = c * Rep n" lift_definition demand_unif :: "('a::finite) pmf" is "\_. 1 / card (UNIV::'a set)" by (auto simp: ennreal_divide_times divide_ennreal[symmetric] ennreal_of_nat_eq_real_of_nat) lift_definition demand_three :: "3 pmf" is "\i. if i = 1 then 1/4 else if i = 2 then 1/2 else 1/4" proof - have *: "(UNIV :: (3 set)) = {0,1,2}" using exhaust_3 by fastforce show ?thesis apply (auto simp: nn_integral_count_space_finite) unfolding * by auto qed abbreviation "fixed_cost \ 4" abbreviation "var_cost \ var_cost_lin 2" abbreviation "inv_cost \ inv_cost_lin 1" abbreviation "revenue \ revenue_lin 8" abbreviation "discount \ 0.99" type_synonym capacity = "30" lemma card_ge_2_imp_ne: "CARD('a) \ 2 \ \(x::'a::finite) y::'a. x \ y" by (meson card_2_iff' ex_card) global_interpretation inventory_ex: inventory fixed_cost "var_cost:: capacity \ real" inv_cost demand_unif revenue discount defines A_inv = inventory_ex.A_inv and transition = inventory_ex.transition and reward = inventory_ex.reward and prob_ge_inv = inventory_ex.prob_ge_inv and order_cost = inventory_ex.order_cost and exp_rev = inventory_ex.exp_rev. abbreviation "K \ inventory_ex.transition" abbreviation "A \ inventory_ex.A_inv" abbreviation "r \ inventory_ex.reward" abbreviation "l \ 0.95" definition "eps = 0.1" definition "fun_to_list f = map f (sorted_list_of_set UNIV)" definition "benchmark_gs (_ :: unit) = map Rep (fun_to_list (vi_policy' K A r l eps 0))" definition "benchmark_vi (_ :: unit) = map Rep (fun_to_list (vi_gs_policy K A r l eps 0))" definition "benchmark_mpi (_ :: unit ) = map Rep (fun_to_list (fst (mpi_user K A r l eps (\_ _. 3))))" definition "benchmark_pi (_ :: unit) = map Rep (fun_to_list (policy_iteration K A r l 0))" fun vs_n where "vs_n 0 v = v" | "vs_n (Suc n) v = vs_n n (mod_MDP_\\<^sub>b K A r l v)" definition "vs_n' n = vs_n n 0" definition "benchmark_vi_n n = (fun_to_list (vs_n n 0))" definition "benchmark_vi_nopol = (fun_to_list (mod_MDP_value_iteration K A r l (1/10) 0))" (* value "benchmark_gs ()" value "benchmark_vi ()" value "benchmark_pi ()" value "benchmark_mpi ()" *) export_code dist vs_n' benchmark_vi_nopol benchmark_vi_n nat_of_integer integer_of_int benchmark_gs benchmark_vi benchmark_mpi benchmark_pi in Haskell module_name DP export_code integer_of_int benchmark_gs benchmark_vi benchmark_mpi benchmark_pi in SML module_name DP end \ No newline at end of file diff --git a/thys/QR_Decomposition/Examples_QR_Abstract_Float.thy b/thys/QR_Decomposition/Examples_QR_Abstract_Float.thy --- a/thys/QR_Decomposition/Examples_QR_Abstract_Float.thy +++ b/thys/QR_Decomposition/Examples_QR_Abstract_Float.thy @@ -1,34 +1,34 @@ (* Title: Examples_QR_Abstract_Float.thy Author: Jose Divasón Author: Jesús Aransay *) section\Examples of execution using floats\ theory Examples_QR_Abstract_Float imports QR_Decomposition - Gauss_Jordan.Code_Real_Approx_By_Float_Haskell + "HOL-Library.Code_Real_Approx_By_Float" begin subsubsection\Examples\ definition "example1 = (let A = list_of_list_to_matrix [[1,2,4],[9,4,5],[0,0,0]]::real^3^3 in matrix_to_list_of_list (divide_by_norm A))" definition "example2 = (let A = list_of_list_to_matrix [[1,2,4],[9,4,5],[0,0,4]]::real^3^3 in matrix_to_list_of_list (fst (QR_decomposition A)))" definition "example3 = (let A = list_of_list_to_matrix [[1,2,4],[9,4,5],[0,0,4]]::real^3^3 in matrix_to_list_of_list (snd (QR_decomposition A)))" definition "example4 = (let A = list_of_list_to_matrix [[1,2,4],[9,4,5],[0,0,4]]::real^3^3 in matrix_to_list_of_list (fst (QR_decomposition A) ** (snd (QR_decomposition A))))" definition "example5 = (let A = list_of_list_to_matrix [[1,sqrt 2,4],[sqrt 5,4,5],[0,sqrt 7,4]]::real^3^3 in matrix_to_list_of_list (fst (QR_decomposition A)))" export_code example1 example2 example3 example4 example5 in SML module_name "QR" end diff --git a/thys/QR_Decomposition/Examples_QR_IArrays_Float.thy b/thys/QR_Decomposition/Examples_QR_IArrays_Float.thy --- a/thys/QR_Decomposition/Examples_QR_IArrays_Float.thy +++ b/thys/QR_Decomposition/Examples_QR_IArrays_Float.thy @@ -1,72 +1,72 @@ (* Title: Examples_QR_IArrays_Float.thy Author: Jose Divasón Author: Jesús Aransay *) section\Examples of execution using floats and IArrays\ theory Examples_QR_IArrays_Float imports QR_Decomposition_IArrays - Gauss_Jordan.Code_Real_Approx_By_Float_Haskell + "HOL-Library.Code_Real_Approx_By_Float" begin subsection\Examples\ definition "example1 = (let A = list_of_list_to_matrix [[1,2,4],[9,4,5],[0,0,0]]::real^3^3 in iarray_of_iarray_to_list_of_list (matrix_to_iarray (divide_by_norm A)))" definition "example2 = (let A = list_of_list_to_matrix [[1,2,4],[9,4,5],[0,0,4]]::real^3^3 in iarray_of_iarray_to_list_of_list (matrix_to_iarray (fst (QR_decomposition A))))" definition "example3 = (let A = list_of_list_to_matrix [[1,2,4],[9,4,5],[0,0,4]]::real^3^3 in iarray_of_iarray_to_list_of_list (matrix_to_iarray (snd (QR_decomposition A))))" definition "example4 = (let A = list_of_list_to_matrix [[1,2,4],[9,4,5],[0,0,4]]::real^3^3 in iarray_of_iarray_to_list_of_list (matrix_to_iarray (fst (QR_decomposition A) ** (snd (QR_decomposition A)))))" definition "example5 = (let A = list_of_list_to_matrix [[1,sqrt 2,4],[sqrt 5,4,5],[0,sqrt 7,4]]::real^3^3 in iarray_of_iarray_to_list_of_list (matrix_to_iarray (fst (QR_decomposition A))))" (*Now there is no problem if there are square roots in the input matrix.*) definition "example6 = (let A = list_of_list_to_matrix [[1,sqrt 2,4],[sqrt 5,4,5],[0,sqrt 7,4]]::real^3^3 in iarray_of_iarray_to_list_of_list (matrix_to_iarray ((fst (QR_decomposition A)))))" definition "example1b = (let A = IArray[IArray[1,2,4],IArray[9,4,5::real],IArray[0,0,0]] in iarray_of_iarray_to_list_of_list ((divide_by_norm_iarray A)))" definition "example2b = (let A = IArray[IArray[1,2,4],IArray[9,4,5],IArray[0,0,4]]in iarray_of_iarray_to_list_of_list ((fst (QR_decomposition_iarrays A))))" definition "example3b = (let A = IArray[IArray[1,2,4],IArray[9,4,5],IArray[0,0,4]] in iarray_of_iarray_to_list_of_list ( (snd (QR_decomposition_iarrays A))))" definition "example4b = (let A = IArray[IArray[1,2,4],IArray[9,4,5],IArray[0,0,4]] in iarray_of_iarray_to_list_of_list ( ((fst (QR_decomposition_iarrays A)) **i (snd (QR_decomposition_iarrays A)))))" definition "example5b = (let A = IArray[IArray[1,2,4],IArray[9,4,5],IArray[0,0,4],IArray[3,5,4]]in iarray_of_iarray_to_list_of_list ( ((fst (QR_decomposition_iarrays A)) **i (snd (QR_decomposition_iarrays A)))))" definition "example6b = (let A = IArray [IArray[1,sqrt 2,4],IArray[sqrt 5,4,5],IArray[0,sqrt 7,4]] in iarray_of_iarray_to_list_of_list (fst (QR_decomposition_iarrays A)))" text\The following example is presented in Chapter 1 of the book \Numerical Methods in Scientific Computing\ by Dahlquist and Bjorck\ definition "book_example = (let A = list_of_list_to_matrix [[1,-0.6691],[1,-0.3907],[1,-0.1219],[1,0.3090],[1,0.5878]]::real^2^5; b = list_to_vec [0.3704,0.5,0.6211,0.8333,0.9804]::real^5; QR = (QR_decomposition A); Q = fst QR; R = snd QR in IArray.list_of (vec_to_iarray (the (inverse_matrix R) ** transpose Q *v b)))" export_code example1 example2 example3 example4 example5 example6 example1b example2b example3b example4b example5b example6b book_example in SML module_name "QR" end