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/Manual/Term4.thy
changeset 2121 f435d8efd751
parent 2120 2786ff1df475
child 2149 95aac598a526
equal deleted inserted replaced
2120:2786ff1df475 2121:f435d8efd751 
    59 
    59 
    60 notation
 
    60 notation
 
    61     alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100)
 
    61     alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100)
 
    62 and alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
 
    62 and alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
 
    63 
    63 
    64 local_setup {*
 
    64 declare perm_fixed[eqvt]
 
    65 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []),
 
    65 equivariance alpha_rtrm4
 
    66   build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms perm_fixed alpha4_inj} ctxt 1) ctxt) ctxt))
 
    66 lemmas alpha4_eqvt = eqvts(1-2)
 
    67 *}
 
    67 lemmas alpha4_eqvt_fixed = alpha4_eqvt(2)[simplified alpha_fix (*fv_fix*)]
 
    68 
       
    69 
       
    70 thm alpha4_eqvt
 
       
    71 lemmas alpha4_eqvt_fixed = alpha4_eqvt(1)[simplified alpha_fix (*fv_fix*)]
 
       
    72 
    68 
    73 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []),
 
    69 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []),
 
    74   build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj} ctxt) ctxt)) *}
 
    70   build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj} ctxt) ctxt)) *}
 
    75 thm alpha4_reflp
 
    71 thm alpha4_reflp
 
    76 
    72 
   161 ML {*
 
   157 ML {*
 
   162   map (lift_thm [@{typ trm4}] @{context})
 
   158   map (lift_thm [@{typ trm4}] @{context})
 
   163   (flat (map (distinct_rel @{context} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases}) [(@{thms rtrm4.distinct},@{term "alpha_rtrm4"})]))
 
   159   (flat (map (distinct_rel @{context} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases}) [(@{thms rtrm4.distinct},@{term "alpha_rtrm4"})]))
 
   164 *}
 
   160 *}
 
   165 
   161 
       
   162 thm eqvts(6-7)
 
   166 ML {*
 
   163 ML {*
 
   167   map (lift_thm [@{typ trm4}] @{context}) @{thms eqvts(1-2)[simplified fv_fix]}
 
   164   map (lift_thm [@{typ trm4}] @{context}) @{thms eqvts(6-7)[simplified fv_fix]}
 
   168 *}
 
   165 *}
 
   169 
   166 
   170 end
 
   167 end
nominal2