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.
LFex.thy
changeset 567 5dffcd087e30
parent 560 d707839bd917
child 573 14682786c356
equal deleted inserted replaced
566:4eca2c3e59f7 567:5dffcd087e30 
   218 
   218 
   219 ML {*
 
   219 ML {*
 
   220   val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM}
 
   220   val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM}
 
   221   val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps}
 
   221   val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps}
 
   222   val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quot
 
   222   val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quot
 
       
   223   val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quot
 
   223 *}
 
   224 *}
 
   224 
   225 
   225 lemma 
   226 lemma 
   226   assumes a0:
 
   227   assumes a0:
 
   227   "P1 TYP TYP"
 
   228   "P1 TYP TYP"
 
   254   shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and>
 
   255   shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and>
 
   255          ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> 
   256          ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> 
   256          ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
 
   257          ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
 
   257 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
 
   258 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
 
   258 apply - 
   259 apply - 
   259 apply(tactic {* lift_tac @{context} @{thm akind_aty_atrm.induct} @{thms alpha_equivps} 1 *})
 
   260 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
 
   260 (*apply(tactic {* regularize_tac @{context} @{thms alpha_equivps} 1 *})
 
   261 apply(tactic {* regularize_tac @{context} @{thms alpha_equivps} 1 *})
 
   261 apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})
 
   262 apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})
 
       
   263 apply(fold perm_kind_def perm_ty_def perm_trm_def FV_ty_def[simplified id_simps] FV_kind_def[simplified id_simps] FV_trm_def[simplified id_simps])
 
   262 apply(tactic {* clean_tac @{context} 1 *})
 
   264 apply(tactic {* clean_tac @{context} 1 *})
 
   263 *)
 
       
   264 (*apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})*)
 
       
   265 (*
 
   265 (*
 
   266 Profiling:
 
   266 Profiling:
 
   267 ML_prf {* fun ith i =  (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *}
 
   267 ML_prf {* fun ith i =  (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *}
 
   268 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *}
 
   268 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *}
 
   269 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 1) (ith 1)) *}
 
   269 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 1) (ith 1)) *}
 
   270 ML_prf {* PolyML.profiling 1 *}
 
   270 ML_prf {* PolyML.profiling 1 *}
 
   271 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *}
 
   271 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *}
 
   272 *)
 
   272 *)
 
   273 apply(unfold perm_kind_def perm_ty_def perm_trm_def)
 
       
   274 apply(tactic {* clean_tac @{context} 1 *})
 
       
   275 done
 
   273 done
 
   276 
   274 
   277 (* Does not work:
 
   275 (* Does not work:
 
   278 lemma
 
   276 lemma
 
   279   assumes a0: "P1 TYP"
 
   277   assumes a0: "P1 TYP"
nominal2