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 2063 e4e128e59c41
parent 2061 37337fd5e8a7
child 2120 2786ff1df475
equal deleted inserted replaced
2062:65bdcc42badd 2063:e4e128e59c41 
    16 ML {*
 
    16 ML {*
 
    17   val dtinfo = Datatype.the_info @{theory} "Term4.rtrm4";
 
    17   val dtinfo = Datatype.the_info @{theory} "Term4.rtrm4";
 
    18   val {descr, sorts, ...} = dtinfo;
 
    18   val {descr, sorts, ...} = dtinfo;
 
    19 *}
 
    19 *}
 
    20 setup {* snd o (define_raw_perms descr sorts @{thm rtrm4.induct} 1) *}
 
    20 setup {* snd o (define_raw_perms descr sorts @{thm rtrm4.induct} 1) *}
 
    21 print_theorems
 
    21 lemmas perm = permute_rtrm4_permute_rtrm4_list.simps(1-3)
 
    22 
    22 lemma perm_fix:
 
    23 (* "repairing" of the permute function *)
 
       
    24 lemma repaired:
 
       
    25   fixes ts::"rtrm4 list"
 
    23   fixes ts::"rtrm4 list"
 
    26   shows "permute_rtrm4_list p ts = p \<bullet> ts"
 
    24   shows "permute_rtrm4_list p ts = p \<bullet> ts"
 
    27   apply(induct ts)
 
    25   by (induct ts) simp_all
 
    28   apply(simp_all)
 
    26 lemmas perm_fixed = perm[simplified perm_fix]
 
    29   done
 
       
    30 
       
    31 thm permute_rtrm4_permute_rtrm4_list.simps
 
       
    32 lemmas perm_fixed = permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
 
       
    33 
    27 
    34 ML {* val bl = [[[BEmy 0], [BEmy 0, BEmy 1], [BSet ([(NONE, 0)], [1])]], [[], [BEmy 0, BEmy 1]]] *}
 
    28 ML {* val bl = [[[BEmy 0], [BEmy 0, BEmy 1], [BSet ([(NONE, 0)], [1])]], [[], [BEmy 0, BEmy 1]]] *}
 
    35 
    29 
    36 local_setup {* fn ctxt => let val (_, _, ctxt') = define_raw_fv descr sorts [] bl ctxt in ctxt' end *}
 
    30 local_setup {* fn ctxt => let val (_, _, ctxt') = define_raw_fv descr sorts [] bl ctxt in ctxt' end *}
 
    37 thm fv_rtrm4.simps fv_rtrm4_list.simps
 
    31 lemmas fv = fv_rtrm4.simps (*fv_rtrm4_list.simps*)
 
       
    32 
       
    33 lemma fv_fix: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))"
 
       
    34   by (rule ext) (induct_tac x, simp_all)
 
       
    35 lemmas fv_fixed = fv[simplified fv_fix]
 
       
    36 
       
    37 (* TODO: check remove 2 *)
 
       
    38 local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms perm_fixed fv_rtrm4.simps fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *}
 
       
    39 thm eqvts(1-2)
 
    38 
    40 
    39 local_setup {* snd o define_raw_alpha dtinfo [] bl [@{term fv_rtrm4}, @{term fv_rtrm4_list}] *}
 
    41 local_setup {* snd o define_raw_alpha dtinfo [] bl [@{term fv_rtrm4}, @{term fv_rtrm4_list}] *}
 
    40 thm alpha_rtrm4_alpha_rtrm4_list.intros
 
    42 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
 
       
    43 lemmas alpha_inj = alpha4_inj(1-3)
 
    41 
    44 
    42 lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4"
 
    45 lemma alpha_fix: "alpha_rtrm4_list = list_rel alpha_rtrm4"
 
    43 apply (rule ext)+
 
    46   apply (rule ext)+
 
    44 apply (induct_tac x xa rule: list_induct2')
 
    47   apply (induct_tac x xa rule: list_induct2')
 
    45 apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros)
 
    48   apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros)
 
    46 apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all)
 
    49   apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all)
 
    47 apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all)
 
    50   apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all)
 
    48 apply rule
 
    51   apply rule
 
    49 apply (erule alpha_rtrm4_list.cases)
 
    52   apply (erule alpha_rtrm4_list.cases)
 
    50 apply simp_all
 
    53   apply simp_all
 
    51 apply (rule alpha_rtrm4_alpha_rtrm4_list.intros)
 
    54   apply (rule alpha_rtrm4_alpha_rtrm4_list.intros)
 
    52 apply simp_all
 
    55   apply simp_all
 
    53 done
 
    56   done
 
    54 
    57 
    55 lemma fix3: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))"
 
    58 lemmas alpha_inj_fixed = alpha_inj[simplified alpha_fix (*fv_fix*)]
 
    56 apply (rule ext)
 
       
    57 apply (induct_tac x)
 
       
    58 apply simp_all
 
       
    59 done
 
       
    60 
    59 
    61 notation
 
    60 notation
 
    62   alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and
 
    61     alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100)
 
    63   alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
 
    62 and alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
 
    64 thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]
 
       
    65 
       
    66 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
 
       
    67 thm alpha4_inj
 
       
    68 
       
    69 lemmas alpha4_inj_fixed = alpha4_inj[simplified fix2 fix3]
 
       
    70 
       
    71 local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] fv_rtrm4.simps fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *}
 
       
    72 thm eqvts(1-2)
 
       
    73 
    63 
    74 local_setup {*
 
    64 local_setup {*
 
    75 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []),
 
    65 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []),
 
    76   build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} ctxt 1) ctxt) ctxt))
 
    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))
 
    77 *}
 
    67 *}
 
    78 thm alpha4_eqvt
 
    68 thm alpha4_eqvt
 
    79 lemmas alpha4_eqvt_fixed = alpha4_eqvt[simplified fix2 fix3]
 
    69 lemmas alpha4_eqvt_fixed = alpha4_eqvt(1)[simplified alpha_fix (*fv_fix*)]
 
    80 
    70 
    81 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []),
 
    71 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []),
 
    82   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)) *}
 
    72   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)) *}
 
    83 thm alpha4_reflp
 
    73 thm alpha4_reflp
 
    84 lemmas alpha4_reflp_fixed = alpha4_reflp[simplified fix2 fix3]
 
       
    85 
    74 
    86 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),
 
    75 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),
 
    87   (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thms alpha4_reflp} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}
 
    76   (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thms alpha4_reflp} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}
 
    88 lemmas alpha4_equivp_fixed = alpha4_equivp[simplified fix2 fix3]
 
    77 lemmas alpha4_equivp_fixed = alpha4_equivp[simplified alpha_fix fv_fix]
 
    89 
    78 
    90 quotient_type 
    79 quotient_type
 
    91   trm4 = rtrm4 / alpha_rtrm4
 
    80   trm4 = rtrm4 / alpha_rtrm4
 
    92   by (simp_all add: alpha4_equivp)
 
    81   by (simp_all add: alpha4_equivp)
 
    93 
    82 
    94 local_setup {*
 
    83 local_setup {*
 
    95 (fn ctxt => ctxt
 
    84 (fn ctxt => ctxt
 
   117 local_setup {* snd o prove_const_rsp [] @{binding rLm4_rsp} [@{term rLm4}]
 
   106 local_setup {* snd o prove_const_rsp [] @{binding rLm4_rsp} [@{term rLm4}]
 
   118   (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *}
 
   107   (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *}
 
   119 
   108 
   120 lemma [quot_respect]:
 
   109 lemma [quot_respect]:
 
   121   "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"
 
   110   "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"
 
   122   by (simp add: alpha4_inj_fixed)
 
   111   by (simp add: alpha_inj_fixed)
 
   123 
   112 
   124 local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp}
 
   113 local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp}
 
   125   [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}]
 
   114   [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}]
 
   126   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *}
 
   115   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *}
 
   127 
   116 
   153 *}
 
   142 *}
 
   154 
   143 
   155 ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *}
 
   144 ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *}
 
   156 
   145 
   157 ML {*
 
   146 ML {*
 
   158   map (lift_thm [@{typ trm4}] @{context}) @{thms fv_rtrm4.simps[simplified fix3] fv_rtrm4_list.simps[simplified fix3]}
 
   147   map (lift_thm [@{typ trm4}] @{context}) @{thms fv_rtrm4.simps[simplified fv_fix] fv_rtrm4_list.simps[simplified fv_fix]}
 
   159 *}
 
   148 *}
 
   160 
   149 
   161 ML {*
 
   150 ML {*
 
   162 val liftd =
 
   151 val liftd =
 
   163   map (Local_Defs.unfold @{context} @{thms id_simps}) (
 
   152   map (Local_Defs.unfold @{context} @{thms id_simps}) (
 
   164     map (Local_Defs.fold @{context} @{thms alphas}) (
 
   153     map (Local_Defs.fold @{context} @{thms alphas}) (
 
   165       map (lift_thm [@{typ trm4}] @{context}) @{thms alpha4_inj_fixed[unfolded alphas]}
 
   154       map (lift_thm [@{typ trm4}] @{context}) @{thms alpha_inj_fixed[unfolded alphas]}
 
   166     )
 
   155     )
 
   167   )
 
   156   )
 
   168 *}
 
   157 *}
 
   169 
   158 
   170 ML {*
 
   159 ML {*
 
   171   map (lift_thm [@{typ trm4}] @{context})
 
   160   map (lift_thm [@{typ trm4}] @{context})
 
   172   (flat (map (distinct_rel @{context} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases}) [(@{thms rtrm4.distinct},@{term "alpha_rtrm4"})]))
 
   161   (flat (map (distinct_rel @{context} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases}) [(@{thms rtrm4.distinct},@{term "alpha_rtrm4"})]))
 
   173 *}
 
   162 *}
 
   174 
   163 
   175 ML {*
 
   164 ML {*
 
   176   map (lift_thm [@{typ trm4}] @{context}) @{thms eqvts(1-2)[simplified fix3]}
 
   165   map (lift_thm [@{typ trm4}] @{context}) @{thms eqvts(1-2)[simplified fv_fix]}
 
   177 *}
 
   166 *}
 
   178 
   167 
   179 end
 
   168 end
nominal2