Session MDP-Algorithms

Theories

• HOL-Library.IArray
• HOL-Data_Structures.Define_Time_Function
  • File ‹Define_Time_0.ML›
  • File ‹Define_Time_Function.ML›
• HOL-Data_Structures.Time_Funs
• HOL-Data_Structures.Array_Specs
• HOL-Library.Tree_Real
• HOL-Data_Structures.Braun_Tree
• HOL-Data_Structures.Array_Braun
• HOL-Data_Structures.Tree2
• HOL-Data_Structures.RBT
• HOL-Data_Structures.Cmp
• HOL-Data_Structures.Less_False
• HOL-Data_Structures.Sorted_Less
• HOL-Data_Structures.List_Ins_Del
• HOL-Data_Structures.Set_Specs
• HOL-Data_Structures.Isin2
• HOL-Data_Structures.RBT_Set
• HOL-Data_Structures.AList_Upd_Del
• HOL-Data_Structures.Map_Specs
• HOL-Data_Structures.Lookup2
• HOL-Data_Structures.RBT_Map
• MDP_fin
• Value_Iteration
• HOL-Library.Code_Abstract_Nat
• HOL-Library.Code_Target_Nat
• HOL-Library.Code_Target_Int
• HOL-Library.Code_Target_Bit_Shifts
• HOL-Library.Code_Target_Numeral
• DiffArray_Base
• DiffArray_ST
• Code_Setup
• VI_Code
• HOL-Library.Code_Real_Approx_By_Float
• Code_Real_Approx_By_Float_Fix
• VI_Code_Export_Float
• VI_Code_Export_Rat
• Policy_Iteration
• Splitting_Methods
• Splitting_Methods_Fin
• GS_Code
• GS_Code_Export_Float
• GS_Code_Export_Rat
• Modified_Policy_Iteration
• MPI_Code
• MPI_Code_Export_Float
• MPI_Code_Export_Rat
• Polynomial_Interpolation.Ring_Hom
• Jordan_Normal_Form.Missing_Misc
• HOL-Algebra.Congruence
• HOL-Algebra.Order
• HOL-Algebra.Lattice
• HOL-Algebra.Complete_Lattice
• HOL-Algebra.Group
• HOL-Algebra.FiniteProduct
• HOL-Algebra.Ring
  • File ‹ringsimp.ML›
• Jordan_Normal_Form.Missing_Ring
• Jordan_Normal_Form.Conjugate
• HOL-Algebra.Module
• Jordan_Normal_Form.Matrix
• HOL-Library.More_List
• HOL-Computational_Algebra.Polynomial
• HOL-Computational_Algebra.Fraction_Field
• HOL-Computational_Algebra.Normalized_Fraction
• HOL-Computational_Algebra.Polynomial_Factorial
• Polynomial_Interpolation.Missing_Unsorted
• Polynomial_Interpolation.Missing_Polynomial
• Polynomial_Factorization.Order_Polynomial
• HOL-Computational_Algebra.Fundamental_Theorem_Algebra
• Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
• Polynomial_Interpolation.Ring_Hom_Poly
• Jordan_Normal_Form.Gauss_Jordan_Elimination
• Jordan_Normal_Form.Column_Operations
• Jordan_Normal_Form.Determinant
• Jordan_Normal_Form.Char_Poly
• Jordan_Normal_Form.Jordan_Normal_Form
• HOL-Algebra.Coset
• VectorSpace.RingModuleFacts
• VectorSpace.FunctionLemmas
• VectorSpace.MonoidSums
• VectorSpace.LinearCombinations
• VectorSpace.SumSpaces
• VectorSpace.VectorSpace
• Jordan_Normal_Form.Missing_VectorSpace
• Jordan_Normal_Form.VS_Connect
• Jordan_Normal_Form.Gram_Schmidt
• Jordan_Normal_Form.Schur_Decomposition
• Jordan_Normal_Form.Jordan_Normal_Form_Existence
• Jordan_Normal_Form.Spectral_Radius
• Perron_Frobenius.Bij_Nat
• HOL-Types_To_Sets.Types_To_Sets
  • File ‹local_typedef.ML›
  • File ‹unoverloading.ML›
  • File ‹internalize_sort.ML›
  • File ‹unoverload_type.ML›
  • File ‹unoverload_def.ML›
• Perron_Frobenius.Cancel_Card_Constraint
  • File ‹cancel_card_constraint.ML›
• HOL-Eisbach.Eisbach
  • File ‹parse_tools.ML›
  • File ‹method_closure.ML›
  • File ‹eisbach_rule_insts.ML›
  • File ‹match_method.ML›
• Perron_Frobenius.HMA_Connect
• Blinfun_To_Matrix
• Policy_Iteration_Fin
• Containers.Containers_Auxiliary
• Deriving.Generator_Aux
  • File ‹bnf_access.ML›
  • File ‹generator_aux.ML›
• Deriving.Derive_Manager
  • File ‹derive_manager.ML›
• Containers.Containers_Generator
  • File ‹containers_generator.ML›
• Containers.Collection_Enum
  • File ‹cenum_generator.ML›
• Deriving.Equality_Generator
  • File ‹equality_generator.ML›
• Deriving.Equality_Instances
• Containers.Collection_Eq
  • File ‹ceq_generator.ML›
• Containers.Equal
• Containers.DList_Set
• Containers.List_Fusion
• HOL-Library.Char_ord
• Containers.Lexicographic_Order
• Containers.Extend_Partial_Order
• Containers.Set_Linorder
• Deriving.Comparator
• Deriving.Comparator_Generator
  • File ‹comparator_generator.ML›
• Deriving.Compare
  • File ‹compare_code.ML›
• Deriving.Compare_Generator
  • File ‹compare_generator.ML›
• Deriving.Compare_Instances
• Containers.Collection_Order
  • File ‹ccompare_generator.ML›
• HOL-Library.RBT_Impl
• Containers.RBT_ext
• Deriving.RBT_Comparator_Impl
• Containers.RBT_Mapping2
• Containers.RBT_Set2
• Containers.Closure_Set
• Containers.Set_Impl
  • File ‹set_impl_generator.ML›
• Jordan_Normal_Form.Matrix_IArray_Impl
• Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
• Jordan_Normal_Form.Determinant_Impl
• Show.Show
  • File ‹show_generator.ML›
• Jordan_Normal_Form.Show_Matrix
• Show.Show_Instances
• Show.Shows_Literal
• Jordan_Normal_Form.Shows_Literal_Matrix
• Jordan_Normal_Form.Matrix_Impl
• PI_Code
• PI_Code_Export_Float
• PI_Code_Export_Rat
• Backward_Induction
• Fin_Code
• Fin_Code_Export_Float
• Fin_Code_Export_Rat