new preficates refl, sym [from Integ/Equiv], antisym
authorpaulson
Thu Jun 10 10:35:58 1999 +0200 (1999-06-10)
changeset 680643c081a0858d
parent 6805 52b13dfbe954
child 6807 6737af18317e
new preficates refl, sym [from Integ/Equiv], antisym
src/HOL/Relation.ML
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.ML	Thu Jun 10 10:34:55 1999 +0200
     1.2 +++ b/src/HOL/Relation.ML	Thu Jun 10 10:35:58 1999 +0200
     1.3 @@ -25,6 +25,19 @@
     1.4  qed "pair_in_Id_conv";
     1.5  Addsimps [pair_in_Id_conv];
     1.6  
     1.7 +Goalw [refl_def] "reflexive Id";
     1.8 +by Auto_tac;
     1.9 +qed "reflexive_Id";
    1.10 +
    1.11 +(*A strange result, since Id is also symmetric.*)
    1.12 +Goalw [antisym_def] "antisym Id";
    1.13 +by Auto_tac;
    1.14 +qed "antisym_Id";
    1.15 +
    1.16 +Goalw [trans_def] "trans Id";
    1.17 +by Auto_tac;
    1.18 +qed "trans_Id";
    1.19 +
    1.20  
    1.21  (** Diagonal relation: indentity restricted to some set **)
    1.22  
    1.23 @@ -108,6 +121,28 @@
    1.24  by (Blast_tac 1);
    1.25  qed "comp_subset_Sigma";
    1.26  
    1.27 +(** Natural deduction for refl(r) **)
    1.28 +
    1.29 +val prems = Goalw [refl_def]
    1.30 +    "[| r <= A Times A;  !! x. x:A ==> (x,x):r |] ==> refl A r";
    1.31 +by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
    1.32 +qed "reflI";
    1.33 +
    1.34 +Goalw [refl_def] "[| refl A r; a:A |] ==> (a,a):r";
    1.35 +by (Blast_tac 1);
    1.36 +qed "reflD";
    1.37 +
    1.38 +(** Natural deduction for antisym(r) **)
    1.39 +
    1.40 +val prems = Goalw [antisym_def]
    1.41 +    "(!! x y. [| (x,y):r;  (y,x):r |] ==> x=y) ==> antisym(r)";
    1.42 +by (REPEAT (ares_tac (prems@[allI,impI]) 1));
    1.43 +qed "antisymI";
    1.44 +
    1.45 +Goalw [antisym_def] "[| antisym(r);  (a,b):r;  (b,a):r |] ==> a=b";
    1.46 +by (Blast_tac 1);
    1.47 +qed "antisymD";
    1.48 +
    1.49  (** Natural deduction for trans(r) **)
    1.50  
    1.51  val prems = Goalw [trans_def]
     2.1 --- a/src/HOL/Relation.thy	Thu Jun 10 10:34:55 1999 +0200
     2.2 +++ b/src/HOL/Relation.thy	Thu Jun 10 10:35:58 1999 +0200
     2.3 @@ -17,22 +17,37 @@
     2.4    Image_def     "r ^^ s == {y. ? x:s. (x,y):r}"
     2.5    
     2.6  constdefs
     2.7 -  Id          :: "('a * 'a)set"               (*the identity relation*)
     2.8 +  Id     :: "('a * 'a)set"                 (*the identity relation*)
     2.9        "Id == {p. ? x. p = (x,x)}"
    2.10  
    2.11    diag   :: "'a set => ('a * 'a)set"
    2.12      "diag(A) == UN x:A. {(x,x)}"
    2.13    
    2.14 -  Domain      :: "('a*'b) set => 'a set"
    2.15 +  Domain :: "('a*'b) set => 'a set"
    2.16      "Domain(r) == {x. ? y. (x,y):r}"
    2.17  
    2.18 -  Range       :: "('a*'b) set => 'b set"
    2.19 +  Range  :: "('a*'b) set => 'b set"
    2.20      "Range(r) == Domain(r^-1)"
    2.21  
    2.22 -  trans       :: "('a * 'a)set => bool"       (*transitivity predicate*)
    2.23 +  refl   :: "['a set, ('a*'a) set] => bool" (*reflexivity over a set*)
    2.24 +    "refl A r == r <= A Times A & (ALL x: A. (x,x) : r)"
    2.25 +
    2.26 +  sym    :: "('a*'a) set=>bool"             (*symmetry predicate*)
    2.27 +    "sym(r) == ALL x y. (x,y): r --> (y,x): r"
    2.28 +
    2.29 +  antisym:: "('a * 'a)set => bool"          (*antisymmetry predicate*)
    2.30 +    "antisym(r) == ALL x y. (x,y):r --> (y,x):r --> x=y"
    2.31 +
    2.32 +  trans  :: "('a * 'a)set => bool"          (*transitivity predicate*)
    2.33      "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
    2.34  
    2.35 -  Univalent   :: "('a * 'b)set => bool"
    2.36 +  Univalent :: "('a * 'b)set => bool"
    2.37      "Univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
    2.38  
    2.39 +syntax
    2.40 +  reflexive :: "('a * 'a)set => bool"       (*reflexivity over a type*)
    2.41 +
    2.42 +translations
    2.43 +  "reflexive" == "refl UNIV"
    2.44 +
    2.45  end