1997 (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))" |
1996 (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))" |
1998 |
1997 |
1999 ML {* @{code ferrack_test} () *} |
1998 ML {* @{code ferrack_test} () *} |
2000 |
1999 |
2001 oracle linr_oracle ("term") = {* |
2000 oracle linr_oracle ("term") = {* |
2002 |
|
2003 let |
2001 let |
2004 |
2002 |
2005 fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t |
2003 fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t |
2006 of NONE => error "Variable not found in the list!" |
2004 of NONE => error "Variable not found in the list!" |
2007 | SOME n => @{code Bound} n) |
2005 | SOME n => @{code Bound} n) |
2008 | num_of_term vs @{term "real (0::int)"} = @{code C} 0 |
2006 | num_of_term vs @{term "real (0::int)"} = @{code C} 0 |
2009 | num_of_term vs @{term "real (1::int)"} = @{code C} 1 |
2007 | num_of_term vs @{term "real (1::int)"} = @{code C} 1 |
2010 | num_of_term vs @{term "0::real"} = @{code C} 0 |
2008 | num_of_term vs @{term "0::real"} = @{code C} 0 |
2011 | num_of_term vs @{term "1::real"} = @{code C} 1 |
2009 | num_of_term vs @{term "1::real"} = @{code C} 1 |
2012 | num_of_term vs (Term.Bound i) = @{code Bound} i |
2010 | num_of_term vs (Bound i) = @{code Bound} i |
2013 | num_of_term vs (@{term "uminus :: real \<Rightarrow> real"} $ t') = @{code Neg} (num_of_term vs t') |
2011 | num_of_term vs (@{term "uminus :: real \<Rightarrow> real"} $ t') = @{code Neg} (num_of_term vs t') |
2014 | num_of_term vs (@{term "op + :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = @{code Add} (num_of_term vs t1, num_of_term vs t2) |
2012 | num_of_term vs (@{term "op + :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = @{code Add} (num_of_term vs t1, num_of_term vs t2) |
2015 | num_of_term vs (@{term "op - :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = @{code Sub} (num_of_term vs t1, num_of_term vs t2) |
2013 | num_of_term vs (@{term "op - :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = @{code Sub} (num_of_term vs t1, num_of_term vs t2) |
2016 | num_of_term vs (@{term "op * :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = (case (num_of_term vs t1) |
2014 | num_of_term vs (@{term "op * :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = (case (num_of_term vs t1) |
2017 of @{code C} i => @{code Mul} (i, num_of_term vs t2) |
2015 of @{code C} i => @{code Mul} (i, num_of_term vs t2) |
2018 | _ => error "num_of_term: unsupported Multiplication") |
2016 | _ => error "num_of_term: unsupported Multiplication") |
2019 | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "number_of :: int \<Rightarrow> int"} $ t')) = @{code C} (HOLogic.dest_numeral t') |
2017 | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "number_of :: int \<Rightarrow> int"} $ t')) = @{code C} (HOLogic.dest_numeral t') |
2020 | num_of_term vs (@{term "number_of :: int \<Rightarrow> int"} $ t') = @{code C} (HOLogic.dest_numeral t') |
2018 | num_of_term vs (@{term "number_of :: int \<Rightarrow> real"} $ t') = @{code C} (HOLogic.dest_numeral t') |
2021 | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term_global @{theory} t); |
2019 | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term_global @{theory} t); |
2022 |
2020 |
2023 fun fm_of_term vs @{term True} = @{code T} |
2021 fun fm_of_term vs @{term True} = @{code T} |
2024 | fm_of_term vs @{term False} = @{code T} |
2022 | fm_of_term vs @{term False} = @{code F} |
2025 | fm_of_term vs (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) |
2023 | fm_of_term vs (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) |
2026 | fm_of_term vs (@{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) |
2024 | fm_of_term vs (@{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) |
2027 | fm_of_term vs (@{term "op = :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) |
2025 | fm_of_term vs (@{term "op = :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) |
2028 | fm_of_term vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) = @{code Iff} (fm_of_term vs t1, fm_of_term vs t2) |
2026 | fm_of_term vs (@{term "op \<longleftrightarrow> :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) = @{code Iff} (fm_of_term vs t1, fm_of_term vs t2) |
2029 | fm_of_term vs (@{term "op &"} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2) |
2027 | fm_of_term vs (@{term "op &"} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2) |
2030 | fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2) |
2028 | fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2) |
2031 | fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2) |
2029 | fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2) |
2032 | fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t') |
2030 | fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t') |
2033 | fm_of_term vs (Const("Ex", _) $ Term.Abs (xn, xT, p)) = |
2031 | fm_of_term vs (Const ("Ex", _) $ Abs (xn, xT, p)) = |
2034 @{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p) |
2032 @{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p) |
2035 | fm_of_term vs (Const("All", _) $ Term.Abs(xn, xT, p)) = |
2033 | fm_of_term vs (Const ("All", _) $ Abs (xn, xT, p)) = |
2036 @{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p) |
2034 @{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p) |
2037 | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term_global @{theory} t); |
2035 | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term_global @{theory} t); |
2038 |
2036 |
2039 fun term_of_num vs (@{code C} i) = @{term "real :: int \<Rightarrow> real"} $ HOLogic.mk_number HOLogic.intT i |
2037 fun term_of_num vs (@{code C} i) = @{term "real :: int \<Rightarrow> real"} $ HOLogic.mk_number HOLogic.intT i |
2040 | term_of_num vs (@{code Bound} n) = fst (the (find_first (fn (_, m) => n = m) vs)) |
2038 | term_of_num vs (@{code Bound} n) = fst (the (find_first (fn (_, m) => n = m) vs)) |
2062 | term_of_fm vs (@{code NEq} t) = term_of_fm vs (@{code NOT} (@{code Eq} t)) |
2060 | term_of_fm vs (@{code NEq} t) = term_of_fm vs (@{code NOT} (@{code Eq} t)) |
2063 | term_of_fm vs (@{code NOT} t') = HOLogic.Not $ term_of_fm vs t' |
2061 | term_of_fm vs (@{code NOT} t') = HOLogic.Not $ term_of_fm vs t' |
2064 | term_of_fm vs (@{code And} (t1, t2)) = HOLogic.conj $ term_of_fm vs t1 $ term_of_fm vs t2 |
2062 | term_of_fm vs (@{code And} (t1, t2)) = HOLogic.conj $ term_of_fm vs t1 $ term_of_fm vs t2 |
2065 | term_of_fm vs (@{code Or} (t1, t2)) = HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2 |
2063 | term_of_fm vs (@{code Or} (t1, t2)) = HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2 |
2066 | term_of_fm vs (@{code Imp} (t1, t2)) = HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2 |
2064 | term_of_fm vs (@{code Imp} (t1, t2)) = HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2 |
2067 | term_of_fm vs (@{code Iff} (t1, t2)) = @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ |
2065 | term_of_fm vs (@{code Iff} (t1, t2)) = @{term "op \<longleftrightarrow> :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ |
2068 term_of_fm vs t1 $ term_of_fm vs t2 |
2066 term_of_fm vs t1 $ term_of_fm vs t2 |
2069 | term_of_fm vs _ = error "If this is raised, Isabelle/HOL or generate_code is inconsistent."; |
2067 | term_of_fm vs _ = error "If this is raised, Isabelle/HOL or generate_code is inconsistent."; |
2070 |
2068 |
2071 in fn thy => fn t => |
2069 in fn thy => fn t => |
2072 let |
2070 let |