merged
authorwenzelm
Fri, 25 Apr 2014 14:39:11 +0200
changeset 56721 f2ffead641d4
parent 56684 d8f32f55e463 (diff)
parent 56720 e1317a26f8c0 (current diff)
child 56722 ba1ac087b3a7
merged
src/Pure/Concurrent/volatile.scala
src/Pure/System/event_bus.scala
--- a/src/Doc/Classes/Classes.thy	Fri Apr 25 14:18:13 2014 +0200
+++ b/src/Doc/Classes/Classes.thy	Fri Apr 25 14:39:11 2014 +0200
@@ -175,7 +175,7 @@
 end %quote
 
 text {*
-  \noindent Note the occurence of the name @{text mult_nat} in the
+  \noindent Note the occurrence of the name @{text mult_nat} in the
   primrec declaration; by default, the local name of a class operation
   @{text f} to be instantiated on type constructor @{text \<kappa>} is
   mangled as @{text f_\<kappa>}.  In case of uncertainty, these names may be
--- a/src/HOL/Auth/Guard/Extensions.thy	Fri Apr 25 14:18:13 2014 +0200
+++ b/src/HOL/Auth/Guard/Extensions.thy	Fri Apr 25 14:39:11 2014 +0200
@@ -37,7 +37,6 @@
 subsubsection{*declarations for tactics*}
 
 declare analz_subset_parts [THEN subsetD, dest]
-declare image_eq_UN [simp]
 declare parts_insert2 [simp]
 declare analz_cut [dest]
 declare split_if_asm [split]
@@ -112,8 +111,9 @@
 
 lemma finite_keysFor [intro]: "finite G ==> finite (keysFor G)"
 apply (simp add: keysFor_def)
-apply (rule finite_UN_I, auto)
-apply (erule finite_induct, auto)
+apply (rule finite_imageI)
+apply (induct G rule: finite_induct)
+apply auto
 apply (case_tac "EX K X. x = Crypt K X", clarsimp)
 apply (subgoal_tac "{Ka. EX Xa. (Ka=K & Xa=X) | Crypt Ka Xa:F}
 = insert K (usekeys F)", auto simp: usekeys_def)
--- a/src/HOL/Auth/Guard/Guard.thy	Fri Apr 25 14:18:13 2014 +0200
+++ b/src/HOL/Auth/Guard/Guard.thy	Fri Apr 25 14:39:11 2014 +0200
@@ -56,7 +56,7 @@
 by (erule guard.induct, auto)
 
 lemma guard_Crypt: "[| Crypt K Y:guard n Ks; K ~:invKey`Ks |] ==> Y:guard n Ks"
-by (ind_cases "Crypt K Y:guard n Ks", auto)
+  by (ind_cases "Crypt K Y:guard n Ks") (auto intro!: image_eqI)
 
 lemma guard_MPair [iff]: "({|X,Y|}:guard n Ks) = (X:guard n Ks & Y:guard n Ks)"
 by (auto, (ind_cases "{|X,Y|}:guard n Ks", auto)+)
--- a/src/HOL/Auth/Guard/GuardK.thy	Fri Apr 25 14:18:13 2014 +0200
+++ b/src/HOL/Auth/Guard/GuardK.thy	Fri Apr 25 14:39:11 2014 +0200
@@ -63,7 +63,7 @@
 by (erule guardK.induct, auto dest: kparts_parts parts_sub)
 
 lemma guardK_Crypt: "[| Crypt K Y:guardK n Ks; K ~:invKey`Ks |] ==> Y:guardK n Ks"
-by (ind_cases "Crypt K Y:guardK n Ks", auto)
+  by (ind_cases "Crypt K Y:guardK n Ks") (auto intro!: image_eqI)
 
 lemma guardK_MPair [iff]: "({|X,Y|}:guardK n Ks)
 = (X:guardK n Ks & Y:guardK n Ks)"
--- a/src/HOL/Auth/Guard/Guard_Shared.thy	Fri Apr 25 14:18:13 2014 +0200
+++ b/src/HOL/Auth/Guard/Guard_Shared.thy	Fri Apr 25 14:39:11 2014 +0200
@@ -171,7 +171,7 @@
 lemma GuardK_Key_analz: "[| GuardK n Ks (spies evs); evs:p;
 shrK_set Ks; good Ks; regular p; n ~:range shrK |] ==> Key n ~:analz (spies evs)"
 apply (clarify, simp only: knows_decomp)
-apply (drule GuardK_invKey_keyset, clarify, simp+, simp add: initState.simps)
+apply (drule GuardK_invKey_keyset, clarify, simp+, simp add: initState.simps image_eq_UN)
 apply clarify
 apply (drule in_good, simp)
 apply (drule in_shrK_set, simp+, clarify)
--- a/src/HOL/Auth/Guard/Proto.thy	Fri Apr 25 14:18:13 2014 +0200
+++ b/src/HOL/Auth/Guard/Proto.thy	Fri Apr 25 14:39:11 2014 +0200
@@ -56,7 +56,7 @@
 Nonce n ~:parts (apm s `(msg `(fst R))) |] ==>
 (EX k. Nonce k:parts {X} & nonce s k = n)"
 apply (erule Nonce_apm, unfold wdef_def)
-apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp)
+apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp simp: image_eq_UN)
 apply (drule_tac x=x in bspec, simp)
 apply (drule_tac Y="msg x" and s=s in apm_parts, simp)
 by (blast dest: parts_parts)
@@ -134,7 +134,7 @@
 
 lemma ok_not_used: "[| Nonce n ~:used evs; ok evs R s;
 ALL x. x:fst R --> is_Says x |] ==> Nonce n ~:parts (apm s `(msg `(fst R)))"
-apply (unfold ok_def, clarsimp)
+apply (unfold ok_def, clarsimp simp: image_eq_UN)
 apply (drule_tac x=x in spec, drule_tac x=x in spec)
 by (auto simp: is_Says_def dest: Says_imp_spies not_used_not_spied parts_parts)
 
@@ -188,10 +188,10 @@
 apply (drule wdef_Nonce, simp+)
 apply (frule ok_not_used, simp+)
 apply (clarify, erule ok_is_Says, simp+)
-apply (clarify, rule_tac x=k in exI, simp add: newn_def)
+apply (clarify, rule_tac x=k in exI, simp add: newn_def image_eq_UN)
 apply (clarify, drule_tac Y="msg x" and s=s in apm_parts)
 apply (drule ok_not_used, simp+)
-by (clarify, erule ok_is_Says, simp+)
+by (clarify, erule ok_is_Says, simp_all add: image_eq_UN)
 
 lemma fresh_rule: "[| evs' @ ev # evs:tr p; wdef p; Nonce n ~:used evs;
 Nonce n:parts {msg ev} |] ==> EX R s. R:p & ap' s R = ev"
--- a/src/HOL/Auth/NS_Public.thy	Fri Apr 25 14:18:13 2014 +0200
+++ b/src/HOL/Auth/NS_Public.thy	Fri Apr 25 14:39:11 2014 +0200
@@ -42,8 +42,7 @@
 declare knows_Spy_partsEs [elim]
 declare knows_Spy_partsEs [elim]
 declare analz_into_parts [dest]
-declare Fake_parts_insert_in_Un  [dest]
-declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
+declare Fake_parts_insert_in_Un [dest]
 
 (*A "possibility property": there are traces that reach the end*)
 lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
--- a/src/HOL/Auth/NS_Public_Bad.thy	Fri Apr 25 14:18:13 2014 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy	Fri Apr 25 14:39:11 2014 +0200
@@ -44,8 +44,7 @@
 
 declare knows_Spy_partsEs [elim]
 declare analz_into_parts [dest]
-declare Fake_parts_insert_in_Un  [dest]
-declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
+declare Fake_parts_insert_in_Un [dest]
 
 (*A "possibility property": there are traces that reach the end*)
 lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
--- a/src/HOL/Auth/NS_Shared.thy	Fri Apr 25 14:18:13 2014 +0200
+++ b/src/HOL/Auth/NS_Shared.thy	Fri Apr 25 14:39:11 2014 +0200
@@ -86,7 +86,6 @@
 declare parts.Body  [dest]
 declare Fake_parts_insert_in_Un  [dest]
 declare analz_into_parts [dest]
-declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
 
 
 text{*A "possibility property": there are traces that reach the end*}
--- a/src/HOL/BNF_FP_Base.thy	Fri Apr 25 14:18:13 2014 +0200
+++ b/src/HOL/BNF_FP_Base.thy	Fri Apr 25 14:39:11 2014 +0200
@@ -166,10 +166,7 @@
 lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g"
   by (erule arg_cong)
 
-lemma snd_o_convol: "(snd \<circ> (\<lambda>x. (f x, g x))) = g"
-  by (rule ext) simp
-
-lemma inj_on_convol_id: "inj_on (\<lambda>x. (x, f x)) X"
+lemma inj_on_convol_ident: "inj_on (\<lambda>x. (x, f x)) X"
   unfolding inj_on_def by simp
 
 lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x"
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Fri Apr 25 14:18:13 2014 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Fri Apr 25 14:39:11 2014 +0200
@@ -174,16 +174,16 @@
 
 subsection {* Alternative rules for @{text length} *}
 
-definition size_list :: "'a list => nat"
-where "size_list = size"
+definition size_list' :: "'a list => nat"
+where "size_list' = size"
 
-lemma size_list_simps:
-  "size_list [] = 0"
-  "size_list (x # xs) = Suc (size_list xs)"
-by (auto simp add: size_list_def)
+lemma size_list'_simps:
+  "size_list' [] = 0"
+  "size_list' (x # xs) = Suc (size_list' xs)"
+by (auto simp add: size_list'_def)
 
-declare size_list_simps[code_pred_def]
-declare size_list_def[symmetric, code_pred_inline]
+declare size_list'_simps[code_pred_def]
+declare size_list'_def[symmetric, code_pred_inline]
 
 
 subsection {* Alternative rules for @{text list_all2} *}
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Apr 25 14:18:13 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Apr 25 14:39:11 2014 +0200
@@ -1077,12 +1077,12 @@
 *)
 subsection {* Inverting list functions *}
 
-code_pred [inductify, skip_proof] size_list .
-code_pred [new_random_dseq inductify] size_list .
-thm size_listP.equation
-thm size_listP.new_random_dseq_equation
+code_pred [inductify, skip_proof] size_list' .
+code_pred [new_random_dseq inductify] size_list' .
+thm size_list'P.equation
+thm size_list'P.new_random_dseq_equation
 
-values [new_random_dseq 2,3,10] 3 "{xs. size_listP (xs::nat list) (5::nat)}"
+values [new_random_dseq 2,3,10] 3 "{xs. size_list'P (xs::nat list) (5::nat)}"
 
 code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat .
 thm concatP.equation
--- a/src/HOL/ROOT	Fri Apr 25 14:18:13 2014 +0200
+++ b/src/HOL/ROOT	Fri Apr 25 14:39:11 2014 +0200
@@ -560,7 +560,6 @@
     HarmonicSeries
     Refute_Examples
     Execute_Choice
-    Summation
     Gauge_Integration
     Dedekind_Real
     Quicksort
--- a/src/HOL/Tools/ATP/atp_problem.ML	Fri Apr 25 14:18:13 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri Apr 25 14:39:11 2014 +0200
@@ -50,7 +50,8 @@
     Class_Decl of string * 'a * 'a list |
     Type_Decl of string * 'a * int |
     Sym_Decl of string * 'a * 'a atp_type |
-    Datatype_Decl of string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list |
+    Datatype_Decl of
+      string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list * bool |
     Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a |
     Formula of (string * string) * atp_formula_role
                * ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula
@@ -194,7 +195,8 @@
   Class_Decl of string * 'a * 'a list |
   Type_Decl of string * 'a * int |
   Sym_Decl of string * 'a * 'a atp_type |
-  Datatype_Decl of string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list |
+  Datatype_Decl of
+    string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list * bool |
   Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a |
   Formula of (string * string) * atp_formula_role
              * ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula
@@ -613,7 +615,9 @@
       (if null xs then "" else "[" ^ commas (map bound_tvar xs) ^ "], ") ^
       typ ty
     fun sort_decl xs ty cl = "sort(" ^ binder_typ xs ty ^ ", " ^ cl ^ ")."
-    fun datatype_decl xs ty tms = "datatype(" ^ commas (binder_typ xs ty :: map term tms) ^ ")."
+    fun datatype_decl xs ty tms exhaust =
+      "datatype(" ^ commas (binder_typ xs ty :: map term tms @ (if exhaust then [] else ["..."])) ^
+      ")."
     fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")."
     fun formula pred (Formula ((ident, alt), kind, phi, _, info)) =
         if pred kind then
@@ -661,7 +665,8 @@
                else NONE
              | _ => NONE) |> flat
     val datatype_decls =
-      filt (try (fn Datatype_Decl (_, xs, ty, tms) => datatype_decl xs ty tms)) |> flat
+      filt (try (fn Datatype_Decl (_, xs, ty, tms, exhaust) => datatype_decl xs ty tms exhaust))
+      |> flat
     val sort_decls =
       filt (try (fn Class_Memb (_, xs, ty, cl) => sort_decl xs ty cl)) |> flat
     val subclass_decls =
@@ -938,9 +943,9 @@
         nice_name ty #>> (fn ty => Type_Decl (ident, ty, ary))
       | nice_line (Sym_Decl (ident, sym, ty)) =
         nice_name sym ##>> nice_type ty #>> (fn (sym, ty) => Sym_Decl (ident, sym, ty))
-      | nice_line (Datatype_Decl (ident, xs, ty, tms)) =
+      | nice_line (Datatype_Decl (ident, xs, ty, tms, exhaust)) =
         nice_bound_tvars xs ##>> nice_type ty ##>> fold_map nice_term tms
-        #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms))
+        #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms, exhaust))
       | nice_line (Class_Memb (ident, xs, ty, cl)) =
         nice_bound_tvars xs ##>> nice_type ty ##>> nice_name cl
         #>> (fn ((xs, ty), cl) => Class_Memb (ident, xs, ty, cl))
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Apr 25 14:18:13 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Apr 25 14:39:11 2014 +0200
@@ -2462,21 +2462,19 @@
 
         fun datatype_of_ctrs (ctrs as (_, T1) :: _) =
           let val ctrs' = map do_ctr ctrs in
-            if forall is_some ctrs' then
-              SOME (native_atp_type_of_typ type_enc false 0 (body_type T1), map_filter I ctrs')
-            else
-              NONE
+            (native_atp_type_of_typ type_enc false 0 (body_type T1), map_filter I ctrs',
+             forall is_some ctrs')
           end
       in
-        map_filter datatype_of_ctrs ctrss
+        ctrss |> map datatype_of_ctrs |> filter_out (null o #2)
       end
     else
       []
   | datatypes_of_sym_table _ _ _ _ _ _ = []
 
-fun decl_line_of_datatype (ty as AType (((_, s'), _), ty_args), ctrs) =
+fun decl_line_of_datatype (ty as AType (((_, s'), _), ty_args), ctrs, exhaust) =
   let val xs = map (fn AType ((name, _), []) => name) ty_args in
-    Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty, ctrs)
+    Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty, ctrs, exhaust)
   end
 
 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
@@ -2589,7 +2587,7 @@
     fun do_line (Class_Decl (_, _, cls)) = fold do_class cls
       | do_line (Type_Decl _) = I
       | do_line (Sym_Decl (_, _, ty)) = do_type ty
-      | do_line (Datatype_Decl (_, xs, ty, tms)) =
+      | do_line (Datatype_Decl (_, xs, ty, tms, _)) =
         fold do_bound_tvars xs #> do_type ty #> fold (do_term false) tms
       | do_line (Class_Memb (_, xs, ty, cl)) = fold do_bound_tvars xs #> do_type ty #> do_class cl
       | do_line (Formula (_, _, phi, _, _)) = do_formula phi
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Apr 25 14:18:13 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Apr 25 14:39:11 2014 +0200
@@ -217,18 +217,23 @@
     val overloaded_size_defs' =
       map (mk_unabs_def 1 o (fn thm => thm RS meta_eq_to_obj_eq)) overloaded_size_defs;
 
+    val all_overloaded_size_defs = overloaded_size_defs @
+      (Spec_Rules.retrieve lthy0 @{const size ('a)}
+       |> map_filter (try (fn (Equational, (_, [thm])) => thm)));
+
     val nested_size_maps = map (pointfill lthy2) nested_size_o_maps @ nested_size_o_maps;
     val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ nested_bnfs @ nesting_bnfs);
 
     fun derive_size_simp size_def' simp0 =
       (trans OF [size_def', simp0])
-      |> Simplifier.asm_full_simplify (ss_only (@{thms inj_on_convol_id snd_o_convol} @
+      |> Simplifier.asm_full_simplify (ss_only (@{thms inj_on_convol_ident id_def o_def snd_conv} @
         all_inj_maps @ nested_size_maps) lthy2)
       |> fold_thms lthy2 size_defs_unused_0;
-    fun derive_overloaded_size_simp size_def' simp0 =
-      (trans OF [size_def', simp0])
+
+    fun derive_overloaded_size_simp overloaded_size_def' simp0 =
+      (trans OF [overloaded_size_def', simp0])
       |> unfold_thms lthy2 @{thms add_0_left add_0_right}
-      |> fold_thms lthy2 overloaded_size_defs';
+      |> fold_thms lthy2 all_overloaded_size_defs;
 
     val size_simpss = map2 (map o derive_size_simp) size_defs' rec_thmss;
     val size_simps = flat size_simpss;
--- a/src/HOL/ex/Summation.thy	Fri Apr 25 14:18:13 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,107 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Some basic facts about discrete summation *}
-
-theory Summation
-imports Main
-begin
-
-text {* Auxiliary. *}
-
-lemma add_setsum_orient:
-  "setsum f {k..<j} + setsum f {l..<k} = setsum f {l..<k} + setsum f {k..<j}"
-  by (fact add.commute)
-
-lemma add_setsum_int:
-  fixes j k l :: int
-  shows "j < k \<Longrightarrow> k < l \<Longrightarrow> setsum f {j..<k} + setsum f {k..<l} = setsum f {j..<l}"
-  by (simp_all add: setsum_Un_Int [symmetric] ivl_disj_un)
-
-text {* The shift operator. *}
-
-definition \<Delta> :: "(int \<Rightarrow> 'a\<Colon>ab_group_add) \<Rightarrow> int \<Rightarrow> 'a" where
-  "\<Delta> f k = f (k + 1) - f k"
-
-lemma \<Delta>_shift:
-  "\<Delta> (\<lambda>k. l + f k) = \<Delta> f"
-  by (simp add: \<Delta>_def fun_eq_iff)
-
-lemma \<Delta>_same_shift:
-  assumes "\<Delta> f = \<Delta> g"
-  shows "\<exists>l. plus l \<circ> f = g"
-proof -
-  fix k
-  from assms have "\<And>k. \<Delta> f k = \<Delta> g k" by simp
-  then have k_incr: "\<And>k. f (k + 1) - g (k + 1) = f k - g k"
-    by (simp add: \<Delta>_def algebra_simps)
-  then have "\<And>k. f ((k - 1) + 1) - g ((k - 1) + 1) = f (k - 1) - g (k - 1)"
-    by blast
-  then have k_decr: "\<And>k. f (k - 1) - g (k - 1) = f k - g k"
-    by simp
-  have "\<And>k. f k - g k = f 0 - g 0"
-  proof -
-    fix k
-    show "f k - g k = f 0 - g 0"
-      by (induct k rule: int_induct) (simp_all add: k_incr k_decr)
-  qed
-  then have "\<And>k. (plus (g 0 - f 0) \<circ> f) k = g k"
-    by (simp add: algebra_simps)
-  then have "plus (g 0 - f 0) \<circ> f = g" ..
-  then show ?thesis ..
-qed
-
-text {* The formal sum operator. *}
-
-definition \<Sigma> :: "(int \<Rightarrow> 'a\<Colon>ab_group_add) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a" where
-  "\<Sigma> f j l = (if j < l then setsum f {j..<l}
-    else if j > l then - setsum f {l..<j}
-    else 0)"
-
-lemma \<Sigma>_same [simp]:
-  "\<Sigma> f j j = 0"
-  by (simp add: \<Sigma>_def)
-
-lemma \<Sigma>_positive:
-  "j < l \<Longrightarrow> \<Sigma> f j l = setsum f {j..<l}"
-  by (simp add: \<Sigma>_def)
-
-lemma \<Sigma>_negative:
-  "j > l \<Longrightarrow> \<Sigma> f j l = - \<Sigma> f l j"
-  by (simp add: \<Sigma>_def)
-
-lemma add_\<Sigma>:
-  "\<Sigma> f j k + \<Sigma> f k l = \<Sigma> f j l"
-  by (simp add: \<Sigma>_def algebra_simps add_setsum_int)
-   (simp_all add: add_setsum_orient [of f k j l]
-      add_setsum_orient [of f j l k]
-      add_setsum_orient [of f j k l] add_setsum_int)
-
-lemma \<Sigma>_incr_upper:
-  "\<Sigma> f j (l + 1) = \<Sigma> f j l + f l"
-proof -
-  have "{l..<l+1} = {l}" by auto
-  then have "\<Sigma> f l (l + 1) = f l" by (simp add: \<Sigma>_def)
-  moreover have "\<Sigma> f j (l + 1) = \<Sigma> f j l + \<Sigma> f l (l + 1)" by (simp add: add_\<Sigma>)
-  ultimately show ?thesis by simp
-qed
-
-text {* Fundamental lemmas: The relation between @{term \<Delta>} and @{term \<Sigma>}. *}
-
-lemma \<Delta>_\<Sigma>:
-  "\<Delta> (\<Sigma> f j) = f"
-proof
-  fix k
-  show "\<Delta> (\<Sigma> f j) k = f k"
-    by (simp add: \<Delta>_def \<Sigma>_incr_upper)
-qed
-
-lemma \<Sigma>_\<Delta>:
-  "\<Sigma> (\<Delta> f) j l = f l - f j"
-proof -
-  from \<Delta>_\<Sigma> have "\<Delta> (\<Sigma> (\<Delta> f) j) = \<Delta> f" .
-  then obtain k where "plus k \<circ> \<Sigma> (\<Delta> f) j = f" by (blast dest: \<Delta>_same_shift)
-  then have "\<And>q. f q = k + \<Sigma> (\<Delta> f) j q" by (simp add: fun_eq_iff)
-  then show ?thesis by simp
-qed
-
-end