src/HOL/UNITY/Rename.thy
author paulson
Fri Feb 18 15:37:08 2000 +0100 (2000-02-18)
changeset 8256 6ba8fa2b0638
child 9403 aad13b59b8d9
permissions -rw-r--r--
Rename: theory for applying a bijection over states to a UNITY program
paulson@8256
     1
(*  Title:      HOL/UNITY/Rename.thy
paulson@8256
     2
    ID:         $Id$
paulson@8256
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@8256
     4
    Copyright   2000  University of Cambridge
paulson@8256
     5
paulson@8256
     6
Renaming of state sets
paulson@8256
     7
*)
paulson@8256
     8
paulson@8256
     9
Rename = Extend +
paulson@8256
    10
paulson@8256
    11
constdefs
paulson@8256
    12
  rename_act :: "['a => 'b, ('a*'a) set] => ('b*'b) set"
paulson@8256
    13
    "rename_act h == extend_act (%(x,u::unit). h x)"
paulson@8256
    14
paulson@8256
    15
(**OR
paulson@8256
    16
      "rename_act h == %act. UN (s,s'): act.  {(h s, h s')}"
paulson@8256
    17
      "rename_act h == %act. (prod_fun h h) `` act"
paulson@8256
    18
**)
paulson@8256
    19
  
paulson@8256
    20
  rename :: "['a => 'b, 'a program] => 'b program"
paulson@8256
    21
    "rename h == extend (%(x,u::unit). h x)"
paulson@8256
    22
paulson@8256
    23
end