src/HOL/Quot/PER0.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 5858 beddc19c107a
permissions -rw-r--r--
tidied; added lemma restrict_to_left
slotosch@2904
     1
(*  Title:      HOL/Quot/PER0.ML
slotosch@2904
     2
    ID:         $Id$
slotosch@2904
     3
    Author:     Oscar Slotosch
slotosch@2904
     4
    Copyright   1997 Technische Universitaet Muenchen
slotosch@2904
     5
slotosch@2904
     6
*)
slotosch@2904
     7
open PER0;
slotosch@2904
     8
slotosch@2904
     9
(* derive the characteristic axioms *)
paulson@5858
    10
Goalw [per_def] "x === y ==> y === x";
paulson@3457
    11
by (etac ax_per_sym 1);
slotosch@2904
    12
qed "per_sym";
slotosch@2904
    13
paulson@5858
    14
Goalw [per_def] "[| x === y; y === z |] ==> x === z";
paulson@3457
    15
by (etac ax_per_trans 1);
paulson@3457
    16
by (assume_tac 1);
slotosch@2904
    17
qed "per_trans";
slotosch@2904
    18
wenzelm@5069
    19
Goalw [per_def] "(x::'a::er) === x";
paulson@3457
    20
by (rtac ax_er_refl 1);
slotosch@2904
    21
qed "er_refl";
slotosch@2904
    22
slotosch@2904
    23
(* now everything works without axclasses *)
slotosch@2904
    24
wenzelm@5069
    25
Goal "x===y=y===x";
paulson@3457
    26
by (rtac iffI 1);
paulson@3457
    27
by (etac per_sym 1);
paulson@3457
    28
by (etac per_sym 1);
slotosch@2904
    29
qed "per_sym2";
slotosch@2904
    30
paulson@5858
    31
Goal "x===y ==> x===x";
paulson@3457
    32
by (rtac per_trans 1);by (assume_tac 1);
paulson@3457
    33
by (etac per_sym 1);
slotosch@2904
    34
qed "sym2refl1";
slotosch@2904
    35
paulson@5858
    36
Goal "x===y ==> y===y";
paulson@3457
    37
by (rtac per_trans 1);by (assume_tac 2);
paulson@3457
    38
by (etac per_sym 1);
slotosch@2904
    39
qed "sym2refl2";
slotosch@2904
    40
paulson@5858
    41
Goalw [Dom] "x:D ==> x === x";
paulson@5858
    42
by (Blast_tac 1);
slotosch@2904
    43
qed "DomainD";
slotosch@2904
    44
paulson@5858
    45
Goalw [Dom] "x === x ==> x:D";
paulson@5858
    46
by (Blast_tac 1);
slotosch@2904
    47
qed "DomainI";
slotosch@2904
    48
wenzelm@5069
    49
Goal "x:D = x===x";
paulson@3457
    50
by (rtac iffI 1);
paulson@3457
    51
by (etac DomainD 1);
paulson@3457
    52
by (etac DomainI 1);
slotosch@2904
    53
qed "DomainEq";
slotosch@2904
    54
wenzelm@5069
    55
Goal "(~ x === y) = (~ y === x)";
paulson@3457
    56
by (rtac (per_sym2 RS arg_cong) 1);
slotosch@2904
    57
qed "per_not_sym";
slotosch@2904
    58
slotosch@2904
    59
(* show that PER work only on D *)
paulson@5858
    60
Goal "x===y ==> x:D";
paulson@3457
    61
by (etac (sym2refl1 RS DomainI) 1);
slotosch@2904
    62
qed "DomainI_left"; 
slotosch@2904
    63
paulson@5858
    64
Goal "x===y ==> y:D";
paulson@3457
    65
by (etac (sym2refl2 RS DomainI) 1);
slotosch@2904
    66
qed "DomainI_right"; 
slotosch@2904
    67
paulson@5858
    68
Goalw [Dom] "x~:D ==> ~x===y";
paulson@5858
    69
by (res_inst_tac [("Q","x===y")] (excluded_middle RS disjE) 1);
paulson@5858
    70
by (assume_tac 1);
paulson@3457
    71
by (dtac sym2refl1 1);
paulson@5858
    72
by (Blast_tac 1);
slotosch@2904
    73
qed "notDomainE1"; 
slotosch@2904
    74
paulson@5858
    75
Goalw [Dom] "x~:D ==> ~y===x";
paulson@5858
    76
by (res_inst_tac [("Q","y===x")] (excluded_middle RS disjE) 1);
paulson@5858
    77
by (assume_tac 1);
paulson@3457
    78
by (dtac sym2refl2 1);
paulson@5858
    79
by (Blast_tac 1);
slotosch@2904
    80
qed "notDomainE2"; 
slotosch@2904
    81
slotosch@2904
    82
(* theorems for equivalence relations *)
wenzelm@5069
    83
Goal "(x::'a::er) : D";
paulson@3457
    84
by (rtac DomainI 1);
paulson@3457
    85
by (rtac er_refl 1);
slotosch@2904
    86
qed "er_Domain";
slotosch@2904
    87
slotosch@2904
    88
(* witnesses for "=>" ::(per,per)per  *)
paulson@5858
    89
Goalw [fun_per_def]"eqv (x::'a::per => 'b::per) y ==> eqv y x";
paulson@5858
    90
by (auto_tac (claset(), simpset() addsimps [per_sym2]));
slotosch@2904
    91
qed "per_sym_fun";
slotosch@2904
    92
paulson@5858
    93
Goalw [fun_per_def] "[| eqv (f::'a::per=>'b::per) g;eqv g h|] ==> eqv f h";
paulson@5858
    94
by Safe_tac;
slotosch@2904
    95
by (REPEAT (dtac spec 1));
slotosch@2904
    96
by (res_inst_tac [("y","g y")] per_trans 1);
paulson@3457
    97
by (rtac mp 1);by (assume_tac 1);
slotosch@2904
    98
by (Asm_simp_tac 1);
paulson@3457
    99
by (rtac mp 1);by (assume_tac 1);
wenzelm@4089
   100
by (asm_simp_tac (simpset() addsimps [sym2refl2]) 1);
slotosch@2904
   101
qed "per_trans_fun";
slotosch@2904
   102
slotosch@2904
   103