src/HOL/MiniML/Type.ML
author berghofe
Fri, 24 Jul 1998 13:19:38 +0200
changeset 5184 9b8547a9496a
parent 5118 6b995dad8a9d
child 5446 506259e4e546
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: 2513
diff changeset
     1
(* Title:     HOL/MiniML/Type.thy
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
     2
   ID:        $Id$
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
     3
   Author:    Wolfgang Naraschewski and Tobias Nipkow
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
     4
   Copyright  1996 TU Muenchen
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
     5
*)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     6
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     7
Addsimps [mgu_eq,mgu_mg,mgu_free];
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     8
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
     9
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    10
(* lemmata for make scheme *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    11
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    12
Goal "mk_scheme t = sch1 =-> sch2 --> (? t1 t2. sch1 = mk_scheme t1 & sch2 = mk_scheme t2)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
    13
by (induct_tac "t" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    14
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    15
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    16
by (Fast_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    17
qed_spec_mp "mk_scheme_Fun";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    18
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    19
Goal "!t'. mk_scheme t = mk_scheme t' --> t=t'";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
    20
by (induct_tac "t" 1);
3018
e65b60b28341 Ran expandshort
paulson
parents: 3008
diff changeset
    21
 by (rtac allI 1);
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
    22
 by (induct_tac "t'" 1);
3018
e65b60b28341 Ran expandshort
paulson
parents: 3008
diff changeset
    23
  by (Simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 3008
diff changeset
    24
 by (Asm_full_simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 3008
diff changeset
    25
by (rtac allI 1);
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
    26
by (induct_tac "t'" 1);
3018
e65b60b28341 Ran expandshort
paulson
parents: 3008
diff changeset
    27
 by (Simp_tac 1);
e65b60b28341 Ran expandshort
paulson
parents: 3008
diff changeset
    28
by (Asm_full_simp_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    29
qed_spec_mp "mk_scheme_injective";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    30
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
    31
Goal "free_tv (mk_scheme t) = free_tv t";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
    32
by (induct_tac "t" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    33
by (ALLGOALS Asm_simp_tac);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    34
qed "free_tv_mk_scheme";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    35
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    36
Addsimps [free_tv_mk_scheme];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    37
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
    38
Goal "$ S (mk_scheme t) = mk_scheme ($ S t)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
    39
by (induct_tac "t" 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    40
by (ALLGOALS Asm_simp_tac);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    41
qed "subst_mk_scheme";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    42
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    43
Addsimps [subst_mk_scheme];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    44
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    45
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    46
(* constructor laws for app_subst *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    47
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    48
Goalw [app_subst_list]
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    49
  "$ S [] = []";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    50
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    51
qed "app_subst_Nil";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    52
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    53
Goalw [app_subst_list]
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    54
  "$ S (x#l) = ($ S x)#($ S l)";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    55
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    56
qed "app_subst_Cons";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    57
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    58
Addsimps [app_subst_Nil,app_subst_Cons];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    59
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    60
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    61
(* constructor laws for new_tv *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    62
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    63
Goalw [new_tv_def]
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    64
  "new_tv n (TVar m) = (m<n)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    65
by (fast_tac (HOL_cs addss simpset()) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    66
qed "new_tv_TVar";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    67
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    68
Goalw [new_tv_def]
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    69
  "new_tv n (FVar m) = (m<n)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    70
by (fast_tac (HOL_cs addss simpset()) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    71
qed "new_tv_FVar";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    72
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    73
Goalw [new_tv_def]
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    74
  "new_tv n (BVar m) = True";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    75
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    76
qed "new_tv_BVar";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    77
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    78
Goalw [new_tv_def]
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    79
  "new_tv n (t1 -> t2) = (new_tv n t1 & new_tv n t2)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    80
by (fast_tac (HOL_cs addss simpset()) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    81
qed "new_tv_Fun";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    82
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    83
Goalw [new_tv_def]
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    84
  "new_tv n (t1 =-> t2) = (new_tv n t1 & new_tv n t2)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    85
by (fast_tac (HOL_cs addss simpset()) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    86
qed "new_tv_Fun2";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    87
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    88
Goalw [new_tv_def]
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    89
  "new_tv n []";
2031
03a843f0f447 Ran expandshort
paulson
parents: 1901
diff changeset
    90
by (Simp_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    91
qed "new_tv_Nil";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    92
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    93
Goalw [new_tv_def]
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    94
  "new_tv n (x#l) = (new_tv n x & new_tv n l)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    95
by (fast_tac (HOL_cs addss simpset()) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    96
qed "new_tv_Cons";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    97
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
    98
Goalw [new_tv_def] "new_tv n TVar";
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
    99
by (strip_tac 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   100
by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def,cod_def]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   101
qed "new_tv_TVar_subst";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   102
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   103
Addsimps [new_tv_TVar,new_tv_FVar,new_tv_BVar,new_tv_Fun,new_tv_Fun2,new_tv_Nil,new_tv_Cons,new_tv_TVar_subst];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   104
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   105
Goalw [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def]
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   106
  "new_tv n id_subst";
3018
e65b60b28341 Ran expandshort
paulson
parents: 3008
diff changeset
   107
by (Simp_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   108
qed "new_tv_id_subst";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   109
Addsimps[new_tv_id_subst];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   110
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   111
Goal "new_tv n (sch::type_scheme) --> \
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   112
\     $(%k. if k<n then S k else S' k) sch = $S sch";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   113
by (induct_tac "sch" 1);
3018
e65b60b28341 Ran expandshort
paulson
parents: 3008
diff changeset
   114
by (ALLGOALS Asm_simp_tac);
2625
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
   115
qed "new_if_subst_type_scheme";
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
   116
Addsimps [new_if_subst_type_scheme];
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
   117
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   118
Goal "new_tv n (A::type_scheme list) --> \
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   119
\     $(%k. if k<n then S k else S' k) A = $S A";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   120
by (induct_tac "A" 1);
3018
e65b60b28341 Ran expandshort
paulson
parents: 3008
diff changeset
   121
by (ALLGOALS Asm_simp_tac);
2625
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
   122
qed "new_if_subst_type_scheme_list";
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
   123
Addsimps [new_if_subst_type_scheme_list];
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
   124
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   125
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   126
(* constructor laws for dom and cod *)
1751
946efd210837 Added thm I_complete_wrt_W to I.
nipkow
parents: 1619
diff changeset
   127
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   128
Goalw [dom_def,id_subst_def,empty_def]
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   129
  "dom id_subst = {}";
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   130
by (Simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   131
qed "dom_id_subst";
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   132
Addsimps [dom_id_subst];
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   133
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   134
Goalw [cod_def]
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   135
  "cod id_subst = {}";
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   136
by (Simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   137
qed "cod_id_subst";
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   138
Addsimps [cod_id_subst];
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   139
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   140
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   141
(* lemmata for free_tv *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   142
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   143
Goalw [free_tv_subst]
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   144
  "free_tv id_subst = {}";
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   145
by (Simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   146
qed "free_tv_id_subst";
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   147
Addsimps [free_tv_id_subst];
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   148
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   149
Goal "!n. n < length A --> x : free_tv (A!n) --> x : free_tv A";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   150
by (induct_tac "A" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   151
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   152
by (rtac allI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   153
by (res_inst_tac [("n","n")] nat_induct 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   154
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   155
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   156
qed_spec_mp "free_tv_nth_A_impl_free_tv_A";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   157
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   158
Addsimps [free_tv_nth_A_impl_free_tv_A];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   159
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   160
Goal "!nat. nat < length A --> x : free_tv (A!nat) --> x : free_tv A";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   161
by (induct_tac "A" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   162
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   163
by (rtac allI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   164
by (res_inst_tac [("n","nat")] nat_induct 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   165
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   166
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   167
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   168
qed_spec_mp "free_tv_nth_nat_A";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   169
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   170
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   171
(* if two substitutions yield the same result if applied to a type
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   172
   structure the substitutions coincide on the free type variables
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   173
   occurring in the type structure *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   174
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   175
Goal "(!x:free_tv t. (S x) = (S' x)) --> $ S (t::typ) = $ S' t";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   176
by (induct_tac "t" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   177
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   178
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   179
qed_spec_mp "typ_substitutions_only_on_free_variables";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   180
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   181
Goal  "(!n. n:(free_tv t) --> S1 n = S2 n) ==> $ S1 (t::typ) = $ S2 t";
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   182
by (rtac typ_substitutions_only_on_free_variables 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   183
by (simp_tac (simpset() addsimps [Ball_def]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   184
qed "eq_free_eq_subst_te";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   185
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   186
Goal "(!x:free_tv sch. (S x) = (S' x)) --> $ S (sch::type_scheme) = $ S' sch";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   187
by (induct_tac "sch" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   188
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   189
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   190
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   191
qed_spec_mp "scheme_substitutions_only_on_free_variables";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   192
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   193
Goal
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   194
  "(!n. n:(free_tv sch) --> S1 n = S2 n) ==> $ S1 (sch::type_scheme) = $ S2 sch";
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   195
by (rtac scheme_substitutions_only_on_free_variables 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   196
by (simp_tac (simpset() addsimps [Ball_def]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   197
qed "eq_free_eq_subst_type_scheme";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   198
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   199
Goal
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   200
  "(!n. n:(free_tv A) --> S1 n = S2 n) --> $S1 (A::type_scheme list) = $S2 A";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   201
by (induct_tac "A" 1); 
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   202
(* case [] *)
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   203
by (fast_tac (HOL_cs addss simpset()) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   204
(* case x#xl *)
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   205
by (fast_tac (HOL_cs addIs [eq_free_eq_subst_type_scheme] addss (simpset())) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   206
qed_spec_mp "eq_free_eq_subst_scheme_list";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   207
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   208
Goal "((!x:A. (P x)) --> Q) ==> ((!x:A Un B. (P x)) --> Q)";
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   209
by (Fast_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   210
val weaken_asm_Un = result ();
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   211
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   212
Goal "(!x:free_tv A. (S x) = (S' x)) --> $ S (A::type_scheme list) = $ S' A";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   213
by (induct_tac "A" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   214
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   215
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   216
by (rtac weaken_asm_Un 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   217
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   218
by (etac scheme_substitutions_only_on_free_variables 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   219
qed_spec_mp "scheme_list_substitutions_only_on_free_variables";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   220
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   221
Goal
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   222
  "$ S1 (t::typ) = $ S2 t --> n:(free_tv t) --> S1 n = S2 n";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   223
by (induct_tac "t" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   224
(* case TVar n *)
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   225
by (fast_tac (HOL_cs addss simpset()) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   226
(* case Fun t1 t2 *)
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   227
by (fast_tac (HOL_cs addss simpset()) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   228
qed_spec_mp "eq_subst_te_eq_free";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   229
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   230
Goal
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   231
  "$ S1 (sch::type_scheme) = $ S2 sch --> n:(free_tv sch) --> S1 n = S2 n";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   232
by (induct_tac "sch" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   233
(* case TVar n *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   234
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   235
(* case BVar n *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   236
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   237
by (etac mk_scheme_injective 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   238
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   239
(* case Fun t1 t2 *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   240
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   241
qed_spec_mp "eq_subst_type_scheme_eq_free";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   242
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   243
Goal
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   244
  "$S1 (A::type_scheme list) = $S2 A --> n:(free_tv A) --> S1 n = S2 n";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   245
by (induct_tac "A" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   246
(* case [] *)
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   247
by (fast_tac (HOL_cs addss simpset()) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   248
(* case x#xl *)
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   249
by (fast_tac (HOL_cs addIs [eq_subst_type_scheme_eq_free] addss (simpset())) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   250
qed_spec_mp "eq_subst_scheme_list_eq_free";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   251
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   252
Goalw [free_tv_subst] 
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   253
      "v : cod S ==> v : free_tv S";
3385
f59e64fe4058 New statement and proof of free_tv_subst_var in order to cope with new
paulson
parents: 3018
diff changeset
   254
by (fast_tac set_cs 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   255
qed "codD";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   256
 
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   257
Goalw [free_tv_subst,dom_def] 
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   258
      "x ~: free_tv S ==> S x = TVar x";
3385
f59e64fe4058 New statement and proof of free_tv_subst_var in order to cope with new
paulson
parents: 3018
diff changeset
   259
by (fast_tac set_cs 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   260
qed "not_free_impl_id";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   261
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   262
Goalw [new_tv_def] 
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   263
      "[| new_tv n t; m:free_tv t |] ==> m<n";
3385
f59e64fe4058 New statement and proof of free_tv_subst_var in order to cope with new
paulson
parents: 3018
diff changeset
   264
by (fast_tac HOL_cs 1 );
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   265
qed "free_tv_le_new_tv";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   266
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   267
Goalw [dom_def,cod_def,UNION_def,Bex_def]
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   268
  "[| v : free_tv(S n); v~=n |] ==> v : cod S";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   269
by (Simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   270
by (safe_tac (empty_cs addSIs [exI,conjI,notI]));
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1400
diff changeset
   271
by (assume_tac 2);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   272
by (rotate_tac 1 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   273
by (Asm_full_simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   274
qed "cod_app_subst";
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   275
Addsimps [cod_app_subst];
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   276
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   277
Goal "free_tv (S (v::nat)) <= insert v (cod S)";
3385
f59e64fe4058 New statement and proof of free_tv_subst_var in order to cope with new
paulson
parents: 3018
diff changeset
   278
by (expand_case_tac "v:dom S" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   279
by (fast_tac (set_cs addss (simpset() addsimps [cod_def])) 1);
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   280
by (fast_tac (set_cs addss (simpset() addsimps [dom_def])) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   281
qed "free_tv_subst_var";
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   282
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   283
Goal "free_tv ($ S (t::typ)) <= cod S Un free_tv t";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   284
by (induct_tac "t" 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   285
(* case TVar n *)
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   286
by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   287
(* case Fun t1 t2 *)
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   288
by (fast_tac (set_cs addss simpset()) 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   289
qed "free_tv_app_subst_te";     
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   290
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   291
Goal "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   292
by (induct_tac "sch" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   293
(* case FVar n *)
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   294
by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   295
(* case BVar n *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   296
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   297
(* case Fun t1 t2 *)
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   298
by (fast_tac (set_cs addss simpset()) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   299
qed "free_tv_app_subst_type_scheme";  
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   300
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   301
Goal "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   302
by (induct_tac "A" 1);
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   303
(* case [] *)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   304
by (Simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   305
(* case a#al *)
3385
f59e64fe4058 New statement and proof of free_tv_subst_var in order to cope with new
paulson
parents: 3018
diff changeset
   306
by (cut_facts_tac [free_tv_app_subst_type_scheme] 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   307
by (fast_tac (set_cs addss simpset()) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   308
qed "free_tv_app_subst_scheme_list";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
   309
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   310
Goalw [free_tv_subst,dom_def]
1521
4ed3004ff75e used qed_spec_mp.
nipkow
parents: 1465
diff changeset
   311
     "free_tv (%u::nat. $ s1 (s2 u) :: typ) <=   \
4ed3004ff75e used qed_spec_mp.
nipkow
parents: 1465
diff changeset
   312
\     free_tv s1 Un free_tv s2";
2513
d708d8cdc8e8 New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents: 2031
diff changeset
   313
by (fast_tac (set_cs addSDs [free_tv_app_subst_te RS subsetD,
3008
0a887d5b6718 Ran expandshort
paulson
parents: 2625
diff changeset
   314
                             free_tv_subst_var RS subsetD] 
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   315
                     addss (simpset() delsimps bex_simps
3008
0a887d5b6718 Ran expandshort
paulson
parents: 2625
diff changeset
   316
                                     addsimps [cod_def,dom_def])) 1);
1521
4ed3004ff75e used qed_spec_mp.
nipkow
parents: 1465
diff changeset
   317
qed "free_tv_comp_subst";
4ed3004ff75e used qed_spec_mp.
nipkow
parents: 1465
diff changeset
   318
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   319
Goalw [o_def] 
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   320
     "free_tv ($ S1 o S2) <= free_tv S1 Un free_tv (S2 :: nat => typ)";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   321
by (rtac free_tv_comp_subst 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   322
qed "free_tv_o_subst";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   323
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   324
Goal "n : free_tv t --> free_tv (S n) <= free_tv ($ S t::typ)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   325
by (induct_tac "t" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   326
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   327
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   328
by (Fast_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   329
qed_spec_mp "free_tv_of_substitutions_extend_to_types";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   330
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   331
Goal "n : free_tv sch --> free_tv (S n) <= free_tv ($ S sch::type_scheme)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   332
by (induct_tac "sch" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   333
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   334
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   335
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   336
by (Fast_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   337
qed_spec_mp "free_tv_of_substitutions_extend_to_schemes";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   338
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   339
Goal "n : free_tv A --> free_tv (S n) <= free_tv ($ S A::type_scheme list)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   340
by (induct_tac "A" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   341
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   342
by (Simp_tac 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   343
by (fast_tac (claset() addDs [free_tv_of_substitutions_extend_to_schemes]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   344
qed_spec_mp "free_tv_of_substitutions_extend_to_scheme_lists";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   345
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   346
Addsimps [free_tv_of_substitutions_extend_to_scheme_lists];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   347
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   348
Goal "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   349
by (induct_tac "sch" 1);
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4502
diff changeset
   350
by (ALLGOALS Asm_simp_tac);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   351
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   352
by (Fast_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   353
qed "free_tv_ML_scheme";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   354
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   355
Goal "!!A::type_scheme list. (n : free_tv A) = (n mem free_tv_ML A)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   356
by (induct_tac "A" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   357
by (Simp_tac 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   358
by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   359
qed "free_tv_ML_scheme_list";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   360
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   361
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   362
(* lemmata for bound_tv *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   363
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   364
Goal "bound_tv (mk_scheme t) = {}";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   365
by (induct_tac "t" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   366
by (ALLGOALS Asm_simp_tac);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   367
qed "bound_tv_mk_scheme";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   368
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   369
Addsimps [bound_tv_mk_scheme];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   370
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   371
Goal "!!sch::type_scheme. bound_tv ($ S sch) = bound_tv sch";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   372
by (induct_tac "sch" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   373
by (ALLGOALS Asm_simp_tac);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   374
qed "bound_tv_subst_scheme";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   375
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   376
Addsimps [bound_tv_subst_scheme];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   377
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   378
Goal "!!A::type_scheme list. bound_tv ($ S A) = bound_tv A";
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   379
by (rtac list.induct 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   380
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   381
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   382
qed "bound_tv_subst_scheme_list";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   383
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   384
Addsimps [bound_tv_subst_scheme_list];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   385
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   386
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   387
(* lemmata for new_tv *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   388
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   389
Goalw [new_tv_def]
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   390
  "new_tv n S = ((!m. n <= m --> (S m = TVar m)) & \
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   391
\                (! l. l < n --> new_tv n (S l) ))";
3385
f59e64fe4058 New statement and proof of free_tv_subst_var in order to cope with new
paulson
parents: 3018
diff changeset
   392
by (safe_tac HOL_cs );
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   393
(* ==> *)
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   394
by (fast_tac (HOL_cs addDs [leD] addss (simpset() addsimps [free_tv_subst,dom_def])) 1);
3385
f59e64fe4058 New statement and proof of free_tv_subst_var in order to cope with new
paulson
parents: 3018
diff changeset
   395
by (subgoal_tac "m:cod S | S l = TVar l" 1);
f59e64fe4058 New statement and proof of free_tv_subst_var in order to cope with new
paulson
parents: 3018
diff changeset
   396
by (safe_tac HOL_cs );
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   397
by (fast_tac (HOL_cs addDs [UnI2] addss (simpset() addsimps [free_tv_subst])) 1);
3018
e65b60b28341 Ran expandshort
paulson
parents: 3008
diff changeset
   398
by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1);
e65b60b28341 Ran expandshort
paulson
parents: 3008
diff changeset
   399
by (Asm_full_simp_tac 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   400
by (fast_tac (set_cs addss (simpset() addsimps [free_tv_subst,cod_def,dom_def])) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   401
(* <== *)
3385
f59e64fe4058 New statement and proof of free_tv_subst_var in order to cope with new
paulson
parents: 3018
diff changeset
   402
by (rewrite_goals_tac [free_tv_subst,cod_def,dom_def] );
f59e64fe4058 New statement and proof of free_tv_subst_var in order to cope with new
paulson
parents: 3018
diff changeset
   403
by (safe_tac set_cs );
f59e64fe4058 New statement and proof of free_tv_subst_var in order to cope with new
paulson
parents: 3018
diff changeset
   404
by (cut_inst_tac [("m","m"),("n","n")] less_linear 1);
f59e64fe4058 New statement and proof of free_tv_subst_var in order to cope with new
paulson
parents: 3018
diff changeset
   405
by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
f59e64fe4058 New statement and proof of free_tv_subst_var in order to cope with new
paulson
parents: 3018
diff changeset
   406
by (cut_inst_tac [("m","ma"),("n","n")] less_linear 1);
f59e64fe4058 New statement and proof of free_tv_subst_var in order to cope with new
paulson
parents: 3018
diff changeset
   407
by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   408
qed "new_tv_subst";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   409
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   410
Goal 
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   411
  "new_tv n  = list_all (new_tv n)";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   412
by (rtac ext 1);
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   413
by (induct_tac "x" 1);
3018
e65b60b28341 Ran expandshort
paulson
parents: 3008
diff changeset
   414
by (ALLGOALS Asm_simp_tac);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   415
qed "new_tv_list";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   416
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   417
(* substitution affects only variables occurring freely *)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   418
Goal
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   419
  "new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   420
by (induct_tac "t" 1);
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4502
diff changeset
   421
by (ALLGOALS Asm_simp_tac);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   422
qed "subst_te_new_tv";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   423
Addsimps [subst_te_new_tv];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   424
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   425
Goal
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   426
  "new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   427
by (induct_tac "sch" 1);
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4502
diff changeset
   428
by (ALLGOALS Asm_simp_tac);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   429
qed_spec_mp "subst_te_new_type_scheme";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   430
Addsimps [subst_te_new_type_scheme];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   431
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   432
Goal
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   433
  "new_tv n (A::type_scheme list) --> $(%x. if x=n then t else S x) A = $S A";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   434
by (induct_tac "A" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   435
by (ALLGOALS Asm_full_simp_tac);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   436
qed_spec_mp "subst_tel_new_scheme_list";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   437
Addsimps [subst_tel_new_scheme_list];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   438
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   439
(* all greater variables are also new *)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   440
Goalw [new_tv_def] 
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   441
  "n<=m ==> new_tv n t ==> new_tv m t";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4089
diff changeset
   442
by Safe_tac;
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   443
by (dtac spec 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   444
by (mp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   445
by (trans_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   446
qed "new_tv_le";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   447
Addsimps [lessI RS less_imp_le RS new_tv_le];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   448
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   449
Goal "n<=m ==> new_tv n (t::typ) ==> new_tv m t";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   450
by (asm_simp_tac (simpset() addsimps [new_tv_le]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   451
qed "new_tv_typ_le";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   452
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   453
Goal "n<=m ==> new_tv n (A::type_scheme list) ==> new_tv m A";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   454
by (asm_simp_tac (simpset() addsimps [new_tv_le]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   455
qed "new_scheme_list_le";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   456
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   457
Goal "n<=m ==> new_tv n (S::subst) ==> new_tv m S";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   458
by (asm_simp_tac (simpset() addsimps [new_tv_le]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   459
qed "new_tv_subst_le";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   460
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   461
(* new_tv property remains if a substitution is applied *)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   462
Goal
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   463
  "[| n<m; new_tv m (S::subst) |] ==> new_tv m (S n)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   464
by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   465
qed "new_tv_subst_var";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   466
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   467
Goal
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   468
  "new_tv n S --> new_tv n (t::typ) --> new_tv n ($ S t)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   469
by (induct_tac "t" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   470
by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   471
qed_spec_mp "new_tv_subst_te";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   472
Addsimps [new_tv_subst_te];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   473
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   474
Goal "new_tv n S --> new_tv n (sch::type_scheme) --> new_tv n ($ S sch)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   475
by (induct_tac "sch" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   476
by (ALLGOALS (Asm_full_simp_tac));
3008
0a887d5b6718 Ran expandshort
paulson
parents: 2625
diff changeset
   477
by (rewtac new_tv_def);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   478
by (simp_tac (simpset() addsimps [free_tv_subst,dom_def,cod_def]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   479
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   480
by (case_tac "S nat = TVar nat" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   481
by (rotate_tac 3 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   482
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   483
by (dres_inst_tac [("x","m")] spec 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   484
by (Fast_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   485
qed_spec_mp "new_tv_subst_type_scheme";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   486
Addsimps [new_tv_subst_type_scheme];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   487
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   488
Goal
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   489
  "new_tv n S --> new_tv n (A::type_scheme list) --> new_tv n ($ S A)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   490
by (induct_tac "A" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   491
by (ALLGOALS(fast_tac (HOL_cs addss (simpset()))));
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   492
qed_spec_mp "new_tv_subst_scheme_list";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   493
Addsimps [new_tv_subst_scheme_list];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   494
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   495
Goal
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   496
  "new_tv n A --> new_tv (Suc n) ((TVar n)#A)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   497
by (simp_tac (simpset() addsimps [new_tv_list]) 1);
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   498
by (induct_tac "A" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   499
by (ALLGOALS Asm_full_simp_tac);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   500
qed "new_tv_Suc_list";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   501
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   502
Goalw [new_tv_def] "!!sch::type_scheme. (free_tv sch) = (free_tv sch') --> (new_tv n sch --> new_tv n sch')";
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   503
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   504
qed_spec_mp "new_tv_only_depends_on_free_tv_type_scheme";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   505
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   506
Goalw [new_tv_def] "!!A::type_scheme list. (free_tv A) = (free_tv A') --> (new_tv n A --> new_tv n A')";
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   507
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   508
qed_spec_mp "new_tv_only_depends_on_free_tv_scheme_list";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   509
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   510
Goalw [new_tv_def]
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   511
  "!nat. nat < length A --> new_tv n A --> (new_tv n (A!nat))";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   512
by (induct_tac "A" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   513
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   514
by (rtac allI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   515
by (res_inst_tac [("n","nat")] nat_induct 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   516
by (strip_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   517
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   518
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   519
qed_spec_mp "new_tv_nth_nat_A";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   520
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   521
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   522
(* composition of substitutions preserves new_tv proposition *)
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   523
Goal "[| new_tv n (S::subst); new_tv n R |] ==> new_tv n (($ R) o S)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   524
by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   525
qed "new_tv_subst_comp_1";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   526
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   527
Goal "[| new_tv n (S::subst); new_tv n R |] ==> new_tv n (%v.$ R (S v))";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   528
by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   529
qed "new_tv_subst_comp_2";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   530
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   531
Addsimps [new_tv_subst_comp_1,new_tv_subst_comp_2];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   532
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   533
(* new type variables do not occur freely in a type structure *)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   534
Goalw [new_tv_def] 
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   535
      "new_tv n A ==> n~:(free_tv A)";
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   536
by (fast_tac (HOL_cs addEs [less_irrefl]) 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   537
qed "new_tv_not_free_tv";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   538
Addsimps [new_tv_not_free_tv];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   539
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   540
Goalw [max_def] "!!n::nat. m < n ==> m < max n n'";
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4502
diff changeset
   541
by (Simp_tac 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4089
diff changeset
   542
by Safe_tac;
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   543
by (trans_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   544
qed "less_maxL";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   545
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   546
Goalw [max_def] "!!n::nat. m < n' ==> m < max n n'";
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4502
diff changeset
   547
by (Simp_tac 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   548
by (fast_tac (claset() addDs [not_leE] addIs [less_trans]) 1);
2625
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
   549
val less_maxR = result();
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   550
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   551
Goalw [new_tv_def] "!!t::typ. ? n. (new_tv n t)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   552
by (induct_tac "t" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   553
by (res_inst_tac [("x","Suc nat")] exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   554
by (Asm_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   555
by (REPEAT (etac exE 1));
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   556
by (rename_tac "n'" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   557
by (res_inst_tac [("x","max n n'")] exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   558
by (Simp_tac 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   559
by (fast_tac (claset() addIs [less_maxR,less_maxL]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   560
qed "fresh_variable_types";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   561
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   562
Addsimps [fresh_variable_types];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   563
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   564
Goalw [new_tv_def] "!!sch::type_scheme. ? n. (new_tv n sch)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   565
by (induct_tac "sch" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   566
by (res_inst_tac [("x","Suc nat")] exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   567
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   568
by (res_inst_tac [("x","Suc nat")] exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   569
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   570
by (REPEAT (etac exE 1));
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   571
by (rename_tac "n'" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   572
by (res_inst_tac [("x","max n n'")] exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   573
by (Simp_tac 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   574
by (fast_tac (claset() addIs [less_maxR,less_maxL]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   575
qed "fresh_variable_type_schemes";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   576
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   577
Addsimps [fresh_variable_type_schemes];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   578
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   579
Goalw [max_def] "!!n::nat. n <= (max n n')";
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4502
diff changeset
   580
by (Simp_tac 1);
2625
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
   581
val le_maxL = result();
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   582
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   583
Goalw [max_def] "!!n'::nat. n' <= (max n n')";
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4502
diff changeset
   584
by (Simp_tac 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   585
by (fast_tac (claset() addDs [not_leE] addIs [less_or_eq_imp_le]) 1);
2625
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
   586
val le_maxR = result();
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   587
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   588
Goal "!!A::type_scheme list. ? n. (new_tv n A)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   589
by (induct_tac "A" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   590
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   591
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   592
by (etac exE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   593
by (cut_inst_tac [("sch","a")] fresh_variable_type_schemes 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   594
by (etac exE 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   595
by (rename_tac "n'" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   596
by (res_inst_tac [("x","(max n n')")] exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   597
by (subgoal_tac "n <= (max n n')" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   598
by (subgoal_tac "n' <= (max n n')" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   599
by (fast_tac (claset() addDs [new_tv_le]) 1);
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   600
by (ALLGOALS (simp_tac (simpset() addsimps [le_maxR,le_maxL])));
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   601
qed "fresh_variable_type_scheme_lists";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   602
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   603
Addsimps [fresh_variable_type_scheme_lists];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   604
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   605
Goal "[| ? n1. (new_tv n1 x); ? n2. (new_tv n2 y)|] ==> ? n. (new_tv n x) & (new_tv n y)";
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   606
by (REPEAT (etac exE 1));
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   607
by (rename_tac "n1 n2" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   608
by (res_inst_tac [("x","(max n1 n2)")] exI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   609
by (subgoal_tac "n1 <= max n1 n2" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   610
by (subgoal_tac "n2 <= max n1 n2" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   611
by (fast_tac (claset() addDs [new_tv_le]) 1);
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   612
by (ALLGOALS (simp_tac (simpset() addsimps [le_maxL,le_maxR])));
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   613
qed "make_one_new_out_of_two";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   614
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   615
Goal "!!(A::type_scheme list) (A'::type_scheme list) (t::typ) (t'::typ). \
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   616
\         ? n. (new_tv n A) & (new_tv n A') & (new_tv n t) & (new_tv n t')" ;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   617
by (cut_inst_tac [("t","t")] fresh_variable_types 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   618
by (cut_inst_tac [("t","t'")] fresh_variable_types 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   619
by (dtac make_one_new_out_of_two 1);
3018
e65b60b28341 Ran expandshort
paulson
parents: 3008
diff changeset
   620
by (assume_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   621
by (thin_tac "? n. new_tv n t'" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   622
by (cut_inst_tac [("A","A")] fresh_variable_type_scheme_lists 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   623
by (cut_inst_tac [("A","A'")] fresh_variable_type_scheme_lists 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   624
by (rotate_tac 1 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   625
by (dtac make_one_new_out_of_two 1);
3018
e65b60b28341 Ran expandshort
paulson
parents: 3008
diff changeset
   626
by (assume_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   627
by (thin_tac "? n. new_tv n A'" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   628
by (REPEAT (etac exE 1));
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   629
by (rename_tac "n2 n1" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   630
by (res_inst_tac [("x","(max n1 n2)")] exI 1);
3008
0a887d5b6718 Ran expandshort
paulson
parents: 2625
diff changeset
   631
by (rewtac new_tv_def);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   632
by (fast_tac (claset() addIs [less_maxL,less_maxR]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   633
qed "ex_fresh_variable";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   634
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   635
(* mgu does not introduce new type variables *)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   636
Goalw [new_tv_def] 
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   637
      "[|mgu t1 t2 = Some u; new_tv n t1; new_tv n t2|] ==> new_tv n u";
3385
f59e64fe4058 New statement and proof of free_tv_subst_var in order to cope with new
paulson
parents: 3018
diff changeset
   638
by (fast_tac (set_cs addDs [mgu_free]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   639
qed "mgu_new";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   640
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   641
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   642
(* lemmata for substitutions *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   643
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   644
Goalw [app_subst_list] 
3438
8d63ff01d37e Type constraint added to ensure that "length" refers to lists. Maybe should
paulson
parents: 3385
diff changeset
   645
   "!!A:: ('a::type_struct) list. length ($ S A) = length A";
3018
e65b60b28341 Ran expandshort
paulson
parents: 3008
diff changeset
   646
by (Simp_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   647
qed "length_app_subst_list";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   648
Addsimps [length_app_subst_list];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   649
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   650
Goal "!!sch::type_scheme. $ TVar sch = sch";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   651
by (induct_tac "sch" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   652
by (ALLGOALS Asm_simp_tac);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   653
qed "subst_TVar_scheme";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   654
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   655
Addsimps [subst_TVar_scheme];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   656
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   657
Goal "!!A::type_scheme list. $ TVar A = A";
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   658
by (rtac list.induct 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   659
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [app_subst_list])));
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   660
qed "subst_TVar_scheme_list";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   661
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   662
Addsimps [subst_TVar_scheme_list];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   663
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   664
(* application of id_subst does not change type expression *)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   665
Goalw [id_subst_def]
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3438
diff changeset
   666
  "$ id_subst = (%t::typ. t)";
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   667
by (rtac ext 1);
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   668
by (induct_tac "t" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   669
by (ALLGOALS Asm_simp_tac);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   670
qed "app_subst_id_te";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   671
Addsimps [app_subst_id_te];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   672
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   673
Goalw [id_subst_def]
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3438
diff changeset
   674
  "$ id_subst = (%sch::type_scheme. sch)";
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   675
by (rtac ext 1);
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   676
by (induct_tac "sch" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   677
by (ALLGOALS Asm_simp_tac);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   678
qed "app_subst_id_type_scheme";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   679
Addsimps [app_subst_id_type_scheme];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   680
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   681
(* application of id_subst does not change list of type expressions *)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   682
Goalw [app_subst_list]
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3438
diff changeset
   683
  "$ id_subst = (%A::type_scheme list. A)";
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   684
by (rtac ext 1); 
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   685
by (induct_tac "A" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   686
by (ALLGOALS Asm_simp_tac);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   687
qed "app_subst_id_tel";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   688
Addsimps [app_subst_id_tel];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   689
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   690
Goal "!!sch::type_scheme. $ id_subst sch = sch";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   691
by (induct_tac "sch" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   692
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [id_subst_def])));
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   693
qed "id_subst_sch";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   694
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   695
Addsimps [id_subst_sch];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   696
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   697
Goal "!!A::type_scheme list. $ id_subst A = A";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   698
by (induct_tac "A" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   699
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   700
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   701
qed "id_subst_A";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   702
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   703
Addsimps [id_subst_A];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   704
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   705
(* composition of substitutions *)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   706
Goalw [id_subst_def,o_def] "$S o id_subst = S";
3018
e65b60b28341 Ran expandshort
paulson
parents: 3008
diff changeset
   707
by (rtac ext 1);
e65b60b28341 Ran expandshort
paulson
parents: 3008
diff changeset
   708
by (Simp_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   709
qed "o_id_subst";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   710
Addsimps[o_id_subst];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   711
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   712
Goal "$ R ($ S t::typ) = $ (%x. $ R (S x) ) t";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   713
by (induct_tac "t" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   714
by (ALLGOALS Asm_simp_tac);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   715
qed "subst_comp_te";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   716
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
   717
Goal "$ R ($ S sch::type_scheme) = $ (%x. $ R (S x) ) sch";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   718
by (induct_tac "sch" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   719
by (ALLGOALS Asm_full_simp_tac);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   720
qed "subst_comp_type_scheme";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   721
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   722
Goalw [app_subst_list]
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   723
  "$ R ($ S A::type_scheme list) = $ (%x. $ R (S x)) A";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   724
by (induct_tac "A" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   725
(* case [] *)
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   726
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   727
(* case x#xl *)
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   728
by (asm_full_simp_tac (simpset() addsimps [subst_comp_type_scheme]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   729
qed "subst_comp_scheme_list";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   730
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   731
Goal "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = $ id_subst A";
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   732
by (rtac scheme_list_substitutions_only_on_free_variables 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   733
by (asm_full_simp_tac (simpset() addsimps [id_subst_def]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   734
qed "subst_id_on_type_scheme_list'";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   735
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   736
Goal "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = A";
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   737
by (stac subst_id_on_type_scheme_list' 1);
3018
e65b60b28341 Ran expandshort
paulson
parents: 3008
diff changeset
   738
by (assume_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   739
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   740
qed "subst_id_on_type_scheme_list";
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   741
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   742
Goal "!n. n < length A --> ($ S A)!n = $S (A!n)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5118
diff changeset
   743
by (induct_tac "A" 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   744
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   745
by (rtac allI 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   746
by (rename_tac "n1" 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   747
by (res_inst_tac[("n","n1")] nat_induct 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   748
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   749
by (Asm_full_simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2513
diff changeset
   750
qed_spec_mp "nth_subst";