[isabelle] Partial functions basics



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.