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.
IntEx.thy
changeset 557 e67961288b12
parent 556 287ea842a7d4
parent 554 8395fc6a6945
child 558 114bb544ecb9
equal deleted inserted replaced
556:287ea842a7d4 557:e67961288b12 
   147 ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] *}
 
   147 ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] *}
 
   148 
   148 
   149 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
 
   149 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
 
   150 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *}
 
   150 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *}
 
   151 
   151 
   152 lemma cheat: "P" sorry
 
       
   153 
       
   154 lemma test1: "my_plus a b = my_plus a b"
 
   152 lemma test1: "my_plus a b = my_plus a b"
 
   155 apply(rule refl)
 
   153 apply(rule refl)
 
   156 done
 
   154 done
 
   157 
   155 
   158 abbreviation 
   156 abbreviation 
   160 abbreviation 
   158 abbreviation 
   161   "Rep \<equiv> REP_my_int"
 
   159   "Rep \<equiv> REP_my_int"
 
   162 abbreviation 
   160 abbreviation 
   163   "Resp \<equiv> Respects"
 
   161   "Resp \<equiv> Respects"
 
   164 
   162 
   165 
       
   166 lemma "PLUS a b = PLUS a b"
 
   163 lemma "PLUS a b = PLUS a b"
 
   167 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
 
   164 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
 
   168 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   165 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   169 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 
   166 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 
   170 apply(tactic {* lambda_allex_prs_tac @{context} 1 *})
 
       
   171 apply(tactic {* clean_tac @{context} 1 *}) 
   167 apply(tactic {* clean_tac @{context} 1 *}) 
   172 done
 
   168 done
 
   173 
   169 
   174 lemma test2: "my_plus a = my_plus a"
 
   170 lemma test2: "my_plus a = my_plus a"
 
   175 apply(rule refl)
 
   171 apply(rule refl)
 
   176 done
 
   172 done
 
   177 
   173 
   178 lemma "PLUS a = PLUS a"
 
   174 lemma "PLUS a = PLUS a"
 
   179 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})
 
   175 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})
 
   180 apply(rule cheat)
 
   176 apply(rule ballI)
 
   181 apply(rule cheat)
 
   177 apply(rule apply_rsp[OF Quotient_my_int ho_plus_rsp])
 
   182 apply(tactic {* clean_tac @{context} 1 *})
 
   178 apply(simp only: in_respects)
 
       
   179 
       
   180 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   181 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   182 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   183 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   184 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   185 apply(rule quot_rel_rsp)
 
       
   186 apply(tactic {* quotient_tac @{context} 1 *})
 
       
   187 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   188 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   189 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   190 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   191 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   192 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   193 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   194 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   195 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   196 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   197 apply(fold PLUS_def)
 
       
   198 apply(tactic {* clean_tac @{context} 1 *})
 
       
   199 thm Quotient_rel_rep
 
       
   200 thm Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]
 
       
   201 apply(simp only: Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
 
   183 done
 
   202 done
 
   184 
   203 
   185 lemma test3: "my_plus = my_plus"
 
   204 lemma test3: "my_plus = my_plus"
 
   186 apply(rule refl)
 
   205 apply(rule refl)
 
   187 done
 
   206 done
 
   188 
   207 
   189 lemma "PLUS = PLUS"
 
   208 lemma "PLUS = PLUS"
 
   190 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
 
   209 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
 
   191 apply(rule cheat)
 
   210 apply(rule ho_plus_rsp)
 
   192 apply(rule cheat)
 
   211 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   193 apply(tactic {* clean_tac @{context} 1 *})
 
   212 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   213 apply(rule quot_rel_rsp)
 
       
   214 apply(tactic {* quotient_tac @{context} 1 *})
 
       
   215 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   216 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   217 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   218 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   219 apply(tactic {* clean_tac @{context} 1 *})
 
       
   220 apply(simp only: Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]])
 
   194 done
 
   221 done
 
   195 
   222 
   196 
   223 
   197 lemma "PLUS a b = PLUS b a"
 
   224 lemma "PLUS a b = PLUS b a"
 
   198 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
 
   225 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
nominal2