Learn how easy it is to sync an existing GitHub or Google Code repo to a SourceForge project! See Demo

Close

[f3dc84]: thys / MiniML / Generalize.thy Maximize Restore History

Download this file

Generalize.thy    178 lines (148 with data), 4.6 kB

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
(* Title: HOL/MiniML/Generalize.thy
ID: $Id: Generalize.thy,v 1.3.2.1 2004-05-21 00:14:35 lsf37 Exp $
Author: Wolfgang Naraschewski and Tobias Nipkow
Copyright 1996 TU Muenchen
*)
header "Generalizing type schemes with respect to a context"
theory Generalize = Instance:
-- "@{text gen}: binding (generalising) the variables which are not free in the context"
types ctxt = "type_scheme list"
consts
gen :: "[ctxt, typ] => type_scheme"
primrec
"gen A (TVar n) = (if (n:(free_tv A)) then (FVar n) else (BVar n))"
"gen A (t1 -> t2) = (gen A t1) =-> (gen A t2)"
-- "executable version of @{text gen}: implementation with @{text free_tv_ML}"
consts
gen_ML_aux :: "[nat list, typ] => type_scheme"
primrec
"gen_ML_aux A (TVar n) = (if (n: set A) then (FVar n) else (BVar n))"
"gen_ML_aux A (t1 -> t2) = (gen_ML_aux A t1) =-> (gen_ML_aux A t2)"
consts
gen_ML :: "[ctxt, typ] => type_scheme"
defs
gen_ML_def: "gen_ML A t == gen_ML_aux (free_tv_ML A) t"
declare equalityE [elim!]
lemma gen_eq_on_free_tv:
"free_tv A = free_tv B ==> gen A t = gen B t"
apply (induct_tac "t")
apply (simp_all (no_asm_simp))
done
lemma gen_without_effect [rule_format (no_asm)]:
"(free_tv t) <= (free_tv sch) --> gen sch t = (mk_scheme t)"
apply (induct_tac "t")
apply (simp (no_asm_simp))
apply (simp (no_asm))
apply fast
done
declare gen_without_effect [simp]
lemma free_tv_gen:
"free_tv (gen ($ S A) t) = free_tv t Int free_tv ($ S A)"
apply (induct_tac "t")
apply (simp (no_asm))
apply (case_tac "nat : free_tv ($ S A) ")
apply (simp (no_asm_simp))
apply fast
apply (simp (no_asm_simp))
apply fast
apply simp
apply fast
done
declare free_tv_gen [simp]
lemma free_tv_gen_cons:
"free_tv (gen ($ S A) t # $ S A) = free_tv ($ S A)"
apply (simp (no_asm))
apply fast
done
declare free_tv_gen_cons [simp]
lemma bound_tv_gen:
"bound_tv (gen A t1) = (free_tv t1) - (free_tv A)"
apply (induct_tac "t1")
apply (simp (no_asm))
apply (case_tac "nat : free_tv A")
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply fast
apply (simp (no_asm_simp))
apply fast
done
declare bound_tv_gen [simp]
lemma new_tv_compatible_gen [rule_format (no_asm)]:
"new_tv n t --> new_tv n (gen A t)"
apply (induct_tac "t")
apply auto
done
lemma gen_eq_gen_ML: "gen A t = gen_ML A t"
apply (unfold gen_ML_def)
apply (induct_tac "t")
apply (simp (no_asm) add: free_tv_ML_scheme_list)
apply (simp (no_asm_simp) add: free_tv_ML_scheme_list)
done
lemma gen_subst_commutes [rule_format (no_asm)]:
"(free_tv S) Int ((free_tv t) - (free_tv A)) = {}
--> gen ($ S A) ($ S t) = $ S (gen A t)"
apply (induct_tac "t")
apply (intro strip)
apply (case_tac "nat: (free_tv A) ")
apply (simp (no_asm_simp))
apply simp
apply (subgoal_tac "nat ~: free_tv S")
prefer 2 apply (fast)
apply (simp add: free_tv_subst dom_def)
apply (cut_tac free_tv_app_subst_scheme_list)
apply fast
apply (simp (no_asm_simp))
apply blast
done
lemma bound_typ_inst_gen [rule_format (no_asm)]:
"free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t"
apply (induct_tac "t")
apply (simp_all (no_asm_simp))
apply fast
done
declare bound_typ_inst_gen [simp]
lemma gen_bound_typ_instance:
"gen ($ S A) ($ S t) <= $ S (gen A t)"
apply (unfold le_type_scheme_def is_bound_typ_instance)
apply safe
apply (rename_tac "R")
apply (rule_tac x = " (%a. bound_typ_inst R (gen ($S A) (S a))) " in exI)
apply (induct_tac "t")
apply (simp (no_asm))
apply (simp (no_asm_simp))
done
lemma free_tv_subset_gen_le:
"free_tv B <= free_tv A ==> gen A t <= gen B t"
apply (unfold le_type_scheme_def is_bound_typ_instance)
apply safe
apply (rename_tac "S")
apply (rule_tac x = "%b. if b:free_tv A then TVar b else S b" in exI)
apply (induct_tac "t")
apply (simp (no_asm_simp))
apply fast
apply (simp (no_asm_simp))
done
lemma gen_t_le_gen_alpha_t [rule_format (no_asm)]:
"new_tv n A -->
gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)"
apply (unfold le_type_scheme_def is_bound_typ_instance)
apply (intro strip)
apply (erule exE)
apply (hypsubst)
apply (rule_tac x = " (%x. S (if n <= x then x - n else x))" in exI)
apply (induct_tac "t")
apply (simp (no_asm))
apply (case_tac "nat : free_tv A")
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (subgoal_tac "n <= n + nat")
apply (frule_tac t = "A" in new_tv_le)
apply assumption
apply (drule new_tv_not_free_tv)
apply (drule new_tv_not_free_tv)
apply (simp (no_asm_simp) add: diff_add_inverse)
apply (simp (no_asm) add: le_add1)
apply (simp (no_asm_simp))
done
declare gen_t_le_gen_alpha_t [simp]
end