--- a/src/Doc/Logics/document/HOL.tex Wed Feb 12 08:35:56 2014 +0100
+++ b/src/Doc/Logics/document/HOL.tex Wed Feb 12 08:35:56 2014 +0100
@@ -1435,7 +1435,7 @@
case $e$ of [] => $a$ | \(x\)\#\(xs\) => b
\end{center}
is defined by translation. For details see~{\S}\ref{sec:HOL:datatype}. There
-is also a case splitting rule \tdx{split_list_case}
+is also a case splitting rule \tdx{list.split}
\[
\begin{array}{l}
P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~
--- a/src/HOL/BNF_GFP.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/BNF_GFP.thy Wed Feb 12 08:35:56 2014 +0100
@@ -272,10 +272,10 @@
lemma nat_rec_Suc_imp: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
by auto
-lemma list_rec_Nil_imp: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
+lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
by auto
-lemma list_rec_Cons_imp: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
+lemma rec_list_Cons_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
by auto
lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
--- a/src/HOL/Decision_Procs/Approximation.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Feb 12 08:35:56 2014 +0100
@@ -3062,7 +3062,7 @@
case 0
then obtain ly uy
where *: "approx_tse prec 0 t ((l + u) * Float 1 -1) 1 f [Some (l, u)] = Some (ly, uy)"
- and **: "cmp ly uy" by (auto elim!: option_caseE)
+ and **: "cmp ly uy" by (auto elim!: case_optionE)
with 0 show ?case by auto
next
case (Suc s)
@@ -3163,7 +3163,7 @@
with assms obtain l u l' u'
where a: "approx prec a [None] = Some (l, u)"
and b: "approx prec b [None] = Some (l', u')"
- unfolding approx_tse_form_def by (auto elim!: option_caseE)
+ unfolding approx_tse_form_def by (auto elim!: case_optionE)
from Bound assms have "i = Var 0" unfolding approx_tse_form_def by auto
hence i: "interpret_floatarith i [x] = x" by auto
@@ -3198,10 +3198,10 @@
show ?thesis using AtLeastAtMost by auto
next
case (Bound x a b f') with assms
- show ?thesis by (auto elim!: option_caseE simp add: f_def approx_tse_form_def)
+ show ?thesis by (auto elim!: case_optionE simp add: f_def approx_tse_form_def)
next
case (Assign x a f') with assms
- show ?thesis by (auto elim!: option_caseE simp add: f_def approx_tse_form_def)
+ show ?thesis by (auto elim!: case_optionE simp add: f_def approx_tse_form_def)
qed } thus ?thesis unfolding f_def by auto
next
case Assign
--- a/src/HOL/HOLCF/Library/List_Cpo.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/HOLCF/Library/List_Cpo.thy Wed Feb 12 08:35:56 2014 +0100
@@ -165,7 +165,7 @@
shows "(\<Squnion>i. A i # B i) = (\<Squnion>i. A i) # (\<Squnion>i. B i)"
by (intro lub_eqI is_lub_Cons cpo_lubI A B)
-lemma cont2cont_list_case:
+lemma cont2cont_case_list:
assumes f: "cont (\<lambda>x. f x)"
assumes g: "cont (\<lambda>x. g x)"
assumes h1: "\<And>y ys. cont (\<lambda>x. h x y ys)"
@@ -186,17 +186,17 @@
apply (case_tac y, simp_all add: g h1)
done
-lemma cont2cont_list_case' [simp, cont2cont]:
+lemma cont2cont_case_list' [simp, cont2cont]:
assumes f: "cont (\<lambda>x. f x)"
assumes g: "cont (\<lambda>x. g x)"
assumes h: "cont (\<lambda>p. h (fst p) (fst (snd p)) (snd (snd p)))"
shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)"
-using assms by (simp add: cont2cont_list_case prod_cont_iff)
+using assms by (simp add: cont2cont_case_list prod_cont_iff)
text {* The simple version (due to Joachim Breitner) is needed if the
element type of the list is not a cpo. *}
-lemma cont2cont_list_case_simple [simp, cont2cont]:
+lemma cont2cont_case_list_simple [simp, cont2cont]:
assumes "cont (\<lambda>x. f1 x)"
assumes "\<And>y ys. cont (\<lambda>x. f2 x y ys)"
shows "cont (\<lambda>x. case l of [] \<Rightarrow> f1 x | y # ys \<Rightarrow> f2 x y ys)"
--- a/src/HOL/HOLCF/Library/Option_Cpo.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/HOLCF/Library/Option_Cpo.thy Wed Feb 12 08:35:56 2014 +0100
@@ -117,7 +117,7 @@
lemmas lub_Some = cont2contlubE [OF cont_Some, symmetric]
-lemma cont2cont_option_case:
+lemma cont2cont_case_option:
assumes f: "cont (\<lambda>x. f x)"
assumes g: "cont (\<lambda>x. g x)"
assumes h1: "\<And>a. cont (\<lambda>x. h x a)"
@@ -134,16 +134,16 @@
apply (case_tac y, simp_all add: g h1)
done
-lemma cont2cont_option_case' [simp, cont2cont]:
+lemma cont2cont_case_option' [simp, cont2cont]:
assumes f: "cont (\<lambda>x. f x)"
assumes g: "cont (\<lambda>x. g x)"
assumes h: "cont (\<lambda>p. h (fst p) (snd p))"
shows "cont (\<lambda>x. case f x of None \<Rightarrow> g x | Some a \<Rightarrow> h x a)"
-using assms by (simp add: cont2cont_option_case prod_cont_iff)
+using assms by (simp add: cont2cont_case_option prod_cont_iff)
text {* Simple version for when the element type is not a cpo. *}
-lemma cont2cont_option_case_simple [simp, cont2cont]:
+lemma cont2cont_case_option_simple [simp, cont2cont]:
assumes "cont (\<lambda>x. f x)"
assumes "\<And>a. cont (\<lambda>x. g x a)"
shows "cont (\<lambda>x. case z of None \<Rightarrow> f x | Some a \<Rightarrow> g x a)"
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Wed Feb 12 08:35:56 2014 +0100
@@ -459,7 +459,7 @@
else raise(''No empty clause''))
}"
-lemma effect_option_case:
+lemma effect_case_option:
assumes "effect (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
obtains "x = None" "effect n h h' r"
| y where "x = Some y" "effect (s y) h h' r"
@@ -500,7 +500,7 @@
}
with assms show ?thesis
unfolding res_thm2.simps get_clause_def
- by (elim effect_bindE effect_ifE effect_nthE effect_raiseE effect_returnE effect_option_case) auto
+ by (elim effect_bindE effect_ifE effect_nthE effect_raiseE effect_returnE effect_case_option) auto
qed
lemma foldM_Inv2:
@@ -543,7 +543,7 @@
show ?thesis
apply auto
apply (auto simp: get_clause_def elim!: effect_bindE effect_nthE)
- apply (auto elim!: effect_bindE effect_nthE effect_option_case effect_raiseE
+ apply (auto elim!: effect_bindE effect_nthE effect_case_option effect_raiseE
effect_returnE effect_updE)
apply (frule foldM_Inv2)
apply assumption
--- a/src/HOL/Import/HOL_Light_Maps.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Import/HOL_Light_Maps.thy Wed Feb 12 08:35:56 2014 +0100
@@ -230,7 +230,7 @@
lemma list_RECURSION:
"\<forall>nil' cons'. \<exists>fn\<Colon>'A list \<Rightarrow> 'Z. fn [] = nil' \<and> (\<forall>(a0\<Colon>'A) a1\<Colon>'A list. fn (a0 # a1) = cons' a0 a1 (fn a1))"
- by (intro allI, rule_tac x="list_rec nil' cons'" in exI) auto
+ by (intro allI, rule_tac x="rec_list nil' cons'" in exI) auto
lemma HD[import_const HD : List.hd]:
"hd ((h\<Colon>'A) # t) = h"
--- a/src/HOL/Lazy_Sequence.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Lazy_Sequence.thy Wed Feb 12 08:35:56 2014 +0100
@@ -71,8 +71,8 @@
"yield (Lazy_Sequence f) = f ()"
by (cases "f ()") (simp_all add: yield_def split_def)
-lemma case_yield_eq [simp]: "option_case g h (yield xq) =
- list_case g (\<lambda>x. curry h x \<circ> lazy_sequence_of_list) (list_of_lazy_sequence xq)"
+lemma case_yield_eq [simp]: "case_option g h (yield xq) =
+ case_list g (\<lambda>x. curry h x \<circ> lazy_sequence_of_list) (list_of_lazy_sequence xq)"
by (cases "list_of_lazy_sequence xq") (simp_all add: yield_def)
lemma lazy_sequence_size_code [code]:
--- a/src/HOL/Library/Countable.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Library/Countable.thy Wed Feb 12 08:35:56 2014 +0100
@@ -90,7 +90,7 @@
text {* Options *}
instance option :: (countable) countable
- by (rule countable_classI [of "option_case 0 (Suc \<circ> to_nat)"])
+ by (rule countable_classI [of "case_option 0 (Suc \<circ> to_nat)"])
(simp split: option.split_asm)
--- a/src/HOL/Matrix_LP/ComputeHOL.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Matrix_LP/ComputeHOL.thy Wed Feb 12 08:35:56 2014 +0100
@@ -62,25 +62,25 @@
lemma compute_None_None_eq: "(None = None) = True" by auto
lemma compute_Some_Some_eq: "(Some x = Some y) = (x = y)" by auto
-definition option_case_compute :: "'b option \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
- where "option_case_compute opt a f = option_case a f opt"
+definition case_option_compute :: "'b option \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
+ where "case_option_compute opt a f = case_option a f opt"
-lemma option_case_compute: "option_case = (\<lambda> a f opt. option_case_compute opt a f)"
- by (simp add: option_case_compute_def)
+lemma case_option_compute: "case_option = (\<lambda> a f opt. case_option_compute opt a f)"
+ by (simp add: case_option_compute_def)
-lemma option_case_compute_None: "option_case_compute None = (\<lambda> a f. a)"
+lemma case_option_compute_None: "case_option_compute None = (\<lambda> a f. a)"
apply (rule ext)+
- apply (simp add: option_case_compute_def)
+ apply (simp add: case_option_compute_def)
done
-lemma option_case_compute_Some: "option_case_compute (Some x) = (\<lambda> a f. f x)"
+lemma case_option_compute_Some: "case_option_compute (Some x) = (\<lambda> a f. f x)"
apply (rule ext)+
- apply (simp add: option_case_compute_def)
+ apply (simp add: case_option_compute_def)
done
-lemmas compute_option_case = option_case_compute option_case_compute_None option_case_compute_Some
+lemmas compute_case_option = case_option_compute case_option_compute_None case_option_compute_Some
-lemmas compute_option = compute_the compute_None_Some_eq compute_Some_None_eq compute_None_None_eq compute_Some_Some_eq compute_option_case
+lemmas compute_option = compute_the compute_None_Some_eq compute_Some_None_eq compute_None_None_eq compute_Some_Some_eq compute_case_option
(**** compute_list_length ****)
@@ -92,27 +92,27 @@
lemmas compute_list_length = length_nil length_cons
-(*** compute_list_case ***)
+(*** compute_case_list ***)
-definition list_case_compute :: "'b list \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b list \<Rightarrow> 'a) \<Rightarrow> 'a"
- where "list_case_compute l a f = list_case a f l"
+definition case_list_compute :: "'b list \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b list \<Rightarrow> 'a) \<Rightarrow> 'a"
+ where "case_list_compute l a f = case_list a f l"
-lemma list_case_compute: "list_case = (\<lambda> (a::'a) f (l::'b list). list_case_compute l a f)"
+lemma case_list_compute: "case_list = (\<lambda> (a::'a) f (l::'b list). case_list_compute l a f)"
apply (rule ext)+
- apply (simp add: list_case_compute_def)
+ apply (simp add: case_list_compute_def)
done
-lemma list_case_compute_empty: "list_case_compute ([]::'b list) = (\<lambda> (a::'a) f. a)"
+lemma case_list_compute_empty: "case_list_compute ([]::'b list) = (\<lambda> (a::'a) f. a)"
apply (rule ext)+
- apply (simp add: list_case_compute_def)
+ apply (simp add: case_list_compute_def)
done
-lemma list_case_compute_cons: "list_case_compute (u#v) = (\<lambda> (a::'a) f. (f (u::'b) v))"
+lemma case_list_compute_cons: "case_list_compute (u#v) = (\<lambda> (a::'a) f. (f (u::'b) v))"
apply (rule ext)+
- apply (simp add: list_case_compute_def)
+ apply (simp add: case_list_compute_def)
done
-lemmas compute_list_case = list_case_compute list_case_compute_empty list_case_compute_cons
+lemmas compute_case_list = case_list_compute case_list_compute_empty case_list_compute_cons
(*** compute_list_nth ***)
(* Of course, you will need computation with nats for this to work \<dots> *)
@@ -122,7 +122,7 @@
(*** compute_list ***)
-lemmas compute_list = compute_list_case compute_list_length compute_list_nth
+lemmas compute_list = compute_case_list compute_list_length compute_list_nth
(*** compute_let ***)
--- a/src/HOL/Matrix_LP/matrixlp.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Matrix_LP/matrixlp.ML Wed Feb 12 08:35:56 2014 +0100
@@ -11,7 +11,7 @@
structure MatrixLP : MATRIX_LP =
struct
-val compute_thms = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let"
+val compute_thms = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_case_list" "ComputeHOL.compute_let"
"ComputeHOL.compute_if" "ComputeFloat.arith" "SparseMatrix.sparse_row_matrix_arith_simps"
"ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
"SparseMatrix.sorted_sp_simps"
--- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Wed Feb 12 08:35:56 2014 +0100
@@ -766,7 +766,7 @@
bs: "set bs = Basis" "distinct bs"
by (metis finite_distinct_list)
from nonempty_Basis s obtain j where j: "j \<in> Basis" "s j \<in> S" by blast
- def y \<equiv> "list_rec
+ def y \<equiv> "rec_list
(s j)
(\<lambda>j _ Y. (\<Sum>i\<in>Basis. (if i = j then s i \<bullet> i else Y \<bullet> i) *\<^sub>R i))"
have "x = (\<Sum>i\<in>Basis. (if i \<in> set bs then s i \<bullet> i else s j \<bullet> i) *\<^sub>R i)"
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 12 08:35:56 2014 +0100
@@ -585,17 +585,17 @@
nitpick [expect = genuine]
oops
-lemma "option_rec n s None = n"
+lemma "rec_option n s None = n"
nitpick [expect = none]
apply simp
done
-lemma "option_rec n s (Some x) = s x"
+lemma "rec_option n s (Some x) = s x"
nitpick [expect = none]
apply simp
done
-lemma "P (option_rec n s x)"
+lemma "P (rec_option n s x)"
nitpick [expect = genuine]
oops
@@ -778,17 +778,17 @@
nitpick [expect = genuine]
oops
-lemma "list_rec nil cons [] = nil"
+lemma "rec_list nil cons [] = nil"
nitpick [card = 1\<emdash>5, expect = none]
apply simp
done
-lemma "list_rec nil cons (x#xs) = cons x xs (list_rec nil cons xs)"
+lemma "rec_list nil cons (x#xs) = cons x xs (rec_list nil cons xs)"
nitpick [card = 1\<emdash>5, expect = none]
apply simp
done
-lemma "P (list_rec nil cons xs)"
+lemma "P (rec_list nil cons xs)"
nitpick [expect = genuine]
oops
--- a/src/HOL/Nominal/Examples/Class3.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Nominal/Examples/Class3.thy Wed Feb 12 08:35:56 2014 +0100
@@ -3618,7 +3618,7 @@
apply(simp add: fresh_atm)
done
-lemma option_case_eqvt1[eqvt_force]:
+lemma case_option_eqvt1[eqvt_force]:
fixes pi1::"name prm"
and pi2::"coname prm"
and B::"(name\<times>trm) option"
@@ -3635,7 +3635,7 @@
apply(perm_simp)
done
-lemma option_case_eqvt2[eqvt_force]:
+lemma case_option_eqvt2[eqvt_force]:
fixes pi1::"name prm"
and pi2::"coname prm"
and B::"(coname\<times>trm) option"
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Wed Feb 12 08:35:56 2014 +0100
@@ -1245,7 +1245,7 @@
val Cons = Term.absfree sumx' (Term.absdummy sum_sbd_listT (Term.absfree rv_rec'
(HOLogic.mk_tuple (map4 mk_Cons ks ss zs zs'))));
- val rhs = mk_list_rec Nil Cons;
+ val rhs = mk_rec_list Nil Cons;
in
fold_rev (Term.absfree o Term.dest_Free) ss rhs
end;
@@ -1270,8 +1270,8 @@
mk_nthN n (Term.list_comb (Const (rv, rvT), ss) $ kl) i
end;
- val rv_Nils = flat (mk_rec_simps n @{thm list_rec_Nil_imp} [rv_def]);
- val rv_Conss = flat (mk_rec_simps n @{thm list_rec_Cons_imp} [rv_def]);
+ val rv_Nils = flat (mk_rec_simps n @{thm rec_list_Nil_imp} [rv_def]);
+ val rv_Conss = flat (mk_rec_simps n @{thm rec_list_Cons_imp} [rv_def]);
val beh_binds = mk_internal_bs behN;
fun beh_bind i = nth beh_binds (i - 1);
--- a/src/HOL/Tools/BNF/bnf_gfp_util.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_util.ML Wed Feb 12 08:35:56 2014 +0100
@@ -22,12 +22,12 @@
val mk_in_rel: term -> term
val mk_equiv: term -> term -> term
val mk_fromCard: term -> term -> term
- val mk_list_rec: term -> term -> term
val mk_nat_rec: term -> term -> term
val mk_prefCl: term -> term
val mk_prefixeq: term -> term -> term
val mk_proj: term -> term
val mk_quotient: term -> term -> term
+ val mk_rec_list: term -> term -> term
val mk_shift: term -> term -> term
val mk_size: term -> term
val mk_toCard: term -> term -> term
@@ -150,12 +150,12 @@
let val T = fastype_of Zero;
in Const (@{const_name nat_rec}, T --> fastype_of Suc --> HOLogic.natT --> T) $ Zero $ Suc end;
-fun mk_list_rec Nil Cons =
+fun mk_rec_list Nil Cons =
let
val T = fastype_of Nil;
val (U, consT) = `(Term.domain_type) (fastype_of Cons);
in
- Const (@{const_name list_rec}, T --> consT --> HOLogic.listT U --> T) $ Nil $ Cons
+ Const (@{const_name rec_list}, T --> consT --> HOLogic.listT U --> T) $ Nil $ Cons
end;
fun mk_InN_not_InM 1 _ = @{thm Inl_not_Inr}
--- a/src/HOL/ex/Refute_Examples.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/ex/Refute_Examples.thy Wed Feb 12 08:35:56 2014 +0100
@@ -547,15 +547,15 @@
refute [expect = genuine]
oops
-lemma "option_rec n s None = n"
+lemma "rec_option n s None = n"
refute [expect = none]
by simp
-lemma "option_rec n s (Some x) = s x"
+lemma "rec_option n s (Some x) = s x"
refute [maxsize = 4, expect = none]
by simp
-lemma "P (option_rec n s x)"
+lemma "P (rec_option n s x)"
refute [expect = genuine]
oops
@@ -764,15 +764,15 @@
refute [expect = potential]
oops
-lemma "list_rec nil cons [] = nil"
+lemma "rec_list nil cons [] = nil"
refute [maxsize = 3, expect = none]
by simp
-lemma "list_rec nil cons (x#xs) = cons x xs (list_rec nil cons xs)"
+lemma "rec_list nil cons (x#xs) = cons x xs (rec_list nil cons xs)"
refute [maxsize = 2, expect = none]
by simp
-lemma "P (list_rec nil cons xs)"
+lemma "P (rec_list nil cons xs)"
refute [expect = potential]
oops
--- a/src/HOL/ex/Tree23.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/ex/Tree23.thy Wed Feb 12 08:35:56 2014 +0100
@@ -331,7 +331,7 @@
lemmas dfull_case_intros =
ord.exhaust [where y=y and P="dfull a (ord_case b c d y)"]
- option.exhaust [where y=y and P="dfull a (option_case b c y)"]
+ option.exhaust [of y "dfull a (case_option b c y)"]
prod.exhaust [where y=y and P="dfull a (prod_case b y)"]
bool.exhaust [where y=y and P="dfull a (bool_case b c y)"]
tree23.exhaust [where y=y and P="dfull a (Some (b, tree23_case c d e y))"]