Commit 973f8b48 authored by Andrei Paskevich's avatar Andrei Paskevich

theories/map.why: remove Select_eq and Select_neq, subsumed by the definition

parent 578c2fca
......@@ -174,9 +174,6 @@ theory HighOrd
end
theory map.Map
syntax function get "(%1[%2])"
syntax function set "(%1[%2 <- %3])"
remove prop Select_eq
remove prop Select_neq
syntax function get "(%1[%2])"
syntax function set "(%1[%2 <- %3])"
end
......@@ -32,16 +32,11 @@ theory HighOrd
end
theory map.Map
syntax function get "%1(%2)"
syntax function get "%1(%2)"
syntax function ([]) "%1(%2)"
syntax function set "(%1 WITH [(%2) |-> %3])"
syntax function ([<-]) "(%1 WITH [(%2) |-> %3])"
remove prop Select_eq
remove prop Select_neq
end
theory Bool
......
......@@ -161,11 +161,6 @@ theory map.Map
meta "encoding:ignore_polymorphism_ls" function ([])
meta "encoding:ignore_polymorphism_ls" function set
meta "encoding:ignore_polymorphism_ls" function ([<-])
meta "encoding:ignore_polymorphism_pr" prop Select_eq
meta "encoding:ignore_polymorphism_pr" prop Select_neq
remove prop Select_eq
remove prop Select_neq
end
theory map.Const
......
......@@ -51,11 +51,6 @@ theory map.Map
meta "encoding:ignore_polymorphism_ls" function ([])
meta "encoding:ignore_polymorphism_ls" function set
meta "encoding:ignore_polymorphism_ls" function ([<-])
meta "encoding:ignore_polymorphism_pr" prop Select_eq
meta "encoding:ignore_polymorphism_pr" prop Select_neq
remove prop Select_eq
remove prop Select_neq
end
import "discrimination.gen"
......@@ -8,34 +8,15 @@ theory Map
type map 'a 'b = 'a -> 'b
(* FIXME: add meta "material_type_arg" type func, 1 for (->) *)
(* FIXME: remove Select_eq, Select_neq, and Const ? *)
(* FIXME: we cannot remove the defining axiom for set in a driver. *)
(*
(** if ['b] is an infinite type, then [map 'a 'b] is infinite *)
meta "material_type_arg" type func, 1
*)
function get (f: map 'a 'b) (x: 'a) : 'b = f x
function set (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b =
fun y -> if y = x then v else f y
(** syntactic sugar *)
function ([]) (f: map 'a 'b) (x: 'a) : 'b = get f x
function ([]) (f: map 'a 'b) (x: 'a) : 'b = f x
function ([<-]) (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b = set f x v
lemma Select_eq :
forall m : map 'a 'b. forall a1 a2 : 'a.
forall b : 'b [m[a1 <- b][a2]].
a1 = a2 -> m[a1 <- b][a2] = b
lemma Select_neq :
forall m : map 'a 'b. forall a1 a2 : 'a.
forall b : 'b [m[a1 <- b][a2]].
a1 <> a2 -> m[a1 <- b][a2] = m[a2]
end
theory Const
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment