--- 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
--- a/src/HOL/Decision_Procs/Reflective_Field.thy Tue Feb 07 22:15:05 2017 +0100
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy Tue Feb 07 22:15:06 2017 +0100
@@ -597,14 +597,14 @@
then have "feval xs e1 \<in> carrier R" "feval xs e2 \<in> carrier R"
"peval xs (Num e2) \<noteq> \<zero>" "nonzero xs (Cond e2)"
by (simp_all add: nonzero_union nonzero_insert split: prod.split_asm)
- from `in_carrier xs` `nonzero xs (Cond e2)`
+ from \<open>in_carrier xs\<close> \<open>nonzero xs (Cond e2)\<close>
have "feval xs e2 = peval xs (Num e2) \<oslash> peval xs (Denom e2)"
by (rule fnorm_correct)
- moreover from `in_carrier xs` `nonzero xs (Cond e2)`
+ moreover from \<open>in_carrier xs\<close> \<open>nonzero xs (Cond e2)\<close>
have "peval xs (Denom e2) \<noteq> \<zero>" by (rule fnorm_correct)
- ultimately have "feval xs e2 \<noteq> \<zero>" using `peval xs (Num e2) \<noteq> \<zero>` `in_carrier xs`
+ ultimately have "feval xs e2 \<noteq> \<zero>" using \<open>peval xs (Num e2) \<noteq> \<zero>\<close> \<open>in_carrier xs\<close>
by (simp add: divide_eq_0_iff)
- with `feval xs e1 \<in> carrier R` `feval xs e2 \<in> carrier R`
+ with \<open>feval xs e1 \<in> carrier R\<close> \<open>feval xs e2 \<in> carrier R\<close>
show ?case by simp
qed (simp_all add: nonzero_union split: prod.split_asm)
@@ -623,17 +623,17 @@
show ?thesis
proof
assume "feval xs e = feval xs e'"
- with `feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d`
- `in_carrier xs` `nonzero xs (Cond e')`
+ with \<open>feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d\<close>
+ \<open>in_carrier xs\<close> \<open>nonzero xs (Cond e')\<close>
have "peval xs n \<oslash> peval xs d = \<zero>"
by (simp add: fexpr_in_carrier minus_eq r_neg)
- with `peval xs d \<noteq> \<zero>` `in_carrier xs`
+ with \<open>peval xs d \<noteq> \<zero>\<close> \<open>in_carrier xs\<close>
show "peval xs n = \<zero>"
by (simp add: divide_eq_0_iff)
next
assume "peval xs n = \<zero>"
- with `feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d` `peval xs d \<noteq> \<zero>`
- `nonzero xs (Cond e)` `nonzero xs (Cond e')` `in_carrier xs`
+ with \<open>feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d\<close> \<open>peval xs d \<noteq> \<zero>\<close>
+ \<open>nonzero xs (Cond e)\<close> \<open>nonzero xs (Cond e')\<close> \<open>in_carrier xs\<close>
show "feval xs e = feval xs e'"
by (simp add: eq_diff0 fexpr_in_carrier)
qed
@@ -652,7 +652,7 @@
definition field_codegen_aux :: "(pexpr \<times> pexpr list) itself" where
"field_codegen_aux = (Code_Evaluation.TERM_OF_EQUAL::(pexpr \<times> pexpr list) itself)"
-ML {*
+ML \<open>
signature FIELD_TAC =
sig
structure Field_Simps:
@@ -916,11 +916,11 @@
end);
end
-*}
+\<close>
context field begin
-local_setup {*
+local_setup \<open>
Local_Theory.declaration {syntax = false, pervasive = false}
(fn phi => Field_Tac.Field_Simps.map (Ring_Tac.insert_rules Field_Tac.eq_field_simps
(Morphism.term phi @{term R},
@@ -929,13 +929,13 @@
Morphism.fact phi @{thms nonzero.simps [meta] nonzero_singleton [meta]},
singleton (Morphism.fact phi) @{thm nth_el_Cons [meta]},
singleton (Morphism.fact phi) @{thm feval_eq}))))
-*}
+\<close>
end
-method_setup field = {*
+method_setup field = \<open>
Scan.lift (Args.mode "prems") -- Attrib.thms >> (fn (in_prem, thms) => fn ctxt =>
SIMPLE_METHOD' (Field_Tac.field_tac in_prem ctxt THEN' Ring_Tac.ring_tac in_prem thms ctxt))
-*} "reduce equations over fields to equations over rings"
+\<close> "reduce equations over fields to equations over rings"
end