src/HOL/Quot/HQUOT.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 6162 484adda70b65
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     1 (*  Title:      HOL/Quot/HQUOT.ML
     2     ID:         $Id$
     3     Author:     Oscar Slotosch
     4     Copyright   1997 Technische Universitaet Muenchen
     5 
     6 *)
     7 
     8 (* first prove some helpful lemmas *)
     9 Goalw [quot_def] "{y. y===x}:quot";
    10 by (Asm_simp_tac 1);
    11 by (blast_tac (claset() addIs [per_sym]) 1);
    12 qed "per_class_rep_quot";
    13 
    14 Goal "Rep_quot a = Rep_quot b ==> a=b";
    15 by (rtac (Rep_quot_inverse RS subst) 1);
    16 by (res_inst_tac [("t","a")] (Rep_quot_inverse RS subst) 1);
    17 by (Asm_simp_tac 1);
    18 qed "quot_eq";
    19 
    20 (* prepare induction and exhaustiveness *)
    21 Goal "!s. s:quot --> P (Abs_quot s) ==> P x";
    22 by (rtac (Abs_quot_inverse RS subst) 1);
    23 by (rtac Rep_quot 1);
    24 by (dres_inst_tac [("x","Rep_quot x")] spec 1);
    25 by (asm_full_simp_tac (HOL_ss addsimps [Rep_quot,Rep_quot_inverse]) 1);
    26 qed "all_q";
    27 
    28 Goal "? s. s:quot & x=Abs_quot s";
    29 by (res_inst_tac [("x","Rep_quot x")] exI 1);
    30 by (asm_full_simp_tac (HOL_ss addsimps [Rep_quot,Rep_quot_inverse]) 1);
    31 qed "exh_q";
    32 
    33 (* some lemmas for the equivalence classes *)
    34 
    35 (* equality and symmetry for equivalence classes *)
    36 Goalw [peclass_def] "x===y==><[x]>=<[y]>";
    37 by (res_inst_tac [("f","Abs_quot")] arg_cong 1);
    38 by (rtac Collect_cong 1);
    39 by (rtac iffI 1);
    40 by (etac per_trans 1);by (assume_tac 1);
    41 by (etac per_trans 1);
    42 by (etac per_sym 1);
    43 qed "per_class_eqI";
    44 
    45 Goalw [peclass_def] "<[(x::'a::er)]>=<[y]>==>x===y";
    46 by (dres_inst_tac [("f","Rep_quot")] arg_cong 1);
    47 by (asm_full_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
    48 by (dres_inst_tac [("c","x")] equalityCE 1);by (assume_tac 3);
    49 by Safe_tac;
    50 by (blast_tac (claset() addIs [er_refl]) 1);
    51 qed "er_class_eqE";
    52 
    53 Goalw [peclass_def] "[|x:D;<[x]>=<[y]>|]==>x===y";
    54 by (dtac DomainD 1);
    55 by (dres_inst_tac [("f","Rep_quot")] arg_cong 1);
    56 by (asm_full_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
    57 by (dres_inst_tac [("c","x")] equalityCE 1);by (assume_tac 3);
    58 by Auto_tac;
    59 qed "per_class_eqE";
    60 
    61 Goal "<[(x::'a::er)]>=<[y]>=x===y";
    62 by (rtac iffI 1);
    63 by (etac er_class_eqE 1);
    64 by (etac per_class_eqI 1);
    65 qed "er_class_eq";
    66 
    67 Goal "x:D==><[x]>=<[y]>=x===y";
    68 by (rtac iffI 1);
    69 by (etac per_class_eqE 1);by (assume_tac 1);
    70 by (etac per_class_eqI 1);
    71 qed "per_class_eq";
    72 
    73 (* inequality *)
    74 Goal "[|x:D;~x===y|]==><[x]>~=<[y]>";
    75 by (rtac notI 1);
    76 by (dtac per_class_eqE 1);
    77 by Auto_tac;
    78 qed "per_class_neqI";
    79 
    80 Goal "~(x::'a::er)===y==><[x]>~=<[y]>";
    81 by (rtac notI 1);
    82 by (dtac er_class_eqE 1);
    83 by Auto_tac;
    84 qed "er_class_neqI";
    85 
    86 Goal "<[x]>~=<[y]>==>~x===y";
    87 by (rtac notI 1);
    88 by (etac notE 1);
    89 by (etac per_class_eqI 1);
    90 qed "per_class_neqE";
    91 
    92 Goal "x:D==><[x]>~=<[y]>=(~x===y)";
    93 by (rtac iffI 1);
    94 by (etac per_class_neqE 1);
    95 by (etac per_class_neqI 1);by (assume_tac 1);
    96 qed "per_class_not";
    97 
    98 Goal "<[(x::'a::er)]>~=<[y]>=(~x===y)";
    99 by (rtac iffI 1);
   100 by (etac per_class_neqE 1);
   101 by (etac er_class_neqI 1);
   102 qed "er_class_not";
   103 
   104 (* exhaustiveness and induction *)
   105 Goalw [peclass_def] "? s. x=<[s]>";
   106 by (rtac all_q 1);
   107 by (strip_tac 1);
   108 by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1);
   109 by (etac exE 1);
   110 by (res_inst_tac [("x","r")] exI 1);
   111 by (rtac quot_eq 1);
   112 by (subgoal_tac "s:quot" 1);
   113 by (asm_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
   114 by (rtac set_ext 1);
   115 by (Blast_tac 1);
   116 by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1);
   117 by (Blast_tac 1);
   118 qed "per_class_exh";
   119 
   120 Goal "!x. P<[x]> ==> P s";
   121 by (cut_facts_tac [read_instantiate[("x","s::'a::per quot")] per_class_exh] 1);
   122 by (Blast_tac 1);
   123 qed "per_class_all";
   124 
   125 (* theorems for any_in *)
   126 Goalw [any_in_def,peclass_def] "any_in<[(s::'a::er)]>===s";
   127 by (rtac selectI2 1);
   128 by (rtac refl 1);
   129 by (fold_goals_tac [peclass_def]);
   130 by (etac er_class_eqE 1);
   131 qed "er_any_in_class";
   132 
   133 Goalw [any_in_def,peclass_def] "s:D==>any_in<[s]>===s";
   134 by (rtac selectI2 1);
   135 by (rtac refl 1);
   136 by (fold_goals_tac [peclass_def]);
   137 by (rtac per_sym 1);
   138 by (etac per_class_eqE 1);
   139 by (etac sym 1);
   140 qed "per_any_in_class";
   141 
   142 Goal "<[any_in (s::'a::er quot)]> = s";
   143 by (rtac per_class_all 1);
   144 by (rtac allI 1);
   145 by (rtac (er_any_in_class RS per_class_eqI) 1);
   146 qed "er_class_any_in";
   147 
   148 (* equivalent theorem for per would need !x.x:D *)
   149 Goal "!x::'a::per. x:D==><[any_in (q::'a::per quot)]> = q";
   150 by (rtac per_class_all 1);
   151 by (rtac allI 1);
   152 by (rtac (per_any_in_class RS per_class_eqI) 1);
   153 by (etac spec 1);
   154 qed "per_class_any_in";
   155 
   156 (* is like theorem for class er *)