src/HOL/Decision_Procs/Approximation.thy
changeset 30413 c41afa5607be
parent 30273 ecd6f0ca62ea
child 30439 57c68b3af2ea
equal deleted inserted replaced
30407:81218f70997f 30413:c41afa5607be
  2420         -- see "The Definition of Standard ML" by R. Milner, M. Tofte and R. Harper (pg. 79) *}
  2420         -- see "The Definition of Standard ML" by R. Milner, M. Tofte and R. Harper (pg. 79) *}
  2421 lemma "d * (i div d) + i mod d = (i::int)" by auto
  2421 lemma "d * (i div d) + i mod d = (i::int)" by auto
  2422 lemma "0 < (d :: int) \<Longrightarrow> 0 \<le> i mod d \<and> i mod d < d" by auto
  2422 lemma "0 < (d :: int) \<Longrightarrow> 0 \<le> i mod d \<and> i mod d < d" by auto
  2423 lemma "(d :: int) < 0 \<Longrightarrow> d < i mod d \<and> i mod d \<le> 0" by auto
  2423 lemma "(d :: int) < 0 \<Longrightarrow> d < i mod d \<and> i mod d \<le> 0" by auto
  2424 
  2424 
  2425 code_const "op div :: int \<Rightarrow> int \<Rightarrow> int" (SML "(fn i => fn d => if d = 0 then 0 else i div d)")
       
  2426 code_const "op mod :: int \<Rightarrow> int \<Rightarrow> int" (SML "(fn i => fn d => if d = 0 then i else i mod d)")
       
  2427 code_const "divmod :: int \<Rightarrow> int \<Rightarrow> (int * int)" (SML "(fn i => fn d => if d = 0 then (0, i) else IntInf.divMod (i, d))")
       
  2428 
       
  2429 ML {*
  2425 ML {*
  2430   val uneq_equations = PureThy.get_thms @{theory} "uneq_equations";
  2426   val uneq_equations = PureThy.get_thms @{theory} "uneq_equations";
  2431   val bounded_by_equations = PureThy.get_thms @{theory} "bounded_by_equations";
  2427   val bounded_by_equations = PureThy.get_thms @{theory} "bounded_by_equations";
  2432   val bounded_by_simpset = (HOL_basic_ss addsimps bounded_by_equations)
  2428   val bounded_by_simpset = (HOL_basic_ss addsimps bounded_by_equations)
  2433 
  2429 
  2446     val prec' = to_nat prec
  2442     val prec' = to_nat prec
  2447 
  2443 
  2448     fun bot_float (Const (@{const_name "times"}, _) $ mantisse $ (Const (@{const_name "pow2"}, _) $ exp))
  2444     fun bot_float (Const (@{const_name "times"}, _) $ mantisse $ (Const (@{const_name "pow2"}, _) $ exp))
  2449                    = @{term "Float"} $ to_int mantisse $ to_int exp
  2445                    = @{term "Float"} $ to_int mantisse $ to_int exp
  2450       | bot_float (Const (@{const_name "divide"}, _) $ mantisse $ (Const (@{const_name "power"}, _) $ ten $ exp))
  2446       | bot_float (Const (@{const_name "divide"}, _) $ mantisse $ (Const (@{const_name "power"}, _) $ ten $ exp))
  2451                    = @{term "float_divl"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ (@{term "power_float (Float 5 1)"} $ to_nat exp)
  2447                    = @{term "float_divl"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ (@{term "power (Float 5 1)"} $ to_nat exp)
  2452       | bot_float (Const (@{const_name "divide"}, _) $ mantisse $ ten)
  2448       | bot_float (Const (@{const_name "divide"}, _) $ mantisse $ ten)
  2453                    = @{term "float_divl"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ @{term "Float 5 1"}
  2449                    = @{term "float_divl"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ @{term "Float 5 1"}
  2454       | bot_float mantisse = @{term "Float"} $ to_int mantisse $ @{term "0 :: int"}
  2450       | bot_float mantisse = @{term "Float"} $ to_int mantisse $ @{term "0 :: int"}
  2455 
  2451 
  2456     fun top_float (Const (@{const_name "times"}, _) $ mantisse $ (Const (@{const_name "pow2"}, _) $ exp))
  2452     fun top_float (Const (@{const_name "times"}, _) $ mantisse $ (Const (@{const_name "pow2"}, _) $ exp))
  2457                    = @{term "Float"} $ to_int mantisse $ to_int exp
  2453                    = @{term "Float"} $ to_int mantisse $ to_int exp
  2458       | top_float (Const (@{const_name "divide"}, _) $ mantisse $ (Const (@{const_name "power"}, _) $ ten $ exp))
  2454       | top_float (Const (@{const_name "divide"}, _) $ mantisse $ (Const (@{const_name "power"}, _) $ ten $ exp))
  2459                    = @{term "float_divr"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ (@{term "power_float (Float 5 1)"} $ to_nat exp)
  2455                    = @{term "float_divr"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ (@{term "power (Float 5 1)"} $ to_nat exp)
  2460       | top_float (Const (@{const_name "divide"}, _) $ mantisse $ ten)
  2456       | top_float (Const (@{const_name "divide"}, _) $ mantisse $ ten)
  2461                    = @{term "float_divr"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ @{term "Float 5 1"}
  2457                    = @{term "float_divr"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ @{term "Float 5 1"}
  2462       | top_float mantisse = @{term "Float"} $ to_int mantisse $ @{term "0 :: int"}
  2458       | top_float mantisse = @{term "Float"} $ to_int mantisse $ @{term "0 :: int"}
  2463 
  2459 
  2464     val goal' : term = List.nth (prems_of thm, i - 1)
  2460     val goal' : term = List.nth (prems_of thm, i - 1)