--- a/src/HOL/UNITY/Lift_prog.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy Mon Mar 01 13:40:23 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/UNITY/Lift_prog.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1999 University of Cambridge
@@ -10,30 +9,28 @@
theory Lift_prog imports Rename begin
-constdefs
-
- insert_map :: "[nat, 'b, nat=>'b] => (nat=>'b)"
+definition insert_map :: "[nat, 'b, nat=>'b] => (nat=>'b)" where
"insert_map i z f k == if k<i then f k
else if k=i then z
else f(k - 1)"
- delete_map :: "[nat, nat=>'b] => (nat=>'b)"
+definition delete_map :: "[nat, nat=>'b] => (nat=>'b)" where
"delete_map i g k == if k<i then g k else g (Suc k)"
- lift_map :: "[nat, 'b * ((nat=>'b) * 'c)] => (nat=>'b) * 'c"
+definition lift_map :: "[nat, 'b * ((nat=>'b) * 'c)] => (nat=>'b) * 'c" where
"lift_map i == %(s,(f,uu)). (insert_map i s f, uu)"
- drop_map :: "[nat, (nat=>'b) * 'c] => 'b * ((nat=>'b) * 'c)"
+definition drop_map :: "[nat, (nat=>'b) * 'c] => 'b * ((nat=>'b) * 'c)" where
"drop_map i == %(g, uu). (g i, (delete_map i g, uu))"
- lift_set :: "[nat, ('b * ((nat=>'b) * 'c)) set] => ((nat=>'b) * 'c) set"
+definition lift_set :: "[nat, ('b * ((nat=>'b) * 'c)) set] => ((nat=>'b) * 'c) set" where
"lift_set i A == lift_map i ` A"
- lift :: "[nat, ('b * ((nat=>'b) * 'c)) program] => ((nat=>'b) * 'c) program"
+definition lift :: "[nat, ('b * ((nat=>'b) * 'c)) program] => ((nat=>'b) * 'c) program" where
"lift i == rename (lift_map i)"
(*simplifies the expression of specifications*)
- sub :: "['a, 'a=>'b] => 'b"
+definition sub :: "['a, 'a=>'b] => 'b" where
"sub == %i f. f i"