Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/Lambda.thy
changeset 1814 01ae96fa4bf9
parent 1811 ae176476b525
child 1816 56cebe7f8e24
equal deleted inserted replaced
1812:2e849bc2163a 1814:01ae96fa4bf9 
   130       [ rtac (Drule.instantiate' [] [SOME @{cterm "- p::perm"}] @{thm permute_boolE}),
 
   130       [ rtac (Drule.instantiate' [] [SOME @{cterm "- p::perm"}] @{thm permute_boolE}),
 
   131         Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [],
 
   131         Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [],
 
   132         atac ])
 
   132         atac ])
 
   133 *}
 
   133 *}
 
   134 
   134 
   135 ML {* try hd [1] *}
 
       
   136 
       
   137 ML {*
 
       
   138 Skip_Proof.cheat_tac
 
       
   139 *}
 
       
   140 
       
   141 
       
   142 lemma [eqvt]:
 
   135 lemma [eqvt]:
 
   143   assumes a: "valid Gamma" 
   136   assumes a: "valid Gamma" 
   144   shows "valid (p \<bullet> Gamma)"
 
   137   shows "valid (p \<bullet> Gamma)"
 
   145 using a
 
   138 using a
 
   146 apply(induct)
 
   139 apply(induct)
 
   153 
   146 
   154 inductive
 
   147 inductive
 
   155   typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
   148   typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
   156 where
 
   149 where
 
   157     t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
 
   150     t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
 
   158   | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
 
   151   | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
 
   159   | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> 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"
 
       
   153 
       
   154 thm typing.induct
 
       
   155 ML {* Inductive.get_monos @{context} *}
 
   160 
   156 
   161 lemma uu[eqvt]:
 
   157 lemma uu[eqvt]:
 
   162   assumes a: "Gamma \<turnstile> t : T" 
   158   assumes a: "Gamma \<turnstile> t : T" 
   163   shows "(p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"
 
   159   shows "(p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"
 
   164 using a
 
   160 using a
 
   165 apply(induct)
 
   161 apply(induct)
 
   166 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
 
   162 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
 
       
   163 apply(perm_strict_simp)
 
       
   164 apply(rule typing.intros)
 
       
   165 apply(rule conj_mono[THEN mp])
 
       
   166 prefer 3
 
       
   167 apply(assumption)
 
       
   168 apply(rule impI)
 
       
   169 prefer 2
 
       
   170 apply(rule impI)
 
       
   171 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
 
       
   172 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
 
       
   173 done
 
       
   174 
       
   175 inductive
 
       
   176   typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
       
   177 where
 
       
   178     t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
 
       
   179   | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
 
       
   180   | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"
 
       
   181 
       
   182 lemma uu[eqvt]:
 
       
   183   assumes a: "Gamma \<turnstile> t : T" 
       
   184   shows "(p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"
 
       
   185 using a
 
       
   186 apply(induct)
 
       
   187 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
 
   167 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
 
   188 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
 
   168 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
 
   189 apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
 
   169 done
 
   190 done
 
   170 
   191 
   171 thm eqvts
 
   192 thm eqvts
 
   172 thm eqvts_raw
 
   193 thm eqvts_raw
 
   173 
   194 
   174 declare permute_lam_raw.simps[eqvt]
 
   195 declare permute_lam_raw.simps[eqvt]
 
   175 
   196 thm alpha_gen_real_eqvt
 
   176 thm alpha_gen_real_eqvt[no_vars]
 
   197 (*declare alpha_gen_real_eqvt[eqvt]*)
 
   177 
       
   178 lemma temporary:
 
       
   179   shows "(p \<bullet> (bs, x) \<approx>gen R f q (cs, y)) = (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
 
       
   180 apply(simp only: permute_bool_def)
 
       
   181 apply(rule iffI)
 
       
   182 apply(rule alpha_gen_real_eqvt)
 
       
   183 apply(assumption)
 
       
   184 apply(drule_tac p="-p" in alpha_gen_real_eqvt(1))
 
       
   185 apply(simp)
 
       
   186 done
 
       
   187 
       
   188 lemma temporary_raw:
 
       
   189   shows "(p \<bullet> alpha_gen) \<equiv> alpha_gen"
 
       
   190 sorry
 
       
   191 
       
   192 declare temporary_raw[eqvt_raw]
 
       
   193 
   198 
   194 lemma
 
   199 lemma
 
   195   assumes a: "alpha_lam_raw t1 t2"
 
   200   assumes a: "alpha_lam_raw t1 t2"
 
   196   shows "alpha_lam_raw (p \<bullet> t1) (p \<bullet> t2)"
 
   201   shows "alpha_lam_raw (p \<bullet> t1) (p \<bullet> t2)"
 
   197 using a
 
   202 using a
 
   198 apply(induct)
 
   203 apply(induct)
 
       
   204 apply(tactic {* my_tac @{context} @{thms alpha_lam_raw.intros} 1 *})
 
   199 apply(tactic {* my_tac @{context} @{thms alpha_lam_raw.intros} 1 *})
 
   205 apply(tactic {* my_tac @{context} @{thms alpha_lam_raw.intros} 1 *})
 
   200 apply(perm_strict_simp)
 
   206 apply(perm_strict_simp)
 
   201 apply(rule alpha_lam_raw.intros)
 
   207 apply(rule alpha_lam_raw.intros)
 
   202 apply(simp)
 
   208 apply(simp)
 
   203 apply(perm_strict_simp)
 
   209 apply(perm_strict_simp)
nominal2