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 582 a082e2d138ab
parent 572 a68c51dd85b3
child 586 cdc6ae1a4ed2
child 591 01a0da807f50
equal deleted inserted replaced
578:070161f1996a 582:a082e2d138ab 
     9 
     9 
    10 quotient my_int = "nat \<times> nat" / intrel
 
    10 quotient my_int = "nat \<times> nat" / intrel
 
    11   apply(unfold equivp_def)
 
    11   apply(unfold equivp_def)
 
    12   apply(auto simp add: mem_def expand_fun_eq)
 
    12   apply(auto simp add: mem_def expand_fun_eq)
 
    13   done
 
    13   done
 
       
    14 
       
    15 thm quotient_equiv
 
    14 
    16 
    15 thm quotient_thm
 
    17 thm quotient_thm
 
    16 
    18 
    17 thm my_int_equivp
 
    19 thm my_int_equivp
 
    18 
    20 
   136 
   138 
   137 ML {* val qty = @{typ "my_int"} *}
 
   139 ML {* val qty = @{typ "my_int"} *}
 
   138 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   140 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   139 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
 
   141 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
 
   140 
   142 
   141 ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] *}
 
   143 ML {* fun lift_tac_intex lthy t = lift_tac lthy t *}
 
   142 
   144 
   143 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
 
   145 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
 
   144 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *}
 
   146 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *}
 
   145 
   147 
   146 lemma test1: "my_plus a b = my_plus a b"
 
   148 lemma test1: "my_plus a b = my_plus a b"
 
   176 apply(simp add: id_simps)
 
   178 apply(simp add: id_simps)
 
   177 apply(tactic {* quotient_tac @{context} 1 *})
 
   179 apply(tactic {* quotient_tac @{context} 1 *})
 
   178 done
 
   180 done
 
   179 *)
 
   181 *)
 
   180 
   182 
   181 
       
   182 
       
   183 lemma "PLUS a b = PLUS a b"
 
   183 lemma "PLUS a b = PLUS a b"
 
   184 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
 
   184 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
 
   185 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   185 apply(tactic {* regularize_tac @{context} 1 *})
 
   186 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 
   186 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 
   187 apply(tactic {* clean_tac @{context} 1 *}) 
   187 apply(tactic {* clean_tac @{context} 1 *}) 
   188 done
 
   188 done
 
   189 
   189 
   190 lemma test2: "my_plus a = my_plus a"
 
   190 lemma test2: "my_plus a = my_plus a"
 
   212 done
 
   212 done
 
   213 
   213 
   214 
   214 
   215 lemma "PLUS a b = PLUS b a"
 
   215 lemma "PLUS a b = PLUS b a"
 
   216 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
 
   216 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
 
   217 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   217 apply(tactic {* regularize_tac @{context} 1 *})
 
   218 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 
   218 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 
   219 apply(tactic {* clean_tac @{context} 1 *})
 
   219 apply(tactic {* clean_tac @{context} 1 *})
 
   220 done
 
   220 done
 
   221 
   221 
   222 lemma plus_assoc_pre:
 
   222 lemma plus_assoc_pre:
 
   227   apply (simp)
 
   227   apply (simp)
 
   228   done
 
   228   done
 
   229 
   229 
   230 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
 
   230 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
 
   231 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
 
   231 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
 
   232 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   232 apply(tactic {* regularize_tac @{context} 1 *})
 
   233 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 
   233 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 
   234 apply(tactic {* clean_tac @{context} 1 *})
 
   234 apply(tactic {* clean_tac @{context} 1 *})
 
   235 done
 
   235 done
 
   236 
   236 
   237 lemma ho_tst: "foldl my_plus x [] = x"
 
   237 lemma ho_tst: "foldl my_plus x [] = x"
 
   238 apply simp
 
   238 apply simp
 
   239 done
 
   239 done
 
   240 
   240 
   241 lemma "foldl PLUS x [] = x"
 
   241 lemma "foldl PLUS x [] = x"
 
   242 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
 
   242 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
 
   243 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   243 apply(tactic {* regularize_tac @{context} 1 *})
 
   244 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 
   244 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 
   245 apply(tactic {* clean_tac @{context} 1 *})
 
   245 apply(tactic {* clean_tac @{context} 1 *})
 
   246 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 
   246 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 
   247 done
 
   247 done
 
   248 
   248 
   249 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
 
   249 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
 
   250 sorry
 
   250 sorry
 
   251 
   251 
   252 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
 
   252 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
 
   253 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
 
   253 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
 
   254 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   254 apply(tactic {* regularize_tac @{context} 1 *})
 
   255 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 
   255 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 
   256 apply(tactic {* clean_tac @{context} 1 *})
 
   256 apply(tactic {* clean_tac @{context} 1 *})
 
   257 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int])
 
   257 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int])
 
   258 done
 
   258 done
 
   259 
   259
nominal2