Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/UNITY/Project.thy
author wenzelm
Mon, 28 Aug 2000 14:09:33 +0200
changeset 9697 c5fc121c2067
parent 8055 bb15396278fb
child 10064 1a77667b21ef
permissions -rw-r--r--
restart_loader: reset_path;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset 
     1
 
(*  Title:      HOL/UNITY/Project.ML
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset 
     2
 
    ID:         $Id$
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset 
     3
 
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset 
     4
 
    Copyright   1999  University of Cambridge
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset 
     5
 












d0e4a6f1f05c
working snapshot with new theory "Project"



paulson


parents: 

diff
changeset




     6


Projections of state sets (also of actions and programs)













d0e4a6f1f05c
working snapshot with new theory "Project"



paulson


parents: 

diff
changeset




     7














d0e4a6f1f05c
working snapshot with new theory "Project"



paulson


parents: 

diff
changeset




     8


Inheritance of GUARANTEES properties under extension













d0e4a6f1f05c
working snapshot with new theory "Project"



paulson


parents: 

diff
changeset




     9


*)













d0e4a6f1f05c
working snapshot with new theory "Project"



paulson


parents: 

diff
changeset




    10









7826






c6a8b73b6c2a
working shapshot with "projecting" and "extending"



paulson


parents: 
7689

diff
changeset




    11


Project = Extend +













c6a8b73b6c2a
working shapshot with "projecting" and "extending"



paulson


parents: 
7689

diff
changeset




    12














c6a8b73b6c2a
working shapshot with "projecting" and "extending"



paulson


parents: 
7689

diff
changeset




    13


constdefs













c6a8b73b6c2a
working shapshot with "projecting" and "extending"



paulson


parents: 
7689

diff
changeset




    14


  projecting :: "['c program => 'c set, 'a*'b => 'c, 













c6a8b73b6c2a
working shapshot with "projecting" and "extending"



paulson


parents: 
7689

diff
changeset




    15


		  'a program, 'c program set, 'a program set] => bool"













c6a8b73b6c2a
working shapshot with "projecting" and "extending"



paulson


parents: 
7689

diff
changeset




    16


  "projecting C h F X' X ==








7880






62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"



paulson


parents: 
7878

diff
changeset




    17


     ALL G. extend h F Join G : X' --> F Join project h (C G) G : X"








7826






c6a8b73b6c2a
working shapshot with "projecting" and "extending"



paulson


parents: 
7689

diff
changeset




    18









8055






bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument



paulson


parents: 
7947

diff
changeset




    19


  extending :: "['c=>'d, 'c program => 'c set, 'a*'b => 'c, 'a program, 













bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument



paulson


parents: 
7947

diff
changeset




    20


		 'c program set, 'a program set] => bool"













bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument



paulson


parents: 
7947

diff
changeset




    21


  "extending v C h F Y' Y ==













bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument



paulson


parents: 
7947

diff
changeset




    22


     ALL G. G : preserves v --> F Join project h (C G) G : Y








7826






c6a8b73b6c2a
working shapshot with "projecting" and "extending"



paulson


parents: 
7689

diff
changeset




    23


            --> extend h F Join G : Y'"













c6a8b73b6c2a
working shapshot with "projecting" and "extending"



paulson


parents: 
7689

diff
changeset




    24














c6a8b73b6c2a
working shapshot with "projecting" and "extending"



paulson


parents: 
7689

diff
changeset




    25


end















isabelle