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 549 f178958d3d81
parent 540 c0b13fb70d6d
child 552 d9151fa76f84
equal deleted inserted replaced
546:8a1f4227dff9 549:f178958d3d81 
   128   apply(cases a)
 
   128   apply(cases a)
 
   129   apply(cases b)
 
   129   apply(cases b)
 
   130   apply(auto)
 
   130   apply(auto)
 
   131   done
 
   131   done
 
   132 
   132 
       
   133 lemma list_equiv_rsp[quotient_rsp]:
 
       
   134   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
 
       
   135 by auto
 
       
   136 
   133 lemma ho_plus_rsp[quotient_rsp]:
 
   137 lemma ho_plus_rsp[quotient_rsp]:
 
   134   shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
 
   138   shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
 
   135 by (simp)
 
   139 by (simp)
 
   136 
   140 
   137 ML {* val qty = @{typ "my_int"} *}
 
   141 ML {* val qty = @{typ "my_int"} *}
 
   147 
   151 
   148 
   152 
   149 lemma "PLUS a b = PLUS b a"
 
   153 lemma "PLUS a b = PLUS b a"
 
   150 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
 
   154 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
 
   151 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   155 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   152 prefer 2
 
   156 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   153 apply(tactic {* clean_tac @{context} 1 *})
 
   157 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   154 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   158 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   155 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   159 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   156 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   160 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   157 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   161 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   158 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   162 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   159 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   163 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   160 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   164 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   161 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   165 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   162 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   166 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   163 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   167 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   164 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   168 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   165 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   169 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   166 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   170 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   167 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   171 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   168 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   172 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   169 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   173 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   170 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   174 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   171 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   175 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   172 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   176 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   173 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   177 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   174 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   178 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   175 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   179 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   176 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
   180 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   181 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 
       
   182 apply(tactic {* clean_tac @{context} 1 *})
 
   177 done
 
   183 done
 
   178 
   184 
   179 lemma plus_assoc_pre:
 
   185 lemma plus_assoc_pre:
 
   180   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
 
   186   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
 
   181   apply (cases i)
 
   187   apply (cases i)
 
   193 
   199 
   194 lemma ho_tst: "foldl my_plus x [] = x"
 
   200 lemma ho_tst: "foldl my_plus x [] = x"
 
   195 apply simp
 
   201 apply simp
 
   196 done
 
   202 done
 
   197 
   203 
   198 
       
   199 
       
   200 
       
   201 
       
   202 
       
   203 (* I believe it's true. *)
 
   204 (* I believe it's true. *)
 
   204 lemma foldl_rsp[quotient_rsp]:
 
   205 lemma foldl_rsp[quotient_rsp]:
 
   205   "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> list_rel op \<approx> ===> op \<approx>) foldl foldl"
 
   206   "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> list_rel op \<approx> ===> op \<approx>) foldl foldl"
 
   206 apply (simp only: fun_rel.simps)
 
   207 apply (simp only: fun_rel.simps)
 
   207 apply (rule allI)
 
   208 apply (rule allI)
 
   220 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
 
   221 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
 
   221 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   222 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   222 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 
   223 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 
   223 apply(rule nil_rsp)
 
   224 apply(rule nil_rsp)
 
   224 apply(tactic {* quotient_tac @{context} 1*})
 
   225 apply(tactic {* quotient_tac @{context} 1*})
 
       
   226 apply(simp only: fun_map.simps id_simps)
 
       
   227 apply(simp only: Quotient_abs_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]])
 
       
   228 apply(simp only: Quotient_abs_rep[OF list_quotient[OF Quotient_my_int]])
 
   225 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
 
   229 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
 
   226 apply(simp only: nil_prs[OF Quotient_my_int])
 
   230 apply(tactic {* clean_tac @{context} 1 *})
 
   227 apply(tactic {* clean_tac @{context} 1 *})
 
   231 sorry
 
   228 done
 
       
   229 
   232 
   230 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
 
   233 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
 
   231 sorry
 
   234 sorry
 
   232 
   235 
   233 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
 
   236 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
 
   234 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
 
   237 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
 
   235 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   238 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   236 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 
   239 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 
   237 apply(rule cons_rsp)
 
   240 apply(rule cons_rsp)
 
   238 apply(tactic {* quotient_tac @{context} 1 *})
 
   241 apply(tactic {* quotient_tac @{context} 1 *})
 
       
   242 apply(simp only: fun_map.simps id_simps)
 
       
   243 apply(simp only: Quotient_abs_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]])
 
       
   244 apply(simp only: Quotient_abs_rep[OF list_quotient[OF Quotient_my_int]])
 
   239 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
 
   245 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
 
   240 apply(simp only: cons_prs[OF Quotient_my_int])
 
   246 apply(simp only: cons_prs[OF Quotient_my_int])
 
   241 apply(tactic {* clean_tac @{context} 1 *})
 
   247 apply(tactic {* clean_tac @{context} 1 *})
 
   242 done
 
   248 done
 
   243 
   249
nominal2