alternative simplification of ^^ to the righthand side;
authorhaftmann
Sat Oct 06 11:08:52 2012 +0200 (2012-10-06)
changeset 49723bbc2942ba09f
parent 49722 c91419b3a425
child 49724 a5842f026d4c
alternative simplification of ^^ to the righthand side;
lifting of comp_fun_commute to ^^
src/HOL/Finite_Set.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Oct 05 18:01:48 2012 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Sat Oct 06 11:08:52 2012 +0200
     1.3 @@ -739,7 +739,7 @@
     1.4  end
     1.5  
     1.6  
     1.7 -subsubsection {* Expressing set operations via @{const fold} *}
     1.8 +subsubsection {* Liftings to @{text comp_fun_commute} etc. *}
     1.9  
    1.10  lemma (in comp_fun_commute) comp_comp_fun_commute:
    1.11    "comp_fun_commute (f \<circ> g)"
    1.12 @@ -751,6 +751,47 @@
    1.13    by (rule comp_fun_idem.intro, rule comp_comp_fun_commute, unfold_locales)
    1.14      (simp_all add: comp_fun_idem)
    1.15  
    1.16 +lemma (in comp_fun_commute) comp_fun_commute_funpow:
    1.17 +  "comp_fun_commute (\<lambda>x. f x ^^ g x)"
    1.18 +proof
    1.19 +  fix y x
    1.20 +  show "f y ^^ g y \<circ> f x ^^ g x = f x ^^ g x \<circ> f y ^^ g y"
    1.21 +  proof (cases "x = y")
    1.22 +    case True then show ?thesis by simp
    1.23 +  next
    1.24 +    case False show ?thesis
    1.25 +    proof (induct "g x" arbitrary: g)
    1.26 +      case 0 then show ?case by simp
    1.27 +    next
    1.28 +      case (Suc n g)
    1.29 +      have hyp1: "f y ^^ g y \<circ> f x = f x \<circ> f y ^^ g y"
    1.30 +      proof (induct "g y" arbitrary: g)
    1.31 +        case 0 then show ?case by simp
    1.32 +      next
    1.33 +        case (Suc n g)
    1.34 +        def h \<equiv> "\<lambda>z. g z - 1"
    1.35 +        with Suc have "n = h y" by simp
    1.36 +        with Suc have hyp: "f y ^^ h y \<circ> f x = f x \<circ> f y ^^ h y"
    1.37 +          by auto
    1.38 +        from Suc h_def have "g y = Suc (h y)" by simp
    1.39 +        then show ?case by (simp add: o_assoc [symmetric] hyp)
    1.40 +          (simp add: o_assoc comp_fun_commute)
    1.41 +      qed
    1.42 +      def h \<equiv> "\<lambda>z. if z = x then g x - 1 else g z"
    1.43 +      with Suc have "n = h x" by simp
    1.44 +      with Suc have "f y ^^ h y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ h y"
    1.45 +        by auto
    1.46 +      with False h_def have hyp2: "f y ^^ g y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ g y" by simp
    1.47 +      from Suc h_def have "g x = Suc (h x)" by simp
    1.48 +      then show ?case by (simp del: funpow.simps add: funpow_Suc_right o_assoc hyp2)
    1.49 +        (simp add: o_assoc [symmetric] hyp1)
    1.50 +    qed
    1.51 +  qed
    1.52 +qed
    1.53 +
    1.54 +
    1.55 +subsubsection {* Expressing set operations via @{const fold} *}
    1.56 +
    1.57  lemma comp_fun_idem_insert:
    1.58    "comp_fun_idem insert"
    1.59  proof
    1.60 @@ -2400,3 +2441,4 @@
    1.61  hide_const (open) Finite_Set.fold Finite_Set.filter
    1.62  
    1.63  end
    1.64 +
     2.1 --- a/src/HOL/Nat.thy	Fri Oct 05 18:01:48 2012 +0200
     2.2 +++ b/src/HOL/Nat.thy	Sat Oct 06 11:08:52 2012 +0200
     2.3 @@ -1249,6 +1249,19 @@
     2.4  
     2.5  end
     2.6  
     2.7 +lemma funpow_Suc_right:
     2.8 +  "f ^^ Suc n = f ^^ n \<circ> f"
     2.9 +proof (induct n)
    2.10 +  case 0 then show ?case by simp
    2.11 +next
    2.12 +  fix n
    2.13 +  assume "f ^^ Suc n = f ^^ n \<circ> f"
    2.14 +  then show "f ^^ Suc (Suc n) = f ^^ Suc n \<circ> f"
    2.15 +    by (simp add: o_assoc)
    2.16 +qed
    2.17 +
    2.18 +lemmas funpow_simps_right = funpow.simps(1) funpow_Suc_right
    2.19 +
    2.20  text {* for code generation *}
    2.21  
    2.22  definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where