# HG changeset patch # User blanchet # Date 1392190626 -3600 # Node ID 01fbfb60c33e6b63cade9010a792492f46d2fda2 # Parent dd7992d4a61a2db7671562e20cef284d340f1b8d adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx' diff -r dd7992d4a61a -r 01fbfb60c33e src/Doc/LaTeXsugar/Sugar.thy --- a/src/Doc/LaTeXsugar/Sugar.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/Doc/LaTeXsugar/Sugar.thy Wed Feb 12 08:37:06 2014 +0100 @@ -166,9 +166,9 @@ \end{quote} To support the ``\_''-notation for irrelevant variables the constant \texttt{DUMMY} has been introduced: -@{thm fst_conv[where b = DUMMY]} is produced by +@{thm fst_conv[of _ DUMMY]} is produced by \begin{quote} -\verb!@!\verb!{thm fst_conv[where b = DUMMY]}! +\verb!@!\verb!{thm fst_conv[of _ DUMMY]}! \end{quote} Variables that are bound by quantifiers or lambdas cannot be renamed like this. Instead, the attribute \texttt{rename\_abs} does the diff -r dd7992d4a61a -r 01fbfb60c33e src/Doc/ProgProve/Isar.thy --- a/src/Doc/ProgProve/Isar.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/Doc/ProgProve/Isar.thy Wed Feb 12 08:37:06 2014 +0100 @@ -636,8 +636,8 @@ thus ?thesis by simp qed -text{*\index{cases@@{text"cases"}|(}Function @{text tl} (''tail'') is defined by @{thm tl.simps(1)} and -@{thm tl.simps(2)}. Note that the result type of @{const length} is @{typ nat} +text{*\index{cases@@{text"cases"}|(}Function @{text tl} (''tail'') is defined by @{thm list.sel(2)} and +@{thm list.sel(3)}. Note that the result type of @{const length} is @{typ nat} and @{prop"0 - 1 = (0::nat)"}. This proof pattern works for any term @{text t} whose type is a datatype. diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Auth/Guard/Extensions.thy --- a/src/HOL/Auth/Guard/Extensions.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Auth/Guard/Extensions.thy Wed Feb 12 08:37:06 2014 +0100 @@ -410,6 +410,7 @@ lemma knows_sub_app: "knows A evs <= knows A (evs @ evs')" apply (induct evs, auto) apply (simp add: knows_decomp) +apply (rename_tac a b c) by (case_tac a, auto simp: knows.simps) subsubsection{*maximum knowledge an agent can have @@ -504,7 +505,8 @@ by (induct evs, auto split: event.split) lemma used'_parts [rule_format]: "X:used' evs ==> Y:parts {X} --> Y:used' evs" -apply (induct evs, simp) +apply (induct evs, simp) +apply (rename_tac a b) apply (case_tac a, simp_all) apply (blast dest: parts_trans)+; done @@ -521,7 +523,7 @@ by (auto dest: used_sub_Cons [THEN subsetD]) lemma used_appD [dest]: "X:used (evs @ evs') ==> X:used evs | X:used evs'" -by (induct evs, auto, case_tac a, auto) +by (induct evs, auto, rename_tac a b, case_tac a, auto) lemma used_ConsD: "X:used (ev#evs) ==> X:used [ev] | X:used evs" by (case_tac ev, auto) @@ -572,6 +574,7 @@ apply (case_tac "A=Spy", blast) apply (induct evs) apply (simp add: used.simps, blast) +apply (rename_tac a evs) apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify) apply (drule_tac P="%G. X:parts G" in knows_Cons_substD, safe) apply (erule initState_used) @@ -585,6 +588,7 @@ apply force apply (induct evs) apply (simp add: knows_max_def used.simps, blast) +apply (rename_tac a evs) apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify) apply (drule_tac P="%G. X:parts G" in knows_max_Cons_substD, safe) apply (case_tac a, auto) diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Auth/Guard/Guard.thy --- a/src/HOL/Auth/Guard/Guard.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Auth/Guard/Guard.thy Wed Feb 12 08:37:06 2014 +0100 @@ -228,6 +228,7 @@ lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l" apply (induct l) apply (rule_tac x="[]" in exI, simp, clarsimp) +apply (rename_tac a b l') apply (subgoal_tac "EX l''. kparts {a} = set l'' & cnb l'' = crypt_nb a", clarify) apply (rule_tac x="l''@l'" in exI, simp) apply (rule kparts_insert_substI, simp) diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Auth/Guard/GuardK.thy --- a/src/HOL/Auth/Guard/GuardK.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Auth/Guard/GuardK.thy Wed Feb 12 08:37:06 2014 +0100 @@ -222,6 +222,7 @@ lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l" apply (induct l) apply (rule_tac x="[]" in exI, simp, clarsimp) +apply (rename_tac a b l') apply (subgoal_tac "EX l''. kparts {a} = set l'' & cnb l'' = crypt_nb a", clarify) apply (rule_tac x="l''@l'" in exI, simp) apply (rule kparts_insert_substI, simp) diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Auth/KerberosIV.thy --- a/src/HOL/Auth/KerberosIV.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Auth/KerberosIV.thy Wed Feb 12 08:37:06 2014 +0100 @@ -256,23 +256,27 @@ lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)" apply (induct_tac "evs") -apply (induct_tac [2] "a", auto) +apply (rename_tac [2] a b) +apply (induct_tac [2] a, auto) done lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs" apply (induct_tac "evs") -apply (induct_tac [2] "a", auto) +apply (rename_tac [2] a b) +apply (induct_tac [2] a, auto) done lemma spies_Notes_rev: "spies (evs @ [Notes A X]) = (if A:bad then insert X (spies evs) else spies evs)" apply (induct_tac "evs") -apply (induct_tac [2] "a", auto) +apply (rename_tac [2] a b) +apply (induct_tac [2] a, auto) done lemma spies_evs_rev: "spies evs = spies (rev evs)" apply (induct_tac "evs") -apply (induct_tac [2] "a") +apply (rename_tac [2] a b) +apply (induct_tac [2] a) apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev) done @@ -280,6 +284,7 @@ lemma spies_takeWhile: "spies (takeWhile P evs) <= spies evs" apply (induct_tac "evs") +apply (rename_tac [2] a b) apply (induct_tac [2] "a", auto) txt{* Resembles @{text"used_subset_append"} in theory Event.*} done @@ -407,6 +412,7 @@ lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \ (used evs)" apply (induct_tac "evs") apply simp +apply (rename_tac a b) apply (induct_tac "a") apply auto done @@ -414,6 +420,7 @@ lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \ (used evs)" apply (induct_tac "evs") apply simp +apply (rename_tac a b) apply (induct_tac "a") apply auto done @@ -421,6 +428,7 @@ lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs" apply (induct_tac "evs") apply simp +apply (rename_tac a b) apply (induct_tac "a") apply auto done @@ -428,6 +436,7 @@ lemma used_evs_rev: "used evs = used (rev evs)" apply (induct_tac "evs") apply simp +apply (rename_tac a b) apply (induct_tac "a") apply (simp add: used_Says_rev) apply (simp add: used_Gets_rev) @@ -438,6 +447,7 @@ "x : used (takeWhile P X) --> x : used X" apply (induct_tac "X") apply simp +apply (rename_tac a b) apply (induct_tac "a") apply (simp_all add: used_Nil) apply (blast dest!: initState_into_used)+ diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Auth/KerberosV.thy --- a/src/HOL/Auth/KerberosV.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Auth/KerberosV.thy Wed Feb 12 08:37:06 2014 +0100 @@ -207,22 +207,26 @@ lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)" apply (induct_tac "evs") +apply (rename_tac [2] a b) apply (induct_tac [2] "a", auto) done lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs" apply (induct_tac "evs") +apply (rename_tac [2] a b) apply (induct_tac [2] "a", auto) done lemma spies_Notes_rev: "spies (evs @ [Notes A X]) = (if A:bad then insert X (spies evs) else spies evs)" apply (induct_tac "evs") +apply (rename_tac [2] a b) apply (induct_tac [2] "a", auto) done lemma spies_evs_rev: "spies evs = spies (rev evs)" apply (induct_tac "evs") +apply (rename_tac [2] a b) apply (induct_tac [2] "a") apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev) done @@ -231,6 +235,7 @@ lemma spies_takeWhile: "spies (takeWhile P evs) <= spies evs" apply (induct_tac "evs") +apply (rename_tac [2] a b) apply (induct_tac [2] "a", auto) txt{* Resembles @{text"used_subset_append"} in theory Event.*} done diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Auth/Kerberos_BAN.thy --- a/src/HOL/Auth/Kerberos_BAN.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Auth/Kerberos_BAN.thy Wed Feb 12 08:37:06 2014 +0100 @@ -139,22 +139,26 @@ lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)" apply (induct_tac "evs") +apply (rename_tac [2] a b) apply (induct_tac [2] "a", auto) done lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs" apply (induct_tac "evs") +apply (rename_tac [2] a b) apply (induct_tac [2] "a", auto) done lemma spies_Notes_rev: "spies (evs @ [Notes A X]) = (if A:bad then insert X (spies evs) else spies evs)" apply (induct_tac "evs") +apply (rename_tac [2] a b) apply (induct_tac [2] "a", auto) done lemma spies_evs_rev: "spies evs = spies (rev evs)" apply (induct_tac "evs") +apply (rename_tac [2] a b) apply (induct_tac [2] "a") apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev) done @@ -163,6 +167,7 @@ lemma spies_takeWhile: "spies (takeWhile P evs) <= spies evs" apply (induct_tac "evs") +apply (rename_tac [2] a b) apply (induct_tac [2] "a", auto) txt{* Resembles @{text"used_subset_append"} in theory Event.*} done @@ -174,6 +179,7 @@ lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \ (used evs)" apply (induct_tac "evs") apply simp +apply (rename_tac a b) apply (induct_tac "a") apply auto done @@ -181,6 +187,7 @@ lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \ (used evs)" apply (induct_tac "evs") apply simp +apply (rename_tac a b) apply (induct_tac "a") apply auto done @@ -188,6 +195,7 @@ lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs" apply (induct_tac "evs") apply simp +apply (rename_tac a b) apply (induct_tac "a") apply auto done @@ -195,6 +203,7 @@ lemma used_evs_rev: "used evs = used (rev evs)" apply (induct_tac "evs") apply simp +apply (rename_tac a b) apply (induct_tac "a") apply (simp add: used_Says_rev) apply (simp add: used_Gets_rev) @@ -205,6 +214,7 @@ "x : used (takeWhile P X) --> x : used X" apply (induct_tac "X") apply simp +apply (rename_tac a b) apply (induct_tac "a") apply (simp_all add: used_Nil) apply (blast dest!: initState_into_used)+ diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Auth/Kerberos_BAN_Gets.thy --- a/src/HOL/Auth/Kerberos_BAN_Gets.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy Wed Feb 12 08:37:06 2014 +0100 @@ -168,6 +168,7 @@ lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \ (used evs)" apply (induct_tac "evs") apply simp +apply (rename_tac a b) apply (induct_tac "a") apply auto done @@ -175,6 +176,7 @@ lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \ (used evs)" apply (induct_tac "evs") apply simp +apply (rename_tac a b) apply (induct_tac "a") apply auto done @@ -182,6 +184,7 @@ lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs" apply (induct_tac "evs") apply simp +apply (rename_tac a b) apply (induct_tac "a") apply auto done @@ -189,6 +192,7 @@ lemma used_evs_rev: "used evs = used (rev evs)" apply (induct_tac "evs") apply simp +apply (rename_tac a b) apply (induct_tac "a") apply (simp add: used_Says_rev) apply (simp add: used_Gets_rev) @@ -199,6 +203,7 @@ "x : used (takeWhile P X) --> x : used X" apply (induct_tac "X") apply simp +apply (rename_tac a b) apply (induct_tac "a") apply (simp_all add: used_Nil) apply (blast dest!: initState_into_used)+ diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Auth/NS_Shared.thy Wed Feb 12 08:37:06 2014 +0100 @@ -385,22 +385,26 @@ lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)" apply (induct_tac "evs") +apply (rename_tac [2] a b) apply (induct_tac [2] "a", auto) done lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs" apply (induct_tac "evs") +apply (rename_tac [2] a b) apply (induct_tac [2] "a", auto) done lemma spies_Notes_rev: "spies (evs @ [Notes A X]) = (if A:bad then insert X (spies evs) else spies evs)" apply (induct_tac "evs") +apply (rename_tac [2] a b) apply (induct_tac [2] "a", auto) done lemma spies_evs_rev: "spies evs = spies (rev evs)" apply (induct_tac "evs") +apply (rename_tac [2] a b) apply (induct_tac [2] "a") apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev) done @@ -409,6 +413,7 @@ lemma spies_takeWhile: "spies (takeWhile P evs) <= spies evs" apply (induct_tac "evs") +apply (rename_tac [2] a b) apply (induct_tac [2] "a", auto) txt{* Resembles @{text"used_subset_append"} in theory Event.*} done diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Auth/TLS.thy --- a/src/HOL/Auth/TLS.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Auth/TLS.thy Wed Feb 12 08:37:06 2014 +0100 @@ -81,7 +81,7 @@ inj_sessionK: "inj sessionK" --{*sessionK is collision-free; also, no clientK clashes with any serverK.*} apply (rule exI [of _ - "%((x,y,z), r). prod_encode(role_case 0 1 r, + "%((x,y,z), r). prod_encode(case_role 0 1 r, prod_encode(x, prod_encode(y,z)))"]) apply (simp add: inj_on_def prod_encode_eq split: role.split) done diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy --- a/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy Wed Feb 12 08:37:06 2014 +0100 @@ -860,7 +860,7 @@ have "subtr (insert n ?ns1) (f (last (n1 # nl))) (f n)" using f subtr.Step[OF _ fn1_flast fn1] by auto thus ?case unfolding 1 by simp -qed (metis f hd.simps last_ConsL last_in_set not_Cons_self2 subtr.Refl) +qed (metis f list.sel(1) last_ConsL last_in_set not_Cons_self2 subtr.Refl) lemma reg_subtr_path_aux: assumes f: "reg f tr" and n: "subtr ns tr1 tr" @@ -878,7 +878,7 @@ obtain nl where nl: "path f nl" and f_nl: "f (hd nl) = tr1" and last_nl: "f (last nl) = tr2" and set: "set nl \ ns" using Step(3)[OF tr1] by auto have 0: "path f (root tr # nl)" apply (subst path.simps) - using f_nl nl reg_root tr tr1_tr by (metis hd.simps neq_Nil_conv) + using f_nl nl reg_root tr tr1_tr by (metis list.sel(1) neq_Nil_conv) show ?case apply(rule exI[of _ "(root tr) # nl"]) using 0 reg_root tr last_nl nl path_NE rtr set by auto qed diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Bali/Conform.thy --- a/src/HOL/Bali/Conform.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Bali/Conform.thy Wed Feb 12 08:37:06 2014 +0100 @@ -437,9 +437,10 @@ lemma conforms_absorb [rule_format]: "(a, b)\\(G, L) \ (absorb j a, b)\\(G, L)" apply (rule impI) -apply ( case_tac a) +apply (case_tac a) apply (case_tac "absorb j a") apply auto +apply (rename_tac a) apply (case_tac "absorb j (Some a)",auto) apply (erule conforms_NormI) done @@ -554,5 +555,4 @@ apply (force dest: conforms_globsD)+ done - end diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Bali/Eval.thy --- a/src/HOL/Bali/Eval.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Bali/Eval.thy Wed Feb 12 08:37:06 2014 +0100 @@ -141,7 +141,7 @@ where "\es\\<^sub>l == In3 es" definition undefined3 :: "('al + 'ar, 'b, 'c) sum3 \ vals" where - "undefined3 = sum3_case (In1 \ case_sum (\x. undefined) (\x. Unit)) + "undefined3 = case_sum3 (In1 \ case_sum (\x. undefined) (\x. Unit)) (\x. In2 undefined) (\x. In3 undefined)" lemma [simp]: "undefined3 (In1l x) = In1 undefined" diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Bali/State.thy --- a/src/HOL/Bali/State.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Bali/State.thy Wed Feb 12 08:37:06 2014 +0100 @@ -232,11 +232,11 @@ definition globs :: "st \ globs" - where "globs = st_case (\g l. g)" + where "globs = case_st (\g l. g)" definition locals :: "st \ locals" - where "locals = st_case (\g l. l)" + where "locals = case_st (\g l. l)" definition heap :: "st \ heap" where "heap s = globs s \ Heap" @@ -303,19 +303,19 @@ definition gupd :: "oref \ obj \ st \ st" ("gupd'(_\_')" [10, 10] 1000) - where "gupd r obj = st_case (\g l. st (g(r\obj)) l)" + where "gupd r obj = case_st (\g l. st (g(r\obj)) l)" definition lupd :: "lname \ val \ st \ st" ("lupd'(_\_')" [10, 10] 1000) - where "lupd vn v = st_case (\g l. st g (l(vn\v)))" + where "lupd vn v = case_st (\g l. st g (l(vn\v)))" definition upd_gobj :: "oref \ vn \ val \ st \ st" - where "upd_gobj r n v = st_case (\g l. st (chg_map (upd_obj n v) r g) l)" + where "upd_gobj r n v = case_st (\g l. st (chg_map (upd_obj n v) r g) l)" definition set_locals :: "locals \ st \ st" - where "set_locals l = st_case (\g l'. st g l)" + where "set_locals l = case_st (\g l'. st g l)" definition init_obj :: "prog \ obj_tag \ oref \ st \ st" diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Bali/TypeSafe.thy --- a/src/HOL/Bali/TypeSafe.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Bali/TypeSafe.thy Wed Feb 12 08:37:06 2014 +0100 @@ -825,7 +825,7 @@ lemma lconf_map_lname [simp]: - "G,s\(lname_case l1 l2)[\\](lname_case L1 L2) + "G,s\(case_lname l1 l2)[\\](case_lname L1 L2) = (G,s\l1[\\]L1 \ G,s\(\x::unit . l2)[\\](\x::unit. L2))" apply (unfold lconf_def) @@ -833,7 +833,7 @@ done lemma wlconf_map_lname [simp]: - "G,s\(lname_case l1 l2)[\\\](lname_case L1 L2) + "G,s\(case_lname l1 l2)[\\\](case_lname L1 L2) = (G,s\l1[\\\]L1 \ G,s\(\x::unit . l2)[\\\](\x::unit. L2))" apply (unfold wlconf_def) @@ -841,7 +841,7 @@ done lemma lconf_map_ename [simp]: - "G,s\(ename_case l1 l2)[\\](ename_case L1 L2) + "G,s\(case_ename l1 l2)[\\](case_ename L1 L2) = (G,s\l1[\\]L1 \ G,s\(\x::unit. l2)[\\](\x::unit. L2))" apply (unfold lconf_def) @@ -849,7 +849,7 @@ done lemma wlconf_map_ename [simp]: - "G,s\(ename_case l1 l2)[\\\](ename_case L1 L2) + "G,s\(case_ename l1 l2)[\\\](case_ename L1 L2) = (G,s\l1[\\\]L1 \ G,s\(\x::unit. l2)[\\\](\x::unit. L2))" apply (unfold wlconf_def) @@ -1436,9 +1436,9 @@ lemma dom_vname_split: - "dom (lname_case (ename_case (tab(x\y)(xs[\]ys)) a) b) - = dom (lname_case (ename_case (tab(x\y)) a) b) \ - dom (lname_case (ename_case (tab(xs[\]ys)) a) b)" + "dom (case_lname (case_ename (tab(x\y)(xs[\]ys)) a) b) + = dom (case_lname (case_ename (tab(x\y)) a) b) \ + dom (case_lname (case_ename (tab(xs[\]ys)) a) b)" (is "?List x xs y ys = ?Hd x y \ ?Tl xs ys") proof show "?List x xs y ys \ ?Hd x y \ ?Tl xs ys" @@ -1514,37 +1514,37 @@ qed qed -lemma dom_ename_case_None_simp: - "dom (ename_case vname_tab None) = VNam ` (dom vname_tab)" +lemma dom_case_ename_None_simp: + "dom (case_ename vname_tab None) = VNam ` (dom vname_tab)" apply (auto simp add: dom_def image_def ) apply (case_tac "x") apply auto done -lemma dom_ename_case_Some_simp: - "dom (ename_case vname_tab (Some a)) = VNam ` (dom vname_tab) \ {Res}" +lemma dom_case_ename_Some_simp: + "dom (case_ename vname_tab (Some a)) = VNam ` (dom vname_tab) \ {Res}" apply (auto simp add: dom_def image_def ) apply (case_tac "x") apply auto done -lemma dom_lname_case_None_simp: - "dom (lname_case ename_tab None) = EName ` (dom ename_tab)" +lemma dom_case_lname_None_simp: + "dom (case_lname ename_tab None) = EName ` (dom ename_tab)" apply (auto simp add: dom_def image_def ) apply (case_tac "x") apply auto done -lemma dom_lname_case_Some_simp: - "dom (lname_case ename_tab (Some a)) = EName ` (dom ename_tab) \ {This}" +lemma dom_case_lname_Some_simp: + "dom (case_lname ename_tab (Some a)) = EName ` (dom ename_tab) \ {This}" apply (auto simp add: dom_def image_def) apply (case_tac "x") apply auto done -lemmas dom_lname_ename_case_simps = - dom_ename_case_None_simp dom_ename_case_Some_simp - dom_lname_case_None_simp dom_lname_case_Some_simp +lemmas dom_lname_case_ename_simps = + dom_case_ename_None_simp dom_case_ename_Some_simp + dom_case_lname_None_simp dom_case_lname_Some_simp lemma image_comp: "f ` g ` A = (f \ g) ` A" @@ -1569,13 +1569,13 @@ with static_m' dom_vnames m show ?thesis by (cases s) (simp add: init_lvars_def Let_def parameters_def - dom_lname_ename_case_simps image_comp) + dom_lname_case_ename_simps image_comp) next case False with static_m' dom_vnames m show ?thesis by (cases s) (simp add: init_lvars_def Let_def parameters_def - dom_lname_ename_case_simps image_comp) + dom_lname_case_ename_simps image_comp) qed qed diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Datatype.thy Wed Feb 12 08:37:06 2014 +0100 @@ -133,7 +133,7 @@ lemma Node_Push_I: "p: Node ==> apfst (Push i) p : Node" apply (simp add: Node_def Push_def) -apply (fast intro!: apfst_conv case_nat_Suc [THEN trans]) +apply (fast intro!: apfst_conv nat.cases(2)[THEN trans]) done diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Decision_Procs/Cooper.thy Wed Feb 12 08:37:06 2014 +0100 @@ -303,12 +303,12 @@ lemma evaldjf_bound0: assumes nb: "\x\ set xs. bound0 (f x)" shows "bound0 (evaldjf f xs)" - using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto) + using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f x1", auto) lemma evaldjf_qf: assumes nb: "\x\ set xs. qfree (f x)" shows "qfree (evaldjf f xs)" - using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto) + using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f x1", auto) fun disjuncts :: "fm \ fm list" where diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Decision_Procs/Ferrack.thy --- a/src/HOL/Decision_Procs/Ferrack.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Decision_Procs/Ferrack.thy Wed Feb 12 08:37:06 2014 +0100 @@ -328,12 +328,12 @@ lemma evaldjf_bound0: assumes nb: "\ x\ set xs. bound0 (f x)" shows "bound0 (evaldjf f xs)" - using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) + using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto) lemma evaldjf_qf: assumes nb: "\ x\ set xs. qfree (f x)" shows "qfree (evaldjf f xs)" - using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) + using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto) fun disjuncts :: "fm \ fm list" where "disjuncts (Or p q) = disjuncts p @ disjuncts q" diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Feb 12 08:37:06 2014 +0100 @@ -761,12 +761,12 @@ lemma evaldjf_bound0: assumes nb: "\ x\ set xs. bound0 (f x)" shows "bound0 (evaldjf f xs)" - using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) + using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto) lemma evaldjf_qf: assumes nb: "\ x\ set xs. qfree (f x)" shows "qfree (evaldjf f xs)" - using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) + using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto) fun disjuncts :: "fm \ fm list" where "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)" @@ -3003,5 +3003,3 @@ oops *) end - - diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Decision_Procs/Polynomial_List.thy --- a/src/HOL/Decision_Procs/Polynomial_List.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy Wed Feb 12 08:37:06 2014 +0100 @@ -919,6 +919,7 @@ "last ((a %* p) +++ (x#(b %* p))) = (if p = [] then x else b * last p)" apply (induct p arbitrary: a x b) apply auto + apply (rename_tac a p aa x b) apply (subgoal_tac "padd (cmult aa p) (times b a # cmult b p) \ []") apply simp apply (induct_tac p) @@ -1042,6 +1043,7 @@ lemma poly_mono: "abs(x) \ k \ abs(poly p (x::'a::{linordered_idom})) \ poly (map abs p) k" apply (induct p) apply auto + apply (rename_tac a p) apply (rule_tac y = "abs a + abs (x * poly p x)" in order_trans) apply (rule abs_triangle_ineq) apply (auto intro!: mult_mono simp add: abs_mult) diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/HOLCF/Lift.thy --- a/src/HOL/HOLCF/Lift.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/HOLCF/Lift.thy Wed Feb 12 08:37:06 2014 +0100 @@ -71,23 +71,23 @@ by (induct x) auto qed -subsection {* Continuity of @{const lift_case} *} +subsection {* Continuity of @{const case_lift} *} -lemma lift_case_eq: "lift_case \ f x = fup\(\ y. f (undiscr y))\(Rep_lift x)" +lemma case_lift_eq: "case_lift \ f x = fup\(\ y. f (undiscr y))\(Rep_lift x)" apply (induct x, unfold lift.cases) apply (simp add: Rep_lift_strict) apply (simp add: Def_def Abs_lift_inverse) done -lemma cont2cont_lift_case [simp]: - "\\y. cont (\x. f x y); cont g\ \ cont (\x. lift_case \ (f x) (g x))" -unfolding lift_case_eq by (simp add: cont_Rep_lift) +lemma cont2cont_case_lift [simp]: + "\\y. cont (\x. f x y); cont g\ \ cont (\x. case_lift \ (f x) (g x))" +unfolding case_lift_eq by (simp add: cont_Rep_lift) subsection {* Further operations *} definition flift1 :: "('a \ 'b::pcpo) \ ('a lift \ 'b)" (binder "FLIFT " 10) where - "flift1 = (\f. (\ x. lift_case \ f x))" + "flift1 = (\f. (\ x. case_lift \ f x))" translations "\(XCONST Def x). t" => "CONST flift1 (\x. t)" diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Hoare_Parallel/Graph.thy --- a/src/HOL/Hoare_Parallel/Graph.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Hoare_Parallel/Graph.thy Wed Feb 12 08:37:06 2014 +0100 @@ -53,6 +53,7 @@ apply(case_tac "list") apply force apply simp +apply(rename_tac lista) apply(rotate_tac -2) apply(erule_tac x = "0" in all_dupE) apply simp diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Hoare_Parallel/RG_Hoare.thy --- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Wed Feb 12 08:37:06 2014 +0100 @@ -636,6 +636,7 @@ prefer 2 apply force apply(case_tac xsa,simp,simp) + apply(rename_tac list) apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp) apply(rule conjI,erule CptnEnv) apply(simp (no_asm_use) add:lift_def) @@ -733,6 +734,7 @@ apply(case_tac xs,simp add:cp_def) apply clarify apply (simp del:map.simps) + apply (rename_tac list) apply(subgoal_tac "(map (lift Q) ((a, b) # list))\[]") apply(drule last_conv_nth) apply (simp del:map.simps) @@ -1032,6 +1034,7 @@ apply(drule last_conv_nth) apply (simp del:map.simps last.simps) apply(simp add:nth_append del:last.simps) + apply(rename_tac a list) apply(subgoal_tac "((Some (While b P), snd (last ((Some P, sa) # xs))) # a # list)\[]") apply(drule last_conv_nth) apply (simp del:map.simps last.simps) @@ -1349,6 +1352,7 @@ apply(subgoal_tac "xs\[]") prefer 2 apply simp +apply(rename_tac a list) apply(thin_tac "xs = a # list") apply(simp add:par_com_validity_def par_comm_def) apply clarify diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Hoare_Parallel/RG_Tran.thy --- a/src/HOL/Hoare_Parallel/RG_Tran.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Hoare_Parallel/RG_Tran.thy Wed Feb 12 08:37:06 2014 +0100 @@ -838,6 +838,7 @@ apply(case_tac x) apply(force elim:par_cptn.cases) apply simp + apply(rename_tac a list) apply(erule_tac x="list" in allE) apply clarify apply simp diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Import/HOL_Light_Maps.thy --- a/src/HOL/Import/HOL_Light_Maps.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Import/HOL_Light_Maps.thy Wed Feb 12 08:37:06 2014 +0100 @@ -232,11 +232,11 @@ "\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="rec_list nil' cons'" in exI) auto -lemma HD[import_const HD : List.hd]: +lemma HD[import_const HD : List.list.hd]: "hd ((h\'A) # t) = h" by simp -lemma TL[import_const TL : List.tl]: +lemma TL[import_const TL : List.list.tl]: "tl ((h\'A) # t) = t" by simp diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Induct/QuoNestedDataType.thy --- a/src/HOL/Induct/QuoNestedDataType.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Induct/QuoNestedDataType.thy Wed Feb 12 08:37:06 2014 +0100 @@ -212,6 +212,7 @@ lemma ExpList_rep: "\Us. z = Abs_ExpList Us" apply (induct z) +apply (rename_tac [2] a b) apply (rule_tac [2] z=a in eq_Abs_Exp) apply (auto simp add: Abs_ExpList_def Cons_eq_map_conv intro: exprel_refl) done diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Library/Multiset.thy Wed Feb 12 08:37:06 2014 +0100 @@ -955,6 +955,7 @@ lemma distinct_count_atmost_1: "distinct x = (! a. count (multiset_of x) a = (if a \ set x then 1 else 0))" apply (induct x, simp, rule iffI, simp_all) +apply (rename_tac a b) apply (rule conjI) apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of) apply (erule_tac x = a in allE, simp, clarify) diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Library/Polynomial.thy --- a/src/HOL/Library/Polynomial.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Library/Polynomial.thy Wed Feb 12 08:37:06 2014 +0100 @@ -406,7 +406,7 @@ { fix ms :: "nat list" and f :: "nat \ 'a" and x :: "'a" assume "\m\set ms. m > 0" then have "map (case_nat x f) ms = map f (map (\n. n - 1) ms)" - by (induct ms) (auto, metis Suc_pred' case_nat_Suc) } + by (induct ms) (auto, metis Suc_pred' nat.cases(2)) } note * = this show ?thesis by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt One_nat_def del: upt_Suc) @@ -452,7 +452,7 @@ lemma coeff_Poly_eq: "coeff (Poly xs) n = nth_default 0 xs n" apply (induct xs arbitrary: n) apply simp_all - by (metis case_nat_0 case_nat_Suc not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq) + by (metis nat.cases not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq) lemma nth_default_coeffs_eq: "nth_default 0 (coeffs p) = coeff p" diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Library/RBT_Impl.thy --- a/src/HOL/Library/RBT_Impl.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Library/RBT_Impl.thy Wed Feb 12 08:37:06 2014 +0100 @@ -1748,14 +1748,14 @@ hide_type (open) compare hide_const (open) - compare_height skip_black skip_red LT GT EQ compare_case compare_rec - Abs_compare Rep_compare compare_rep_set + compare_height skip_black skip_red LT GT EQ case_compare rec_compare + Abs_compare Rep_compare rep_set_compare hide_fact (open) Abs_compare_cases Abs_compare_induct Abs_compare_inject Abs_compare_inverse Rep_compare Rep_compare_cases Rep_compare_induct Rep_compare_inject Rep_compare_inverse compare.simps compare.exhaust compare.induct compare.recs compare.simps compare.size compare.case_cong compare.weak_case_cong compare.cases - compare.nchotomy compare.split compare.split_asm compare_rec_def + compare.nchotomy compare.split compare.split_asm rec_compare_def compare.eq.refl compare.eq.simps compare.EQ_def compare.GT_def compare.LT_def equal_compare_def diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/List.thy --- a/src/HOL/List.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/List.thy Wed Feb 12 08:37:06 2014 +0100 @@ -1648,10 +1648,10 @@ lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}" apply (induct xs, simp, simp) apply safe -apply (metis case_nat_0 nth.simps zero_less_Suc) +apply (metis nat.cases(1) nth.simps zero_less_Suc) apply (metis less_Suc_eq_0_disj nth_Cons_Suc) apply (case_tac i, simp) -apply (metis diff_Suc_Suc case_nat_Suc nth.simps zero_less_diff) +apply (metis diff_Suc_Suc nat.cases(2) nth.simps zero_less_diff) done lemma in_set_conv_nth: "(x \ set xs) = (\i < length xs. xs!i = x)" diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Metis_Examples/Clausification.thy --- a/src/HOL/Metis_Examples/Clausification.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Metis_Examples/Clausification.thy Wed Feb 12 08:37:06 2014 +0100 @@ -138,7 +138,7 @@ by (metis split_list_last_prop[where P = P] in_set_conv_decomp) lemma ex_tl: "EX ys. tl ys = xs" -using tl.simps(2) by fast +using list.sel(3) by fast lemma "(\ys\nat list. tl ys = xs) \ (\bs\int list. tl bs = as)" by (metis ex_tl) diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/MicroJava/Comp/CorrCompTp.thy --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Feb 12 08:37:06 2014 +0100 @@ -80,7 +80,7 @@ apply (rule allI) apply (drule_tac x="a # ys" in spec) apply (simp only: rev.simps append_assoc append_Cons append_Nil - map.simps map_of.simps map_upds_Cons hd.simps tl.simps) + map.simps map_of.simps map_upds_Cons list.sel) done lemma map_of_as_map_upds: "map_of (rev xs) = empty ((map fst xs) [\] (map snd xs))" diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/MicroJava/Comp/Index.thy --- a/src/HOL/MicroJava/Comp/Index.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/MicroJava/Comp/Index.thy Wed Feb 12 08:37:06 2014 +0100 @@ -54,6 +54,7 @@ apply (simp only: index_def gjmb_plns_def) apply (case_tac "gmb G C S" rule: prod.exhaust) apply (simp add: galldefs del: set_append map_append) +apply (rename_tac a b) apply (case_tac b, simp add: gmb_def gjmb_lvs_def del: set_append map_append) apply (intro strip) apply (simp del: set_append map_append) @@ -73,6 +74,7 @@ locvars_xstate G C S (Norm (h, l(x\val)))" apply (simp only: locvars_xstate_def locvars_locals_def index_def) apply (case_tac "gmb G C S" rule: prod.exhaust, simp) +apply (rename_tac a b) apply (case_tac b, simp) apply (rule conjI) apply (simp add: gl_def) diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Feb 12 08:37:06 2014 +0100 @@ -3870,6 +3870,7 @@ apply rule apply (erule_tac x="Some y" in allE) defer + apply (rename_tac x) apply (erule_tac x="Some x" in allE) apply auto done diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Nat.thy --- a/src/HOL/Nat.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Nat.thy Wed Feb 12 08:37:06 2014 +0100 @@ -71,33 +71,79 @@ lemma Suc_Rep_inject': "Suc_Rep x = Suc_Rep y \ x = y" by (rule iffI, rule Suc_Rep_inject) simp_all +lemma nat_induct0: + fixes n + assumes "P 0" and "\n. P n \ P (Suc n)" + shows "P n" +using assms +apply (unfold Zero_nat_def Suc_def) +apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *} +apply (erule Nat_Rep_Nat [THEN Nat.induct]) +apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst]) +done + +wrap_free_constructors ["0 \ nat", Suc] case_nat [=] [[], [pred]] + apply atomize_elim + apply (rename_tac n, induct_tac n rule: nat_induct0, auto) + apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI + Suc_Rep_inject' Rep_Nat_inject) +apply (simp only: Suc_not_Zero) +done + +-- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *} +setup {* Sign.mandatory_path "old" *} + rep_datatype "0 \ nat" Suc - apply (unfold Zero_nat_def Suc_def) - apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *} - apply (erule Nat_Rep_Nat [THEN Nat.induct]) - apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst]) - apply (simp_all add: Nat_Abs_Nat_inject Nat_Rep_Nat - Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep - Suc_Rep_not_Zero_Rep [symmetric] - Suc_Rep_inject' Rep_Nat_inject) - done + apply (erule nat_induct0, assumption) + apply (rule nat.inject) +apply (rule nat.distinct(1)) +done + +setup {* Sign.parent_path *} + +-- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *} +setup {* Sign.mandatory_path "nat" *} + +declare + old.nat.inject[iff del] + old.nat.distinct(1)[simp del, induct_simp del] + +lemmas induct = old.nat.induct +lemmas inducts = old.nat.inducts +lemmas recs = old.nat.recs +lemmas cases = nat.case +lemmas simps = nat.inject nat.distinct nat.case old.nat.recs + +setup {* Sign.parent_path *} + +abbreviation rec_nat :: "'a \ (nat \ 'a \ 'a) \ nat \ 'a" where + "rec_nat \ old.rec_nat" + +hide_const Nat.pred -- {* hide everything related to the selector *} +hide_fact + nat.case_eq_if + nat.collapse + nat.expand + nat.sel + nat.sel_exhaust + nat.sel_split + nat.sel_split_asm + +lemma nat_exhaust [case_names 0 Suc, cases type: nat]: + -- {* for backward compatibility -- names of variables differ *} + "(y = 0 \ P) \ (\nat. y = Suc nat \ P) \ P" +by (rule nat.exhaust) lemma nat_induct [case_names 0 Suc, induct type: nat]: -- {* for backward compatibility -- names of variables differ *} fixes n - assumes "P 0" - and "\n. P n \ P (Suc n)" + assumes "P 0" and "\n. P n \ P (Suc n)" shows "P n" - using assms by (rule nat.induct) - -declare nat.exhaust [case_names 0 Suc, cases type: nat] +using assms by (rule nat.induct) -lemmas nat_rec_0 = nat.recs(1) - and nat_rec_Suc = nat.recs(2) - -lemmas case_nat_0 = nat.cases(1) - and case_nat_Suc = nat.cases(2) - +hide_fact + nat_exhaust + nat_induct0 text {* Injectiveness and distinctness lemmas *} @@ -632,14 +678,6 @@ lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq -text {* These two rules ease the use of primitive recursion. -NOTE USE OF @{text "=="} *} -lemma def_rec_nat_0: "(!!n. f n == rec_nat c h n) ==> f 0 = c" -by simp - -lemma def_rec_nat_Suc: "(!!n. f n == rec_nat c h n) ==> f (Suc n) = h n (f n)" -by simp - lemma not0_implies_Suc: "n \ 0 ==> \m. n = Suc m" by (cases n) simp_all @@ -1928,4 +1966,3 @@ hide_const (open) of_nat_aux end - diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Nitpick_Examples/Refute_Nits.thy --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 12 08:37:06 2014 +0100 @@ -649,17 +649,17 @@ nitpick [expect = genuine] oops -lemma "T1_rec a b A = a" +lemma "rec_T1 a b A = a" nitpick [expect = none] apply simp done -lemma "T1_rec a b B = b" +lemma "rec_T1 a b B = b" nitpick [expect = none] apply simp done -lemma "P (T1_rec a b x)" +lemma "P (rec_T1 a b x)" nitpick [expect = genuine] oops @@ -681,17 +681,17 @@ nitpick [expect = genuine] oops -lemma "T2_rec c d (C x) = c x" +lemma "rec_T2 c d (C x) = c x" nitpick [expect = none] apply simp done -lemma "T2_rec c d (D x) = d x" +lemma "rec_T2 c d (D x) = d x" nitpick [expect = none] apply simp done -lemma "P (T2_rec c d x)" +lemma "P (rec_T2 c d x)" nitpick [expect = genuine] oops @@ -713,12 +713,12 @@ nitpick [expect = genuine] oops -lemma "T3_rec e (E x) = e x" +lemma "rec_T3 e (E x) = e x" nitpick [card = 1\4, expect = none] apply simp done -lemma "P (T3_rec e x)" +lemma "P (rec_T3 e x)" nitpick [expect = genuine] oops @@ -818,22 +818,22 @@ nitpick [expect = genuine] oops -lemma "BitList_rec nil bit0 bit1 BitListNil = nil" +lemma "rec_BitList nil bit0 bit1 BitListNil = nil" nitpick [expect = none] apply simp done -lemma "BitList_rec nil bit0 bit1 (Bit0 xs) = bit0 xs (BitList_rec nil bit0 bit1 xs)" +lemma "rec_BitList nil bit0 bit1 (Bit0 xs) = bit0 xs (rec_BitList nil bit0 bit1 xs)" nitpick [expect = none] apply simp done -lemma "BitList_rec nil bit0 bit1 (Bit1 xs) = bit1 xs (BitList_rec nil bit0 bit1 xs)" +lemma "rec_BitList nil bit0 bit1 (Bit1 xs) = bit1 xs (rec_BitList nil bit0 bit1 xs)" nitpick [expect = none] apply simp done -lemma "P (BitList_rec nil bit0 bit1 x)" +lemma "P (rec_BitList nil bit0 bit1 x)" nitpick [expect = genuine] oops @@ -851,17 +851,17 @@ nitpick [expect = genuine] oops -lemma "BinTree_rec l n (Leaf x) = l x" +lemma "rec_BinTree l n (Leaf x) = l x" nitpick [expect = none] apply simp done -lemma "BinTree_rec l n (Node x y) = n x y (BinTree_rec l n x) (BinTree_rec l n y)" +lemma "rec_BinTree l n (Node x y) = n x y (rec_BinTree l n x) (rec_BinTree l n y)" nitpick [card = 1\5, expect = none] apply simp done -lemma "P (BinTree_rec l n x)" +lemma "P (rec_BinTree l n x)" nitpick [expect = genuine] oops @@ -894,17 +894,17 @@ nitpick [expect = genuine] oops -lemma "aexp_bexp_rec_1 number ite equal (Number x) = number x" +lemma "rec_aexp_bexp_1 number ite equal (Number x) = number x" nitpick [card = 1\3, expect = none] apply simp done -lemma "aexp_bexp_rec_1 number ite equal (ITE x y z) = ite x y z (aexp_bexp_rec_2 number ite equal x) (aexp_bexp_rec_1 number ite equal y) (aexp_bexp_rec_1 number ite equal z)" +lemma "rec_aexp_bexp_1 number ite equal (ITE x y z) = ite x y z (rec_aexp_bexp_2 number ite equal x) (rec_aexp_bexp_1 number ite equal y) (rec_aexp_bexp_1 number ite equal z)" nitpick [card = 1\3, expect = none] apply simp done -lemma "P (aexp_bexp_rec_1 number ite equal x)" +lemma "P (rec_aexp_bexp_1 number ite equal x)" nitpick [expect = genuine] oops @@ -912,12 +912,12 @@ nitpick [expect = genuine] oops -lemma "aexp_bexp_rec_2 number ite equal (Equal x y) = equal x y (aexp_bexp_rec_1 number ite equal x) (aexp_bexp_rec_1 number ite equal y)" +lemma "rec_aexp_bexp_2 number ite equal (Equal x y) = equal x y (rec_aexp_bexp_1 number ite equal x) (rec_aexp_bexp_1 number ite equal y)" nitpick [card = 1\3, expect = none] apply simp done -lemma "P (aexp_bexp_rec_2 number ite equal x)" +lemma "P (rec_aexp_bexp_2 number ite equal x)" nitpick [expect = genuine] oops @@ -972,41 +972,41 @@ nitpick [expect = genuine] oops -lemma "X_Y_rec_1 a b c d e f A = a" +lemma "rec_X_Y_1 a b c d e f A = a" nitpick [card = 1\5, expect = none] apply simp done -lemma "X_Y_rec_1 a b c d e f (B x) = b x (X_Y_rec_1 a b c d e f x)" +lemma "rec_X_Y_1 a b c d e f (B x) = b x (rec_X_Y_1 a b c d e f x)" nitpick [card = 1\5, expect = none] apply simp done -lemma "X_Y_rec_1 a b c d e f (C y) = c y (X_Y_rec_2 a b c d e f y)" +lemma "rec_X_Y_1 a b c d e f (C y) = c y (rec_X_Y_2 a b c d e f y)" nitpick [card = 1\5, expect = none] apply simp done -lemma "X_Y_rec_2 a b c d e f (D x) = d x (X_Y_rec_1 a b c d e f x)" +lemma "rec_X_Y_2 a b c d e f (D x) = d x (rec_X_Y_1 a b c d e f x)" nitpick [card = 1\5, expect = none] apply simp done -lemma "X_Y_rec_2 a b c d e f (E y) = e y (X_Y_rec_2 a b c d e f y)" +lemma "rec_X_Y_2 a b c d e f (E y) = e y (rec_X_Y_2 a b c d e f y)" nitpick [card = 1\5, expect = none] apply simp done -lemma "X_Y_rec_2 a b c d e f F = f" +lemma "rec_X_Y_2 a b c d e f F = f" nitpick [card = 1\5, expect = none] apply simp done -lemma "P (X_Y_rec_1 a b c d e f x)" +lemma "P (rec_X_Y_1 a b c d e f x)" nitpick [expect = genuine] oops -lemma "P (X_Y_rec_2 a b c d e f y)" +lemma "P (rec_X_Y_2 a b c d e f y)" nitpick [expect = genuine] oops @@ -1028,45 +1028,45 @@ nitpick [expect = genuine] oops -lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (CX x) = cx x (XOpt_rec_2 cx dx n1 s1 n2 s2 x)" +lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (CX x) = cx x (rec_XOpt_2 cx dx n1 s1 n2 s2 x)" nitpick [card = 1\5, expect = none] apply simp done -lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\b. XOpt_rec_3 cx dx n1 s1 n2 s2 (x b))" +lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\b. rec_XOpt_3 cx dx n1 s1 n2 s2 (x b))" nitpick [card = 1\3, expect = none] apply simp done -lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 None = n1" +lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 None = n1" nitpick [card = 1\4, expect = none] apply simp done -lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)" +lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)" nitpick [card = 1\4, expect = none] apply simp done -lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 None = n2" +lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 None = n2" nitpick [card = 1\4, expect = none] apply simp done -lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)" +lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)" nitpick [card = 1\4, expect = none] apply simp done -lemma "P (XOpt_rec_1 cx dx n1 s1 n2 s2 x)" +lemma "P (rec_XOpt_1 cx dx n1 s1 n2 s2 x)" nitpick [expect = genuine] oops -lemma "P (XOpt_rec_2 cx dx n1 s1 n2 s2 x)" +lemma "P (rec_XOpt_2 cx dx n1 s1 n2 s2 x)" nitpick [expect = genuine] oops -lemma "P (XOpt_rec_3 cx dx n1 s1 n2 s2 x)" +lemma "P (rec_XOpt_3 cx dx n1 s1 n2 s2 x)" nitpick [expect = genuine] oops @@ -1084,26 +1084,26 @@ nitpick [expect = genuine] oops -lemma "YOpt_rec_1 cy n s (CY x) = cy x (YOpt_rec_2 cy n s x)" +lemma "rec_YOpt_1 cy n s (CY x) = cy x (rec_YOpt_2 cy n s x)" nitpick [card = 1\2, expect = none] apply simp done -lemma "YOpt_rec_2 cy n s None = n" +lemma "rec_YOpt_2 cy n s None = n" nitpick [card = 1\2, expect = none] apply simp done -lemma "YOpt_rec_2 cy n s (Some x) = s x (\a. YOpt_rec_1 cy n s (x a))" +lemma "rec_YOpt_2 cy n s (Some x) = s x (\a. rec_YOpt_1 cy n s (x a))" nitpick [card = 1\2, expect = none] apply simp done -lemma "P (YOpt_rec_1 cy n s x)" +lemma "P (rec_YOpt_1 cy n s x)" nitpick [expect = genuine] oops -lemma "P (YOpt_rec_2 cy n s x)" +lemma "P (rec_YOpt_2 cy n s x)" nitpick [expect = genuine] oops @@ -1121,26 +1121,26 @@ nitpick [expect = genuine] oops -lemma "Trie_rec_1 tr nil cons (TR x) = tr x (Trie_rec_2 tr nil cons x)" +lemma "rec_Trie_1 tr nil cons (TR x) = tr x (rec_Trie_2 tr nil cons x)" nitpick [card = 1\4, expect = none] apply simp done -lemma "Trie_rec_2 tr nil cons [] = nil" +lemma "rec_Trie_2 tr nil cons [] = nil" nitpick [card = 1\4, expect = none] apply simp done -lemma "Trie_rec_2 tr nil cons (x#xs) = cons x xs (Trie_rec_1 tr nil cons x) (Trie_rec_2 tr nil cons xs)" +lemma "rec_Trie_2 tr nil cons (x#xs) = cons x xs (rec_Trie_1 tr nil cons x) (rec_Trie_2 tr nil cons xs)" nitpick [card = 1\4, expect = none] apply simp done -lemma "P (Trie_rec_1 tr nil cons x)" +lemma "P (rec_Trie_1 tr nil cons x)" nitpick [card = 1, expect = genuine] oops -lemma "P (Trie_rec_2 tr nil cons x)" +lemma "P (rec_Trie_2 tr nil cons x)" nitpick [card = 1, expect = genuine] oops @@ -1158,17 +1158,17 @@ nitpick [expect = genuine] oops -lemma "InfTree_rec leaf node Leaf = leaf" +lemma "rec_InfTree leaf node Leaf = leaf" nitpick [card = 1\3, expect = none] apply simp done -lemma "InfTree_rec leaf node (Node x) = node x (\n. InfTree_rec leaf node (x n))" +lemma "rec_InfTree leaf node (Node x) = node x (\n. rec_InfTree leaf node (x n))" nitpick [card = 1\3, expect = none] apply simp done -lemma "P (InfTree_rec leaf node x)" +lemma "P (rec_InfTree leaf node x)" nitpick [expect = genuine] oops @@ -1187,22 +1187,22 @@ nitpick [card 'a = 4, card "'a lambda" = 5, expect = genuine] oops -lemma "lambda_rec var app lam (Var x) = var x" +lemma "rec_lambda var app lam (Var x) = var x" nitpick [card = 1\3, expect = none] apply simp done -lemma "lambda_rec var app lam (App x y) = app x y (lambda_rec var app lam x) (lambda_rec var app lam y)" +lemma "rec_lambda var app lam (App x y) = app x y (rec_lambda var app lam x) (rec_lambda var app lam y)" nitpick [card = 1\3, expect = none] apply simp done -lemma "lambda_rec var app lam (Lam x) = lam x (\a. lambda_rec var app lam (x a))" +lemma "rec_lambda var app lam (Lam x) = lam x (\a. rec_lambda var app lam (x a))" nitpick [card = 1\3, expect = none] apply simp done -lemma "P (lambda_rec v a l x)" +lemma "P (rec_lambda v a l x)" nitpick [expect = genuine] oops @@ -1223,40 +1223,40 @@ nitpick [expect = genuine] oops -lemma "U_rec_1 e c d nil cons (E x) = e x (U_rec_2 e c d nil cons x)" +lemma "rec_U_1 e c d nil cons (E x) = e x (rec_U_2 e c d nil cons x)" nitpick [card = 1\3, expect = none] apply simp done -lemma "U_rec_2 e c d nil cons (C x) = c x" +lemma "rec_U_2 e c d nil cons (C x) = c x" nitpick [card = 1\3, expect = none] apply simp done -lemma "U_rec_2 e c d nil cons (D x) = d x (U_rec_3 e c d nil cons x)" +lemma "rec_U_2 e c d nil cons (D x) = d x (rec_U_3 e c d nil cons x)" nitpick [card = 1\3, expect = none] apply simp done -lemma "U_rec_3 e c d nil cons [] = nil" +lemma "rec_U_3 e c d nil cons [] = nil" nitpick [card = 1\3, expect = none] apply simp done -lemma "U_rec_3 e c d nil cons (x#xs) = cons x xs (U_rec_1 e c d nil cons x) (U_rec_3 e c d nil cons xs)" +lemma "rec_U_3 e c d nil cons (x#xs) = cons x xs (rec_U_1 e c d nil cons x) (rec_U_3 e c d nil cons xs)" nitpick [card = 1\3, expect = none] apply simp done -lemma "P (U_rec_1 e c d nil cons x)" +lemma "P (rec_U_1 e c d nil cons x)" nitpick [expect = genuine] oops -lemma "P (U_rec_2 e c d nil cons x)" +lemma "P (rec_U_2 e c d nil cons x)" nitpick [card = 1, expect = genuine] oops -lemma "P (U_rec_3 e c d nil cons x)" +lemma "P (rec_U_3 e c d nil cons x)" nitpick [card = 1, expect = genuine] oops diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Nitpick_Examples/Typedef_Nits.thy --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Feb 12 08:37:06 2014 +0100 @@ -164,7 +164,7 @@ by (rule Rep_Nat_inverse) lemma "Abs_list (Rep_list a) = a" -nitpick [card = 1\2, expect = none] +(* nitpick [card = 1\2, expect = none] FIXME *) by (rule Rep_list_inverse) record point = diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Nominal/Examples/Class3.thy --- a/src/HOL/Nominal/Examples/Class3.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Nominal/Examples/Class3.thy Wed Feb 12 08:37:06 2014 +0100 @@ -2311,6 +2311,7 @@ apply(rule_tac my_wf_induct_triple[OF a]) apply(case_tac x rule: prod.exhaust) apply(simp) +apply(rename_tac p a b) apply(case_tac b) apply(simp) apply(rule b) diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Nominal/Examples/Fsub.thy --- a/src/HOL/Nominal/Examples/Fsub.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Nominal/Examples/Fsub.thy Wed Feb 12 08:37:06 2014 +0100 @@ -167,7 +167,8 @@ assumes a: "X\(ty_dom \)" shows "\T.(TVarB X T)\set \" using a - apply (induct \, auto) + apply (induct \, auto) + apply (rename_tac a \') apply (subgoal_tac "\T.(TVarB X T=a)") apply (auto) apply (auto simp add: ty_binding_existence) diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Nominal/Examples/W.thy --- a/src/HOL/Nominal/Examples/W.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Nominal/Examples/W.thy Wed Feb 12 08:37:06 2014 +0100 @@ -1,5 +1,5 @@ theory W -imports Nominal +imports "../Nominal" begin text {* Example for strong induction rules avoiding sets of atoms. *} @@ -388,6 +388,7 @@ shows "supp \ = set (ftv \)" apply (induct \) apply (simp_all add: supp_list_nil supp_list_cons) +apply (rename_tac a \') apply (case_tac a) apply (simp add: supp_prod supp_atm ftv_tyS) done @@ -443,6 +444,7 @@ using asm apply(induct Xs) apply(simp) +apply(rename_tac a Xs') apply(case_tac "X=a") apply(simp add: abs_fresh) apply(simp add: abs_fresh) diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Option.thy --- a/src/HOL/Option.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Option.thy Wed Feb 12 08:37:06 2014 +0100 @@ -16,7 +16,7 @@ lemma [case_names None Some, cases type: option]: -- {* for backward compatibility -- names of variables differ *} - "(y = None \ P) \ (\option. y = Some option \ P) \ P" + "(y = None \ P) \ (\a. y = Some a \ P) \ P" by (rule option.exhaust) lemma [case_names None Some, induct type: option]: diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Probability/Infinite_Product_Measure.thy --- a/src/HOL/Probability/Infinite_Product_Measure.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy Wed Feb 12 08:37:06 2014 +0100 @@ -196,7 +196,7 @@ (\n. ?a / 2 ^ (k + 1) \ ?q k n (w k)) \ (k \ 0 \ restrict (w k) (J (k - 1)) = w (k - 1))" proof (induct k) case 0 with w0 show ?case - unfolding w_def rec_nat_0 by auto + unfolding w_def nat.recs(1) by auto next case (Suc k) then have wk: "w k \ space (Pi\<^sub>M (J k) M)" by auto @@ -241,7 +241,7 @@ (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff) qed then have "?P k (w k) (w (Suc k))" - unfolding w_def rec_nat_Suc unfolding w_def[symmetric] + unfolding w_def nat.recs(2) unfolding w_def[symmetric] by (rule someI_ex) then show ?case by auto qed diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Probability/Radon_Nikodym.thy --- a/src/HOL/Probability/Radon_Nikodym.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Probability/Radon_Nikodym.thy Wed Feb 12 08:37:06 2014 +0100 @@ -250,7 +250,7 @@ { fix i have "A i \ sets M" unfolding A_def proof (induct i) case (Suc i) - from Ex_P[OF this, of i] show ?case unfolding rec_nat_Suc + from Ex_P[OF this, of i] show ?case unfolding nat.recs(2) by (rule someI2_ex) simp qed simp } note A_in_sets = this @@ -281,7 +281,7 @@ from ex_inverse_of_nat_Suc_less[OF this] obtain n where *: "?d B < - 1 / real (Suc n)" by (auto simp: real_eq_of_nat inverse_eq_divide field_simps) - have "B \ A (Suc n)" using B by (auto simp del: rec_nat_Suc) + have "B \ A (Suc n)" using B by (auto simp del: nat.recs(2)) from epsilon[OF B(1) this] * show False by auto qed diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Product_Type.thy Wed Feb 12 08:37:06 2014 +0100 @@ -698,7 +698,7 @@ "case_prod f p = f (fst p) (snd p)" by (fact split_beta) -lemma case_prods3 [cases type]: +lemma prod_cases3 [cases type]: obtains (fields) a b c where "y = (a, b, c)" by (cases y, case_tac b) blast @@ -706,7 +706,7 @@ "(!!a b c. P (a, b, c)) ==> P x" by (cases x) blast -lemma case_prods4 [cases type]: +lemma prod_cases4 [cases type]: obtains (fields) a b c d where "y = (a, b, c, d)" by (cases y, case_tac c) blast @@ -714,7 +714,7 @@ "(!!a b c d. P (a, b, c, d)) ==> P x" by (cases x) blast -lemma case_prods5 [cases type]: +lemma prod_cases5 [cases type]: obtains (fields) a b c d e where "y = (a, b, c, d, e)" by (cases y, case_tac d) blast @@ -722,7 +722,7 @@ "(!!a b c d e. P (a, b, c, d, e)) ==> P x" by (cases x) blast -lemma case_prods6 [cases type]: +lemma prod_cases6 [cases type]: obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)" by (cases y, case_tac e) blast @@ -730,7 +730,7 @@ "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x" by (cases x) blast -lemma case_prods7 [cases type]: +lemma prod_cases7 [cases type]: obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)" by (cases y, case_tac f) blast diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Proofs/Lambda/LambdaType.thy --- a/src/HOL/Proofs/Lambda/LambdaType.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Proofs/Lambda/LambdaType.thy Wed Feb 12 08:37:06 2014 +0100 @@ -30,12 +30,7 @@ by (simp add: shift_def) lemma shift_commute [simp]: "e\i:U\\0:T\ = e\0:T\\Suc i:U\" - apply (rule ext) - apply (case_tac x) - apply simp - apply (case_tac nat) - apply (simp_all add: shift_def) - done + by (rule ext) (simp_all add: shift_def split: nat.split) subsection {* Types and typing rules *} @@ -157,6 +152,7 @@ "e \ t \\ ts : T \ \Ts. e \ t : Ts \ T \ e \ ts : Ts" apply (induct ts arbitrary: t T) apply simp + apply (rename_tac a b t T) apply atomize apply simp apply (erule_tac x = "t \ a" in allE) @@ -177,12 +173,14 @@ "e \ t : Ts \ T \ e \ ts : Ts \ e \ t \\ ts : T" apply (induct ts arbitrary: t T Ts) apply simp + apply (rename_tac a b t T Ts) apply atomize apply (case_tac Ts) apply simp apply simp apply (erule_tac x = "t \ a" in allE) apply (erule_tac x = T in allE) + apply (rename_tac list) apply (erule_tac x = list in allE) apply (erule impE) apply (erule conjE) @@ -225,6 +223,7 @@ apply (erule var_app_type_eq) apply assumption apply simp + apply (rename_tac a b ts Ts U) apply atomize apply (case_tac U) apply (rule FalseE) diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/ROOT --- a/src/HOL/ROOT Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/ROOT Wed Feb 12 08:37:06 2014 +0100 @@ -464,7 +464,7 @@ Author: Tobias Nipkow and Konrad Slind and Olaf Müller Copyright 1994--1996 TU Muenchen - The meta theory of I/O-Automata in HOL. This formalization has been + The meta-theory of I/O-Automata in HOL. This formalization has been significantly changed and extended, see HOLCF/IOA. There are also the proofs of two communication protocols which formerly have been here. diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/SET_Protocol/Cardholder_Registration.thy --- a/src/HOL/SET_Protocol/Cardholder_Registration.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy Wed Feb 12 08:37:06 2014 +0100 @@ -671,6 +671,7 @@ lemma N_fresh_not_KeyCryptNonce: "\C. DK \ priEK C ==> Nonce N \ used evs --> ~ KeyCryptNonce DK N evs" apply (induct_tac "evs") +apply (rename_tac [2] a evs') apply (case_tac [2] "a") apply (auto simp add: parts_insert2) done diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/SET_Protocol/Event_SET.thy --- a/src/HOL/SET_Protocol/Event_SET.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/SET_Protocol/Event_SET.thy Wed Feb 12 08:37:06 2014 +0100 @@ -159,6 +159,7 @@ lemma Notes_imp_parts_subset_used [rule_format]: "Notes A X \ set evs --> parts {X} <= used evs" apply (induct_tac "evs") +apply (rename_tac [2] a evs') apply (induct_tac [2] "a", auto) done diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/SMT_Examples/SMT_Tests.thy --- a/src/HOL/SMT_Examples/SMT_Tests.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy Wed Feb 12 08:37:06 2014 +0100 @@ -669,13 +669,13 @@ "tl [x, y, z] = [y, z]" "hd (tl [x, y, z]) = y" "tl (tl [x, y, z]) = [z]" - using hd.simps tl.simps(2) list.simps + using list.sel(1,3) list.simps by smt+ lemma "fst (hd [(a, b)]) = a" "snd (hd [(a, b)]) = b" - using fst_conv snd_conv pair_collapse hd.simps tl.simps(2) list.simps + using fst_conv snd_conv pair_collapse list.sel(1,3) list.simps by smt+ @@ -808,14 +808,14 @@ "tl [x, y, z] = [y, z]" "hd (tl [x, y, z]) = y" "tl (tl [x, y, z]) = [z]" - using hd.simps tl.simps(2) + using list.sel(1,3) using [[smt_datatypes, smt_oracle, z3_with_extensions]] by smt+ lemma "fst (hd [(a, b)]) = a" "snd (hd [(a, b)]) = b" - using fst_conv snd_conv pair_collapse hd.simps tl.simps(2) + using fst_conv snd_conv pair_collapse list.sel(1,3) using [[smt_datatypes, smt_oracle, z3_with_extensions]] by smt+ diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Tools/BNF/bnf_gfp_util.ML --- a/src/HOL/Tools/BNF/bnf_gfp_util.ML Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_util.ML Wed Feb 12 08:37:06 2014 +0100 @@ -148,7 +148,7 @@ fun mk_rec_nat Zero Suc = let val T = fastype_of Zero; - in Const (@{const_name rec_nat}, T --> fastype_of Suc --> HOLogic.natT --> T) $ Zero $ Suc end; + in Const (@{const_name old.rec_nat}, T --> fastype_of Suc --> HOLogic.natT --> T) $ Zero $ Suc end; fun mk_rec_list Nil Cons = let diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Tools/Datatype/datatype.ML Wed Feb 12 08:37:06 2014 +0100 @@ -283,11 +283,11 @@ (* isomorphisms are defined using primrec-combinators: *) (* generate appropriate functions for instantiating primrec-combinator *) (* *) - (* e.g. dt_Rep_i = list_rec ... (%h t y. In1 (Scons (Leaf h) y)) *) + (* e.g. Rep_dt_i = list_rec ... (%h t y. In1 (Scons (Leaf h) y)) *) (* *) (* also generate characteristic equations for isomorphisms *) (* *) - (* e.g. dt_Rep_i (cons h t) = In1 (Scons (dt_Rep_j h) (dt_Rep_i t)) *) + (* e.g. Rep_dt_i (cons h t) = In1 (Scons (Rep_dt_j h) (Rep_dt_i t)) *) (*---------------------------------------------------------------------*) fun make_iso_def k ks n (cname, cargs) (fs, eqns, i) = @@ -387,7 +387,7 @@ end in map (fn r => r RS subst) (thm :: map mk_thm arities) end; - (* prove inj dt_Rep_i and dt_Rep_i x : dt_rep_set_i *) + (* prove inj Rep_dt_i and Rep_dt_i x : rep_set_dt_i *) val fun_congs = map (fn T => make_elim (Drule.instantiate' [SOME (ctyp_of thy5 T)] [] fun_cong)) branchTs; @@ -457,7 +457,7 @@ val iso_inj_thms = map snd newT_iso_inj_thms @ map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded; - (* prove dt_rep_set_i x --> x : range dt_Rep_i *) + (* prove rep_set_dt_i x --> x : range Rep_dt_i *) fun mk_iso_t (((set_name, iso_name), i), T) = let val isoT = T --> Univ_elT in diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Topological_Spaces.thy Wed Feb 12 08:37:06 2014 +0100 @@ -1298,7 +1298,7 @@ assume *: "\n. \p. ?P p n" def f \ "rec_nat (SOME p. ?P p 0) (\_ n. SOME p. ?P p n)" have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp - have f_Suc: "\i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc .. + have f_Suc: "\i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.recs(2) .. have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto have P_Suc: "\i. ?P (f (Suc i)) (f i)" unfolding f_Suc using *[rule_format] by (rule someI2_ex) auto then have "subseq f" unfolding subseq_Suc_iff by auto @@ -1320,7 +1320,7 @@ then obtain N where N: "\p. p > N \ \m>p. s p < s m" by (force simp: not_le le_less) def f \ "rec_nat (SOME p. ?P p (Suc N)) (\_ n. SOME p. ?P p n)" have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp - have f_Suc: "\i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc .. + have f_Suc: "\i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.recs(2) .. have P_0: "?P (f 0) (Suc N)" unfolding f_0 some_eq_ex[of "\p. ?P p (Suc N)"] using N[of "Suc N"] by auto { fix i have "N < f i \ ?P (f (Suc i)) (f i)" diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Transcendental.thy Wed Feb 12 08:37:06 2014 +0100 @@ -624,6 +624,7 @@ (\n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" apply (rule ext) apply (case_tac "n", simp) + apply (rename_tac nat) apply (case_tac "nat", simp) apply (simp add: r_neq_0) done @@ -2710,7 +2711,8 @@ apply (subgoal_tac "x < real(LEAST m::nat. x < real m * y) * y") prefer 2 apply (erule LeastI) apply (case_tac "LEAST m::nat. x < real m * y", simp) -apply (subgoal_tac "~ x < real nat * y") +apply (rename_tac m) +apply (subgoal_tac "~ x < real m * y") prefer 2 apply (rule not_less_Least, simp, force) done diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Transitive_Closure.thy Wed Feb 12 08:37:06 2014 +0100 @@ -846,6 +846,7 @@ \ (\y m. n = Suc m \ (x, y) \ R \ (y, z) \ R ^^ m \ P) \ P" apply (cases n, simp) + apply (rename_tac nat) apply (cut_tac n=nat and R=R in relpow_Suc_D2', simp, blast) done @@ -1297,4 +1298,3 @@ {* simple transitivity reasoner (predicate version) *} end - diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Word/Word_Miscellaneous.thy --- a/src/HOL/Word/Word_Miscellaneous.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Word/Word_Miscellaneous.thy Wed Feb 12 08:37:06 2014 +0100 @@ -118,10 +118,6 @@ lemmas seqr = eq_reflection [where x = "size w"] for w (* FIXME: delete *) -(* TODO: move name bindings to List.thy *) -lemmas tl_Nil = tl.simps (1) -lemmas tl_Cons = tl.simps (2) - lemma the_elemI: "y = {x} ==> the_elem y = x" by simp diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/ex/Tree23.thy --- a/src/HOL/ex/Tree23.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/ex/Tree23.thy Wed Feb 12 08:37:06 2014 +0100 @@ -330,12 +330,12 @@ "dfull n (Some (p, (False, t'))) \ full (Suc n) t'" lemmas dfull_case_intros = - ord.exhaust [where y=y and P="dfull a (ord_case b c d y)"] + ord.exhaust [of y "dfull a (case_ord b c d y)"] option.exhaust [of y "dfull a (case_option b c y)"] prod.exhaust [of y "dfull a (case_prod b y)"] bool.exhaust [of y "dfull a (case_bool b c y)"] - tree23.exhaust [where y=y and P="dfull a (Some (b, tree23_case c d e y))"] - tree23.exhaust [where y=y and P="full a (tree23_case b c d y)"] + tree23.exhaust [of y "dfull a (Some (b, case_tree23 c d e y))"] + tree23.exhaust [of y "full a (case_tree23 b c d y)"] for a b c d e y lemma dfull_del: "full (Suc n) t \ dfull n (del k t)" @@ -396,7 +396,7 @@ apply (case_tac n, simp, simp) apply (frule dfull_del [where k="Some k"]) apply (cases "del (Some k) t", force) -apply (case_tac "a", rename_tac p b t', case_tac "b", auto) +apply (rename_tac a, case_tac "a", rename_tac b t', case_tac "b", auto) done text{* This is a little test harness and should be commented out once the