--- a/src/HOL/Decision_Procs/Conversions.thy Tue Feb 07 22:15:05 2017 +0100
+++ b/src/HOL/Decision_Procs/Conversions.thy Tue Feb 07 22:15:06 2017 +0100
@@ -6,24 +6,24 @@
imports Main
begin
-ML {*
+ML \<open>
fun tactic_of_conv cv i st =
if i > Thm.nprems_of st then Seq.empty
else Seq.single (Conv.gconv_rule cv i st);
fun binop_conv cv cv' = Conv.combination_conv (Conv.arg_conv cv) cv';
-*}
+\<close>
-ML {*
+ML \<open>
fun err s ct =
error (s ^ ": " ^ Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct));
-*}
+\<close>
attribute_setup meta =
- {* Scan.succeed (fn (ctxt, th) => (NONE, SOME (mk_meta_eq th))) *}
- {* convert equality to meta equality *}
+ \<open>Scan.succeed (fn (ctxt, th) => (NONE, SOME (mk_meta_eq th)))\<close>
+ \<open>convert equality to meta equality\<close>
-ML {*
+ML \<open>
fun mk_obj_eq th = th RS @{thm meta_eq_to_obj_eq};
fun strip_app ct = ct |> Drule.strip_comb |>> Thm.term_of |>> dest_Const |>> fst;
@@ -77,20 +77,20 @@
fun args1 conv ct = conv (Thm.dest_arg ct);
fun args2 conv ct = conv (Thm.dest_arg1 ct) (Thm.dest_arg ct);
-*}
+\<close>
-ML {*
+ML \<open>
fun strip_numeral ct = (case strip_app ct of
(@{const_name uminus}, [n]) => (case strip_app n of
(@{const_name numeral}, [b]) => (@{const_name uminus}, [b])
| _ => ("", []))
| x => x);
-*}
+\<close>
lemma nat_minus1_eq: "nat (- 1) = 0"
by simp
-ML {*
+ML \<open>
fun nat_conv i = (case strip_app i of
(@{const_name zero_class.zero}, []) => @{thm nat_0 [meta]}
| (@{const_name one_class.one}, []) => @{thm transfer_nat_int_numerals(2) [meta, symmetric]}
@@ -98,9 +98,9 @@
| (@{const_name uminus}, [b]) => (case strip_app b of
(@{const_name one_class.one}, []) => @{thm nat_minus1_eq [meta]}
| (@{const_name numeral}, [b']) => inst [] [b'] @{thm nat_neg_numeral [meta]}));
-*}
+\<close>
-ML {*
+ML \<open>
fun add_num_conv b b' = (case (strip_app b, strip_app b') of
((@{const_name Num.One}, []), (@{const_name Num.One}, [])) =>
@{thm add_num_simps(1) [meta]}
@@ -132,9 +132,9 @@
transitive'
(inst [] [m, n] @{thm add_num_simps(9) [meta]})
(cong1 (cong2' add_num_conv (args2 add_num_conv) Thm.reflexive)));
-*}
+\<close>
-ML {*
+ML \<open>
fun BitM_conv m = (case strip_app m of
(@{const_name Num.One}, []) => @{thm BitM.simps(1) [meta]}
| (@{const_name Num.Bit0}, [n]) =>
@@ -143,13 +143,13 @@
(cong1 (args1 BitM_conv))
| (@{const_name Num.Bit1}, [n]) =>
inst [] [n] @{thm BitM.simps(3) [meta]});
-*}
+\<close>
lemma dbl_neg_numeral:
"Num.dbl (- Num.numeral k) = - Num.numeral (Num.Bit0 k)"
by simp
-ML {*
+ML \<open>
fun dbl_conv a =
let
val dbl_neg_numeral_a = inst [a] [] @{thm dbl_neg_numeral [meta]};
@@ -162,13 +162,13 @@
| (@{const_name numeral}, [k]) => inst [] [k] dbl_numeral_a
| (@{const_name uminus}, [k]) => inst [] [k] dbl_neg_numeral_a
end;
-*}
+\<close>
lemma dbl_inc_neg_numeral:
"Num.dbl_inc (- Num.numeral k) = - Num.numeral (Num.BitM k)"
by simp
-ML {*
+ML \<open>
fun dbl_inc_conv a =
let
val dbl_inc_neg_numeral_a = inst [a] [] @{thm dbl_inc_neg_numeral [meta]};
@@ -184,13 +184,13 @@
(inst [] [k] dbl_inc_neg_numeral_a)
(cong1 (cong1 (args1 BitM_conv)))
end;
-*}
+\<close>
lemma dbl_dec_neg_numeral:
"Num.dbl_dec (- Num.numeral k) = - Num.numeral (Num.Bit1 k)"
by simp
-ML {*
+ML \<open>
fun dbl_dec_conv a =
let
val dbl_dec_neg_numeral_a = inst [a] [] @{thm dbl_dec_neg_numeral [meta]};
@@ -206,9 +206,9 @@
(inst [] [k] dbl_dec_numeral_a)
(cong1 (args1 BitM_conv))
end;
-*}
+\<close>
-ML {*
+ML \<open>
fun sub_conv a =
let
val [sub_One_One, sub_One_Bit0, sub_One_Bit1,
@@ -251,9 +251,9 @@
(inst [] [k, l] sub_Bit1_Bit1)
(cong1' dbl_conv_a (args2 conv)))
in conv end;
-*}
+\<close>
-ML {*
+ML \<open>
fun expand1 a =
let val numeral_1_eq_1_a = inst [a] [] @{thm numeral_One [meta, symmetric]}
in
@@ -283,9 +283,9 @@
numeral_1_eq_1_a)
| _ => eq
end;
-*}
+\<close>
-ML {*
+ML \<open>
fun plus_conv f a =
let
val add_0_a = inst [a] [] @{thm add_0 [meta]};
@@ -304,13 +304,13 @@
in f conv end;
val nat_plus_conv = plus_conv I @{ctyp nat};
-*}
+\<close>
lemma neg_numeral_plus_neg_numeral:
"- Num.numeral m + - Num.numeral n = (- Num.numeral (m + n) ::'a::neg_numeral)"
by simp
-ML {*
+ML \<open>
fun plus_neg_conv a =
let
val numeral_plus_neg_numeral_a =
@@ -341,12 +341,12 @@
fun plus_conv' a = norm1_eq a oo plus_conv (plus_neg_conv a) a;
val int_plus_conv = plus_conv' @{ctyp int};
-*}
+\<close>
lemma minus_one: "- 1 = - 1" by simp
lemma minus_numeral: "- numeral b = - numeral b" by simp
-ML {*
+ML \<open>
fun uminus_conv a =
let
val minus_zero_a = inst [a] [] @{thm minus_zero [meta]};
@@ -363,9 +363,9 @@
end;
val int_neg_conv = uminus_conv @{ctyp int};
-*}
+\<close>
-ML {*
+ML \<open>
fun minus_conv a =
let
val [numeral_minus_numeral_a, numeral_minus_neg_numeral_a,
@@ -402,9 +402,9 @@
in norm1_eq_a oo conv end;
val int_minus_conv = minus_conv @{ctyp int};
-*}
+\<close>
-ML {*
+ML \<open>
val int_numeral = Thm.apply @{cterm "numeral :: num \<Rightarrow> int"};
val nat_minus_refl = Thm.reflexive @{cterm "minus :: nat \<Rightarrow> nat \<Rightarrow> nat"};
@@ -421,9 +421,9 @@
(inst [] [m, n] @{thm diff_nat_numeral [meta]})
(cong1' nat_conv (args2 int_minus_conv))
| _ => cong2'' nat_minus_conv (expand1_nat m) (expand1_nat n));
-*}
+\<close>
-ML {*
+ML \<open>
fun mult_num_conv m n = (case (strip_app m, strip_app n) of
(_, (@{const_name Num.One}, [])) =>
inst [] [m] @{thm mult_num_simps(1) [meta]}
@@ -447,9 +447,9 @@
(cong1 (cong2' add_num_conv
(args2 add_num_conv)
(cong1 (args2 mult_num_conv)))));
-*}
+\<close>
-ML {*
+ML \<open>
fun mult_conv f a =
let
val mult_zero_left_a = inst [a] [] @{thm mult_zero_left [meta]};
@@ -469,9 +469,9 @@
in norm1_eq_a oo f conv end;
val nat_mult_conv = mult_conv I @{ctyp nat};
-*}
+\<close>
-ML {*
+ML \<open>
fun mult_neg_conv a =
let
val [neg_numeral_times_neg_numeral_a, neg_numeral_times_numeral_a,
@@ -498,9 +498,9 @@
fun mult_conv' a = mult_conv (mult_neg_conv a) a;
val int_mult_conv = mult_conv' @{ctyp int};
-*}
+\<close>
-ML {*
+ML \<open>
fun eq_num_conv m n = (case (strip_app m, strip_app n) of
((@{const_name Num.One}, []), (@{const_name Num.One}, [])) =>
@{thm eq_num_simps(1) [meta]}
@@ -524,9 +524,9 @@
Thm.transitive
(inst [] [m, n] @{thm eq_num_simps(9) [meta]})
(eq_num_conv m n));
-*}
+\<close>
-ML {*
+ML \<open>
fun eq_conv f a =
let
val zero_eq_zero_a = inst [a] [] @{thm refl [of 0, THEN Eq_TrueI]};
@@ -552,9 +552,9 @@
in f conv end;
val nat_eq_conv = eq_conv I @{ctyp nat};
-*}
+\<close>
-ML {*
+ML \<open>
fun eq_neg_conv a =
let
val neg_numeral_neq_zero_a =
@@ -587,9 +587,9 @@
fun eq_conv' a = eq_conv (eq_neg_conv a) a;
val int_eq_conv = eq_conv' @{ctyp int};
-*}
+\<close>
-ML {*
+ML \<open>
fun le_num_conv m n = (case (strip_app m, strip_app n) of
((@{const_name Num.One}, []), _) =>
inst [] [n] @{thm le_num_simps(1) [meta]}
@@ -637,9 +637,9 @@
Thm.transitive
(inst [] [m, n] @{thm less_num_simps(7) [meta]})
(less_num_conv m n));
-*}
+\<close>
-ML {*
+ML \<open>
fun le_conv f a =
let
val zero_le_zero_a = inst [a] [] @{thm order_refl [of 0, THEN Eq_TrueI]};
@@ -665,9 +665,9 @@
in f conv end;
val nat_le_conv = le_conv I @{ctyp nat};
-*}
+\<close>
-ML {*
+ML \<open>
fun le_neg_conv a =
let
val neg_numeral_le_zero_a =
@@ -700,9 +700,9 @@
fun le_conv' a = le_conv (le_neg_conv a) a;
val int_le_conv = le_conv' @{ctyp int};
-*}
+\<close>
-ML {*
+ML \<open>
fun less_conv f a =
let
val not_zero_less_zero_a = inst [a] [] @{thm less_irrefl [of 0, THEN Eq_FalseI]};
@@ -728,9 +728,9 @@
in f conv end;
val nat_less_conv = less_conv I @{ctyp nat};
-*}
+\<close>
-ML {*
+ML \<open>
fun less_neg_conv a =
let
val neg_numeral_less_zero_a =
@@ -763,9 +763,9 @@
fun less_conv' a = less_conv (less_neg_conv a) a;
val int_less_conv = less_conv' @{ctyp int};
-*}
+\<close>
-ML {*
+ML \<open>
fun If_conv a =
let
val if_True = inst [a] [] @{thm if_True [meta]};
@@ -804,9 +804,9 @@
| _ => err "If_conv" (Thm.rhs_of p_eq)
end
end;
-*}
+\<close>
-ML {*
+ML \<open>
fun drop_conv a =
let
val drop_0_a = inst [a] [] @{thm drop_0 [meta]};
@@ -823,9 +823,9 @@
Thm.reflexive
(cong2' conv (args2 nat_minus_conv) Thm.reflexive))))
in conv end;
-*}
+\<close>
-ML {*
+ML \<open>
fun nth_conv a =
let
val nth_Cons_a = inst [a] [] @{thm nth_Cons' [meta]};
@@ -839,6 +839,6 @@
Thm.reflexive
(cong2' conv Thm.reflexive (args2 nat_minus_conv))))
in conv end;
-*}
+\<close>
end