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"; 