src/HOLCF/IOA/meta_theory/Simulations.ML
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 10798 0a1446ff6aff
child 12218 6597093b77e7
permissions -rw-r--r--
` -> $
     1 (*  Title:      HOLCF/IOA/meta_theory/Simulations.ML
     2     ID:         $Id$
     3     Author:     Olaf Mueller
     4     Copyright   1997  TU Muenchen
     5 
     6 Simulations in HOLCF/IOA
     7 *)
     8 
     9 
    10 
    11 Goal "(A~={}) = (? x. x:A)";
    12 by (safe_tac set_cs);
    13 by Auto_tac;
    14 qed"set_non_empty";
    15 
    16 Goal "(A Int B ~= {}) = (? x. x: A & x:B)";
    17 by (simp_tac (simpset() addsimps [set_non_empty]) 1);
    18 qed"Int_non_empty";
    19 
    20 
    21 Goalw [Image_def]
    22 "(R``{x} Int S ~= {}) = (? y. (x,y):R & y:S)";
    23 by (simp_tac (simpset() addsimps [Int_non_empty]) 1);
    24 qed"Sim_start_convert";
    25 
    26 Addsimps [Sim_start_convert];
    27 
    28 
    29 Goalw [is_ref_map_def,is_simulation_def]
    30 "!! f. is_ref_map f C A ==> is_simulation {p. (snd p) = f (fst p)} C A";
    31 (* start states *)
    32 by (Asm_full_simp_tac 1);
    33 (* main case *)
    34 by (Blast_tac 1);
    35 qed"ref_map_is_simulation";
    36 
    37 
    38 
    39