src/HOL/ex/CodeRevappl.thy
changeset 22528 8501c4a62a3c
parent 22527 84690fcd3db9
child 22529 902ed60d53a7
     1.1 --- a/src/HOL/ex/CodeRevappl.thy	Tue Mar 27 09:19:37 2007 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,42 +0,0 @@
     1.4 -(*  ID:         $Id$
     1.5 -    Author:     Florian Haftmann, TU Muenchen
     1.6 -*)
     1.7 -
     1.8 -header {* Combinators for structured results *}
     1.9 -
    1.10 -theory CodeRevappl
    1.11 -imports Main
    1.12 -begin
    1.13 -
    1.14 -section {* Combinators for structured results *}
    1.15 -
    1.16 -
    1.17 -subsection {* primitive definitions *}
    1.18 -
    1.19 -definition
    1.20 -  revappl :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b" (infixl "\<triangleright>" 55)
    1.21 -  revappl_def: "x \<triangleright> f = f x"
    1.22 -  revappl_snd :: "'c \<times> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<times> 'b" (infixl "|\<triangleright>" 55)
    1.23 -  revappl_snd_split: "z |\<triangleright> f = (fst z , f (snd z))"
    1.24 -  revappl_swamp :: "'c \<times> 'a \<Rightarrow> ('a \<Rightarrow> 'd \<times> 'b) \<Rightarrow> ('c \<times> 'd) \<times> 'b" (infixl "|\<triangleright>\<triangleright>" 55)
    1.25 -  revappl_swamp_split: "z |\<triangleright>\<triangleright> f = ((fst z, fst (f (snd z))), snd (f (snd z)))"
    1.26 -  revappl_uncurry :: "'c \<times> 'a \<Rightarrow> ('c \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b" (infixl "\<turnstile>\<triangleright>" 55)
    1.27 -  revappl_uncurry_split: "z \<turnstile>\<triangleright> f = f (fst z) (snd z)"
    1.28 -
    1.29 -
    1.30 -subsection {* lemmas *}
    1.31 -
    1.32 -lemma revappl_snd_def [code]:
    1.33 -  "(y, x) |\<triangleright> f = (y, f x)" unfolding revappl_snd_split by simp
    1.34 -
    1.35 -lemma revappl_swamp_def [code]:
    1.36 -  "(y, x) |\<triangleright>\<triangleright> f = (let (z, w) = f x in ((y, z), w))" unfolding Let_def revappl_swamp_split split_def by simp
    1.37 -
    1.38 -lemma revappl_uncurry_def [code]:
    1.39 -  "(y, x) \<turnstile>\<triangleright> f = f y x" unfolding revappl_uncurry_split by simp
    1.40 -
    1.41 -lemmas revappl = revappl_def revappl_snd_def revappl_swamp_def revappl_uncurry_def
    1.42 -
    1.43 -lemmas revappl_split = revappl_def revappl_snd_split revappl_swamp_split revappl_uncurry_split
    1.44 -
    1.45 -end
    1.46 \ No newline at end of file