src/HOL/MiniML/Generalize.ML
author wenzelm
Thu Jan 23 14:19:16 1997 +0100 (1997-01-23)
changeset 2545 d10abc8c11fb
parent 2525 477c05586286
child 3018 e65b60b28341
permissions -rw-r--r--
added AxClasses test;
nipkow@2525
     1
(* Title:     HOL/MiniML/Generalize.ML
nipkow@2525
     2
   ID:        $Id$
nipkow@2525
     3
   Author:    Wolfgang Naraschewski and Tobias Nipkow
nipkow@2525
     4
   Copyright  1996 TU Muenchen
nipkow@2525
     5
*)
nipkow@2525
     6
nipkow@2525
     7
AddSEs [equalityE];
nipkow@2525
     8
nipkow@2525
     9
goal thy "!!A B. free_tv A = free_tv B ==> gen A t = gen B t";
nipkow@2525
    10
by (typ.induct_tac "t" 1);
nipkow@2525
    11
by (ALLGOALS Asm_simp_tac);
nipkow@2525
    12
qed "gen_eq_on_free_tv";
nipkow@2525
    13
nipkow@2525
    14
goal thy "!!t.(free_tv t) <= (free_tv sch) --> gen sch t = (mk_scheme t)";
nipkow@2525
    15
by (typ.induct_tac "t" 1);
nipkow@2525
    16
by (Asm_simp_tac 1);
nipkow@2525
    17
by (Simp_tac 1);
nipkow@2525
    18
by (Fast_tac 1);
nipkow@2525
    19
qed_spec_mp "gen_without_effect";
nipkow@2525
    20
nipkow@2525
    21
Addsimps [gen_without_effect];
nipkow@2525
    22
nipkow@2525
    23
goal thy "!!A. free_tv (gen ($ S A) t) = free_tv t Int free_tv ($ S A)";
nipkow@2525
    24
by (typ.induct_tac "t" 1);
nipkow@2525
    25
by (Simp_tac 1);
nipkow@2525
    26
by (case_tac "nat : free_tv ($ S A)" 1);
nipkow@2525
    27
by (Asm_simp_tac 1);
nipkow@2525
    28
by (Fast_tac 1);
nipkow@2525
    29
by (Asm_simp_tac 1);
nipkow@2525
    30
by (Fast_tac 1);
nipkow@2525
    31
by (Asm_full_simp_tac 1);
nipkow@2525
    32
by (Fast_tac 1);
nipkow@2525
    33
qed "free_tv_gen";
nipkow@2525
    34
nipkow@2525
    35
Addsimps [free_tv_gen];
nipkow@2525
    36
nipkow@2525
    37
goal thy "!!A. free_tv (gen ($ S A) t # $ S A) = free_tv ($ S A)";
nipkow@2525
    38
by (Simp_tac 1);
nipkow@2525
    39
by (Fast_tac 1);
nipkow@2525
    40
qed "free_tv_gen_cons";
nipkow@2525
    41
nipkow@2525
    42
Addsimps [free_tv_gen_cons];
nipkow@2525
    43
nipkow@2525
    44
goal thy "!!A. bound_tv (gen A t1) = (free_tv t1) - (free_tv A)";
nipkow@2525
    45
by (typ.induct_tac "t1" 1);
nipkow@2525
    46
by (Simp_tac 1);
nipkow@2525
    47
by (case_tac "nat : free_tv A" 1);
nipkow@2525
    48
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
nipkow@2525
    49
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
nipkow@2525
    50
by (Fast_tac 1);
nipkow@2525
    51
by (Asm_simp_tac 1);
nipkow@2525
    52
by (Fast_tac 1);
nipkow@2525
    53
qed "bound_tv_gen";
nipkow@2525
    54
nipkow@2525
    55
Addsimps [bound_tv_gen];
nipkow@2525
    56
nipkow@2525
    57
goal thy "!!A. new_tv n t --> new_tv n (gen A t)";
nipkow@2525
    58
by (typ.induct_tac "t" 1);
nipkow@2525
    59
by (Simp_tac 1);
nipkow@2525
    60
by (case_tac "nat : free_tv A" 1);
nipkow@2525
    61
by (Asm_simp_tac 1);
nipkow@2525
    62
by (Asm_simp_tac 1);
nipkow@2525
    63
by (Asm_full_simp_tac 1);
nipkow@2525
    64
qed_spec_mp "new_tv_compatible_gen";
nipkow@2525
    65
nipkow@2525
    66
goalw thy [gen_ML_def] "!!A. gen A t = gen_ML A t";
nipkow@2525
    67
by (typ.induct_tac "t" 1);
nipkow@2525
    68
by (simp_tac (!simpset addsimps [free_tv_ML_scheme_list]) 1);
nipkow@2525
    69
by (asm_simp_tac (!simpset addsimps [free_tv_ML_scheme_list]) 1);
nipkow@2525
    70
qed "gen_eq_gen_ML";
nipkow@2525
    71
nipkow@2525
    72
goal thy "!!S. (free_tv S) Int ((free_tv t) - (free_tv A)) = {} \
nipkow@2525
    73
\          --> gen ($ S A) ($ S t) = $ S (gen A t)";
nipkow@2525
    74
by (typ.induct_tac "t" 1);
nipkow@2525
    75
by (strip_tac 1);
nipkow@2525
    76
by (case_tac "nat:(free_tv A)" 1);
nipkow@2525
    77
by (Asm_simp_tac 1);
nipkow@2525
    78
by (Asm_full_simp_tac 1);
nipkow@2525
    79
by (subgoal_tac "nat ~: free_tv S" 1);
nipkow@2525
    80
by (Fast_tac 2);
nipkow@2525
    81
by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,de_Morgan_disj]) 1);
nipkow@2525
    82
by (split_tac [expand_if] 1);
nipkow@2525
    83
by (cut_facts_tac [free_tv_app_subst_scheme_list] 1);
nipkow@2525
    84
by (Fast_tac 1);
nipkow@2525
    85
by (Asm_simp_tac 1);
nipkow@2525
    86
by (Best_tac 1);
nipkow@2525
    87
qed_spec_mp "gen_subst_commutes";
nipkow@2525
    88
nipkow@2525
    89
goal Generalize.thy "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t";
nipkow@2525
    90
by(typ.induct_tac "t" 1);
nipkow@2525
    91
by(ALLGOALS Asm_simp_tac);
nipkow@2525
    92
by(Fast_tac 1);
nipkow@2525
    93
qed_spec_mp "bound_typ_inst_gen";
nipkow@2525
    94
Addsimps [bound_typ_inst_gen];
nipkow@2525
    95
nipkow@2525
    96
goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
nipkow@2525
    97
  "gen ($ S A) ($ S t) <= $ S (gen A t)";
nipkow@2525
    98
by(safe_tac (!claset));
nipkow@2525
    99
by(rename_tac "R" 1);
nipkow@2525
   100
by(res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
nipkow@2525
   101
by(typ.induct_tac "t" 1);
nipkow@2525
   102
 by(simp_tac (!simpset setloop (split_tac[expand_if])) 1);
nipkow@2525
   103
by(Asm_simp_tac 1);
nipkow@2525
   104
qed "gen_bound_typ_instance";
nipkow@2525
   105
nipkow@2525
   106
goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
nipkow@2525
   107
  "!!A B. free_tv B <= free_tv A ==> gen A t <= gen B t";
nipkow@2525
   108
by(safe_tac (!claset));
nipkow@2525
   109
by(rename_tac "S" 1);
nipkow@2525
   110
by(res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
nipkow@2525
   111
by (typ.induct_tac "t" 1);
nipkow@2525
   112
 by(asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
nipkow@2525
   113
 by(Fast_tac 1);
nipkow@2525
   114
by(Asm_simp_tac 1);
nipkow@2525
   115
qed "free_tv_subset_gen_le";
nipkow@2525
   116
nipkow@2525
   117
goalw thy [le_type_scheme_def,is_bound_typ_instance] 
nipkow@2525
   118
      "!!A. new_tv n A --> gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)";
nipkow@2525
   119
by (strip_tac 1);
nipkow@2525
   120
by (etac exE 1);
nipkow@2525
   121
by (hyp_subst_tac 1);
nipkow@2525
   122
by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1);
nipkow@2525
   123
by (typ.induct_tac "t" 1);
nipkow@2525
   124
by (Simp_tac 1);
nipkow@2525
   125
by (case_tac "nat : free_tv A" 1);
nipkow@2525
   126
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
nipkow@2525
   127
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
nipkow@2525
   128
by (subgoal_tac "n <= n + nat" 1);
nipkow@2525
   129
by (forw_inst_tac [("t","A")] new_tv_le 1);
nipkow@2525
   130
ba 1;
nipkow@2525
   131
by (dtac new_tv_not_free_tv 1);
nipkow@2525
   132
by (dtac new_tv_not_free_tv 1);
nipkow@2525
   133
by (asm_simp_tac (!simpset addsimps [diff_add_inverse]) 1);
nipkow@2525
   134
by (simp_tac (!simpset addsimps [le_add1]) 1);
nipkow@2525
   135
by (Asm_simp_tac 1);
nipkow@2525
   136
qed_spec_mp "gen_t_le_gen_alpha_t";
nipkow@2525
   137
nipkow@2525
   138
Addsimps [gen_t_le_gen_alpha_t];