equal
deleted
inserted
replaced
447 lemma [code]: |
447 lemma [code]: |
448 "iter f step ss w = while (\<lambda>(ss, w). \<not> is_empty w) |
448 "iter f step ss w = while (\<lambda>(ss, w). \<not> is_empty w) |
449 (\<lambda>(ss, w). |
449 (\<lambda>(ss, w). |
450 let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p})) |
450 let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p})) |
451 (ss, w)" |
451 (ss, w)" |
452 unfolding iter_def List_Set.is_empty_def some_elem_def .. |
452 unfolding iter_def More_Set.is_empty_def some_elem_def .. |
453 |
453 |
454 lemma JVM_sup_unfold [code]: |
454 lemma JVM_sup_unfold [code]: |
455 "JVMType.sup S m n = lift2 (Opt.sup |
455 "JVMType.sup S m n = lift2 (Opt.sup |
456 (Product.sup (Listn.sup (JType.sup S)) |
456 (Product.sup (Listn.sup (JType.sup S)) |
457 (\<lambda>x y. OK (map2 (lift2 (JType.sup S)) x y))))" |
457 (\<lambda>x y. OK (map2 (lift2 (JType.sup S)) x y))))" |