author | wenzelm |
Fri, 18 Aug 2017 20:47:47 +0200 | |
changeset 66453 | cc19f7ca2ed6 |
parent 63167 | 0909deb8059b |
child 68249 | 949d93804740 |
permissions | -rw-r--r-- |
26195 | 1 |
theory W |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63167
diff
changeset
|
2 |
imports "HOL-Nominal.Nominal" |
26195 | 3 |
begin |
4 |
||
63167 | 5 |
text \<open>Example for strong induction rules avoiding sets of atoms.\<close> |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
6 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
7 |
atom_decl tvar var |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
8 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
9 |
abbreviation |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
10 |
"difference_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_ - _" [60,60] 60) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
11 |
where |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
12 |
"xs - ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
13 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
14 |
lemma difference_eqvt_tvar[eqvt]: |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
15 |
fixes pi::"tvar prm" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
16 |
and Xs Ys::"tvar list" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
17 |
shows "pi\<bullet>(Xs - Ys) = (pi\<bullet>Xs) - (pi\<bullet>Ys)" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
18 |
by (induct Xs) (simp_all add: eqvts) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
19 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
20 |
lemma difference_fresh: |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
21 |
fixes X::"tvar" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
22 |
and Xs Ys::"tvar list" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
23 |
assumes a: "X\<in>set Ys" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
24 |
shows "X\<sharp>(Xs - Ys)" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
25 |
using a |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
26 |
by (induct Xs) (auto simp add: fresh_list_nil fresh_list_cons fresh_atm) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
27 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
28 |
lemma difference_supset: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
29 |
fixes xs::"'a list" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
30 |
and ys::"'a list" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
31 |
and zs::"'a list" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
32 |
assumes asm: "set xs \<subseteq> set ys" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
33 |
shows "xs - ys = []" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
34 |
using asm |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
35 |
by (induct xs) (auto) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
36 |
|
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
37 |
nominal_datatype ty = |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
38 |
TVar "tvar" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
39 |
| Fun "ty" "ty" ("_\<rightarrow>_" [100,100] 100) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
40 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
41 |
nominal_datatype tyS = |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
42 |
Ty "ty" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
43 |
| ALL "\<guillemotleft>tvar\<guillemotright>tyS" ("\<forall>[_]._" [100,100] 100) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
44 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
45 |
nominal_datatype trm = |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
46 |
Var "var" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
47 |
| App "trm" "trm" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
48 |
| Lam "\<guillemotleft>var\<guillemotright>trm" ("Lam [_]._" [100,100] 100) |
58219
61b852f90161
improved 'datatype_compat' further for recursion through functions
blanchet
parents:
55417
diff
changeset
|
49 |
| Let "\<guillemotleft>var\<guillemotright>trm" "trm" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
50 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
51 |
abbreviation |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
52 |
LetBe :: "var \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" ("Let _ be _ in _" [100,100,100] 100) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
53 |
where |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
54 |
"Let x be t1 in t2 \<equiv> trm.Let x t2 t1" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
55 |
|
41798 | 56 |
type_synonym |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
57 |
Ctxt = "(var\<times>tyS) list" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
58 |
|
63167 | 59 |
text \<open>free type variables\<close> |
29098
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
60 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
61 |
consts ftv :: "'a \<Rightarrow> tvar list" |
29098
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
62 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
63 |
overloading |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
64 |
ftv_prod \<equiv> "ftv :: ('a \<times> 'b) \<Rightarrow> tvar list" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
65 |
ftv_tvar \<equiv> "ftv :: tvar \<Rightarrow> tvar list" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
66 |
ftv_var \<equiv> "ftv :: var \<Rightarrow> tvar list" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
67 |
ftv_list \<equiv> "ftv :: 'a list \<Rightarrow> tvar list" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
68 |
ftv_ty \<equiv> "ftv :: ty \<Rightarrow> tvar list" |
29098
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
69 |
begin |
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
70 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
71 |
primrec |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
72 |
ftv_prod |
29098
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
73 |
where |
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
74 |
"ftv_prod (x, y) = (ftv x) @ (ftv y)" |
29098
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
75 |
|
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
76 |
definition |
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
77 |
ftv_tvar :: "tvar \<Rightarrow> tvar list" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
78 |
where |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
79 |
[simp]: "ftv_tvar X \<equiv> [(X::tvar)]" |
29098
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
80 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
81 |
definition |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
82 |
ftv_var :: "var \<Rightarrow> tvar list" |
29098
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
83 |
where |
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
84 |
[simp]: "ftv_var x \<equiv> []" |
29098
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
85 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
86 |
primrec |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
87 |
ftv_list |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
88 |
where |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
89 |
"ftv_list [] = []" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
90 |
| "ftv_list (x#xs) = (ftv x)@(ftv_list xs)" |
29098
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
91 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
92 |
nominal_primrec |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
93 |
ftv_ty :: "ty \<Rightarrow> tvar list" |
29098
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
94 |
where |
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
95 |
"ftv_ty (TVar X) = [X]" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
96 |
| "ftv_ty (T1 \<rightarrow>T2) = (ftv_ty T1) @ (ftv_ty T2)" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
97 |
by (rule TrueI)+ |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
98 |
|
29098
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
99 |
end |
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
100 |
|
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
101 |
lemma ftv_ty_eqvt[eqvt]: |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
102 |
fixes pi::"tvar prm" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
103 |
and T::"ty" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
104 |
shows "pi\<bullet>(ftv T) = ftv (pi\<bullet>T)" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
105 |
by (nominal_induct T rule: ty.strong_induct) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
106 |
(perm_simp add: append_eqvt)+ |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
107 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
108 |
overloading |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
109 |
ftv_tyS \<equiv> "ftv :: tyS \<Rightarrow> tvar list" |
29098
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
110 |
begin |
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
111 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
112 |
nominal_primrec |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
113 |
ftv_tyS :: "tyS \<Rightarrow> tvar list" |
29098
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
114 |
where |
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
115 |
"ftv_tyS (Ty T) = ((ftv (T::ty))::tvar list)" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
116 |
| "ftv_tyS (\<forall>[X].S) = (ftv_tyS S) - [X]" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
117 |
apply(finite_guess add: ftv_ty_eqvt fs_tvar1)+ |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
118 |
apply(rule TrueI)+ |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
119 |
apply(rule difference_fresh) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
120 |
apply(simp) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
121 |
apply(fresh_guess add: ftv_ty_eqvt fs_tvar1)+ |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
122 |
done |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
123 |
|
29098
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
124 |
end |
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
125 |
|
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
126 |
lemma ftv_tyS_eqvt[eqvt]: |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
127 |
fixes pi::"tvar prm" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
128 |
and S::"tyS" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
129 |
shows "pi\<bullet>(ftv S) = ftv (pi\<bullet>S)" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
130 |
apply(nominal_induct S rule: tyS.strong_induct) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
131 |
apply(simp add: eqvts) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
132 |
apply(simp only: ftv_tyS.simps) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
133 |
apply(simp only: eqvts) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
134 |
apply(simp add: eqvts) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
135 |
done |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
136 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
137 |
lemma ftv_Ctxt_eqvt[eqvt]: |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
138 |
fixes pi::"tvar prm" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
139 |
and \<Gamma>::"Ctxt" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
140 |
shows "pi\<bullet>(ftv \<Gamma>) = ftv (pi\<bullet>\<Gamma>)" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
141 |
by (induct \<Gamma>) (auto simp add: eqvts) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
142 |
|
63167 | 143 |
text \<open>Valid\<close> |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
144 |
inductive |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
145 |
valid :: "Ctxt \<Rightarrow> bool" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
146 |
where |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
147 |
V_Nil[intro]: "valid []" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
148 |
| V_Cons[intro]: "\<lbrakk>valid \<Gamma>;x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((x,S)#\<Gamma>)" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
149 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
150 |
equivariance valid |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
151 |
|
63167 | 152 |
text \<open>General\<close> |
39246 | 153 |
primrec gen :: "ty \<Rightarrow> tvar list \<Rightarrow> tyS" where |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
154 |
"gen T [] = Ty T" |
39246 | 155 |
| "gen T (X#Xs) = \<forall>[X].(gen T Xs)" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
156 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
157 |
lemma gen_eqvt[eqvt]: |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
158 |
fixes pi::"tvar prm" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
159 |
shows "pi\<bullet>(gen T Xs) = gen (pi\<bullet>T) (pi\<bullet>Xs)" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
160 |
by (induct Xs) (simp_all add: eqvts) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
161 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
162 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
163 |
|
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
164 |
abbreviation |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
165 |
close :: "Ctxt \<Rightarrow> ty \<Rightarrow> tyS" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
166 |
where |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
167 |
"close \<Gamma> T \<equiv> gen T ((ftv T) - (ftv \<Gamma>))" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
168 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
169 |
lemma close_eqvt[eqvt]: |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
170 |
fixes pi::"tvar prm" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
171 |
shows "pi\<bullet>(close \<Gamma> T) = close (pi\<bullet>\<Gamma>) (pi\<bullet>T)" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
172 |
by (simp_all only: eqvts) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
173 |
|
63167 | 174 |
text \<open>Substitution\<close> |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
175 |
|
41798 | 176 |
type_synonym Subst = "(tvar\<times>ty) list" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
177 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
178 |
consts |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
179 |
psubst :: "Subst \<Rightarrow> 'a \<Rightarrow> 'a" ("_<_>" [100,60] 120) |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
180 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
181 |
abbreviation |
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
182 |
subst :: "'a \<Rightarrow> tvar \<Rightarrow> ty \<Rightarrow> 'a" ("_[_::=_]" [100,100,100] 100) |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
183 |
where |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
184 |
"smth[X::=T] \<equiv> ([(X,T)])<smth>" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
185 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
186 |
fun |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
187 |
lookup :: "Subst \<Rightarrow> tvar \<Rightarrow> ty" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
188 |
where |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
189 |
"lookup [] X = TVar X" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
190 |
| "lookup ((Y,T)#\<theta>) X = (if X=Y then T else lookup \<theta> X)" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
191 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
192 |
lemma lookup_eqvt[eqvt]: |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
193 |
fixes pi::"tvar prm" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
194 |
shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
195 |
by (induct \<theta>) (auto simp add: eqvts) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
196 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
197 |
lemma lookup_fresh: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
198 |
fixes X::"tvar" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
199 |
assumes a: "X\<sharp>\<theta>" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
200 |
shows "lookup \<theta> X = TVar X" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
201 |
using a |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
202 |
by (induct \<theta>) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
203 |
(auto simp add: fresh_list_cons fresh_prod fresh_atm) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
204 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
205 |
overloading |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
206 |
psubst_ty \<equiv> "psubst :: Subst \<Rightarrow> ty \<Rightarrow> ty" |
29098
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
207 |
begin |
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
208 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
209 |
nominal_primrec |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
210 |
psubst_ty |
29098
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
211 |
where |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
212 |
"\<theta><TVar X> = lookup \<theta> X" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
213 |
| "\<theta><T\<^sub>1 \<rightarrow> T\<^sub>2> = (\<theta><T\<^sub>1>) \<rightarrow> (\<theta><T\<^sub>2>)" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
214 |
by (rule TrueI)+ |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
215 |
|
29098
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
216 |
end |
6b23a58cc67c
Unified syntax of nominal_primrec with the one used by fun(ction) and new
berghofe
parents:
28655
diff
changeset
|
217 |
|
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
218 |
lemma psubst_ty_eqvt[eqvt]: |
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
219 |
fixes pi::"tvar prm" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
220 |
and \<theta>::"Subst" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
221 |
and T::"ty" |
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
222 |
shows "pi\<bullet>(\<theta><T>) = (pi\<bullet>\<theta>)<(pi\<bullet>T)>" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
223 |
by (induct T rule: ty.induct) (simp_all add: eqvts) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
224 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
225 |
overloading |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
226 |
psubst_tyS \<equiv> "psubst :: Subst \<Rightarrow> tyS \<Rightarrow> tyS" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
227 |
begin |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
228 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
229 |
nominal_primrec |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
230 |
psubst_tyS :: "Subst \<Rightarrow> tyS \<Rightarrow> tyS" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
231 |
where |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
232 |
"\<theta><(Ty T)> = Ty (\<theta><T>)" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
233 |
| "X\<sharp>\<theta> \<Longrightarrow> \<theta><(\<forall>[X].S)> = \<forall>[X].(\<theta><S>)" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
234 |
apply(finite_guess add: psubst_ty_eqvt fs_tvar1)+ |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
235 |
apply(rule TrueI)+ |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
236 |
apply(simp add: abs_fresh) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
237 |
apply(fresh_guess add: psubst_ty_eqvt fs_tvar1)+ |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
238 |
done |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
239 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
240 |
end |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
241 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
242 |
overloading |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
243 |
psubst_Ctxt \<equiv> "psubst :: Subst \<Rightarrow> Ctxt \<Rightarrow> Ctxt" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
244 |
begin |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
245 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
246 |
fun |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
247 |
psubst_Ctxt :: "Subst \<Rightarrow> Ctxt \<Rightarrow> Ctxt" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
248 |
where |
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
249 |
"psubst_Ctxt \<theta> [] = []" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
250 |
| "psubst_Ctxt \<theta> ((x,S)#\<Gamma>) = (x,\<theta><S>)#(psubst_Ctxt \<theta> \<Gamma>)" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
251 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
252 |
end |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
253 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
254 |
lemma fresh_lookup: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
255 |
fixes X::"tvar" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
256 |
and \<theta>::"Subst" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
257 |
and Y::"tvar" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
258 |
assumes asms: "X\<sharp>Y" "X\<sharp>\<theta>" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
259 |
shows "X\<sharp>(lookup \<theta> Y)" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
260 |
using asms |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
261 |
by (induct \<theta>) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
262 |
(auto simp add: fresh_list_cons fresh_prod fresh_atm) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
263 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
264 |
lemma fresh_psubst_ty: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
265 |
fixes X::"tvar" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
266 |
and \<theta>::"Subst" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
267 |
and T::"ty" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
268 |
assumes asms: "X\<sharp>\<theta>" "X\<sharp>T" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
269 |
shows "X\<sharp>\<theta><T>" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
270 |
using asms |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
271 |
by (nominal_induct T rule: ty.strong_induct) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
272 |
(auto simp add: fresh_list_append fresh_list_cons fresh_prod fresh_lookup) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
273 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
274 |
lemma fresh_psubst_tyS: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
275 |
fixes X::"tvar" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
276 |
and \<theta>::"Subst" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
277 |
and S::"tyS" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
278 |
assumes asms: "X\<sharp>\<theta>" "X\<sharp>S" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
279 |
shows "X\<sharp>\<theta><S>" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
280 |
using asms |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
281 |
by (nominal_induct S avoiding: \<theta> X rule: tyS.strong_induct) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
282 |
(auto simp add: fresh_psubst_ty abs_fresh) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
283 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
284 |
lemma fresh_psubst_Ctxt: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
285 |
fixes X::"tvar" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
286 |
and \<theta>::"Subst" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
287 |
and \<Gamma>::"Ctxt" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
288 |
assumes asms: "X\<sharp>\<theta>" "X\<sharp>\<Gamma>" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
289 |
shows "X\<sharp>\<theta><\<Gamma>>" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
290 |
using asms |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
291 |
by (induct \<Gamma>) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
292 |
(auto simp add: fresh_psubst_tyS fresh_list_cons) |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
293 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
294 |
lemma subst_freshfact2_ty: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
295 |
fixes X::"tvar" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
296 |
and Y::"tvar" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
297 |
and T::"ty" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
298 |
assumes asms: "X\<sharp>S" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
299 |
shows "X\<sharp>T[X::=S]" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
300 |
using asms |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
301 |
by (nominal_induct T rule: ty.strong_induct) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
302 |
(auto simp add: fresh_atm) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
303 |
|
63167 | 304 |
text \<open>instance of a type scheme\<close> |
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
305 |
inductive |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
306 |
inst :: "ty \<Rightarrow> tyS \<Rightarrow> bool"("_ \<prec> _" [50,51] 50) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
307 |
where |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
308 |
I_Ty[intro]: "T \<prec> (Ty T)" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
309 |
| I_All[intro]: "\<lbrakk>X\<sharp>T'; T \<prec> S\<rbrakk> \<Longrightarrow> T[X::=T'] \<prec> \<forall>[X].S" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
310 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
311 |
equivariance inst[tvar] |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
312 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
313 |
nominal_inductive inst |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
314 |
by (simp_all add: abs_fresh subst_freshfact2_ty) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
315 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
316 |
lemma subst_forget_ty: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
317 |
fixes T::"ty" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
318 |
and X::"tvar" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
319 |
assumes a: "X\<sharp>T" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
320 |
shows "T[X::=S] = T" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
321 |
using a |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
322 |
by (nominal_induct T rule: ty.strong_induct) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
323 |
(auto simp add: fresh_atm) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
324 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
325 |
lemma psubst_ty_lemma: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
326 |
fixes \<theta>::"Subst" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
327 |
and X::"tvar" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
328 |
and T'::"ty" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
329 |
and T::"ty" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
330 |
assumes a: "X\<sharp>\<theta>" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
331 |
shows "\<theta><T[X::=T']> = (\<theta><T>)[X::=\<theta><T'>]" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
332 |
using a |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
333 |
apply(nominal_induct T avoiding: \<theta> X T' rule: ty.strong_induct) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
334 |
apply(auto simp add: ty.inject lookup_fresh) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
335 |
apply(rule sym) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
336 |
apply(rule subst_forget_ty) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
337 |
apply(rule fresh_lookup) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
338 |
apply(simp_all add: fresh_atm) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
339 |
done |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
340 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
341 |
lemma general_preserved: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
342 |
fixes \<theta>::"Subst" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
343 |
assumes a: "T \<prec> S" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
344 |
shows "\<theta><T> \<prec> \<theta><S>" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
345 |
using a |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
346 |
apply(nominal_induct T S avoiding: \<theta> rule: inst.strong_induct) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
347 |
apply(auto)[1] |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
348 |
apply(simp add: psubst_ty_lemma) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
349 |
apply(rule_tac I_All) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
350 |
apply(simp add: fresh_psubst_ty) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
351 |
apply(simp) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
352 |
done |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
353 |
|
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
354 |
|
63167 | 355 |
text\<open>typing judgements\<close> |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
356 |
inductive |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
357 |
typing :: "Ctxt \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
358 |
where |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
359 |
T_VAR[intro]: "\<lbrakk>valid \<Gamma>; (x,S)\<in>set \<Gamma>; T \<prec> S\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
360 |
| T_APP[intro]: "\<lbrakk>\<Gamma> \<turnstile> t\<^sub>1 : T\<^sub>1\<rightarrow>T\<^sub>2; \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t\<^sub>1 t\<^sub>2 : T\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
361 |
| T_LAM[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,Ty T\<^sub>1)#\<Gamma>) \<turnstile> t : T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T\<^sub>1\<rightarrow>T\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
362 |
| T_LET[intro]: "\<lbrakk>x\<sharp>\<Gamma>; \<Gamma> \<turnstile> t\<^sub>1 : T\<^sub>1; ((x,close \<Gamma> T\<^sub>1)#\<Gamma>) \<turnstile> t\<^sub>2 : T\<^sub>2; set (ftv T\<^sub>1 - ftv \<Gamma>) \<sharp>* T\<^sub>2\<rbrakk> |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
363 |
\<Longrightarrow> \<Gamma> \<turnstile> Let x be t\<^sub>1 in t\<^sub>2 : T\<^sub>2" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
364 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
365 |
equivariance typing[tvar] |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
366 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
367 |
lemma fresh_tvar_trm: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
368 |
fixes X::"tvar" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
369 |
and t::"trm" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
370 |
shows "X\<sharp>t" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
371 |
by (nominal_induct t rule: trm.strong_induct) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
372 |
(simp_all add: fresh_atm abs_fresh) |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
373 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
374 |
lemma ftv_ty: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
375 |
fixes T::"ty" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
376 |
shows "supp T = set (ftv T)" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
377 |
by (nominal_induct T rule: ty.strong_induct) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
378 |
(simp_all add: ty.supp supp_atm) |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
379 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
380 |
lemma ftv_tyS: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
381 |
fixes S::"tyS" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
382 |
shows "supp S = set (ftv S)" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
383 |
by (nominal_induct S rule: tyS.strong_induct) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
384 |
(auto simp add: tyS.supp abs_supp ftv_ty) |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
385 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
386 |
lemma ftv_Ctxt: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
387 |
fixes \<Gamma>::"Ctxt" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
388 |
shows "supp \<Gamma> = set (ftv \<Gamma>)" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
389 |
apply (induct \<Gamma>) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
390 |
apply (simp_all add: supp_list_nil supp_list_cons) |
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
53015
diff
changeset
|
391 |
apply (rename_tac a \<Gamma>') |
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
392 |
apply (case_tac a) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
393 |
apply (simp add: supp_prod supp_atm ftv_tyS) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
394 |
done |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
395 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
396 |
lemma ftv_tvars: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
397 |
fixes Tvs::"tvar list" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
398 |
shows "supp Tvs = set Tvs" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
399 |
by (induct Tvs) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
400 |
(simp_all add: supp_list_nil supp_list_cons supp_atm) |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
401 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
402 |
lemma difference_supp: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
403 |
fixes xs ys::"tvar list" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
404 |
shows "((supp (xs - ys))::tvar set) = supp xs - supp ys" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
405 |
by (induct xs) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
406 |
(auto simp add: supp_list_nil supp_list_cons ftv_tvars) |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
407 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
408 |
lemma set_supp_eq: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
409 |
fixes xs::"tvar list" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
410 |
shows "set xs = supp xs" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
411 |
by (induct xs) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
412 |
(simp_all add: supp_list_nil supp_list_cons supp_atm) |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
413 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
414 |
nominal_inductive2 typing |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
415 |
avoids T_LET: "set (ftv T\<^sub>1 - ftv \<Gamma>)" |
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
416 |
apply (simp add: fresh_star_def fresh_def ftv_Ctxt) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
417 |
apply (simp add: fresh_star_def fresh_tvar_trm) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
418 |
apply assumption |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
419 |
apply simp |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
420 |
done |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
421 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
422 |
lemma perm_fresh_fresh_aux: |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
423 |
"\<forall>(x,y)\<in>set (pi::tvar prm). x \<sharp> z \<and> y \<sharp> z \<Longrightarrow> pi \<bullet> (z::'a::pt_tvar) = z" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
424 |
apply (induct pi rule: rev_induct) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
425 |
apply simp |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
426 |
apply (simp add: split_paired_all pt_tvar2) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
427 |
apply (frule_tac x="(a, b)" in bspec) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
428 |
apply simp |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
429 |
apply (simp add: perm_fresh_fresh) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
430 |
done |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
431 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
432 |
lemma freshs_mem: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
433 |
fixes S::"tvar set" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
434 |
assumes "x \<in> S" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
435 |
and "S \<sharp>* z" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
436 |
shows "x \<sharp> z" |
41893 | 437 |
using assms by (simp add: fresh_star_def) |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
438 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
439 |
lemma fresh_gen_set: |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
440 |
fixes X::"tvar" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
441 |
and Xs::"tvar list" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
442 |
assumes asm: "X\<in>set Xs" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
443 |
shows "X\<sharp>gen T Xs" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
444 |
using asm |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
445 |
apply(induct Xs) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
446 |
apply(simp) |
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
53015
diff
changeset
|
447 |
apply(rename_tac a Xs') |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
448 |
apply(case_tac "X=a") |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
449 |
apply(simp add: abs_fresh) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
450 |
apply(simp add: abs_fresh) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
451 |
done |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
452 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
453 |
lemma close_fresh: |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
454 |
fixes \<Gamma>::"Ctxt" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
455 |
shows "\<forall>(X::tvar)\<in>set ((ftv T) - (ftv \<Gamma>)). X\<sharp>(close \<Gamma> T)" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
456 |
by (simp add: fresh_gen_set) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
457 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
458 |
lemma gen_supp: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
459 |
shows "(supp (gen T Xs)::tvar set) = supp T - supp Xs" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
460 |
by (induct Xs) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
461 |
(auto simp add: supp_list_nil supp_list_cons tyS.supp abs_supp supp_atm) |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
462 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
463 |
lemma minus_Int_eq: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
464 |
shows "T - (T - U) = T \<inter> U" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
465 |
by blast |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
466 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
467 |
lemma close_supp: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
468 |
shows "supp (close \<Gamma> T) = set (ftv T) \<inter> set (ftv \<Gamma>)" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
469 |
apply (simp add: gen_supp difference_supp ftv_ty ftv_Ctxt) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
470 |
apply (simp only: set_supp_eq minus_Int_eq) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
471 |
done |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
472 |
|
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
473 |
lemma better_T_LET: |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
474 |
assumes x: "x\<sharp>\<Gamma>" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
475 |
and t1: "\<Gamma> \<turnstile> t\<^sub>1 : T\<^sub>1" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
476 |
and t2: "((x,close \<Gamma> T\<^sub>1)#\<Gamma>) \<turnstile> t\<^sub>2 : T\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
477 |
shows "\<Gamma> \<turnstile> Let x be t\<^sub>1 in t\<^sub>2 : T\<^sub>2" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
478 |
proof - |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
479 |
have fin: "finite (set (ftv T\<^sub>1 - ftv \<Gamma>))" by simp |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
480 |
obtain pi where pi1: "(pi \<bullet> set (ftv T\<^sub>1 - ftv \<Gamma>)) \<sharp>* (T\<^sub>2, \<Gamma>)" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
481 |
and pi2: "set pi \<subseteq> set (ftv T\<^sub>1 - ftv \<Gamma>) \<times> (pi \<bullet> set (ftv T\<^sub>1 - ftv \<Gamma>))" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
482 |
by (rule at_set_avoiding [OF at_tvar_inst fin fs_tvar1, of "(T\<^sub>2, \<Gamma>)"]) |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
483 |
from pi1 have pi1': "(pi \<bullet> set (ftv T\<^sub>1 - ftv \<Gamma>)) \<sharp>* \<Gamma>" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
484 |
by (simp add: fresh_star_prod) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
485 |
have Gamma_fresh: "\<forall>(x,y)\<in>set pi. x \<sharp> \<Gamma> \<and> y \<sharp> \<Gamma>" |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
486 |
apply (rule ballI) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
487 |
apply (simp add: split_paired_all) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
488 |
apply (drule subsetD [OF pi2]) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
489 |
apply (erule SigmaE) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
490 |
apply (drule freshs_mem [OF _ pi1']) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
491 |
apply (simp add: ftv_Ctxt [symmetric] fresh_def) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
492 |
done |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
493 |
have close_fresh': "\<forall>(x, y)\<in>set pi. x \<sharp> close \<Gamma> T\<^sub>1 \<and> y \<sharp> close \<Gamma> T\<^sub>1" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
494 |
apply (rule ballI) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
495 |
apply (simp add: split_paired_all) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
496 |
apply (drule subsetD [OF pi2]) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
497 |
apply (erule SigmaE) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
498 |
apply (drule bspec [OF close_fresh]) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
499 |
apply (drule freshs_mem [OF _ pi1']) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
500 |
apply (simp add: fresh_def close_supp ftv_Ctxt) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
501 |
done |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
502 |
note x |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
503 |
moreover from Gamma_fresh perm_boolI [OF t1, of pi] |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
504 |
have "\<Gamma> \<turnstile> t\<^sub>1 : pi \<bullet> T\<^sub>1" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
505 |
by (simp add: perm_fresh_fresh_aux eqvts fresh_tvar_trm) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
506 |
moreover from t2 close_fresh' |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
507 |
have "(x,(pi \<bullet> close \<Gamma> T\<^sub>1))#\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
508 |
by (simp add: perm_fresh_fresh_aux) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
509 |
with Gamma_fresh have "(x,close \<Gamma> (pi \<bullet> T\<^sub>1))#\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
510 |
by (simp add: close_eqvt perm_fresh_fresh_aux) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
511 |
moreover from pi1 Gamma_fresh |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
41893
diff
changeset
|
512 |
have "set (ftv (pi \<bullet> T\<^sub>1) - ftv \<Gamma>) \<sharp>* T\<^sub>2" |
28655
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
513 |
by (simp only: eqvts fresh_star_prod perm_fresh_fresh_aux) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
514 |
ultimately show ?thesis by (rule T_LET) |
2822c56dd1cf
Example for using the generalized version of nominal_inductive.
berghofe
parents:
26195
diff
changeset
|
515 |
qed |
26195 | 516 |
|
32137
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
517 |
lemma ftv_ty_subst: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
518 |
fixes T::"ty" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
519 |
and \<theta>::"Subst" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
520 |
and X Y ::"tvar" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
521 |
assumes a1: "X \<in> set (ftv T)" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
522 |
and a2: "Y \<in> set (ftv (lookup \<theta> X))" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
523 |
shows "Y \<in> set (ftv (\<theta><T>))" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
524 |
using a1 a2 |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
525 |
by (nominal_induct T rule: ty.strong_induct) (auto) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
526 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
527 |
lemma ftv_tyS_subst: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
528 |
fixes S::"tyS" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
529 |
and \<theta>::"Subst" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
530 |
and X Y::"tvar" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
531 |
assumes a1: "X \<in> set (ftv S)" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
532 |
and a2: "Y \<in> set (ftv (lookup \<theta> X))" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
533 |
shows "Y \<in> set (ftv (\<theta><S>))" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
534 |
using a1 a2 |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
535 |
by (nominal_induct S avoiding: \<theta> Y rule: tyS.strong_induct) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
536 |
(auto simp add: ftv_ty_subst fresh_atm) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
537 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
538 |
lemma ftv_Ctxt_subst: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
539 |
fixes \<Gamma>::"Ctxt" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
540 |
and \<theta>::"Subst" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
541 |
assumes a1: "X \<in> set (ftv \<Gamma>)" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
542 |
and a2: "Y \<in> set (ftv (lookup \<theta> X))" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
543 |
shows "Y \<in> set (ftv (\<theta><\<Gamma>>))" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
544 |
using a1 a2 |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
545 |
by (induct \<Gamma>) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
546 |
(auto simp add: ftv_tyS_subst) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
547 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
548 |
lemma gen_preserved1: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
549 |
assumes asm: "Xs \<sharp>* \<theta>" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
550 |
shows "\<theta><gen T Xs> = gen (\<theta><T>) Xs" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
551 |
using asm |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
552 |
by (induct Xs) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
553 |
(auto simp add: fresh_star_def) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
554 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
555 |
lemma gen_preserved2: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
556 |
fixes T::"ty" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
557 |
and \<Gamma>::"Ctxt" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
558 |
assumes asm: "((ftv T) - (ftv \<Gamma>)) \<sharp>* \<theta>" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
559 |
shows "((ftv (\<theta><T>)) - (ftv (\<theta><\<Gamma>>))) = ((ftv T) - (ftv \<Gamma>))" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
560 |
using asm |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
561 |
apply(nominal_induct T rule: ty.strong_induct) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
562 |
apply(auto simp add: fresh_star_def) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
563 |
apply(simp add: lookup_fresh) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
564 |
apply(simp add: ftv_Ctxt[symmetric]) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
565 |
apply(fold fresh_def) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
566 |
apply(rule fresh_psubst_Ctxt) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
567 |
apply(assumption) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
568 |
apply(assumption) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
569 |
apply(rule difference_supset) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
570 |
apply(auto) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
571 |
apply(simp add: ftv_Ctxt_subst) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
572 |
done |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
573 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
574 |
lemma close_preserved: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
575 |
fixes \<Gamma>::"Ctxt" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
576 |
assumes asm: "((ftv T) - (ftv \<Gamma>)) \<sharp>* \<theta>" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
577 |
shows "\<theta><close \<Gamma> T> = close (\<theta><\<Gamma>>) (\<theta><T>)" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
578 |
using asm |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
579 |
by (simp add: gen_preserved1 gen_preserved2) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
580 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
581 |
lemma var_fresh_for_ty: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
582 |
fixes x::"var" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
583 |
and T::"ty" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
584 |
shows "x\<sharp>T" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
585 |
by (nominal_induct T rule: ty.strong_induct) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
586 |
(simp_all add: fresh_atm) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
587 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
588 |
lemma var_fresh_for_tyS: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
589 |
fixes x::"var" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
590 |
and S::"tyS" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
591 |
shows "x\<sharp>S" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
592 |
by (nominal_induct S rule: tyS.strong_induct) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
593 |
(simp_all add: abs_fresh var_fresh_for_ty) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
594 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
595 |
lemma psubst_fresh_Ctxt: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
596 |
fixes x::"var" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
597 |
and \<Gamma>::"Ctxt" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
598 |
and \<theta>::"Subst" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
599 |
shows "x\<sharp>\<theta><\<Gamma>> = x\<sharp>\<Gamma>" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
600 |
by (induct \<Gamma>) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
601 |
(auto simp add: fresh_list_cons fresh_list_nil fresh_prod var_fresh_for_tyS) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
602 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
603 |
lemma psubst_valid: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
604 |
fixes \<theta>::Subst |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
605 |
and \<Gamma>::Ctxt |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
606 |
assumes a: "valid \<Gamma>" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
607 |
shows "valid (\<theta><\<Gamma>>)" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
608 |
using a |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
609 |
by (induct) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
610 |
(auto simp add: psubst_fresh_Ctxt) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
611 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
612 |
lemma psubst_in: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
613 |
fixes \<Gamma>::"Ctxt" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
614 |
and \<theta>::"Subst" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
615 |
and pi::"tvar prm" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
616 |
and S::"tyS" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
617 |
assumes a: "(x,S)\<in>set \<Gamma>" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
618 |
shows "(x,\<theta><S>)\<in>set (\<theta><\<Gamma>>)" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
619 |
using a |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
620 |
by (induct \<Gamma>) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
621 |
(auto simp add: calc_atm) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
622 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
623 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
624 |
lemma typing_preserved: |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
625 |
fixes \<theta>::"Subst" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
626 |
and pi::"tvar prm" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
627 |
assumes a: "\<Gamma> \<turnstile> t : T" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
628 |
shows "(\<theta><\<Gamma>>) \<turnstile> t : (\<theta><T>)" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
629 |
using a |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
630 |
proof (nominal_induct \<Gamma> t T avoiding: \<theta> rule: typing.strong_induct) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
631 |
case (T_VAR \<Gamma> x S T) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
632 |
have a1: "valid \<Gamma>" by fact |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
633 |
have a2: "(x, S) \<in> set \<Gamma>" by fact |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
634 |
have a3: "T \<prec> S" by fact |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
635 |
have "valid (\<theta><\<Gamma>>)" using a1 by (simp add: psubst_valid) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
636 |
moreover |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
637 |
have "(x,\<theta><S>)\<in>set (\<theta><\<Gamma>>)" using a2 by (simp add: psubst_in) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
638 |
moreover |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
639 |
have "\<theta><T> \<prec> \<theta><S>" using a3 by (simp add: general_preserved) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
640 |
ultimately show "(\<theta><\<Gamma>>) \<turnstile> Var x : (\<theta><T>)" by (simp add: typing.T_VAR) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
641 |
next |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
642 |
case (T_APP \<Gamma> t1 T1 T2 t2) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
643 |
have "\<theta><\<Gamma>> \<turnstile> t1 : \<theta><T1 \<rightarrow> T2>" by fact |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
644 |
then have "\<theta><\<Gamma>> \<turnstile> t1 : (\<theta><T1>) \<rightarrow> (\<theta><T2>)" by simp |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
645 |
moreover |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
646 |
have "\<theta><\<Gamma>> \<turnstile> t2 : \<theta><T1>" by fact |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
647 |
ultimately show "\<theta><\<Gamma>> \<turnstile> App t1 t2 : \<theta><T2>" by (simp add: typing.T_APP) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
648 |
next |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
649 |
case (T_LAM x \<Gamma> T1 t T2) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
650 |
fix pi::"tvar prm" and \<theta>::"Subst" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
651 |
have "x\<sharp>\<Gamma>" by fact |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
652 |
then have "x\<sharp>\<theta><\<Gamma>>" by (simp add: psubst_fresh_Ctxt) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
653 |
moreover |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
654 |
have "\<theta><((x, Ty T1)#\<Gamma>)> \<turnstile> t : \<theta><T2>" by fact |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
655 |
then have "((x, Ty (\<theta><T1>))#(\<theta><\<Gamma>>)) \<turnstile> t : \<theta><T2>" by (simp add: calc_atm) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
656 |
ultimately show "\<theta><\<Gamma>> \<turnstile> Lam [x].t : \<theta><T1 \<rightarrow> T2>" by (simp add: typing.T_LAM) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
657 |
next |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
658 |
case (T_LET x \<Gamma> t1 T1 t2 T2) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
659 |
have vc: "((ftv T1) - (ftv \<Gamma>)) \<sharp>* \<theta>" by fact |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
660 |
have "x\<sharp>\<Gamma>" by fact |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
661 |
then have a1: "x\<sharp>\<theta><\<Gamma>>" by (simp add: calc_atm psubst_fresh_Ctxt) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
662 |
have a2: "\<theta><\<Gamma>> \<turnstile> t1 : \<theta><T1>" by fact |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
663 |
have a3: "\<theta><((x, close \<Gamma> T1)#\<Gamma>)> \<turnstile> t2 : \<theta><T2>" by fact |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
664 |
from a2 a3 show "\<theta><\<Gamma>> \<turnstile> Let x be t1 in t2 : \<theta><T2>" |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
665 |
apply - |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
666 |
apply(rule better_T_LET) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
667 |
apply(rule a1) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
668 |
apply(rule a2) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
669 |
apply(simp add: close_preserved vc) |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
670 |
done |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
671 |
qed |
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
672 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
673 |
|
3b260527fc11
tuned proofs and added some lemmas
Christian Urban <urbanc@in.tum.de>
parents:
29608
diff
changeset
|
674 |
|
26195 | 675 |
end |