Re: [isabelle] Partial functions basics



Hi Roger,

For this you want "f ++ g". Such things are defined in Map.thy -- see here:

http://isabelle.in.tum.de/library/HOL/HOL/Map.html

Best wishes,
John

On 9 Jan 2014, at 17:21, Roger H. <s57076 at hotmail.com> wrote:

> Hi,
> 
> how can i make "f ∪ g"?
> 
> definition f :: "nat ⇀ nat" where
> "f = [1 ↦ 0, 2 ↦ 5]"
> definition g :: "nat ⇀ nat" where 
> "g = [3 ↦ 7, 4 ↦ 9]"
> definition f_union_g :: "nat ⇀ nat" where
> "f_union_g = [1 ↦ 0, 2 ↦ 5, 3 ↦ 7, 4 ↦ 9]"
> 
> So how should i define f_union_g?
> 
> And generally in what class.thy can i find such operators on partial functions?
> 
> Thank you!
> 
> 
> 
> 
> 		 	   		  





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.