src/HOL/UNITY/Rename.thy
changeset 8256 6ba8fa2b0638
child 9403 aad13b59b8d9
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/UNITY/Rename.thy	Fri Feb 18 15:37:08 2000 +0100
     1.3 @@ -0,0 +1,23 @@
     1.4 +(*  Title:      HOL/UNITY/Rename.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   2000  University of Cambridge
     1.8 +
     1.9 +Renaming of state sets
    1.10 +*)
    1.11 +
    1.12 +Rename = Extend +
    1.13 +
    1.14 +constdefs
    1.15 +  rename_act :: "['a => 'b, ('a*'a) set] => ('b*'b) set"
    1.16 +    "rename_act h == extend_act (%(x,u::unit). h x)"
    1.17 +
    1.18 +(**OR
    1.19 +      "rename_act h == %act. UN (s,s'): act.  {(h s, h s')}"
    1.20 +      "rename_act h == %act. (prod_fun h h) `` act"
    1.21 +**)
    1.22 +  
    1.23 +  rename :: "['a => 'b, 'a program] => 'b program"
    1.24 +    "rename h == extend (%(x,u::unit). h x)"
    1.25 +
    1.26 +end