src/HOL/MicroJava/DFA/Listn.thy
changeset 35416 d8d7d1b785af
parent 35102 cc7a0b9f938c
child 42150 b0c0638c4aad
     1.1 --- a/src/HOL/MicroJava/DFA/Listn.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/MicroJava/DFA/Listn.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -9,12 +9,10 @@
     1.4  imports Err
     1.5  begin
     1.6  
     1.7 -constdefs
     1.8 -
     1.9 - list :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a list set"
    1.10 +definition list :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a list set" where
    1.11  "list n A == {xs. length xs = n & set xs <= A}"
    1.12  
    1.13 - le :: "'a ord \<Rightarrow> ('a list)ord"
    1.14 +definition le :: "'a ord \<Rightarrow> ('a list)ord" where
    1.15  "le r == list_all2 (%x y. x <=_r y)"
    1.16  
    1.17  abbreviation
    1.18 @@ -27,8 +25,7 @@
    1.19         ("(_ /<[_] _)" [50, 0, 51] 50)
    1.20    where "x <[r] y == x <_(le r) y"
    1.21  
    1.22 -constdefs
    1.23 - map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
    1.24 +definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
    1.25  "map2 f == (%xs ys. map (split f) (zip xs ys))"
    1.26  
    1.27  abbreviation
    1.28 @@ -36,19 +33,17 @@
    1.29         ("(_ /+[_] _)" [65, 0, 66] 65)
    1.30    where "x +[f] y == x +_(map2 f) y"
    1.31  
    1.32 -consts coalesce :: "'a err list \<Rightarrow> 'a list err"
    1.33 -primrec
    1.34 -"coalesce [] = OK[]"
    1.35 -"coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)"
    1.36 +primrec coalesce :: "'a err list \<Rightarrow> 'a list err" where
    1.37 +  "coalesce [] = OK[]"
    1.38 +| "coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)"
    1.39  
    1.40 -constdefs
    1.41 - sl :: "nat \<Rightarrow> 'a sl \<Rightarrow> 'a list sl"
    1.42 +definition sl :: "nat \<Rightarrow> 'a sl \<Rightarrow> 'a list sl" where
    1.43  "sl n == %(A,r,f). (list n A, le r, map2 f)"
    1.44  
    1.45 - sup :: "('a \<Rightarrow> 'b \<Rightarrow> 'c err) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list err"
    1.46 +definition sup :: "('a \<Rightarrow> 'b \<Rightarrow> 'c err) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list err" where
    1.47  "sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err"
    1.48  
    1.49 - upto_esl :: "nat \<Rightarrow> 'a esl \<Rightarrow> 'a list esl"
    1.50 +definition upto_esl :: "nat \<Rightarrow> 'a esl \<Rightarrow> 'a list esl" where
    1.51  "upto_esl m == %(A,r,f). (Union{list n A |n. n <= m}, le r, sup f)"
    1.52  
    1.53  lemmas [simp] = set_update_subsetI