src/HOL/MiniML/Generalize.ML
author berghofe
Fri, 24 Jul 1998 13:19:38 +0200
changeset 5184 9b8547a9496a
parent 5118 6b995dad8a9d
child 5522 982c710450c6
permissions -rw-r--r--
Adapted to new datatype package.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     1
(* Title:     HOL/MiniML/Generalize.ML
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     2
   ID:        $Id$
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     3
   Author:    Wolfgang Naraschewski and Tobias Nipkow
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     4
   Copyright  1996 TU Muenchen
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     5
*)
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     6
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     7
AddSEs [equalityE];
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
     8
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
     9
Goal "free_tv A = free_tv B ==> gen A t = gen B t";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
    10
by (induct_tac "t" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    11
by (ALLGOALS Asm_simp_tac);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    12
qed "gen_eq_on_free_tv";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    13
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
    14
Goal "(free_tv t) <= (free_tv sch) --> gen sch t = (mk_scheme t)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
    15
by (induct_tac "t" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    16
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    17
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    18
by (Fast_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    19
qed_spec_mp "gen_without_effect";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    20
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    21
Addsimps [gen_without_effect];
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    22
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
    23
Goal "free_tv (gen ($ S A) t) = free_tv t Int free_tv ($ S A)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
    24
by (induct_tac "t" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    25
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    26
by (case_tac "nat : free_tv ($ S A)" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    27
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    28
by (Fast_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    29
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    30
by (Fast_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    31
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    32
by (Fast_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    33
qed "free_tv_gen";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    34
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    35
Addsimps [free_tv_gen];
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    36
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
    37
Goal "free_tv (gen ($ S A) t # $ S A) = free_tv ($ S A)";
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    38
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    39
by (Fast_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    40
qed "free_tv_gen_cons";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    41
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    42
Addsimps [free_tv_gen_cons];
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    43
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
    44
Goal "bound_tv (gen A t1) = (free_tv t1) - (free_tv A)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
    45
by (induct_tac "t1" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    46
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    47
by (case_tac "nat : free_tv A" 1);
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4681
diff changeset
    48
by (Asm_simp_tac 1);
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4681
diff changeset
    49
by (Asm_simp_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    50
by (Fast_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    51
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    52
by (Fast_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    53
qed "bound_tv_gen";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    54
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    55
Addsimps [bound_tv_gen];
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    56
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
    57
Goal "new_tv n t --> new_tv n (gen A t)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
    58
by (induct_tac "t" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    59
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    60
by (case_tac "nat : free_tv A" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    61
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    62
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    63
qed_spec_mp "new_tv_compatible_gen";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    64
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
    65
Goalw [gen_ML_def] "gen A t = gen_ML A t";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
    66
by (induct_tac "t" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    67
by (simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1);
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    68
by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    69
qed "gen_eq_gen_ML";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    70
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
    71
Goal "(free_tv S) Int ((free_tv t) - (free_tv A)) = {} \
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
    72
\     --> gen ($ S A) ($ S t) = $ S (gen A t)";
4681
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4153
diff changeset
    73
by (induct_tac "t" 1);
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4153
diff changeset
    74
 by (strip_tac 1);
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4153
diff changeset
    75
 by (case_tac "nat:(free_tv A)" 1);
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4153
diff changeset
    76
  by (Asm_simp_tac 1);
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4153
diff changeset
    77
 by (Asm_full_simp_tac 1);
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4153
diff changeset
    78
 by (subgoal_tac "nat ~: free_tv S" 1);
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4153
diff changeset
    79
  by (Fast_tac 2);
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4153
diff changeset
    80
 by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def]) 1);
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4153
diff changeset
    81
 by (cut_facts_tac [free_tv_app_subst_scheme_list] 1);
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4153
diff changeset
    82
 by (Fast_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    83
by (Asm_simp_tac 1);
4681
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4153
diff changeset
    84
by (Blast_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    85
qed_spec_mp "gen_subst_commutes";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    86
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    87
Goal "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
    88
by (induct_tac "t" 1);
3018
e65b60b28341 Ran expandshort
paulson
parents: 2525
diff changeset
    89
by (ALLGOALS Asm_simp_tac);
e65b60b28341 Ran expandshort
paulson
parents: 2525
diff changeset
    90
by (Fast_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    91
qed_spec_mp "bound_typ_inst_gen";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    92
Addsimps [bound_typ_inst_gen];
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    93
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    94
Goalw [le_type_scheme_def,is_bound_typ_instance]
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
    95
  "gen ($ S A) ($ S t) <= $ S (gen A t)";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4089
diff changeset
    96
by Safe_tac;
3018
e65b60b28341 Ran expandshort
paulson
parents: 2525
diff changeset
    97
by (rename_tac "R" 1);
e65b60b28341 Ran expandshort
paulson
parents: 2525
diff changeset
    98
by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
    99
by (induct_tac "t" 1);
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4681
diff changeset
   100
 by (Simp_tac 1);
3018
e65b60b28341 Ran expandshort
paulson
parents: 2525
diff changeset
   101
by (Asm_simp_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   102
qed "gen_bound_typ_instance";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   103
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   104
Goalw [le_type_scheme_def,is_bound_typ_instance]
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   105
  "free_tv B <= free_tv A ==> gen A t <= gen B t";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4089
diff changeset
   106
by Safe_tac;
3018
e65b60b28341 Ran expandshort
paulson
parents: 2525
diff changeset
   107
by (rename_tac "S" 1);
e65b60b28341 Ran expandshort
paulson
parents: 2525
diff changeset
   108
by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   109
by (induct_tac "t" 1);
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4681
diff changeset
   110
 by (Asm_simp_tac 1);
3018
e65b60b28341 Ran expandshort
paulson
parents: 2525
diff changeset
   111
 by (Fast_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 2525
diff changeset
   112
by (Asm_simp_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   113
qed "free_tv_subset_gen_le";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   114
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   115
Goalw [le_type_scheme_def,is_bound_typ_instance] 
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   116
  "new_tv n A --> \
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   117
\  gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)";
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   118
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   119
by (etac exE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   120
by (hyp_subst_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   121
by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1);
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   122
by (induct_tac "t" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   123
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   124
by (case_tac "nat : free_tv A" 1);
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4681
diff changeset
   125
by (Asm_simp_tac 1);
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4681
diff changeset
   126
by (Asm_simp_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   127
by (subgoal_tac "n <= n + nat" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   128
by (forw_inst_tac [("t","A")] new_tv_le 1);
3018
e65b60b28341 Ran expandshort
paulson
parents: 2525
diff changeset
   129
by (assume_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   130
by (dtac new_tv_not_free_tv 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   131
by (dtac new_tv_not_free_tv 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   132
by (asm_simp_tac (simpset() addsimps [diff_add_inverse]) 1);
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   133
by (simp_tac (simpset() addsimps [le_add1]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   134
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   135
qed_spec_mp "gen_t_le_gen_alpha_t";
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   136
477c05586286 The new version of MiniML including "let".
nipkow
parents:
diff changeset
   137
Addsimps [gen_t_le_gen_alpha_t];