adapted theories to 'xxx_case' to 'case_xxx'
authorblanchet
Wed Feb 12 08:35:57 2014 +0100 (2014-02-12)
changeset 55416dd7992d4a61a
parent 55415 05f5fdb8d093
child 55417 01fbfb60c33e
adapted theories to 'xxx_case' to 'case_xxx'
* * *
'char_case' -> 'case_char' and same for 'rec'
* * *
compile
* * *
renamed 'xxx_case' to 'case_xxx'
src/HOL/Auth/Public.thy
src/HOL/Auth/Shared.thy
src/HOL/Code_Numeral.thy
src/HOL/HOLCF/IOA/Storage/Action.thy
src/HOL/Lazy_Sequence.thy
src/HOL/Library/Bit.thy
src/HOL/Library/IArray.thy
src/HOL/Predicate.thy
src/HOL/SET_Protocol/Message_SET.thy
src/HOL/String.thy
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/ex/Refute_Examples.thy
     1.1 --- a/src/HOL/Auth/Public.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/Auth/Public.thy	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -61,7 +61,7 @@
     1.4    injective_publicKey:
     1.5      "publicKey b A = publicKey c A' ==> b=c & A=A'"
     1.6     apply (rule exI [of _ 
     1.7 -       "%b A. 2 * agent_case 0 (\<lambda>n. n + 2) 1 A + keymode_case 0 1 b"])
     1.8 +       "%b A. 2 * case_agent 0 (\<lambda>n. n + 2) 1 A + case_keymode 0 1 b"])
     1.9     apply (auto simp add: inj_on_def split: agent.split keymode.split)
    1.10     apply presburger
    1.11     apply presburger
    1.12 @@ -137,7 +137,7 @@
    1.13  specification (shrK)
    1.14    inj_shrK: "inj shrK"
    1.15    --{*No two agents have the same long-term key*}
    1.16 -   apply (rule exI [of _ "agent_case 0 (\<lambda>n. n + 2) 1"]) 
    1.17 +   apply (rule exI [of _ "case_agent 0 (\<lambda>n. n + 2) 1"]) 
    1.18     apply (simp add: inj_on_def split: agent.split) 
    1.19     done
    1.20  
     2.1 --- a/src/HOL/Auth/Shared.thy	Wed Feb 12 08:35:57 2014 +0100
     2.2 +++ b/src/HOL/Auth/Shared.thy	Wed Feb 12 08:35:57 2014 +0100
     2.3 @@ -17,7 +17,7 @@
     2.4  specification (shrK)
     2.5    inj_shrK: "inj shrK"
     2.6    --{*No two agents have the same long-term key*}
     2.7 -   apply (rule exI [of _ "agent_case 0 (\<lambda>n. n + 2) 1"]) 
     2.8 +   apply (rule exI [of _ "case_agent 0 (\<lambda>n. n + 2) 1"]) 
     2.9     apply (simp add: inj_on_def split: agent.split) 
    2.10     done
    2.11  
     3.1 --- a/src/HOL/Code_Numeral.thy	Wed Feb 12 08:35:57 2014 +0100
     3.2 +++ b/src/HOL/Code_Numeral.thy	Wed Feb 12 08:35:57 2014 +0100
     3.3 @@ -783,7 +783,7 @@
     3.4    by (rule is_measure_trivial)
     3.5  
     3.6  
     3.7 -subsection {* Inductive represenation of target language naturals *}
     3.8 +subsection {* Inductive representation of target language naturals *}
     3.9  
    3.10  lift_definition Suc :: "natural \<Rightarrow> natural"
    3.11    is Nat.Suc
    3.12 @@ -794,7 +794,7 @@
    3.13  rep_datatype "0::natural" Suc
    3.14    by (transfer, fact nat.induct nat.inject nat.distinct)+
    3.15  
    3.16 -lemma natural_case [case_names nat, cases type: natural]:
    3.17 +lemma natural_cases [case_names nat, cases type: natural]:
    3.18    fixes m :: natural
    3.19    assumes "\<And>n. m = of_nat n \<Longrightarrow> P"
    3.20    shows P
    3.21 @@ -876,7 +876,7 @@
    3.22    by transfer (simp add: fun_eq_iff)
    3.23  
    3.24  lemma [code, code_unfold]:
    3.25 -  "natural_case f g n = (if n = 0 then f else g (n - 1))"
    3.26 +  "case_natural f g n = (if n = 0 then f else g (n - 1))"
    3.27    by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def)
    3.28  
    3.29  declare natural.recs [code del]
     4.1 --- a/src/HOL/HOLCF/IOA/Storage/Action.thy	Wed Feb 12 08:35:57 2014 +0100
     4.2 +++ b/src/HOL/HOLCF/IOA/Storage/Action.thy	Wed Feb 12 08:35:57 2014 +0100
     4.3 @@ -8,9 +8,9 @@
     4.4  imports Main
     4.5  begin
     4.6  
     4.7 -datatype action = New  | Loc nat | Free nat
     4.8 +datatype action = New | Loc nat | Free nat
     4.9  
    4.10 -lemma [cong]: "!!x. x = y ==> action_case a b c x = action_case a b c y"
    4.11 +lemma [cong]: "!!x. x = y ==> case_action a b c x = case_action a b c y"
    4.12    by simp
    4.13  
    4.14  end
     5.1 --- a/src/HOL/Lazy_Sequence.thy	Wed Feb 12 08:35:57 2014 +0100
     5.2 +++ b/src/HOL/Lazy_Sequence.thy	Wed Feb 12 08:35:57 2014 +0100
     5.3 @@ -35,12 +35,12 @@
     5.4    "size (xq :: 'a lazy_sequence) = 0"
     5.5    by (cases xq) simp
     5.6  
     5.7 -lemma lazy_sequence_case [simp]:
     5.8 -  "lazy_sequence_case f xq = f (list_of_lazy_sequence xq)"
     5.9 +lemma case_lazy_sequence [simp]:
    5.10 +  "case_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
    5.11    by (cases xq) auto
    5.12  
    5.13 -lemma lazy_sequence_rec [simp]:
    5.14 -  "lazy_sequence_rec f xq = f (list_of_lazy_sequence xq)"
    5.15 +lemma rec_lazy_sequence [simp]:
    5.16 +  "rec_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
    5.17    by (cases xq) auto
    5.18  
    5.19  definition Lazy_Sequence :: "(unit \<Rightarrow> ('a \<times> 'a lazy_sequence) option) \<Rightarrow> 'a lazy_sequence"
    5.20 @@ -346,4 +346,3 @@
    5.21    if_seq_def those_def not_seq_def product_def 
    5.22  
    5.23  end
    5.24 -
     6.1 --- a/src/HOL/Library/Bit.thy	Wed Feb 12 08:35:57 2014 +0100
     6.2 +++ b/src/HOL/Library/Bit.thy	Wed Feb 12 08:35:57 2014 +0100
     6.3 @@ -102,10 +102,10 @@
     6.4  begin
     6.5  
     6.6  definition plus_bit_def:
     6.7 -  "x + y = bit_case y (bit_case 1 0 y) x"
     6.8 +  "x + y = case_bit y (case_bit 1 0 y) x"
     6.9  
    6.10  definition times_bit_def:
    6.11 -  "x * y = bit_case 0 y x"
    6.12 +  "x * y = case_bit 0 y x"
    6.13  
    6.14  definition uminus_bit_def [simp]:
    6.15    "- x = (x :: bit)"
    6.16 @@ -167,7 +167,7 @@
    6.17  
    6.18  definition of_bit :: "bit \<Rightarrow> 'a"
    6.19  where
    6.20 -  "of_bit b = bit_case 0 1 b" 
    6.21 +  "of_bit b = case_bit 0 1 b" 
    6.22  
    6.23  lemma of_bit_eq [simp, code]:
    6.24    "of_bit 0 = 0"
     7.1 --- a/src/HOL/Library/IArray.thy	Wed Feb 12 08:35:57 2014 +0100
     7.2 +++ b/src/HOL/Library/IArray.thy	Wed Feb 12 08:35:57 2014 +0100
     7.3 @@ -63,11 +63,11 @@
     7.4  by (cases as) simp
     7.5  
     7.6  lemma [code]:
     7.7 -"iarray_rec f as = f (IArray.list_of as)"
     7.8 +"rec_iarray f as = f (IArray.list_of as)"
     7.9  by (cases as) simp
    7.10  
    7.11  lemma [code]:
    7.12 -"iarray_case f as = f (IArray.list_of as)"
    7.13 +"case_iarray f as = f (IArray.list_of as)"
    7.14  by (cases as) simp
    7.15  
    7.16  lemma [code]:
     8.1 --- a/src/HOL/Predicate.thy	Wed Feb 12 08:35:57 2014 +0100
     8.2 +++ b/src/HOL/Predicate.thy	Wed Feb 12 08:35:57 2014 +0100
     8.3 @@ -531,11 +531,11 @@
     8.4    by (fact equal_refl)
     8.5  
     8.6  lemma [code]:
     8.7 -  "pred_case f P = f (eval P)"
     8.8 +  "case_pred f P = f (eval P)"
     8.9    by (cases P) simp
    8.10  
    8.11  lemma [code]:
    8.12 -  "pred_rec f P = f (eval P)"
    8.13 +  "rec_pred f P = f (eval P)"
    8.14    by (cases P) simp
    8.15  
    8.16  inductive eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where "eq x x"
    8.17 @@ -722,4 +722,3 @@
    8.18  hide_fact (open) null_def member_def
    8.19  
    8.20  end
    8.21 -
     9.1 --- a/src/HOL/SET_Protocol/Message_SET.thy	Wed Feb 12 08:35:57 2014 +0100
     9.2 +++ b/src/HOL/SET_Protocol/Message_SET.thy	Wed Feb 12 08:35:57 2014 +0100
     9.3 @@ -80,7 +80,7 @@
     9.4  
     9.5  
     9.6  definition nat_of_agent :: "agent => nat" where
     9.7 -   "nat_of_agent == agent_case (curry prod_encode 0)
     9.8 +   "nat_of_agent == case_agent (curry prod_encode 0)
     9.9                                 (curry prod_encode 1)
    9.10                                 (curry prod_encode 2)
    9.11                                 (curry prod_encode 3)
    10.1 --- a/src/HOL/String.thy	Wed Feb 12 08:35:57 2014 +0100
    10.2 +++ b/src/HOL/String.thy	Wed Feb 12 08:35:57 2014 +0100
    10.3 @@ -286,13 +286,13 @@
    10.4  
    10.5  code_datatype Char -- {* drop case certificate for char *}
    10.6  
    10.7 -lemma char_case_code [code]:
    10.8 -  "char_case f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
    10.9 +lemma case_char_code [code]:
   10.10 +  "case_char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
   10.11    by (cases c)
   10.12      (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.cases)
   10.13  
   10.14  lemma [code]:
   10.15 -  "char_rec = char_case"
   10.16 +  "rec_char = case_char"
   10.17    by (simp add: fun_eq_iff split: char.split)
   10.18  
   10.19  definition char_of_nat :: "nat \<Rightarrow> char" where
    11.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Feb 12 08:35:57 2014 +0100
    11.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Feb 12 08:35:57 2014 +0100
    11.3 @@ -1226,8 +1226,8 @@
    11.4          mk_nthN n (Term.list_comb (Const (Lev, LevT), ss) $ nat) i
    11.5        end;
    11.6  
    11.7 -    val Lev_0s = flat (mk_rec_simps n @{thm nat_rec_0_imp} [Lev_def]);
    11.8 -    val Lev_Sucs = flat (mk_rec_simps n @{thm nat_rec_Suc_imp} [Lev_def]);
    11.9 +    val Lev_0s = flat (mk_rec_simps n @{thm rec_nat_0_imp} [Lev_def]);
   11.10 +    val Lev_Sucs = flat (mk_rec_simps n @{thm rec_nat_Suc_imp} [Lev_def]);
   11.11  
   11.12      val rv_bind = mk_internal_b rvN;
   11.13      val rv_def_bind = rpair [] (Thm.def_binding rv_bind);
   11.14 @@ -1433,7 +1433,7 @@
   11.15            split_conj_thm (if n = 1 then set_rv_Lev' RS mk_conjunctN n i RS mp
   11.16              else set_rv_Lev' RS mk_conjunctN n i RS mp RSN
   11.17                (2, @{thm sum.weak_case_cong} RS iffD1) RS
   11.18 -              (mk_case_sumN n i' RS iffD1))) ks) ks
   11.19 +              (mk_sum_caseN n i' RS iffD1))) ks) ks
   11.20        end;
   11.21  
   11.22      val set_Lev_thmsss =
    12.1 --- a/src/HOL/ex/Refute_Examples.thy	Wed Feb 12 08:35:57 2014 +0100
    12.2 +++ b/src/HOL/ex/Refute_Examples.thy	Wed Feb 12 08:35:57 2014 +0100
    12.3 @@ -639,15 +639,15 @@
    12.4  refute [expect = genuine]
    12.5  oops
    12.6  
    12.7 -lemma "T1_rec a b A = a"
    12.8 +lemma "rec_T1 a b A = a"
    12.9  refute [expect = none]
   12.10  by simp
   12.11  
   12.12 -lemma "T1_rec a b B = b"
   12.13 +lemma "rec_T1 a b B = b"
   12.14  refute [expect = none]
   12.15  by simp
   12.16  
   12.17 -lemma "P (T1_rec a b x)"
   12.18 +lemma "P (rec_T1 a b x)"
   12.19  refute [expect = genuine]
   12.20  oops
   12.21  
   12.22 @@ -669,15 +669,15 @@
   12.23  refute [expect = genuine]
   12.24  oops
   12.25  
   12.26 -lemma "T2_rec c d (C x) = c x"
   12.27 +lemma "rec_T2 c d (C x) = c x"
   12.28  refute [maxsize = 4, expect = none]
   12.29  by simp
   12.30  
   12.31 -lemma "T2_rec c d (D x) = d x"
   12.32 +lemma "rec_T2 c d (D x) = d x"
   12.33  refute [maxsize = 4, expect = none]
   12.34  by simp
   12.35  
   12.36 -lemma "P (T2_rec c d x)"
   12.37 +lemma "P (rec_T2 c d x)"
   12.38  refute [expect = genuine]
   12.39  oops
   12.40  
   12.41 @@ -699,11 +699,11 @@
   12.42  refute [expect = genuine]
   12.43  oops
   12.44  
   12.45 -lemma "T3_rec e (E x) = e x"
   12.46 +lemma "rec_T3 e (E x) = e x"
   12.47  refute [maxsize = 2, expect = none]
   12.48  by simp
   12.49  
   12.50 -lemma "P (T3_rec e x)"
   12.51 +lemma "P (rec_T3 e x)"
   12.52  refute [expect = genuine]
   12.53  oops
   12.54  
   12.55 @@ -802,19 +802,19 @@
   12.56  refute [expect = potential]
   12.57  oops
   12.58  
   12.59 -lemma "BitList_rec nil bit0 bit1 BitListNil = nil"
   12.60 +lemma "rec_BitList nil bit0 bit1 BitListNil = nil"
   12.61  refute [maxsize = 4, expect = none]
   12.62  by simp
   12.63  
   12.64 -lemma "BitList_rec nil bit0 bit1 (Bit0 xs) = bit0 xs (BitList_rec nil bit0 bit1 xs)"
   12.65 +lemma "rec_BitList nil bit0 bit1 (Bit0 xs) = bit0 xs (rec_BitList nil bit0 bit1 xs)"
   12.66  refute [maxsize = 2, expect = none]
   12.67  by simp
   12.68  
   12.69 -lemma "BitList_rec nil bit0 bit1 (Bit1 xs) = bit1 xs (BitList_rec nil bit0 bit1 xs)"
   12.70 +lemma "rec_BitList nil bit0 bit1 (Bit1 xs) = bit1 xs (rec_BitList nil bit0 bit1 xs)"
   12.71  refute [maxsize = 2, expect = none]
   12.72  by simp
   12.73  
   12.74 -lemma "P (BitList_rec nil bit0 bit1 x)"
   12.75 +lemma "P (rec_BitList nil bit0 bit1 x)"
   12.76  refute [expect = potential]
   12.77  oops
   12.78  
   12.79 @@ -832,7 +832,7 @@
   12.80  refute [expect = potential]
   12.81  oops
   12.82  
   12.83 -lemma "BinTree_rec l n (Leaf x) = l x"
   12.84 +lemma "rec_BinTree l n (Leaf x) = l x"
   12.85    refute [maxsize = 1, expect = none]
   12.86    (* The "maxsize = 1" tests are a bit pointless: for some formulae
   12.87       below, refute will find no countermodel simply because this
   12.88 @@ -840,11 +840,11 @@
   12.89       larger size already takes too long. *)
   12.90  by simp
   12.91  
   12.92 -lemma "BinTree_rec l n (Node x y) = n x y (BinTree_rec l n x) (BinTree_rec l n y)"
   12.93 +lemma "rec_BinTree l n (Node x y) = n x y (rec_BinTree l n x) (rec_BinTree l n y)"
   12.94  refute [maxsize = 1, expect = none]
   12.95  by simp
   12.96  
   12.97 -lemma "P (BinTree_rec l n x)"
   12.98 +lemma "P (rec_BinTree l n x)"
   12.99  refute [expect = potential]
  12.100  oops
  12.101  
  12.102 @@ -877,15 +877,15 @@
  12.103  refute [expect = potential]
  12.104  oops
  12.105  
  12.106 -lemma "aexp_bexp_rec_1 number ite equal (Number x) = number x"
  12.107 +lemma "rec_aexp_bexp_1 number ite equal (Number x) = number x"
  12.108  refute [maxsize = 1, expect = none]
  12.109  by simp
  12.110  
  12.111 -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)"
  12.112 +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)"
  12.113  refute [maxsize = 1, expect = none]
  12.114  by simp
  12.115  
  12.116 -lemma "P (aexp_bexp_rec_1 number ite equal x)"
  12.117 +lemma "P (rec_aexp_bexp_1 number ite equal x)"
  12.118  refute [expect = potential]
  12.119  oops
  12.120  
  12.121 @@ -893,11 +893,11 @@
  12.122  refute [expect = potential]
  12.123  oops
  12.124  
  12.125 -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)"
  12.126 +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)"
  12.127  refute [maxsize = 1, expect = none]
  12.128  by simp
  12.129  
  12.130 -lemma "P (aexp_bexp_rec_2 number ite equal x)"
  12.131 +lemma "P (rec_aexp_bexp_2 number ite equal x)"
  12.132  refute [expect = potential]
  12.133  oops
  12.134  
  12.135 @@ -952,35 +952,35 @@
  12.136  refute [expect = potential]
  12.137  oops
  12.138  
  12.139 -lemma "X_Y_rec_1 a b c d e f A = a"
  12.140 +lemma "rec_X_Y_1 a b c d e f A = a"
  12.141  refute [maxsize = 3, expect = none]
  12.142  by simp
  12.143  
  12.144 -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)"
  12.145 +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)"
  12.146  refute [maxsize = 1, expect = none]
  12.147  by simp
  12.148  
  12.149 -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)"
  12.150 +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)"
  12.151  refute [maxsize = 1, expect = none]
  12.152  by simp
  12.153  
  12.154 -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)"
  12.155 +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)"
  12.156  refute [maxsize = 1, expect = none]
  12.157  by simp
  12.158  
  12.159 -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)"
  12.160 +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)"
  12.161  refute [maxsize = 1, expect = none]
  12.162  by simp
  12.163  
  12.164 -lemma "X_Y_rec_2 a b c d e f F = f"
  12.165 +lemma "rec_X_Y_2 a b c d e f F = f"
  12.166  refute [maxsize = 3, expect = none]
  12.167  by simp
  12.168  
  12.169 -lemma "P (X_Y_rec_1 a b c d e f x)"
  12.170 +lemma "P (rec_X_Y_1 a b c d e f x)"
  12.171  refute [expect = potential]
  12.172  oops
  12.173  
  12.174 -lemma "P (X_Y_rec_2 a b c d e f y)"
  12.175 +lemma "P (rec_X_Y_2 a b c d e f y)"
  12.176  refute [expect = potential]
  12.177  oops
  12.178  
  12.179 @@ -1002,39 +1002,39 @@
  12.180  refute [expect = potential]
  12.181  oops
  12.182  
  12.183 -lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (CX x) = cx x (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
  12.184 +lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (CX x) = cx x (rec_XOpt_2 cx dx n1 s1 n2 s2 x)"
  12.185  refute [maxsize = 1, expect = none]
  12.186  by simp
  12.187  
  12.188 -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))"
  12.189 +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))"
  12.190  refute [maxsize = 1, expect = none]
  12.191  by simp
  12.192  
  12.193 -lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 None = n1"
  12.194 +lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 None = n1"
  12.195  refute [maxsize = 2, expect = none]
  12.196  by simp
  12.197  
  12.198 -lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
  12.199 +lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
  12.200  refute [maxsize = 1, expect = none]
  12.201  by simp
  12.202  
  12.203 -lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 None = n2"
  12.204 +lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 None = n2"
  12.205  refute [maxsize = 2, expect = none]
  12.206  by simp
  12.207  
  12.208 -lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
  12.209 +lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
  12.210  refute [maxsize = 1, expect = none]
  12.211  by simp
  12.212  
  12.213 -lemma "P (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
  12.214 +lemma "P (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
  12.215  refute [expect = potential]
  12.216  oops
  12.217  
  12.218 -lemma "P (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
  12.219 +lemma "P (rec_XOpt_2 cx dx n1 s1 n2 s2 x)"
  12.220  refute [expect = potential]
  12.221  oops
  12.222  
  12.223 -lemma "P (XOpt_rec_3 cx dx n1 s1 n2 s2 x)"
  12.224 +lemma "P (rec_XOpt_3 cx dx n1 s1 n2 s2 x)"
  12.225  refute [expect = potential]
  12.226  oops
  12.227  
  12.228 @@ -1052,23 +1052,23 @@
  12.229  refute [expect = potential]
  12.230  oops
  12.231  
  12.232 -lemma "YOpt_rec_1 cy n s (CY x) = cy x (YOpt_rec_2 cy n s x)"
  12.233 +lemma "rec_YOpt_1 cy n s (CY x) = cy x (rec_YOpt_2 cy n s x)"
  12.234  refute [maxsize = 1, expect = none]
  12.235  by simp
  12.236  
  12.237 -lemma "YOpt_rec_2 cy n s None = n"
  12.238 +lemma "rec_YOpt_2 cy n s None = n"
  12.239  refute [maxsize = 2, expect = none]
  12.240  by simp
  12.241  
  12.242 -lemma "YOpt_rec_2 cy n s (Some x) = s x (\<lambda>a. YOpt_rec_1 cy n s (x a))"
  12.243 +lemma "rec_YOpt_2 cy n s (Some x) = s x (\<lambda>a. rec_YOpt_1 cy n s (x a))"
  12.244  refute [maxsize = 1, expect = none]
  12.245  by simp
  12.246  
  12.247 -lemma "P (YOpt_rec_1 cy n s x)"
  12.248 +lemma "P (rec_YOpt_1 cy n s x)"
  12.249  refute [expect = potential]
  12.250  oops
  12.251  
  12.252 -lemma "P (YOpt_rec_2 cy n s x)"
  12.253 +lemma "P (rec_YOpt_2 cy n s x)"
  12.254  refute [expect = potential]
  12.255  oops
  12.256  
  12.257 @@ -1086,23 +1086,23 @@
  12.258  refute [expect = potential]
  12.259  oops
  12.260  
  12.261 -lemma "Trie_rec_1 tr nil cons (TR x) = tr x (Trie_rec_2 tr nil cons x)"
  12.262 +lemma "rec_Trie_1 tr nil cons (TR x) = tr x (rec_Trie_2 tr nil cons x)"
  12.263  refute [maxsize = 1, expect = none]
  12.264  by simp
  12.265  
  12.266 -lemma "Trie_rec_2 tr nil cons [] = nil"
  12.267 +lemma "rec_Trie_2 tr nil cons [] = nil"
  12.268  refute [maxsize = 3, expect = none]
  12.269  by simp
  12.270  
  12.271 -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)"
  12.272 +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)"
  12.273  refute [maxsize = 1, expect = none]
  12.274  by simp
  12.275  
  12.276 -lemma "P (Trie_rec_1 tr nil cons x)"
  12.277 +lemma "P (rec_Trie_1 tr nil cons x)"
  12.278  refute [expect = potential]
  12.279  oops
  12.280  
  12.281 -lemma "P (Trie_rec_2 tr nil cons x)"
  12.282 +lemma "P (rec_Trie_2 tr nil cons x)"
  12.283  refute [expect = potential]
  12.284  oops
  12.285  
  12.286 @@ -1120,15 +1120,15 @@
  12.287  refute [expect = potential]
  12.288  oops
  12.289  
  12.290 -lemma "InfTree_rec leaf node Leaf = leaf"
  12.291 +lemma "rec_InfTree leaf node Leaf = leaf"
  12.292  refute [maxsize = 2, expect = none]
  12.293  by simp
  12.294  
  12.295 -lemma "InfTree_rec leaf node (Node x) = node x (\<lambda>n. InfTree_rec leaf node (x n))"
  12.296 +lemma "rec_InfTree leaf node (Node x) = node x (\<lambda>n. rec_InfTree leaf node (x n))"
  12.297  refute [maxsize = 1, expect = none]
  12.298  by simp
  12.299  
  12.300 -lemma "P (InfTree_rec leaf node x)"
  12.301 +lemma "P (rec_InfTree leaf node x)"
  12.302  refute [expect = potential]
  12.303  oops
  12.304  
  12.305 @@ -1146,19 +1146,19 @@
  12.306  refute [expect = potential]
  12.307  oops
  12.308  
  12.309 -lemma "lambda_rec var app lam (Var x) = var x"
  12.310 +lemma "rec_lambda var app lam (Var x) = var x"
  12.311  refute [maxsize = 1, expect = none]
  12.312  by simp
  12.313  
  12.314 -lemma "lambda_rec var app lam (App x y) = app x y (lambda_rec var app lam x) (lambda_rec var app lam y)"
  12.315 +lemma "rec_lambda var app lam (App x y) = app x y (rec_lambda var app lam x) (rec_lambda var app lam y)"
  12.316  refute [maxsize = 1, expect = none]
  12.317  by simp
  12.318  
  12.319 -lemma "lambda_rec var app lam (Lam x) = lam x (\<lambda>a. lambda_rec var app lam (x a))"
  12.320 +lemma "rec_lambda var app lam (Lam x) = lam x (\<lambda>a. rec_lambda var app lam (x a))"
  12.321  refute [maxsize = 1, expect = none]
  12.322  by simp
  12.323  
  12.324 -lemma "P (lambda_rec v a l x)"
  12.325 +lemma "P (rec_lambda v a l x)"
  12.326  refute [expect = potential]
  12.327  oops
  12.328  
  12.329 @@ -1179,35 +1179,35 @@
  12.330  refute [expect = potential]
  12.331  oops
  12.332  
  12.333 -lemma "U_rec_1 e c d nil cons (E x) = e x (U_rec_2 e c d nil cons x)"
  12.334 +lemma "rec_U_1 e c d nil cons (E x) = e x (rec_U_2 e c d nil cons x)"
  12.335  refute [maxsize = 1, expect = none]
  12.336  by simp
  12.337  
  12.338 -lemma "U_rec_2 e c d nil cons (C x) = c x"
  12.339 +lemma "rec_U_2 e c d nil cons (C x) = c x"
  12.340  refute [maxsize = 1, expect = none]
  12.341  by simp
  12.342  
  12.343 -lemma "U_rec_2 e c d nil cons (D x) = d x (U_rec_3 e c d nil cons x)"
  12.344 +lemma "rec_U_2 e c d nil cons (D x) = d x (rec_U_3 e c d nil cons x)"
  12.345  refute [maxsize = 1, expect = none]
  12.346  by simp
  12.347  
  12.348 -lemma "U_rec_3 e c d nil cons [] = nil"
  12.349 +lemma "rec_U_3 e c d nil cons [] = nil"
  12.350  refute [maxsize = 2, expect = none]
  12.351  by simp
  12.352  
  12.353 -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)"
  12.354 +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)"
  12.355  refute [maxsize = 1, expect = none]
  12.356  by simp
  12.357  
  12.358 -lemma "P (U_rec_1 e c d nil cons x)"
  12.359 +lemma "P (rec_U_1 e c d nil cons x)"
  12.360  refute [expect = potential]
  12.361  oops
  12.362  
  12.363 -lemma "P (U_rec_2 e c d nil cons x)"
  12.364 +lemma "P (rec_U_2 e c d nil cons x)"
  12.365  refute [expect = potential]
  12.366  oops
  12.367  
  12.368 -lemma "P (U_rec_3 e c d nil cons x)"
  12.369 +lemma "P (rec_U_3 e c d nil cons x)"
  12.370  refute [expect = potential]
  12.371  oops
  12.372