src/HOL/Decision_Procs/MIR.thy
changeset 62342 1cf129590be8
parent 61945 1135b8de26c3
child 63600 d0fa16751d14
equal deleted inserted replaced
62341:a594429637fd 62342:1cf129590be8
  5545   | num_of_term vs (@{term "op * :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
  5545   | num_of_term vs (@{term "op * :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
  5546       (case (num_of_term vs t1)
  5546       (case (num_of_term vs t1)
  5547        of @{code C} i => @{code Mul} (i, num_of_term vs t2)
  5547        of @{code C} i => @{code Mul} (i, num_of_term vs t2)
  5548         | _ => error "num_of_term: unsupported Multiplication")
  5548         | _ => error "num_of_term: unsupported Multiplication")
  5549   | num_of_term vs (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "numeral :: _ \<Rightarrow> int"} $ t')) =
  5549   | num_of_term vs (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "numeral :: _ \<Rightarrow> int"} $ t')) =
  5550       mk_C (HOLogic.dest_num t')
  5550       mk_C (HOLogic.dest_numeral t')
  5551   | num_of_term vs (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "- numeral :: _ \<Rightarrow> int"} $ t')) =
  5551   | num_of_term vs (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "- numeral :: _ \<Rightarrow> int"} $ t')) =
  5552       mk_C (~ (HOLogic.dest_num t'))
  5552       mk_C (~ (HOLogic.dest_numeral t'))
  5553   | num_of_term vs (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "floor :: real \<Rightarrow> int"} $ t')) =
  5553   | num_of_term vs (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "floor :: real \<Rightarrow> int"} $ t')) =
  5554       @{code Floor} (num_of_term vs t')
  5554       @{code Floor} (num_of_term vs t')
  5555   | num_of_term vs (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "ceiling :: real \<Rightarrow> int"} $ t')) =
  5555   | num_of_term vs (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "ceiling :: real \<Rightarrow> int"} $ t')) =
  5556       @{code Neg} (@{code Floor} (@{code Neg} (num_of_term vs t')))
  5556       @{code Neg} (@{code Floor} (@{code Neg} (num_of_term vs t')))
  5557   | num_of_term vs (@{term "numeral :: _ \<Rightarrow> real"} $ t') =
  5557   | num_of_term vs (@{term "numeral :: _ \<Rightarrow> real"} $ t') =
  5558       mk_C (HOLogic.dest_num t')
  5558       mk_C (HOLogic.dest_numeral t')
  5559   | num_of_term vs (@{term "- numeral :: _ \<Rightarrow> real"} $ t') =
  5559   | num_of_term vs (@{term "- numeral :: _ \<Rightarrow> real"} $ t') =
  5560       mk_C (~ (HOLogic.dest_num t'))
  5560       mk_C (~ (HOLogic.dest_numeral t'))
  5561   | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t);
  5561   | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t);
  5562 
  5562 
  5563 fun fm_of_term vs @{term True} = @{code T}
  5563 fun fm_of_term vs @{term True} = @{code T}
  5564   | fm_of_term vs @{term False} = @{code F}
  5564   | fm_of_term vs @{term False} = @{code F}
  5565   | fm_of_term vs (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) =
  5565   | fm_of_term vs (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) =
  5567   | fm_of_term vs (@{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) =
  5567   | fm_of_term vs (@{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) =
  5568       @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
  5568       @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
  5569   | fm_of_term vs (@{term "op = :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) =
  5569   | fm_of_term vs (@{term "op = :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) =
  5570       @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
  5570       @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
  5571   | fm_of_term vs (@{term "op rdvd"} $ (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
  5571   | fm_of_term vs (@{term "op rdvd"} $ (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
  5572       mk_Dvd (HOLogic.dest_num t1, num_of_term vs t2)
  5572       mk_Dvd (HOLogic.dest_numeral t1, num_of_term vs t2)
  5573   | fm_of_term vs (@{term "op rdvd"} $ (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "- numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
  5573   | fm_of_term vs (@{term "op rdvd"} $ (@{term "of_int :: int \<Rightarrow> real"} $ (@{term "- numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
  5574       mk_Dvd (~ (HOLogic.dest_num t1), num_of_term vs t2)
  5574       mk_Dvd (~ (HOLogic.dest_numeral t1), num_of_term vs t2)
  5575   | fm_of_term vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
  5575   | fm_of_term vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
  5576       @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
  5576       @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
  5577   | fm_of_term vs (@{term HOL.conj} $ t1 $ t2) =
  5577   | fm_of_term vs (@{term HOL.conj} $ t1 $ t2) =
  5578       @{code And} (fm_of_term vs t1, fm_of_term vs t2)
  5578       @{code And} (fm_of_term vs t1, fm_of_term vs t2)
  5579   | fm_of_term vs (@{term HOL.disj} $ t1 $ t2) =
  5579   | fm_of_term vs (@{term HOL.disj} $ t1 $ t2) =