It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...
authornipkow
Mon Sep 01 22:10:42 2008 +0200 (2008-09-01)
changeset 28072a45e8c872dc1
parent 28071 6ab5b4595f64
child 28073 5e9f00f4f209
It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Mon Sep 01 19:17:47 2008 +0200
     1.2 +++ b/src/HOL/List.thy	Mon Sep 01 22:10:42 2008 +0200
     1.3 @@ -3626,6 +3626,14 @@
     1.4  
     1.5  text {* Code for bounded quantification and summation over nats. *}
     1.6  
     1.7 +lemma atMost_upto [code unfold]:
     1.8 +  "{..n} = set [0..<Suc n]"
     1.9 +by auto
    1.10 +
    1.11 +lemma atLeast_upt [code unfold]:
    1.12 +  "{..<n} = set [0..<n]"
    1.13 +by auto
    1.14 +
    1.15  lemma greaterThanLessThan_upt [code unfold]:
    1.16    "{n<..<m} = set [Suc n..<m]"
    1.17  by auto