isabelle - How to define a supremum on a set? -


i'm trying describe type system of programming language. has common subtype types (voidtype) , common supertype types (anytype):

datatype type =   voidtype |   anytype |   booleantype |   ebooleantype |   realtype |   integertype |   unlimnattype |   stringtype  fun subtype_strict_fun :: "type ⇒ type ⇒ bool" (infix "<:sf" 55)   "_ <:sf voidtype = false" | "voidtype <:sf _ = true" | "anytype <:sf _ = false" | "_ <:sf anytype = true" | "booleantype <:sf ebooleantype = true" | "integertype <:sf realtype = true" | "unlimnattype <:sf integertype = true" | "unlimnattype <:sf realtype = true" | "_ <:sf _ = false"  definition subtype_fun :: "type ⇒ type ⇒ bool" (infix "<:f" 55)   "x <:f y ≡ x = y ∨ x <:sf y"

i'm trying instantinate type ccpo:

instantiation type :: ccpo begin  definition "less_eq = subtype_fun" definition "less = subtype_strict_fun"  lemma subtype_strict_eq_subtype:   "(x <:sf y) = (x <:f y ∧ ¬ y <:f x)"   (cases x; cases y; simp add: subtype_fun_def)  lemma subtype_refl:   "x <:f x"   (simp add: subtype_fun_def)  lemma subtype_trans:   "x <:f y ⟹ y <:f z ⟹ x <:f z"   (cases x; cases y; cases z; simp add: subtype_fun_def)  lemma subtype_antisym:   "x <:f y ⟹ y <:f x ⟹ x = y"   (cases x; cases y; simp add: subtype_fun_def)  instance   apply intro_classes   apply (simp add: less_eq_type_def less_type_def subtype_strict_eq_subtype)   apply (simp add: less_eq_type_def less_type_def subtype_refl)   apply (metis less_eq_type_def subtype_trans)   apply (metis less_eq_type_def subtype_antisym)  end

could suggest how define supremum function sup :: ocl.type set ⇒ ocl.type?

the type ocl.type finite, sets of type ocl.type set finite, too. moreover, there top element in hierarchy. therefore, can define sup operation folding sup on given set. locale comm_monoid_set provides necessary infrastructure. first, instantiate type classes semilattice_sup , order_top. interpret comm_monoid_set:

interpretation ocl': abel_semigroup sup "top :: ocl.type" <proof> interpretation ocl: comm_monoid_set sup "top :: ocl.type" <proof>

this generates folded sup operation on sets under name ocl.f. so,

definition "sup_ocl = ocl.f id"

gives definition sup operation. general construction works finite upper semilattice top element. not give dedicated setup reasoning ocl.type hierarchy in particular. you'll have derive appropriate rules yourself.


Comments

Post a Comment

Popular posts from this blog

python - Selenium remoteWebDriver (& SauceLabs) Firefox moseMoveTo action exception -

while performing simple hover test on firefox through selenium (3.4.0) python bindings (3.4.3) using of available os in saucelabs (except linux, latest available firefox version old), performing following actionchain: hover = actionchains(driver) hover.move_to_element(elm_men_menu).perform() it throws following error: taceback: file [...] in testhover hover.perform() file "/usr/local/lib/python2.7/dist-packages/selenium/webdriver/common/action_chains.py", line 80, in perform action() file "/usr/local/lib/python2.7/dist-packages/selenium/webdriver/common/action_chains.py", line 290, in <lambda> command.move_to, {'element': to_element.id})) file "/usr/local/lib/python2.7/dist-packages/selenium/webdriver/remote/webdriver.py", line 256, in execute self.error_handler.check_response(response) file "/usr/local/lib/python2.7/...
Read more

html - How to custom Bootstrap grid height? -

why bootstrap grid has height 591.067 ? did height came ? .main-post { padding: 20px; background-color: #fff; border: 1px solid #d8d8d8; margin-bottom: 100px; } .main-post .post-categories { margin-bottom: 10px } .main-post h3 { margin: 0 0 10px; color: #777; letter-spacing: -1px; font-weight: bold } .main-post .post-author, .main-post .post-date, .main-post .post-comments { font-size: 12px } .main-post img { display: block; margin: 10px 0; } .main-post .post-summary { line-height: 1.7; color: #888 } .main-post { color: #999 } <div class="col-sm-6"> <div class="main-post"> <h3 class="post-title"> <a href="#"> post title </a> </...
Read more

transpose - Maple isnt executing function but prints function term -

im using maple im in worksheetmode tried using maple input , 2d input , want transpose matrix a: := `<|>`(`<,>`(1, .5, -2), `<,>`(.5, 9/4+b, 5+3*b), `<,>`(-2, 5+3*b, 18+9*b+4*a)); b:= transpose(a); when exectute sheet dont translated values, there same input. matrix looks same input matrix plus function term. you can see picture in following link: why arent functions executed? meanwhile b:=a^+ doing right way , transposed matrix. other functions return function body instead needed values... if using 2d input mode (the default) space you've got between transpose , bracketed (b) interpreted multiplcation. rid of such space. also, either load package @ start of document like, with(linearalgebra): before calling transpose command package, or call it's full name like, linearalgebra:-transpose(b);
Read more