/[mojave]/metaprl/theories/czf/czf_itt_inv_image.ml
ViewVC logotype

Diff of /metaprl/theories/czf/czf_itt_inv_image.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3566 by xiny, Sun Mar 24 08:21:13 2002 UTC revision 3567 by xiny, Tue Apr 9 05:57:26 2002 UTC
# Line 1  Line 1 
1  include Czf_itt_set  include Czf_itt_set
2  include Czf_itt_member  include Czf_itt_set_bvd
3    
4  open Printf  open Printf
5  open Mp_debug  open Mp_debug
# Line 23  Line 23 
23  open Base_dtactic  open Base_dtactic
24  open Base_auto_tactic  open Base_auto_tactic
25    
26  declare inv_image{'s; x. 'a['x]; 't}  (* { x in s | a(x) in t } *)  (* The inverse image of t in s: { x in s | a(x) in t } *)
27    declare inv_image{'s; x. 'a['x]; 't}
28    
29    prim_rw unfold_inv_image: inv_image{'s; x. 'a['x]; 't} <-->
30       setbvd_prop{'s; x. mem{'a['x]; 't}}
31    
32    let fold_inv_image = makeFoldC << inv_image{'s; x. 'a['x]; 't} >> unfold_inv_image
33    
34  dform inv_image_df : parens :: except_mode[src] :: inv_image{'s; x. 'a; 't} =  dform inv_image_df : parens :: except_mode[src] :: inv_image{'s; x. 'a; 't} =
35     pushm[0] `"{" slot{'x} Nuprl_font!member `"s " slot{'s} `"| " slot{'a} " " Nuprl_font!member `"s " slot{'t} `"}" popm     pushm[0] `"{" slot{'x} " " Nuprl_font!member `"s " slot{'s} `" | " slot{'a} " " Nuprl_font!member `"s " slot{'t} `"}" popm
36    
37  (*  (*
38   * Axioms for inverse image.   * Axioms for inverse image.
# Line 53  Line 59 
59     sequent [squash] { 'H; x: mem{'y; inv_image{'s; x. 'a['x]; 't}}; 'J['x] >- isset{'t} } -->     sequent [squash] { 'H; x: mem{'y; inv_image{'s; x. 'a['x]; 't}}; 'J['x] >- isset{'t} } -->
60     sequent ['ext] { 'H; x: mem{'y; inv_image{'s; x. 'a['x]; 't}}; 'J['x]; z: set >- isset{'a['z]} } -->     sequent ['ext] { 'H; x: mem{'y; inv_image{'s; x. 'a['x]; 't}}; 'J['x]; z: set >- isset{'a['z]} } -->
61     sequent ['ext] { 'H; x: mem{'y; inv_image{'s; x. 'a['x]; 't}}; 'J['x] >- fun_set{x. 'a['x]} } -->     sequent ['ext] { 'H; x: mem{'y; inv_image{'s; x. 'a['x]; 't}}; 'J['x] >- fun_set{x. 'a['x]} } -->
62     sequent ['ext] { 'H; x: mem{'y; inv_image{'s; x. 'a['x]; 't}}; 'J['x] >- mem{'y; 's} } -->     sequent ['ext] { 'H; x: mem{'y; inv_image{'s; x. 'a['x]; 't}}; 'J['x]; v: mem{'y; 's}; w: mem{'a['y]; 't} >- 'C['x] } -->
    sequent ['ext] { 'H; x: mem{'y; inv_image{'s; x. 'a['x]; 't}}; 'J['x]; w: mem{'a['y]; 't} >- 'C['x] } -->  
63     sequent ['ext] { 'H; x: mem{'y; inv_image{'s; x. 'a['x]; 't}}; 'J['x] >- 'C['x] }     sequent ['ext] { 'H; x: mem{'y; inv_image{'s; x. 'a['x]; 't}}; 'J['x] >- 'C['x] }

Legend:
Removed from v.3566  
changed lines
  Added in v.3567

  ViewVC Help
Powered by ViewVC 1.1.26