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 514 6b3be083229c
parent 513 eed5d55ea9a6
parent 510 8dbc521ee97f
child 515 b00a9b58264d
equal deleted inserted replaced
513:eed5d55ea9a6 514:6b3be083229c 
   126   shows "Lam a t = Lam b s"
 
   126   shows "Lam a t = Lam b s"
 
   127 using a
 
   127 using a
 
   128 unfolding fresh_def supp_def
 
   128 unfolding fresh_def supp_def
 
   129 sorry
 
   129 sorry
 
   130 
   130 
   131 lemma perm_rsp[quot_rsp]:
 
   131 lemma perm_rsp[quotient_rsp]:
 
   132   "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>"
 
   132   "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>"
 
   133   apply(auto)
 
   133   apply(auto)
 
   134   (* this is propably true if some type conditions are imposed ;o) *)
 
   134   (* this is propably true if some type conditions are imposed ;o) *)
 
   135   sorry
 
   135   sorry
 
   136 
   136 
   138   "(op = ===> alpha ===> op =) fresh fresh"
 
   138   "(op = ===> alpha ===> op =) fresh fresh"
 
   139   apply(auto)
 
   139   apply(auto)
 
   140   (* this is probably only true if some type conditions are imposed *)
 
   140   (* this is probably only true if some type conditions are imposed *)
 
   141   sorry
 
   141   sorry
 
   142 
   142 
   143 lemma rVar_rsp[quot_rsp]:
 
   143 lemma rVar_rsp[quotient_rsp]:
 
   144   "(op = ===> alpha) rVar rVar"
 
   144   "(op = ===> alpha) rVar rVar"
 
   145 by (auto intro:a1)
 
   145 by (auto intro:a1)
 
   146 
   146 
   147 lemma rApp_rsp[quot_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp"
 
   147 lemma rApp_rsp[quotient_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp"
 
   148 by (auto intro:a2)
 
   148 by (auto intro:a2)
 
   149 
   149 
   150 lemma rLam_rsp[quot_rsp]: "(op = ===> alpha ===> alpha) rLam rLam"
 
   150 lemma rLam_rsp[quotient_rsp]: "(op = ===> alpha ===> alpha) rLam rLam"
 
   151   apply(auto)
 
   151   apply(auto)
 
   152   apply(rule a3)
 
   152   apply(rule a3)
 
   153   apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst)
 
   153   apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst)
 
   154   apply(rule sym)
 
   154   apply(rule sym)
 
   155   apply(rule trans)
 
   155   apply(rule trans)
 
   158   apply(simp add: pt_name1)
 
   158   apply(simp add: pt_name1)
 
   159   apply(assumption)
 
   159   apply(assumption)
 
   160   apply(simp add: abs_fresh)
 
   160   apply(simp add: abs_fresh)
 
   161   done
 
   161   done
 
   162 
   162 
   163 lemma rfv_rsp[quot_rsp]: "(alpha ===> op =) rfv rfv"
 
   163 lemma rfv_rsp[quotient_rsp]: "(alpha ===> op =) rfv rfv"
 
   164   sorry
 
   164   sorry
 
   165 
   165 
   166 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)"
 
   166 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)"
 
   167 apply (auto)
 
   167 apply (auto)
 
   168 apply (erule alpha.cases)
 
   168 apply (erule alpha.cases)
 
   172 ML {* val qty = @{typ "lam"} *}
 
   172 ML {* val qty = @{typ "lam"} *}
 
   173 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *}
 
   173 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *}
 
   174 
   174 
   175 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   175 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   176 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
 
   176 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
 
   177 ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] [quot] *}
 
   177 ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] *}
 
   178 
   178 
   179 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
 
   179 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
 
   180 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *})
 
   180 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *})
 
   181 done
 
   181 done
 
   182 
   182 
   310 
   310 
   311 lemma real_alpha_lift:
 
   311 lemma real_alpha_lift:
 
   312   "\<lbrakk>t = [(a, b)] \<bullet> s; a \<sharp> [b].s\<rbrakk> \<Longrightarrow> Lam a t = Lam b s"
 
   312   "\<lbrakk>t = [(a, b)] \<bullet> s; a \<sharp> [b].s\<rbrakk> \<Longrightarrow> Lam a t = Lam b s"
 
   313 apply (tactic {* procedure_tac @{context} @{thm real_alpha_pre} 1 *})
 
   313 apply (tactic {* procedure_tac @{context} @{thm real_alpha_pre} 1 *})
 
   314 prefer 2
 
   314 prefer 2
 
   315 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   315 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   316 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   316 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   317 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   317 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   318 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   318 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   319 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   319 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   320 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   320 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   321 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   321 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   322 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   322 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   323 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   323 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   324 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   324 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   325 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   325 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   326 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   326 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   327 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   327 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   328 apply (tactic {* all_inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   328 apply (tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   329 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   329 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   330 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   330 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   331 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   331 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   332 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   332 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   333 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   333 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   334 apply (simp only: perm_prs)
 
   334 apply (simp only: perm_prs)
 
   335 prefer 2
 
   335 prefer 2
 
   336 apply (tactic {* all_inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   336 apply (tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   337 prefer 3
 
   337 prefer 3
 
   338 apply (tactic {* clean_tac @{context} [quot] 1 *})
 
   338 apply (tactic {* clean_tac @{context} 1 *})
 
   339 
       
   340 thm all_prs
 
       
   341 thm REP_ABS_RSP
 
       
   342 thm ball_reg_eqv_range
 
       
   343 
       
   344 
       
   345 thm perm_lam_def
 
       
   346 apply (simp only: perm_prs)
 
   339 apply (simp only: perm_prs)
 
   347 (*apply (tactic {* regularize_tac @{context} [quot] 1 *})*)
 
   340 (*apply (tactic {* regularize_tac @{context} 1 *})*)
 
   348 sorry
 
   341 sorry
 
   349 
   342 
   350 done
 
   343 done
 
   351 
   344
nominal2