1202375Srdivacky(* 2202375Srdivacky * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3202375Srdivacky * 4202375Srdivacky * SPDX-License-Identifier: BSD-2-Clause 5202375Srdivacky *) 6202375Srdivacky 7202375Srdivacky(* Author: Thomas Sewell 8202375Srdivacky 9202375Srdivacky Library routines etc expected by Haskell code. 10202375Srdivacky*) 11202375Srdivacky 12202375Srdivackytheory HaskellLib_H 13202375Srdivackyimports 14202375Srdivacky Lib 15263508Sdim NatBitwise 16202375Srdivacky More_Numeral_Type 17249423Sdim NonDetMonadVCG 18202375Srdivackybegin 19202375Srdivacky 20202375Srdivackyabbreviation (input) "flip \<equiv> swp" 21202375Srdivacky 22202375Srdivackyabbreviation(input) bind_drop :: "('a, 'c) nondet_monad \<Rightarrow> ('a, 'b) nondet_monad 23249423Sdim \<Rightarrow> ('a, 'b) nondet_monad" (infixl ">>'_" 60) 24249423Sdim where "bind_drop \<equiv> (\<lambda>x y. bind x (K_bind y))" 25249423Sdim 26249423Sdimlemma bind_drop_test: 27249423Sdim "foldr bind_drop x (return ()) = sequence_x x" 28251662Sdim by (rule ext, simp add: sequence_x_def) 29249423Sdim 30251662Sdim(* If the given monad is deterministic, this function converts 31249423Sdim the nondet_monad type into a normal deterministic state monad *) 32249423Sdimdefinition 33249423Sdim runState :: "('s, 'a) nondet_monad \<Rightarrow> 's \<Rightarrow> ('a \<times> 's)" where 34249423Sdim "runState f s \<equiv> THE x. x \<in> fst (f s)" 35249423Sdim 36249423Sdimdefinition 37249423Sdim sassert :: "bool \<Rightarrow> 'a \<Rightarrow> 'a" where 38249423Sdim "sassert P \<equiv> if P then id else (\<lambda>x. undefined)" 39249423Sdim 40249423Sdimlemma sassert_cong[fundef_cong]: 41251662Sdim "\<lbrakk> P = P'; P' \<Longrightarrow> s = s' \<rbrakk> \<Longrightarrow> sassert P s = sassert P' s'" 42249423Sdim apply (simp add: sassert_def) 43249423Sdim done 44249423Sdim 45249423Sdimdefinition 46251662Sdim haskell_assert :: "bool \<Rightarrow> unit list \<Rightarrow> ('a, unit) nondet_monad" where 47249423Sdim "haskell_assert P L \<equiv> assert P" 48249423Sdim 49249423Sdimdefinition 50251662Sdim haskell_assertE :: "bool \<Rightarrow> unit list \<Rightarrow> ('a, 'e + unit) nondet_monad" where 51249423Sdim "haskell_assertE P L \<equiv> assertE P" 52249423Sdim 53251662Sdimdeclare haskell_assert_def [simp] haskell_assertE_def [simp] 54249423Sdim 55249423Sdimdefinition 56249423Sdim stateAssert :: "('a \<Rightarrow> bool) \<Rightarrow> unit list \<Rightarrow> ('a, unit) nondet_monad" where 57249423Sdim "stateAssert P L \<equiv> get >>= (\<lambda>s. assert (P s))" 58249423Sdim 59249423Sdimdefinition 60251662Sdim haskell_fail :: "unit list \<Rightarrow> ('a, 'b) nondet_monad" where 61249423Sdim haskell_fail_def[simp]: 62249423Sdim "haskell_fail L \<equiv> fail" 63249423Sdim 64249423Sdimdefinition 65251662Sdim catchError_def[simp]: 66249423Sdim "catchError \<equiv> handleE" 67249423Sdim 68249423Sdimdefinition 69249423Sdim "curry1 \<equiv> id" 70249423Sdimdefinition 71249423Sdim "curry2 \<equiv> curry" 72249423Sdimdefinition 73249423Sdim "curry3 f a b c \<equiv> f (a, b, c)" 74249423Sdimdefinition 75249423Sdim "curry4 f a b c d \<equiv> f (a, b, c, d)" 76249423Sdimdefinition 77249423Sdim "curry5 f a b c d e \<equiv> f (a, b, c, d, e)" 78251662Sdim 79251662Sdimdeclare curry1_def[simp] curry2_def[simp] 80251662Sdim curry3_def[simp] curry4_def[simp] curry5_def[simp] 81251662Sdim 82251662Sdimdefinition 83249423Sdim "split1 \<equiv> id" 84249423Sdimdefinition 85249423Sdim "split2 \<equiv> case_prod" 86251662Sdimdefinition 87249423Sdim "split3 f \<equiv> \<lambda>(a, b, c). f a b c" 88249423Sdimdefinition 89249423Sdim "split4 f \<equiv> \<lambda>(a, b, c, d). f a b c d" 90249423Sdimdefinition 91251662Sdim "split5 f \<equiv> \<lambda>(a, b, c, d, e). f a b c d e" 92249423Sdim 93249423Sdimdeclare split1_def[simp] split2_def[simp] 94249423Sdim 95249423Sdimlemma split3_simp[simp]: "split3 f (a, b, c) = f a b c" 96251662Sdim by (simp add: split3_def) 97249423Sdim 98249423Sdimlemma split4_simp[simp]: "split4 f (a, b, c, d) = f a b c d" 99251662Sdim by (simp add: split4_def) 100249423Sdim 101249423Sdimlemma split5_simp[simp]: "split5 f (a, b, c, d, e) = f a b c d e" 102249423Sdim by (simp add: split5_def) 103249423Sdim 104249423Sdimdefinition 105249423Sdim "Just \<equiv> Some" 106249423Sdimdefinition 107249423Sdim "Nothing \<equiv> None" 108251662Sdim 109249423Sdimdefinition 110249423Sdim "fromJust \<equiv> the" 111249423Sdimdefinition 112249423Sdim "isJust x \<equiv> x \<noteq> None" 113249423Sdim 114249423Sdimdefinition 115249423Sdim "tail \<equiv> tl" 116251662Sdimdefinition 117249423Sdim "head \<equiv> hd" 118249423Sdim 119251662Sdimdefinition 120249423Sdim error :: "unit list \<Rightarrow> 'a" where 121249423Sdim "error \<equiv> \<lambda>x. undefined" 122249423Sdim 123249423Sdimdefinition 124249423Sdim "reverse \<equiv> rev" 125249423Sdim 126249423Sdimdefinition 127249423Sdim "isNothing x \<equiv> x = None" 128251662Sdim 129249423Sdimdefinition 130251662Sdim "maybeApply \<equiv> option_map" 131249423Sdim 132249423Sdimdefinition 133249423Sdim "maybe \<equiv> case_option" 134251662Sdim 135249423Sdimdefinition 136249423Sdim "foldR f init L \<equiv> foldr f L init" 137249423Sdim 138251662Sdimdefinition 139249423Sdim "elem x L \<equiv> x \<in> set L" 140249423Sdim 141249423Sdimdefinition 142249423Sdim "notElem x L \<equiv> x \<notin> set L" 143249423Sdim 144249423Sdimtype_synonym ordering = bool 145249423Sdim 146251662Sdimdefinition 147249423Sdim compare :: "('a :: ord) \<Rightarrow> 'a \<Rightarrow> ordering" where 148249423Sdim "compare \<equiv> (<)" 149249423Sdim 150249423Sdimprimrec 151251662Sdim insertBy :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" 152249423Sdimwhere 153249423Sdim "insertBy f a [] = [a]" 154249423Sdim| "insertBy f a (b # bs) = (if (f a b) then (a # b # bs) else (b # (insertBy f a bs)))" 155249423Sdim 156249423Sdimlemma insertBy_length [simp]: 157249423Sdim "length (insertBy f a as) = (1 + length as)" 158249423Sdim by (induct as) simp_all 159251662Sdim 160249423Sdimprimrec 161249423Sdim sortBy :: "('a \<Rightarrow> 'a \<Rightarrow> ordering) \<Rightarrow> 'a list \<Rightarrow> 'a list" 162251662Sdimwhere 163249423Sdim "sortBy f [] = []" 164249423Sdim| "sortBy f (a # as) = insertBy f a (sortBy f as)" 165249423Sdim 166249423Sdimlemma sortBy_length: 167249423Sdim "length (sortBy f as) = length as" 168249423Sdim by (induct as) simp_all 169251662Sdim 170249423Sdimdefinition 171249423Sdim "sortH \<equiv> sortBy compare" 172249423Sdim 173249423Sdimdefinition 174249423Sdim "catMaybes \<equiv> (map the) \<circ> (filter isJust)" 175249423Sdim 176249423Sdimdefinition 177249423Sdim "runExceptT \<equiv> id" 178249423Sdim 179251662Sdimdeclare Just_def[simp] Nothing_def[simp] fromJust_def[simp] 180249423Sdim isJust_def[simp] tail_def[simp] head_def[simp] 181249423Sdim error_def[simp] reverse_def[simp] isNothing_def[simp] 182251662Sdim maybeApply_def[simp] maybe_def[simp] 183249423Sdim foldR_def[simp] elem_def[simp] notElem_def[simp] 184249423Sdim catMaybes_def[simp] runExceptT_def[simp] 185249423Sdim 186249423Sdimdefinition 187249423Sdim "headM L \<equiv> (case L of (h # t) \<Rightarrow> return h | _ \<Rightarrow> fail)" 188249423Sdim 189249423Sdimdefinition 190249423Sdim "tailM L \<equiv> (case L of (h # t) \<Rightarrow> return t | _ \<Rightarrow> fail)" 191249423Sdim 192249423Sdimaxiomatization 193249423Sdim typeOf :: "'a \<Rightarrow> unit list" 194251662Sdim 195249423Sdimdefinition 196249423Sdim "either f1 f2 c \<equiv> case c of Inl r1 \<Rightarrow> f1 r1 | Inr r2 \<Rightarrow> f2 r2" 197249423Sdim 198249423Sdimlemma either_simp[simp]: "either = case_sum" 199249423Sdim apply (rule ext)+ 200249423Sdim apply (simp add: either_def) 201249423Sdim done 202249423Sdim 203249423Sdimclass HS_bit = bit_operations + 204249423Sdim fixes shiftL :: "'a \<Rightarrow> nat \<Rightarrow> 'a" 205249423Sdim fixes shiftR :: "'a \<Rightarrow> nat \<Rightarrow> 'a" 206249423Sdim fixes bitSize :: "'a \<Rightarrow> nat" 207249423Sdim 208249423Sdiminstantiation word :: (len0) HS_bit 209249423Sdimbegin 210249423Sdim 211249423Sdimdefinition 212249423Sdim shiftL_word[simp]: "(shiftL :: 'a::len0 word \<Rightarrow> nat \<Rightarrow> 'a word) \<equiv> shiftl" 213249423Sdim 214249423Sdimdefinition 215249423Sdim shiftR_word[simp]: "(shiftR :: 'a::len0 word \<Rightarrow> nat \<Rightarrow> 'a word) \<equiv> shiftr" 216249423Sdim 217251662Sdimdefinition 218249423Sdim bitSize_word[simp]: "(bitSize :: 'a::len0 word \<Rightarrow> nat) \<equiv> size" 219249423Sdim 220249423Sdiminstance .. 221249423Sdim 222249423Sdimend 223249423Sdim 224249423Sdiminstantiation nat :: HS_bit 225249423Sdimbegin 226249423Sdim 227249423Sdimdefinition 228249423Sdim shiftL_nat: "shiftL (x :: nat) n \<equiv> (2 ^ n) * x" 229249423Sdim 230249423Sdimdefinition 231251662Sdim shiftR_nat: "shiftR (x :: nat) n \<equiv> x div (2 ^ n)" 232249423Sdim 233249423Sdimtext \<open>bitSize not defined for nat\<close> 234249423Sdim 235249423Sdiminstance .. 236249423Sdim 237249423Sdimend 238249423Sdim 239249423Sdimclass finiteBit = bit_operations + 240249423Sdim fixes finiteBitSize :: "'a \<Rightarrow> nat" 241249423Sdim 242249423Sdiminstantiation word :: (len0) finiteBit 243249423Sdimbegin 244249423Sdim 245249423Sdimdefinition 246249423Sdim finiteBitSize_word[simp]: "(finiteBitSize :: 'a::len0 word \<Rightarrow> nat) \<equiv> size" 247249423Sdim 248249423Sdiminstance .. 249249423Sdim 250249423Sdimend 251249423Sdim 252249423Sdimdefinition bit :: "nat \<Rightarrow> 'a::{one,HS_bit}" where 253249423Sdim bit_def[simp]: "bit x \<equiv> shiftL 1 x" 254249423Sdim 255249423Sdimdefinition 256249423Sdim"isAligned x n \<equiv> x && mask n = 0" 257249423Sdim 258249423Sdimclass integral = ord + 259249423Sdim fixes fromInteger :: "nat \<Rightarrow> 'a" 260251662Sdim fixes toInteger :: "'a \<Rightarrow> nat" 261249423Sdim assumes integral_inv: "fromInteger \<circ> toInteger = id" 262249423Sdim 263249423Sdiminstantiation nat :: integral 264249423Sdimbegin 265249423Sdim 266249423Sdimdefinition 267251662Sdim fromInteger_nat: "fromInteger \<equiv> id" 268249423Sdim 269249423Sdimdefinition 270249423Sdim toInteger_nat: "toInteger \<equiv> id" 271249423Sdim 272249423Sdiminstance 273249423Sdim apply (intro_classes) 274249423Sdim apply (simp add: toInteger_nat fromInteger_nat) 275249423Sdim done 276249423Sdim 277249423Sdimend 278249423Sdim 279249423Sdim 280249423Sdiminstantiation word :: (len) integral 281251662Sdimbegin 282249423Sdim 283249423Sdimdefinition 284249423Sdim fromInteger_word: "fromInteger \<equiv> of_nat :: nat \<Rightarrow> 'a::len word" 285249423Sdim 286249423Sdimdefinition 287249423Sdim toInteger_word: "toInteger \<equiv> unat" 288249423Sdim 289249423Sdiminstance 290249423Sdim apply (intro_classes) 291249423Sdim apply (rule ext) 292249423Sdim apply (simp add: toInteger_word fromInteger_word) 293249423Sdim done 294249423Sdim 295249423Sdimend 296249423Sdim 297249423Sdimdefinition 298249423Sdim fromIntegral :: "('a :: integral) \<Rightarrow> ('b :: integral)" where 299249423Sdim "fromIntegral \<equiv> fromInteger \<circ> toInteger" 300249423Sdim 301249423Sdimlemma fromIntegral_simp1[simp]: "(fromIntegral :: nat \<Rightarrow> ('a :: len) word) = of_nat" 302249423Sdim by (simp add: fromIntegral_def fromInteger_word toInteger_nat) 303249423Sdim 304249423Sdimlemma fromIntegral_simp2[simp]: "fromIntegral = unat" 305249423Sdim by (simp add: fromIntegral_def fromInteger_nat toInteger_word) 306249423Sdim 307249423Sdimlemma fromIntegral_simp3[simp]: "fromIntegral = ucast" 308249423Sdim apply (simp add: fromIntegral_def fromInteger_word toInteger_word) 309251662Sdim apply (rule ext) 310249423Sdim apply (simp add: ucast_def) 311249423Sdim apply (subst word_of_nat) 312249423Sdim apply (simp add: unat_def) 313249423Sdim done 314249423Sdim 315249423Sdimlemma fromIntegral_simp_nat[simp]: "(fromIntegral :: nat \<Rightarrow> nat) = id" 316249423Sdim by (simp add: fromIntegral_def fromInteger_nat toInteger_nat) 317249423Sdim 318249423Sdimdefinition 319249423Sdim infix_apply :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("_ `~_~` _" [81, 100, 80] 80) where 320249423Sdim infix_apply_def[simp]: 321249423Sdim "infix_apply a f b \<equiv> f a b" 322249423Sdim 323249423Sdimterm "return $ a `~b~` c d" 324249423Sdim 325249423Sdimdefinition 326249423Sdim zip3 :: "'a list \<Rightarrow> 'b list \<Rightarrow> 'c list \<Rightarrow> ('a \<times> 'b \<times> 'c) list" where 327249423Sdim "zip3 a b c \<equiv> zip a (zip b c)" 328249423Sdim 329249423Sdim(* avoid even attempting haskell's show class *) 330249423Sdimdefinition 331249423Sdim "show" :: "'a \<Rightarrow> unit list" where 332249423Sdim "show x \<equiv> []" 333249423Sdim 334249423Sdimlemma show_simp_away[simp]: "S @ show t = S" 335249423Sdim by (simp add: show_def) 336249423Sdim 337249423Sdimdefinition 338249423Sdim "andList \<equiv> foldl (\<and>) True" 339249423Sdim 340249423Sdimdefinition 341249423Sdim "orList \<equiv> foldl (\<or>) False" 342249423Sdim 343249423Sdimprimrec 344251662Sdim mapAccumL :: "('a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'c) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'a \<times> ('c list)" 345249423Sdimwhere 346249423Sdim "mapAccumL f s [] = (s, [])" 347249423Sdim| "mapAccumL f s (x#xs) = ( 348251662Sdim let (s', r) = f s x; 349249423Sdim (s'', rs) = mapAccumL f s' xs 350249423Sdim in (s'', r#rs) 351249423Sdim )" 352249423Sdim 353249423Sdimprimrec 354249423Sdim untilM :: "('b \<Rightarrow> ('s, 'a option) nondet_monad) \<Rightarrow> 'b list \<Rightarrow> ('s, 'a option) nondet_monad" 355249423Sdimwhere 356249423Sdim "untilM f [] = return None" 357249423Sdim| "untilM f (x#xs) = do 358249423Sdim r \<leftarrow> f x; 359249423Sdim case r of 360249423Sdim None \<Rightarrow> untilM f xs 361249423Sdim | Some res \<Rightarrow> return (Some res) 362249423Sdim od" 363249423Sdim 364249423Sdimprimrec 365249423Sdim untilME :: "('c \<Rightarrow> ('s, ('a + 'b option)) nondet_monad) \<Rightarrow> 'c list \<Rightarrow> ('s, 'a + 'b option) nondet_monad" 366249423Sdimwhere 367249423Sdim "untilME f [] = returnOk None" 368249423Sdim| "untilME f (x#xs) = doE 369249423Sdim r \<leftarrow> f x; 370249423Sdim case r of 371249423Sdim None \<Rightarrow> untilME f xs 372249423Sdim | Some res \<Rightarrow> returnOk (Some res) 373249423Sdim odE" 374249423Sdim 375249423Sdimprimrec 376249423Sdim findM :: "('a \<Rightarrow> ('s, bool) nondet_monad) \<Rightarrow> 'a list \<Rightarrow> ('s, 'a option) nondet_monad" 377249423Sdimwhere 378249423Sdim "findM f [] = return None" 379249423Sdim| "findM f (x#xs) = do 380249423Sdim r \<leftarrow> f x; 381249423Sdim if r 382249423Sdim then return (Some x) 383249423Sdim else findM f xs 384249423Sdim od" 385249423Sdim 386249423Sdimprimrec 387249423Sdim findME :: "('a \<Rightarrow> ('s, ('e + bool)) nondet_monad) \<Rightarrow> 'a list \<Rightarrow> ('s, ('e + 'a option)) nondet_monad" 388249423Sdimwhere 389249423Sdim "findME f [] = returnOk None" 390249423Sdim| "findME f (x#xs) = doE 391249423Sdim r \<leftarrow> f x; 392249423Sdim if r 393249423Sdim then returnOk (Some x) 394249423Sdim else findME f xs 395249423Sdim odE" 396249423Sdim 397249423Sdimprimrec 398249423Sdim tails :: "'a list \<Rightarrow> 'a list list" 399249423Sdimwhere 400249423Sdim "tails [] = [[]]" 401249423Sdim| "tails (x#xs) = (x#xs)#(tails xs)" 402249423Sdim 403249423Sdimlemma finite_surj_type: 404249423Sdim "\<lbrakk> (\<forall>x. \<exists>y. (x :: 'b) = f (y :: 'a)); finite (UNIV :: 'a set) \<rbrakk> \<Longrightarrow> finite (UNIV :: 'b set)" 405249423Sdim apply (erule finite_surj) 406249423Sdim apply safe 407249423Sdim apply (erule allE) 408249423Sdim apply safe 409249423Sdim apply (erule image_eqI) 410249423Sdim apply simp 411249423Sdim done 412249423Sdim 413249423Sdimlemma finite_finite[simp]: "finite (s :: ('a :: finite) set)" 414249423Sdim by simp 415249423Sdim 416249423Sdimlemma finite_inv_card_less': 417249423Sdim "U = (UNIV :: ('a :: finite) set) \<Longrightarrow> (card (U - insert a s) < card (U - s)) = (a \<notin> s)" 418249423Sdim apply (case_tac "a \<in> s") 419251662Sdim apply (simp_all add: insert_absorb) 420249423Sdim apply (subgoal_tac "card s < card U") 421249423Sdim apply (simp add: card_Diff_subset) 422249423Sdim apply (rule psubset_card_mono) 423249423Sdim apply safe 424249423Sdim apply simp_all 425249423Sdim done 426249423Sdim 427249423Sdimlemma finite_inv_card_less: 428249423Sdim "(card (UNIV - insert (a :: ('a :: finite)) s) < card (UNIV - s)) = (a \<notin> s)" 429249423Sdim by (simp add: finite_inv_card_less') 430249423Sdim 431249423Sdimdefinition 432249423Sdim "minimum ls \<equiv> Min (set ls)" 433249423Sdimdefinition 434249423Sdim "maximum ls \<equiv> Max (set ls)" 435249423Sdim 436249423Sdimprimrec (nonexhaustive) 437249423Sdim hdCons :: "'a \<Rightarrow> 'a list list \<Rightarrow> 'a list list" 438249423Sdimwhere 439249423Sdim "hdCons x (ys # zs) = (x # ys) # zs" 440249423Sdim 441251662Sdimprimrec 442249423Sdim rangesBy :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list list" 443249423Sdimwhere 444251662Sdim "rangesBy f [] = []" 445249423Sdim| "rangesBy f (x # xs) = 446249423Sdim (case xs of [] \<Rightarrow> [[x]] 447249423Sdim | (y # ys) \<Rightarrow> if (f x y) then hdCons x (rangesBy f xs) 448249423Sdim else [x] # (rangesBy f xs))" 449249423Sdim 450249423Sdimdefinition 451249423Sdim partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<times> 'a list" where 452249423Sdim "partition f xs \<equiv> (filter f xs, filter (\<lambda>x. \<not> f x) xs)" 453249423Sdim 454249423Sdimdefinition 455249423Sdim listSubtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where 456249423Sdim "listSubtract xs ys \<equiv> filter (\<lambda>x. x \<in> set ys) xs" 457249423Sdim 458249423Sdimdefinition 459251662Sdim init :: "'a list \<Rightarrow> 'a list" where 460249423Sdim "init xs \<equiv> case (length xs) of Suc n \<Rightarrow> take n xs | _ \<Rightarrow> undefined" 461249423Sdim 462249423Sdimprimrec 463249423Sdim break :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> ('a list \<times> 'a list)" 464249423Sdimwhere 465249423Sdim "break f [] = ([], [])" 466251662Sdim| "break f (x # xs) = 467249423Sdim (if f x 468249423Sdim then ([], x # xs) 469249423Sdim else (\<lambda>(ys, zs). (x # ys, zs)) (break f xs))" 470249423Sdim 471249423Sdimdefinition 472249423Sdim "uncurry \<equiv> case_prod" 473249423Sdim 474249423Sdimdefinition 475249423Sdim sum :: "'a list \<Rightarrow> 'a::{plus,zero}" where 476249423Sdim "sum \<equiv> foldl (+) 0" 477249423Sdim 478249423Sdimdefinition 479249423Sdim "replicateM n m \<equiv> sequence (replicate n m)" 480249423Sdim 481249423Sdimdefinition 482249423Sdim maybeToMonad_def[simp]: 483249423Sdim "maybeToMonad \<equiv> assert_opt" 484249423Sdim 485249423Sdimdefinition 486249423Sdim funArray :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" where 487249423Sdim funArray_def[simp]: 488249423Sdim "funArray \<equiv> id" 489249423Sdim 490249423Sdimdefinition 491249423Sdim funPartialArray :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a :: enumeration_alt \<times> 'a) \<Rightarrow> ('a \<Rightarrow> 'b)" where 492263508Sdim "funPartialArray f xrange \<equiv> \<lambda>x. (if x \<in> set [fst xrange .e. snd xrange] then f x else undefined)" 493249423Sdim 494249423Sdimdefinition 495249423Sdim forM_def[simp]: 496249423Sdim "forM xs f \<equiv> mapM f xs" 497249423Sdim 498251662Sdimdefinition 499249423Sdim forM_x_def[simp]: 500249423Sdim "forM_x xs f \<equiv> mapM_x f xs" 501249423Sdim 502249423Sdimdefinition 503249423Sdim forME_x_def[simp]: 504249423Sdim "forME_x xs f \<equiv> mapME_x f xs" 505249423Sdim 506249423Sdimdefinition 507249423Sdim arrayListUpdate :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<Rightarrow> 'b)" (infixl "aLU" 90) 508249423Sdimwhere 509249423Sdim arrayListUpdate_def[simp]: 510249423Sdim "arrayListUpdate f l \<equiv> foldl (\<lambda>f p. f(fst p := snd p)) f l" 511249423Sdim 512251662Sdimdefinition 513249423Sdim "genericTake \<equiv> take \<circ> fromIntegral" 514249423Sdim 515249423Sdimdefinition 516249423Sdim "genericLength \<equiv> fromIntegral \<circ> length" 517249423Sdim 518249423Sdimabbreviation 519249423Sdim "null == List.null" 520249423Sdim 521249423Sdimsyntax (input) 522249423Sdim "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" ("[_ | __") 523251662Sdim 524249423Sdimlemma "[(x,1) . x \<leftarrow> [0..10]] = [(x,1) | x \<leftarrow> [0..10]]" by (rule refl) 525249423Sdim 526249423Sdimend 527249423Sdim