# HG changeset patch
# User blanchet
# Date 1392190557 -3600
# Node ID dd7992d4a61a2db7671562e20cef284d340f1b8d
# Parent  05f5fdb8d093bd108d0e50b40a1f319a10fc6db7
adapted theories to 'xxx_case' to 'case_xxx'
* * *
'char_case' -> 'case_char' and same for 'rec'
* * *
compile
* * *
renamed 'xxx_case' to 'case_xxx'

diff -r 05f5fdb8d093 -r dd7992d4a61a src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Auth/Public.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -61,7 +61,7 @@
   injective_publicKey:
     "publicKey b A = publicKey c A' ==> b=c & A=A'"
    apply (rule exI [of _ 
-       "%b A. 2 * agent_case 0 (\<lambda>n. n + 2) 1 A + keymode_case 0 1 b"])
+       "%b A. 2 * case_agent 0 (\<lambda>n. n + 2) 1 A + case_keymode 0 1 b"])
    apply (auto simp add: inj_on_def split: agent.split keymode.split)
    apply presburger
    apply presburger
@@ -137,7 +137,7 @@
 specification (shrK)
   inj_shrK: "inj shrK"
   --{*No two agents have the same long-term key*}
-   apply (rule exI [of _ "agent_case 0 (\<lambda>n. n + 2) 1"]) 
+   apply (rule exI [of _ "case_agent 0 (\<lambda>n. n + 2) 1"]) 
    apply (simp add: inj_on_def split: agent.split) 
    done
 
diff -r 05f5fdb8d093 -r dd7992d4a61a src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Auth/Shared.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -17,7 +17,7 @@
 specification (shrK)
   inj_shrK: "inj shrK"
   --{*No two agents have the same long-term key*}
-   apply (rule exI [of _ "agent_case 0 (\<lambda>n. n + 2) 1"]) 
+   apply (rule exI [of _ "case_agent 0 (\<lambda>n. n + 2) 1"]) 
    apply (simp add: inj_on_def split: agent.split) 
    done
 
diff -r 05f5fdb8d093 -r dd7992d4a61a src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Code_Numeral.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -783,7 +783,7 @@
   by (rule is_measure_trivial)
 
 
-subsection {* Inductive represenation of target language naturals *}
+subsection {* Inductive representation of target language naturals *}
 
 lift_definition Suc :: "natural \<Rightarrow> natural"
   is Nat.Suc
@@ -794,7 +794,7 @@
 rep_datatype "0::natural" Suc
   by (transfer, fact nat.induct nat.inject nat.distinct)+
 
-lemma natural_case [case_names nat, cases type: natural]:
+lemma natural_cases [case_names nat, cases type: natural]:
   fixes m :: natural
   assumes "\<And>n. m = of_nat n \<Longrightarrow> P"
   shows P
@@ -876,7 +876,7 @@
   by transfer (simp add: fun_eq_iff)
 
 lemma [code, code_unfold]:
-  "natural_case f g n = (if n = 0 then f else g (n - 1))"
+  "case_natural f g n = (if n = 0 then f else g (n - 1))"
   by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def)
 
 declare natural.recs [code del]
diff -r 05f5fdb8d093 -r dd7992d4a61a src/HOL/HOLCF/IOA/Storage/Action.thy
--- a/src/HOL/HOLCF/IOA/Storage/Action.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Action.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -8,9 +8,9 @@
 imports Main
 begin
 
-datatype action = New  | Loc nat | Free nat
+datatype action = New | Loc nat | Free nat
 
-lemma [cong]: "!!x. x = y ==> action_case a b c x = action_case a b c y"
+lemma [cong]: "!!x. x = y ==> case_action a b c x = case_action a b c y"
   by simp
 
 end
diff -r 05f5fdb8d093 -r dd7992d4a61a src/HOL/Lazy_Sequence.thy
--- a/src/HOL/Lazy_Sequence.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Lazy_Sequence.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -35,12 +35,12 @@
   "size (xq :: 'a lazy_sequence) = 0"
   by (cases xq) simp
 
-lemma lazy_sequence_case [simp]:
-  "lazy_sequence_case f xq = f (list_of_lazy_sequence xq)"
+lemma case_lazy_sequence [simp]:
+  "case_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
   by (cases xq) auto
 
-lemma lazy_sequence_rec [simp]:
-  "lazy_sequence_rec f xq = f (list_of_lazy_sequence xq)"
+lemma rec_lazy_sequence [simp]:
+  "rec_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
   by (cases xq) auto
 
 definition Lazy_Sequence :: "(unit \<Rightarrow> ('a \<times> 'a lazy_sequence) option) \<Rightarrow> 'a lazy_sequence"
@@ -346,4 +346,3 @@
   if_seq_def those_def not_seq_def product_def 
 
 end
-
diff -r 05f5fdb8d093 -r dd7992d4a61a src/HOL/Library/Bit.thy
--- a/src/HOL/Library/Bit.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Library/Bit.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -102,10 +102,10 @@
 begin
 
 definition plus_bit_def:
-  "x + y = bit_case y (bit_case 1 0 y) x"
+  "x + y = case_bit y (case_bit 1 0 y) x"
 
 definition times_bit_def:
-  "x * y = bit_case 0 y x"
+  "x * y = case_bit 0 y x"
 
 definition uminus_bit_def [simp]:
   "- x = (x :: bit)"
@@ -167,7 +167,7 @@
 
 definition of_bit :: "bit \<Rightarrow> 'a"
 where
-  "of_bit b = bit_case 0 1 b" 
+  "of_bit b = case_bit 0 1 b" 
 
 lemma of_bit_eq [simp, code]:
   "of_bit 0 = 0"
diff -r 05f5fdb8d093 -r dd7992d4a61a src/HOL/Library/IArray.thy
--- a/src/HOL/Library/IArray.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Library/IArray.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -63,11 +63,11 @@
 by (cases as) simp
 
 lemma [code]:
-"iarray_rec f as = f (IArray.list_of as)"
+"rec_iarray f as = f (IArray.list_of as)"
 by (cases as) simp
 
 lemma [code]:
-"iarray_case f as = f (IArray.list_of as)"
+"case_iarray f as = f (IArray.list_of as)"
 by (cases as) simp
 
 lemma [code]:
diff -r 05f5fdb8d093 -r dd7992d4a61a src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Predicate.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -531,11 +531,11 @@
   by (fact equal_refl)
 
 lemma [code]:
-  "pred_case f P = f (eval P)"
+  "case_pred f P = f (eval P)"
   by (cases P) simp
 
 lemma [code]:
-  "pred_rec f P = f (eval P)"
+  "rec_pred f P = f (eval P)"
   by (cases P) simp
 
 inductive eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where "eq x x"
@@ -722,4 +722,3 @@
 hide_fact (open) null_def member_def
 
 end
-
diff -r 05f5fdb8d093 -r dd7992d4a61a src/HOL/SET_Protocol/Message_SET.thy
--- a/src/HOL/SET_Protocol/Message_SET.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -80,7 +80,7 @@
 
 
 definition nat_of_agent :: "agent => nat" where
-   "nat_of_agent == agent_case (curry prod_encode 0)
+   "nat_of_agent == case_agent (curry prod_encode 0)
                                (curry prod_encode 1)
                                (curry prod_encode 2)
                                (curry prod_encode 3)
diff -r 05f5fdb8d093 -r dd7992d4a61a src/HOL/String.thy
--- a/src/HOL/String.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/String.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -286,13 +286,13 @@
 
 code_datatype Char -- {* drop case certificate for char *}
 
-lemma char_case_code [code]:
-  "char_case f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
+lemma case_char_code [code]:
+  "case_char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
   by (cases c)
     (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.cases)
 
 lemma [code]:
-  "char_rec = char_case"
+  "rec_char = case_char"
   by (simp add: fun_eq_iff split: char.split)
 
 definition char_of_nat :: "nat \<Rightarrow> char" where
diff -r 05f5fdb8d093 -r dd7992d4a61a src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Feb 12 08:35:57 2014 +0100
@@ -1226,8 +1226,8 @@
         mk_nthN n (Term.list_comb (Const (Lev, LevT), ss) $ nat) i
       end;
 
-    val Lev_0s = flat (mk_rec_simps n @{thm nat_rec_0_imp} [Lev_def]);
-    val Lev_Sucs = flat (mk_rec_simps n @{thm nat_rec_Suc_imp} [Lev_def]);
+    val Lev_0s = flat (mk_rec_simps n @{thm rec_nat_0_imp} [Lev_def]);
+    val Lev_Sucs = flat (mk_rec_simps n @{thm rec_nat_Suc_imp} [Lev_def]);
 
     val rv_bind = mk_internal_b rvN;
     val rv_def_bind = rpair [] (Thm.def_binding rv_bind);
@@ -1433,7 +1433,7 @@
           split_conj_thm (if n = 1 then set_rv_Lev' RS mk_conjunctN n i RS mp
             else set_rv_Lev' RS mk_conjunctN n i RS mp RSN
               (2, @{thm sum.weak_case_cong} RS iffD1) RS
-              (mk_case_sumN n i' RS iffD1))) ks) ks
+              (mk_sum_caseN n i' RS iffD1))) ks) ks
       end;
 
     val set_Lev_thmsss =
diff -r 05f5fdb8d093 -r dd7992d4a61a src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -639,15 +639,15 @@
 refute [expect = genuine]
 oops
 
-lemma "T1_rec a b A = a"
+lemma "rec_T1 a b A = a"
 refute [expect = none]
 by simp
 
-lemma "T1_rec a b B = b"
+lemma "rec_T1 a b B = b"
 refute [expect = none]
 by simp
 
-lemma "P (T1_rec a b x)"
+lemma "P (rec_T1 a b x)"
 refute [expect = genuine]
 oops
 
@@ -669,15 +669,15 @@
 refute [expect = genuine]
 oops
 
-lemma "T2_rec c d (C x) = c x"
+lemma "rec_T2 c d (C x) = c x"
 refute [maxsize = 4, expect = none]
 by simp
 
-lemma "T2_rec c d (D x) = d x"
+lemma "rec_T2 c d (D x) = d x"
 refute [maxsize = 4, expect = none]
 by simp
 
-lemma "P (T2_rec c d x)"
+lemma "P (rec_T2 c d x)"
 refute [expect = genuine]
 oops
 
@@ -699,11 +699,11 @@
 refute [expect = genuine]
 oops
 
-lemma "T3_rec e (E x) = e x"
+lemma "rec_T3 e (E x) = e x"
 refute [maxsize = 2, expect = none]
 by simp
 
-lemma "P (T3_rec e x)"
+lemma "P (rec_T3 e x)"
 refute [expect = genuine]
 oops
 
@@ -802,19 +802,19 @@
 refute [expect = potential]
 oops
 
-lemma "BitList_rec nil bit0 bit1 BitListNil = nil"
+lemma "rec_BitList nil bit0 bit1 BitListNil = nil"
 refute [maxsize = 4, expect = none]
 by simp
 
-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)"
 refute [maxsize = 2, expect = none]
 by simp
 
-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)"
 refute [maxsize = 2, expect = none]
 by simp
 
-lemma "P (BitList_rec nil bit0 bit1 x)"
+lemma "P (rec_BitList nil bit0 bit1 x)"
 refute [expect = potential]
 oops
 
@@ -832,7 +832,7 @@
 refute [expect = potential]
 oops
 
-lemma "BinTree_rec l n (Leaf x) = l x"
+lemma "rec_BinTree l n (Leaf x) = l x"
   refute [maxsize = 1, expect = none]
   (* The "maxsize = 1" tests are a bit pointless: for some formulae
      below, refute will find no countermodel simply because this
@@ -840,11 +840,11 @@
      larger size already takes too long. *)
 by simp
 
-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)"
 refute [maxsize = 1, expect = none]
 by simp
 
-lemma "P (BinTree_rec l n x)"
+lemma "P (rec_BinTree l n x)"
 refute [expect = potential]
 oops
 
@@ -877,15 +877,15 @@
 refute [expect = potential]
 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"
 refute [maxsize = 1, expect = none]
 by simp
 
-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)"
 refute [maxsize = 1, expect = none]
 by simp
 
-lemma "P (aexp_bexp_rec_1 number ite equal x)"
+lemma "P (rec_aexp_bexp_1 number ite equal x)"
 refute [expect = potential]
 oops
 
@@ -893,11 +893,11 @@
 refute [expect = potential]
 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)"
 refute [maxsize = 1, expect = none]
 by simp
 
-lemma "P (aexp_bexp_rec_2 number ite equal x)"
+lemma "P (rec_aexp_bexp_2 number ite equal x)"
 refute [expect = potential]
 oops
 
@@ -952,35 +952,35 @@
 refute [expect = potential]
 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"
 refute [maxsize = 3, expect = none]
 by simp
 
-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)"
 refute [maxsize = 1, expect = none]
 by simp
 
-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)"
 refute [maxsize = 1, expect = none]
 by simp
 
-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)"
 refute [maxsize = 1, expect = none]
 by simp
 
-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)"
 refute [maxsize = 1, expect = none]
 by simp
 
-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"
 refute [maxsize = 3, expect = none]
 by simp
 
-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)"
 refute [expect = potential]
 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)"
 refute [expect = potential]
 oops
 
@@ -1002,39 +1002,39 @@
 refute [expect = potential]
 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)"
 refute [maxsize = 1, expect = none]
 by simp
 
-lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>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 (\<lambda>b. rec_XOpt_3 cx dx n1 s1 n2 s2 (x b))"
 refute [maxsize = 1, expect = none]
 by simp
 
-lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 None = n1"
+lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 None = n1"
 refute [maxsize = 2, expect = none]
 by simp
 
-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)"
 refute [maxsize = 1, expect = none]
 by simp
 
-lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 None = n2"
+lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 None = n2"
 refute [maxsize = 2, expect = none]
 by simp
 
-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)"
 refute [maxsize = 1, expect = none]
 by simp
 
-lemma "P (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
+lemma "P (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
 refute [expect = potential]
 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)"
 refute [expect = potential]
 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)"
 refute [expect = potential]
 oops
 
@@ -1052,23 +1052,23 @@
 refute [expect = potential]
 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)"
 refute [maxsize = 1, expect = none]
 by simp
 
-lemma "YOpt_rec_2 cy n s None = n"
+lemma "rec_YOpt_2 cy n s None = n"
 refute [maxsize = 2, expect = none]
 by simp
 
-lemma "YOpt_rec_2 cy n s (Some x) = s x (\<lambda>a. YOpt_rec_1 cy n s (x a))"
+lemma "rec_YOpt_2 cy n s (Some x) = s x (\<lambda>a. rec_YOpt_1 cy n s (x a))"
 refute [maxsize = 1, expect = none]
 by simp
 
-lemma "P (YOpt_rec_1 cy n s x)"
+lemma "P (rec_YOpt_1 cy n s x)"
 refute [expect = potential]
 oops
 
-lemma "P (YOpt_rec_2 cy n s x)"
+lemma "P (rec_YOpt_2 cy n s x)"
 refute [expect = potential]
 oops
 
@@ -1086,23 +1086,23 @@
 refute [expect = potential]
 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)"
 refute [maxsize = 1, expect = none]
 by simp
 
-lemma "Trie_rec_2 tr nil cons [] = nil"
+lemma "rec_Trie_2 tr nil cons [] = nil"
 refute [maxsize = 3, expect = none]
 by simp
 
-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)"
 refute [maxsize = 1, expect = none]
 by simp
 
-lemma "P (Trie_rec_1 tr nil cons x)"
+lemma "P (rec_Trie_1 tr nil cons x)"
 refute [expect = potential]
 oops
 
-lemma "P (Trie_rec_2 tr nil cons x)"
+lemma "P (rec_Trie_2 tr nil cons x)"
 refute [expect = potential]
 oops
 
@@ -1120,15 +1120,15 @@
 refute [expect = potential]
 oops
 
-lemma "InfTree_rec leaf node Leaf = leaf"
+lemma "rec_InfTree leaf node Leaf = leaf"
 refute [maxsize = 2, expect = none]
 by simp
 
-lemma "InfTree_rec leaf node (Node x) = node x (\<lambda>n. InfTree_rec leaf node (x n))"
+lemma "rec_InfTree leaf node (Node x) = node x (\<lambda>n. rec_InfTree leaf node (x n))"
 refute [maxsize = 1, expect = none]
 by simp
 
-lemma "P (InfTree_rec leaf node x)"
+lemma "P (rec_InfTree leaf node x)"
 refute [expect = potential]
 oops
 
@@ -1146,19 +1146,19 @@
 refute [expect = potential]
 oops
 
-lemma "lambda_rec var app lam (Var x) = var x"
+lemma "rec_lambda var app lam (Var x) = var x"
 refute [maxsize = 1, expect = none]
 by simp
 
-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)"
 refute [maxsize = 1, expect = none]
 by simp
 
-lemma "lambda_rec var app lam (Lam x) = lam x (\<lambda>a. lambda_rec var app lam (x a))"
+lemma "rec_lambda var app lam (Lam x) = lam x (\<lambda>a. rec_lambda var app lam (x a))"
 refute [maxsize = 1, expect = none]
 by simp
 
-lemma "P (lambda_rec v a l x)"
+lemma "P (rec_lambda v a l x)"
 refute [expect = potential]
 oops
 
@@ -1179,35 +1179,35 @@
 refute [expect = potential]
 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)"
 refute [maxsize = 1, expect = none]
 by simp
 
-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"
 refute [maxsize = 1, expect = none]
 by simp
 
-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)"
 refute [maxsize = 1, expect = none]
 by simp
 
-lemma "U_rec_3 e c d nil cons [] = nil"
+lemma "rec_U_3 e c d nil cons [] = nil"
 refute [maxsize = 2, expect = none]
 by simp
 
-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)"
 refute [maxsize = 1, expect = none]
 by simp
 
-lemma "P (U_rec_1 e c d nil cons x)"
+lemma "P (rec_U_1 e c d nil cons x)"
 refute [expect = potential]
 oops
 
-lemma "P (U_rec_2 e c d nil cons x)"
+lemma "P (rec_U_2 e c d nil cons x)"
 refute [expect = potential]
 oops
 
-lemma "P (U_rec_3 e c d nil cons x)"
+lemma "P (rec_U_3 e c d nil cons x)"
 refute [expect = potential]
 oops