# HG changeset patch # User blanchet # Date 1392190556 -3600 # Node ID a8e96847523c38f661c08f7bba47fb3dd2a57ac9 # Parent eb2caacf3ba47cf9e18df1016901faeda5e282e4 adapted theories to '{case,rec}_{list,option}' names diff -r eb2caacf3ba4 -r a8e96847523c src/Doc/Logics/document/HOL.tex --- 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{|}~ diff -r eb2caacf3ba4 -r a8e96847523c src/HOL/BNF_GFP.thy --- 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) \ 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) \ f [] = f1" +lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \ f [] = f1" by auto -lemma list_rec_Cons_imp: "f = list_rec f1 (%x xs rec. f2 x xs rec) \ f (x # xs) = f2 x xs (f xs)" +lemma rec_list_Cons_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \ f (x # xs) = f2 x xs (f xs)" by auto lemma not_arg_cong_Inr: "x \ y \ Inr x \ Inr y" diff -r eb2caacf3ba4 -r a8e96847523c src/HOL/Decision_Procs/Approximation.thy --- 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 diff -r eb2caacf3ba4 -r a8e96847523c src/HOL/HOLCF/Library/List_Cpo.thy --- 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 "(\i. A i # B i) = (\i. A i) # (\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 (\x. f x)" assumes g: "cont (\x. g x)" assumes h1: "\y ys. cont (\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 (\x. f x)" assumes g: "cont (\x. g x)" assumes h: "cont (\p. h (fst p) (fst (snd p)) (snd (snd p)))" shows "cont (\x. case f x of [] \ g x | y # ys \ 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 (\x. f1 x)" assumes "\y ys. cont (\x. f2 x y ys)" shows "cont (\x. case l of [] \ f1 x | y # ys \ f2 x y ys)" diff -r eb2caacf3ba4 -r a8e96847523c src/HOL/HOLCF/Library/Option_Cpo.thy --- 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 (\x. f x)" assumes g: "cont (\x. g x)" assumes h1: "\a. cont (\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 (\x. f x)" assumes g: "cont (\x. g x)" assumes h: "cont (\p. h (fst p) (snd p))" shows "cont (\x. case f x of None \ g x | Some a \ 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 (\x. f x)" assumes "\a. cont (\x. g x a)" shows "cont (\x. case z of None \ f x | Some a \ g x a)" diff -r eb2caacf3ba4 -r a8e96847523c src/HOL/Imperative_HOL/ex/SatChecker.thy --- 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 \ n | Some y \ 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 diff -r eb2caacf3ba4 -r a8e96847523c src/HOL/Import/HOL_Light_Maps.thy --- 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: "\nil' cons'. \fn\'A list \ 'Z. fn [] = nil' \ (\(a0\'A) a1\'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\'A) # t) = h" diff -r eb2caacf3ba4 -r a8e96847523c src/HOL/Lazy_Sequence.thy --- 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 (\x. curry h x \ lazy_sequence_of_list) (list_of_lazy_sequence xq)" +lemma case_yield_eq [simp]: "case_option g h (yield xq) = + case_list g (\x. curry h x \ 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]: diff -r eb2caacf3ba4 -r a8e96847523c src/HOL/Library/Countable.thy --- 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 \ to_nat)"]) + by (rule countable_classI [of "case_option 0 (Suc \ to_nat)"]) (simp split: option.split_asm) diff -r eb2caacf3ba4 -r a8e96847523c src/HOL/Matrix_LP/ComputeHOL.thy --- 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 \ 'a \ ('b \ 'a) \ 'a" - where "option_case_compute opt a f = option_case a f opt" +definition case_option_compute :: "'b option \ 'a \ ('b \ 'a) \ 'a" + where "case_option_compute opt a f = case_option a f opt" -lemma option_case_compute: "option_case = (\ a f opt. option_case_compute opt a f)" - by (simp add: option_case_compute_def) +lemma case_option_compute: "case_option = (\ 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 = (\ a f. a)" +lemma case_option_compute_None: "case_option_compute None = (\ 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) = (\ a f. f x)" +lemma case_option_compute_Some: "case_option_compute (Some x) = (\ 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 \ 'a \ ('b \ 'b list \ 'a) \ 'a" - where "list_case_compute l a f = list_case a f l" +definition case_list_compute :: "'b list \ 'a \ ('b \ 'b list \ 'a) \ 'a" + where "case_list_compute l a f = case_list a f l" -lemma list_case_compute: "list_case = (\ (a::'a) f (l::'b list). list_case_compute l a f)" +lemma case_list_compute: "case_list = (\ (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) = (\ (a::'a) f. a)" +lemma case_list_compute_empty: "case_list_compute ([]::'b list) = (\ (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) = (\ (a::'a) f. (f (u::'b) v))" +lemma case_list_compute_cons: "case_list_compute (u#v) = (\ (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 \ *) @@ -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 ***) diff -r eb2caacf3ba4 -r a8e96847523c src/HOL/Matrix_LP/matrixlp.ML --- 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" diff -r eb2caacf3ba4 -r a8e96847523c src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy --- 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 \ Basis" "s j \ S" by blast - def y \ "list_rec + def y \ "rec_list (s j) (\j _ Y. (\i\Basis. (if i = j then s i \ i else Y \ i) *\<^sub>R i))" have "x = (\i\Basis. (if i \ set bs then s i \ i else s j \ i) *\<^sub>R i)" diff -r eb2caacf3ba4 -r a8e96847523c src/HOL/Nitpick_Examples/Refute_Nits.thy --- 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\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\5, expect = none] apply simp done -lemma "P (list_rec nil cons xs)" +lemma "P (rec_list nil cons xs)" nitpick [expect = genuine] oops diff -r eb2caacf3ba4 -r a8e96847523c src/HOL/Nominal/Examples/Class3.thy --- 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\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\trm) option" diff -r eb2caacf3ba4 -r a8e96847523c src/HOL/Tools/BNF/bnf_gfp.ML --- 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); diff -r eb2caacf3ba4 -r a8e96847523c src/HOL/Tools/BNF/bnf_gfp_util.ML --- 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} diff -r eb2caacf3ba4 -r a8e96847523c src/HOL/ex/Refute_Examples.thy --- 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 diff -r eb2caacf3ba4 -r a8e96847523c src/HOL/ex/Tree23.thy --- 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))"]