14 use "ProgLang/calculate.sml" (*???*) |
14 use "ProgLang/calculate.sml" (*???*) |
15 use "ProgLang/rewrite.sml" (*?*** At command "end" (line 205../ListC.thy*) |
15 use "ProgLang/rewrite.sml" (*?*** At command "end" (line 205../ListC.thy*) |
16 |
16 |
17 text {* 'nat' in List.thy replaced by 'real' *} |
17 text {* 'nat' in List.thy replaced by 'real' *} |
18 |
18 |
19 primrec length_' :: "'a list => real" |
19 primrec LENGTH :: "'a list => real" |
20 where |
20 where |
21 LENGTH_NIL: "length_' [] = 0" (*length: 'a list => nat*) |
21 LENGTH_NIL: "LENGTH [] = 0" (*length: 'a list => nat*) |
22 | LENGTH_CONS: "length_' (x#xs) = 1 + length_' xs" |
22 | LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs" |
23 |
23 |
24 primrec del :: "['a list, 'a] => 'a list" |
24 primrec del :: "['a list, 'a] => 'a list" |
25 where |
25 where |
26 del_base: "del [] x = []" |
26 del_base: "del [] x = []" |
27 | del_rec: "del (y#ys) x = (if x = y then ys else y#(del ys x))" |
27 | del_rec: "del (y#ys) x = (if x = y then ys else y#(del ys x))" |
29 definition |
29 definition |
30 list_diff :: "['a list, 'a list] => 'a list" (* as -- bs *) |
30 list_diff :: "['a list, 'a list] => 'a list" (* as -- bs *) |
31 ("(_ --/ _)" [66, 66] 65) |
31 ("(_ --/ _)" [66, 66] 65) |
32 where "a -- b == foldl del a b" |
32 where "a -- b == foldl del a b" |
33 |
33 |
34 consts nth_' :: "[real, 'a list] => 'a" |
34 consts NTH :: "[real, 'a list] => 'a" |
35 axioms |
35 axioms |
36 (*** more than one non-variable in pattern in "nth_ 1 [x] = x"--*) |
36 (*** more than one non-variable in pattern in "nth_ 1 [x] = x"--*) |
37 NTH_NIL: "nth_' 1 (x#xs) = x" |
37 NTH_NIL: "NTH 1 (x#xs) = x" |
38 (* NTH_CONS: "nth_' n (x#xs) = nth_' (n+ -1) xs" *) |
38 (* NTH_CONS: "NTH n (x#xs) = NTH (n+ -1) xs" *) |
39 |
39 |
40 (*rewriter does not reach base case ...... ; |
40 (*rewriter does not reach base case ...... ; |
41 the condition involves another rule set (erls, eval_binop in Atools):*) |
41 the condition involves another rule set (erls, eval_binop in Atools):*) |
42 NTH_CONS: "1 < n ==> nth_' n (x#xs) = nth_' (n+ - 1) xs" |
42 NTH_CONS: "1 < n ==> NTH n (x#xs) = NTH (n+ - 1) xs" |
43 |
43 |
44 (*primrec from Isabelle/src/HOL/List.thy -- def.twice not allowed*) |
44 (*primrec from Isabelle/src/HOL/List.thy -- def.twice not allowed*) |
45 (*primrec*) |
45 (*primrec*) |
46 hd_thm: "hd(x#xs) = x" |
46 hd_thm: "hd(x#xs) = x" |
47 (*primrec*) |
47 (*primrec*) |