equal
deleted
inserted
replaced
7 nominal_datatype lam = |
7 nominal_datatype lam = |
8 Var "name" |
8 Var "name" |
9 | App "lam" "lam" |
9 | App "lam" "lam" |
10 | Lam x::"name" l::"lam" bind x in l |
10 | Lam x::"name" l::"lam" bind x in l |
11 |
11 |
|
12 thm lam.fv |
|
13 thm lam.supp |
12 lemmas supp_fn' = lam.fv[simplified lam.supp] |
14 lemmas supp_fn' = lam.fv[simplified lam.supp] |
13 |
15 |
14 declare lam.perm[eqvt] |
16 declare lam.perm[eqvt] |
15 |
17 |
16 section {* Strong Induction Principles*} |
18 section {* Strong Induction Principles*} |
149 | v2[intro]: "\<lbrakk>valid' \<Gamma>;atom x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid' ((x,T)#\<Gamma>)" |
151 | v2[intro]: "\<lbrakk>valid' \<Gamma>;atom x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid' ((x,T)#\<Gamma>)" |
150 | t'_Var[intro]: "\<lbrakk>valid' \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Var x : T" |
152 | t'_Var[intro]: "\<lbrakk>valid' \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Var x : T" |
151 | t'_App[intro]: "\<lbrakk>\<Gamma> |\<Turnstile> t1 : T1\<rightarrow>T2; \<Gamma> |\<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> App t1 t2 : T2" |
153 | t'_App[intro]: "\<lbrakk>\<Gamma> |\<Turnstile> t1 : T1\<rightarrow>T2; \<Gamma> |\<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> App t1 t2 : T2" |
152 | t'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> |\<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Lam x t : T1\<rightarrow>T2" |
154 | t'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> |\<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Lam x t : T1\<rightarrow>T2" |
153 |
155 |
154 use "../../Nominal-General/nominal_eqvt.ML" |
|
155 |
|
156 equivariance valid |
156 equivariance valid |
157 equivariance typing |
157 equivariance typing |
|
158 equivariance typing' |
|
159 equivariance typing2' |
|
160 equivariance typing'' |
158 |
161 |
159 thm valid.eqvt |
162 thm valid.eqvt |
160 thm typing.eqvt |
163 thm typing.eqvt |
161 thm eqvts |
164 thm eqvts |
162 thm eqvts_raw |
165 thm eqvts_raw |
163 |
166 |
164 equivariance typing' |
|
165 equivariance typing2' |
|
166 equivariance typing'' |
|
167 |
|
168 ML {* |
|
169 fun mk_minus p = |
|
170 Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p |
|
171 *} |
|
172 |
167 |
173 inductive |
168 inductive |
174 tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" |
169 tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" |
175 for r :: "('a \<Rightarrow> 'a \<Rightarrow> bool)" |
170 for r :: "('a \<Rightarrow> 'a \<Rightarrow> bool)" |
176 where |
171 where |