# HG changeset patch # User haftmann # Date 1349514532 -7200 # Node ID bbc2942ba09f59d6a19212fc83643e796e7bbe61 # Parent c91419b3a4256c43e9bd4d21791d799594e2b130 alternative simplification of ^^ to the righthand side; lifting of comp_fun_commute to ^^ diff -r c91419b3a425 -r bbc2942ba09f src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Fri Oct 05 18:01:48 2012 +0200 +++ b/src/HOL/Finite_Set.thy Sat Oct 06 11:08:52 2012 +0200 @@ -739,7 +739,7 @@ end -subsubsection {* Expressing set operations via @{const fold} *} +subsubsection {* Liftings to @{text comp_fun_commute} etc. *} lemma (in comp_fun_commute) comp_comp_fun_commute: "comp_fun_commute (f \ g)" @@ -751,6 +751,47 @@ by (rule comp_fun_idem.intro, rule comp_comp_fun_commute, unfold_locales) (simp_all add: comp_fun_idem) +lemma (in comp_fun_commute) comp_fun_commute_funpow: + "comp_fun_commute (\x. f x ^^ g x)" +proof + fix y x + show "f y ^^ g y \ f x ^^ g x = f x ^^ g x \ f y ^^ g y" + proof (cases "x = y") + case True then show ?thesis by simp + next + case False show ?thesis + proof (induct "g x" arbitrary: g) + case 0 then show ?case by simp + next + case (Suc n g) + have hyp1: "f y ^^ g y \ f x = f x \ f y ^^ g y" + proof (induct "g y" arbitrary: g) + case 0 then show ?case by simp + next + case (Suc n g) + def h \ "\z. g z - 1" + with Suc have "n = h y" by simp + with Suc have hyp: "f y ^^ h y \ f x = f x \ f y ^^ h y" + by auto + from Suc h_def have "g y = Suc (h y)" by simp + then show ?case by (simp add: o_assoc [symmetric] hyp) + (simp add: o_assoc comp_fun_commute) + qed + def h \ "\z. if z = x then g x - 1 else g z" + with Suc have "n = h x" by simp + with Suc have "f y ^^ h y \ f x ^^ h x = f x ^^ h x \ f y ^^ h y" + by auto + with False h_def have hyp2: "f y ^^ g y \ f x ^^ h x = f x ^^ h x \ f y ^^ g y" by simp + from Suc h_def have "g x = Suc (h x)" by simp + then show ?case by (simp del: funpow.simps add: funpow_Suc_right o_assoc hyp2) + (simp add: o_assoc [symmetric] hyp1) + qed + qed +qed + + +subsubsection {* Expressing set operations via @{const fold} *} + lemma comp_fun_idem_insert: "comp_fun_idem insert" proof @@ -2400,3 +2441,4 @@ hide_const (open) Finite_Set.fold Finite_Set.filter end + diff -r c91419b3a425 -r bbc2942ba09f src/HOL/Nat.thy --- a/src/HOL/Nat.thy Fri Oct 05 18:01:48 2012 +0200 +++ b/src/HOL/Nat.thy Sat Oct 06 11:08:52 2012 +0200 @@ -1249,6 +1249,19 @@ end +lemma funpow_Suc_right: + "f ^^ Suc n = f ^^ n \ f" +proof (induct n) + case 0 then show ?case by simp +next + fix n + assume "f ^^ Suc n = f ^^ n \ f" + then show "f ^^ Suc (Suc n) = f ^^ Suc n \ f" + by (simp add: o_assoc) +qed + +lemmas funpow_simps_right = funpow.simps(1) funpow_Suc_right + text {* for code generation *} definition funpow :: "nat \ ('a \ 'a) \ 'a \ 'a" where