src/HOL/Extraction/Pigeonhole.thy
changeset 21062 876dd2695423
parent 20933 3f999b73f6d5
child 21127 c8e862897d13
equal deleted inserted replaced
21061:580dfc999ef6 21062:876dd2695423
   301 
   301 
   302 ML "PH.pigeonhole 8 (PH.sel [0,1,2,3,4,5,6,3,7,8])"
   302 ML "PH.pigeonhole 8 (PH.sel [0,1,2,3,4,5,6,3,7,8])"
   303 
   303 
   304 definition
   304 definition
   305   arbitrary_nat :: "nat \<times> nat"
   305   arbitrary_nat :: "nat \<times> nat"
   306   "arbitrary_nat = arbitrary"
   306   [symmetric, code inline]: "arbitrary_nat = arbitrary"
   307   arbitrary_nat_subst :: "nat \<times> nat"
   307   arbitrary_nat_subst :: "nat \<times> nat"
   308   "arbitrary_nat_subst = (0, 0)"
   308   "arbitrary_nat_subst = (0, 0)"
   309 
   309 
   310 lemma [code func]:
   310 lemma [code func]:
   311   "arbitrary_nat = arbitrary_nat" ..
   311   "arbitrary_nat = arbitrary_nat" ..
   312 
   312 
   313 declare arbitrary_nat_def [symmetric, code inline]
   313 code_axioms
   314 
       
   315 code_constsubst
       
   316   arbitrary_nat \<equiv> arbitrary_nat_subst
   314   arbitrary_nat \<equiv> arbitrary_nat_subst
   317 
   315 
   318 definition
   316 definition
   319   "test n = pigeonhole n (\<lambda>m. m - 1)"
   317   "test n = pigeonhole n (\<lambda>m. m - 1)"
   320   "test' n = pigeonhole_slow n (\<lambda>m. m - 1)"
   318   "test' n = pigeonhole_slow n (\<lambda>m. m - 1)"