src/HOL/UNITY/LessThan.ML
changeset 7878 43b03d412b82
parent 7521 a18adacbdbd2
child 7915 c7fd7eb3b0ef
equal deleted inserted replaced
7877:e5e019d60f71 7878:43b03d412b82
     5 
     5 
     6 lessThan, greaterThan, atLeast, atMost
     6 lessThan, greaterThan, atLeast, atMost
     7 *)
     7 *)
     8 
     8 
     9 
     9 
       
    10 (*** Restrict [MOVE TO RELATION.THY??] ***)
       
    11 
       
    12 Goalw [Restrict_def] "((x,y): Restrict A r) = ((x,y): r & x: A)";
       
    13 by (Blast_tac 1);
       
    14 qed "Restrict_iff";
       
    15 AddIffs [Restrict_iff];
       
    16 
       
    17 Goal "Restrict UNIV = id";
       
    18 by (rtac ext 1);
       
    19 by (auto_tac (claset(), simpset() addsimps [Restrict_def]));
       
    20 qed "Restrict_UNIV";
       
    21 Addsimps [Restrict_UNIV];
       
    22 
       
    23 Goal "Restrict {} r = {}";
       
    24 by (auto_tac (claset(), simpset() addsimps [Restrict_def]));
       
    25 qed "Restrict_empty";
       
    26 Addsimps [Restrict_empty];
       
    27 
       
    28 Goalw [Restrict_def] "Restrict A (Restrict B r) = Restrict (A Int B) r";
       
    29 by (Blast_tac 1);
       
    30 qed "Restrict_Int";
       
    31 Addsimps [Restrict_Int];
       
    32 
       
    33 Goalw [Restrict_def] "Domain r <= A ==> Restrict A r = r";
       
    34 by Auto_tac;
       
    35 qed "Restrict_triv";
       
    36 
       
    37 Goalw [Restrict_def] "Restrict A r <= r";
       
    38 by Auto_tac;
       
    39 qed "Restrict_subset";
       
    40 
       
    41 Goalw [Restrict_def]
       
    42      "[| A <= B;  Restrict B r = Restrict B s |] \
       
    43 \     ==> Restrict A r = Restrict A s";
       
    44 by (blast_tac (claset() addSEs [equalityE]) 1);
       
    45 qed "Restrict_eq_mono";
       
    46 
       
    47 Goalw [Restrict_def, image_def]
       
    48      "[| s : RR;  Restrict A r = Restrict A s |] \
       
    49 \     ==> Restrict A r : Restrict A `` RR";
       
    50 by Auto_tac;
       
    51 qed "Restrict_imageI";
       
    52 
       
    53 Goal "(Restrict A `` (Restrict A `` r - s)) = (Restrict A `` r - s)";
       
    54 by Auto_tac;
       
    55 by (rewrite_goals_tac [image_def, Restrict_def]);
       
    56 by (Blast_tac 1);
       
    57 qed "Restrict_image_Diff";
       
    58 
       
    59 (*Nothing to do with Restrict, but to specialized for Fun.ML?*)
       
    60 Goal "f``(g``A - B) = (UN x: (A - g-`` B). {f(g(x))})";
       
    61 by (Blast_tac 1);
       
    62 qed "image_Diff_image_eq";
       
    63 
       
    64 
    10 (*** lessThan ***)
    65 (*** lessThan ***)
    11 
    66 
    12 Goalw [lessThan_def] "(i: lessThan k) = (i<k)";
    67 Goalw [lessThan_def] "(i: lessThan k) = (i<k)";
    13 by (Blast_tac 1);
    68 by (Blast_tac 1);
    14 qed "lessThan_iff";
    69 qed "lessThan_iff";