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.
LamEx.thy
changeset 376 e99c0334d8bf
parent 370 09e28d4c19aa
child 378 86fba2c4eeef
equal deleted inserted replaced
375:f7dee6e808eb 376:e99c0334d8bf 
   117 lemma pi_lam_com:
 
   117 lemma pi_lam_com:
 
   118   fixes pi::"'x prm"
 
   118   fixes pi::"'x prm"
 
   119   shows "(pi\<bullet>rLam a t) \<approx> rLam (pi\<bullet>a) (pi\<bullet>t)"
 
   119   shows "(pi\<bullet>rLam a t) \<approx> rLam (pi\<bullet>a) (pi\<bullet>t)"
 
   120   sorry
 
   120   sorry
 
   121 
   121 
   122 lemma fv_var:
 
       
   123   shows "fv (Var a) = {a}"
 
       
   124 sorry
 
       
   125 
       
   126 lemma fv_app:
 
       
   127   shows "fv (App t1 t2) = (fv t1) \<union> (fv t2)"
 
       
   128 sorry
 
       
   129 
       
   130 lemma fv_lam:
 
       
   131   shows "fv (Lam a t) = (fv t) - {a}"
 
       
   132 sorry
 
       
   133 
       
   134 lemma real_alpha:
 
   122 lemma real_alpha:
 
   135   assumes "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s"
 
   123   assumes "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s"
 
   136   shows "Lam a t = Lam b s"
 
   124   shows "Lam a t = Lam b s"
 
   137 sorry
 
   125 sorry
 
   138 
   126 
   192 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   180 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   193 ML {* val consts = lookup_quot_consts defs *}
 
   181 ML {* val consts = lookup_quot_consts defs *}
 
   194 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
 
   182 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
 
   195 ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *}
 
   183 ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *}
 
   196 
   184 
   197 lemma "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
 
   185 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
 
   198 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *})
 
   186 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *})
 
   199 done
 
   187 done
 
   200 
   188 
   201 ML {* val pi_app = lift_thm_lam @{context} @{thm pi_app_com} *}
 
   189 lemma pi_app: "(pi\<Colon>('x \<times> 'x) list) \<bullet> App (x\<Colon>lam) (xa\<Colon>lam) = App (pi \<bullet> x) (pi \<bullet> xa)"
 
   202 lemma "(pi\<Colon>('x \<times> 'x) list) \<bullet> App (x\<Colon>lam) (xa\<Colon>lam) = App (pi \<bullet> x) (pi \<bullet> xa)"
 
       
   203 apply (tactic {* lift_tac_lam @{context} @{thm pi_app_com} 1 *})
 
   190 apply (tactic {* lift_tac_lam @{context} @{thm pi_app_com} 1 *})
 
   204 done
 
   191 done
 
   205 ML {* val pi_lam = lift_thm_lam @{context} @{thm pi_lam_com} *}
 
   192 
   206 lemma "(pi\<Colon>('x \<times> 'x) list) \<bullet> Lam (a\<Colon>name) (x\<Colon>lam) = Lam (pi \<bullet> a) (pi \<bullet> x)"
 
   193 lemma pi_lam: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Lam (a\<Colon>name) (x\<Colon>lam) = Lam (pi \<bullet> a) (pi \<bullet> x)"
 
   207 apply (tactic {* lift_tac_lam @{context} @{thm pi_lam_com} 1 *})
 
   194 apply (tactic {* lift_tac_lam @{context} @{thm pi_lam_com} 1 *})
 
   208 done
 
   195 done
 
   209 
   196 
   210 ML {* val fv_var = lift_thm_lam @{context} @{thm rfv_var} *}
 
   197 lemma fv_var: "fv (Var (a\<Colon>name)) = {a}"
 
   211 lemma "\<forall>a. fv (Var (a\<Colon>name)) = {a}"
 
       
   212 apply (tactic {* lift_tac_lam @{context} @{thm rfv_var} 1 *})
 
   198 apply (tactic {* lift_tac_lam @{context} @{thm rfv_var} 1 *})
 
   213 done
 
   199 done
 
   214 ML {* val fv_app = lift_thm_lam @{context} @{thm rfv_app} *}
 
   200 
   215 lemma "fv (App (x\<Colon>lam) (xa\<Colon>lam)) = fv x \<union> fv xa"
 
   201 lemma fv_app: "fv (App (x\<Colon>lam) (xa\<Colon>lam)) = fv x \<union> fv xa"
 
   216 (*apply (tactic {* lift_tac_lam @{context} @{thm rfv_app} 1 *})*)
 
   202 apply (tactic {* lift_tac_lam @{context} @{thm rfv_app} 1 *})
 
   217 sorry
 
   203 done
 
   218 ML {* val fv_lam = lift_thm_lam @{context} @{thm rfv_lam} *}
 
   204 
   219 lemma "fv (Lam (a\<Colon>name) (x\<Colon>lam)) = fv x - {a}"
 
   205 lemma fv_lam: "fv (Lam (a\<Colon>name) (x\<Colon>lam)) = fv x - {a}"
 
   220 (*apply (tactic {* lift_tac_lam @{context} @{thm rfv_lam} 1 *})*)
 
   206 apply (tactic {* lift_tac_lam @{context} @{thm rfv_lam} 1 *})
 
   221 sorry
 
   207 done
 
   222 
   208 
   223 ML {* val a1 = lift_thm_lam @{context} @{thm a1} *}
 
   209 lemma a1: "(a\<Colon>name) = (b\<Colon>name) \<Longrightarrow> Var a = Var b"
 
   224 lemma "(a\<Colon>name) = (b\<Colon>name) \<Longrightarrow> Var a = Var b"
 
       
   225 apply (tactic {* lift_tac_lam @{context} @{thm a1} 1 *})
 
   210 apply (tactic {* lift_tac_lam @{context} @{thm a1} 1 *})
 
   226 done
 
   211 done
 
   227 ML {* val a2 = lift_thm_lam @{context} @{thm a2} *}
 
   212 
   228 lemma "\<lbrakk>(x\<Colon>lam) = (xa\<Colon>lam); (xb\<Colon>lam) = (xc\<Colon>lam)\<rbrakk> \<Longrightarrow> App x xb = App xa xc"
 
   213 lemma a2: "\<lbrakk>(x\<Colon>lam) = (xa\<Colon>lam); (xb\<Colon>lam) = (xc\<Colon>lam)\<rbrakk> \<Longrightarrow> App x xb = App xa xc"
 
   229 apply (tactic {* lift_tac_lam @{context} @{thm a2} 1 *})
 
   214 apply (tactic {* lift_tac_lam @{context} @{thm a2} 1 *})
 
   230 done
 
   215 done
 
   231 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *}
 
   216 
   232 lemma "\<lbrakk>(x\<Colon>lam) = [(a\<Colon>name, b\<Colon>name)] \<bullet> (xa\<Colon>lam); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> Lam a x = Lam b xa"
 
   217 lemma a3: "\<lbrakk>(x\<Colon>lam) = [(a\<Colon>name, b\<Colon>name)] \<bullet> (xa\<Colon>lam); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> Lam a x = Lam b xa"
 
   233 (*apply (tactic {* lift_tac_lam @{context} @{thm a3} 1 *})*)
 
   218 apply (tactic {* lift_tac_lam @{context} @{thm a3} 1 *})
 
   234 sorry
 
   219 done
 
   235 
   220 
   236 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *}
 
   221 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *}
 
   237 lemma "\<lbrakk>(x\<Colon>lam) = (xa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. \<lbrakk>x = Var a; xa = Var b; a = b\<rbrakk> \<Longrightarrow> P\<Colon>bool;
 
   222 lemma "\<lbrakk>(x\<Colon>lam) = (xa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. \<lbrakk>x = Var a; xa = Var b; a = b\<rbrakk> \<Longrightarrow> P\<Colon>bool;
 
   238      \<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = App x xb; xa = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
 
   223      \<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = App x xb; xa = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
 
   239      \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam. \<lbrakk>x = Lam a x; xa = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk>
 
   224      \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam. \<lbrakk>x = Lam a x; xa = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk>
 
   240     \<Longrightarrow> P"
 
   225     \<Longrightarrow> P"
 
   241 (* apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *}) *)
 
   226 apply (tactic {* procedure_tac @{thm alpha.cases} @{context} 1 *})
 
   242 sorry
 
   227 sorry
 
   243 ML {* val alpha_induct = lift_thm_lam @{context} @{thm alpha.induct} *}
 
   228 ML {* val alpha_induct = lift_thm_lam @{context} @{thm alpha.induct} *}
 
   244 lemma "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> bool) (Var a) (Var b);
 
   229 lemma "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> bool) (Var a) (Var b);
 
   245      \<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
 
   230      \<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
 
   246      \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam.
 
   231      \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam.
 
   247         \<lbrakk>x = [(a, b)] \<bullet> xa; qxb x ([(a, b)] \<bullet> xa); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> qxb (Lam a x) (Lam b xa)\<rbrakk>
 
   232         \<lbrakk>x = [(a, b)] \<bullet> xa; qxb x ([(a, b)] \<bullet> xa); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> qxb (Lam a x) (Lam b xa)\<rbrakk>
 
   248     \<Longrightarrow> qxb qx qxa"
 
   233     \<Longrightarrow> qxb qx qxa"
 
   249 (* apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *}) *)
 
   234 (* apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *}) *)
 
   250 sorry
 
   235 sorry
 
   251 
   236 
   252 lemma "(Var a = Var b) = (a = b)"
 
   237 lemma var_inject: "(Var a = Var b) = (a = b)"
 
   253 apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *})
 
   238 apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *})
 
   254 done
 
   239 done
 
   255 
       
   256 local_setup {*
 
       
   257   Quotient.note (@{binding "pi_var"}, pi_var) #> snd #>
 
       
   258   Quotient.note (@{binding "pi_app"}, pi_app) #> snd #>
 
       
   259   Quotient.note (@{binding "pi_lam"}, pi_lam) #> snd #>
 
       
   260   Quotient.note (@{binding "a1"}, a1) #> snd #>
 
       
   261   Quotient.note (@{binding "a2"}, a2) #> snd #>
 
       
   262   Quotient.note (@{binding "a3"}, a3) #> snd #>
 
       
   263   Quotient.note (@{binding "alpha_cases"}, alpha_cases) #> snd #>
 
       
   264   Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd #>
 
       
   265   Quotient.note (@{binding "var_inject"}, var_inject) #> snd
 
       
   266 *}
 
       
   267 
       
   268 thm alpha.cases
 
       
   269 thm alpha_cases
 
       
   270 thm alpha.induct
 
       
   271 thm alpha_induct
 
       
   272 
   240 
   273 lemma var_supp:
 
   241 lemma var_supp:
 
   274   shows "supp (Var a) = ((supp a)::name set)"
 
   242   shows "supp (Var a) = ((supp a)::name set)"
 
   275   apply(simp add: supp_def)
 
   243   apply(simp add: supp_def)
 
   276   apply(simp add: pi_var)
 
   244   apply(simp add: pi_var)
 
   352     ]);
 
   320     ]);
 
   353 *}*)
 
   321 *}*)
 
   354 ML_prf {*
 
   322 ML_prf {*
 
   355   fun r_mk_comb_tac_lam lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms
 
   323   fun r_mk_comb_tac_lam lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms
 
   356 *}
 
   324 *}
 
   357 apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   358 apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   359 apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   360 apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   361 apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   362 apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   363 apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   364 apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   365 apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   366 apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   367 apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   368 apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   369 apply (tactic {*  (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   370 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   371 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   372 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   373 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   374 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   375 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
 
   325 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
 
   376 
   326 
   377 
   327 
   378 
   328 
   379 
   329
nominal2