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.
FSet.thy
changeset 514 6b3be083229c
parent 509 d62b6517a0ab
child 516 bed81795848c
equal deleted inserted replaced
513:eed5d55ea9a6 514:6b3be083229c 
   133      (if rsp_fold f
 
   133      (if rsp_fold f
 
   134      then (
 
   134      then (
 
   135        if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A))
 
   135        if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A))
 
   136      ) else z)"
 
   136      ) else z)"
 
   137 
   137 
   138 (* fold1_def is not usable, but: *)
 
       
   139 thm fold1.simps
 
       
   140 
       
   141 lemma fs1_strong_cases:
 
   138 lemma fs1_strong_cases:
 
   142   fixes X :: "'a list"
 
   139   fixes X :: "'a list"
 
   143   shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"
 
   140   shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"
 
   144   apply (induct X)
 
   141   apply (induct X)
 
   145   apply (simp)
 
   142   apply (simp)
 
   178   fixes z
 
   175   fixes z
 
   179   assumes a: "x \<approx> y"
 
   176   assumes a: "x \<approx> y"
 
   180   shows "(z memb x) = (z memb y)"
 
   177   shows "(z memb x) = (z memb y)"
 
   181   using a by induct auto
 
   178   using a by induct auto
 
   182 
   179 
   183 lemma ho_memb_rsp[quot_rsp]:
 
   180 lemma ho_memb_rsp[quotient_rsp]:
 
   184   "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
 
   181   "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
 
   185   by (simp add: memb_rsp)
 
   182   by (simp add: memb_rsp)
 
   186 
   183 
   187 lemma card1_rsp:
 
   184 lemma card1_rsp:
 
   188   fixes a b :: "'a list"
 
   185   fixes a b :: "'a list"
 
   189   assumes e: "a \<approx> b"
 
   186   assumes e: "a \<approx> b"
 
   190   shows "card1 a = card1 b"
 
   187   shows "card1 a = card1 b"
 
   191   using e by induct (simp_all add:memb_rsp)
 
   188   using e by induct (simp_all add:memb_rsp)
 
   192 
   189 
   193 lemma ho_card1_rsp[quot_rsp]: 
   190 lemma ho_card1_rsp[quotient_rsp]: 
   194   "(op \<approx> ===> op =) card1 card1"
 
   191   "(op \<approx> ===> op =) card1 card1"
 
   195   by (simp add: card1_rsp)
 
   192   by (simp add: card1_rsp)
 
   196 
   193 
   197 lemma cons_rsp[quot_rsp]:
 
   194 lemma cons_rsp[quotient_rsp]:
 
   198   fixes z
 
   195   fixes z
 
   199   assumes a: "xs \<approx> ys"
 
   196   assumes a: "xs \<approx> ys"
 
   200   shows "(z # xs) \<approx> (z # ys)"
 
   197   shows "(z # xs) \<approx> (z # ys)"
 
   201   using a by (rule list_eq.intros(5))
 
   198   using a by (rule list_eq.intros(5))
 
   202 
   199 
   203 lemma ho_cons_rsp[quot_rsp]:
 
   200 lemma ho_cons_rsp[quotient_rsp]:
 
   204   "(op = ===> op \<approx> ===> op \<approx>) op # op #"
 
   201   "(op = ===> op \<approx> ===> op \<approx>) op # op #"
 
   205   by (simp add: cons_rsp)
 
   202   by (simp add: cons_rsp)
 
   206 
   203 
   207 lemma append_rsp_fst:
 
   204 lemma append_rsp_fst:
 
   208   assumes a : "l1 \<approx> l2"
 
   205   assumes a : "l1 \<approx> l2"
 
   255   apply (rule append_rsp_fst)
 
   252   apply (rule append_rsp_fst)
 
   256   using b apply (assumption)
 
   253   using b apply (assumption)
 
   257   apply (rule append_sym_rsp)
 
   254   apply (rule append_sym_rsp)
 
   258   done
 
   255   done
 
   259 
   256 
   260 lemma ho_append_rsp[quot_rsp]:
 
   257 lemma ho_append_rsp[quotient_rsp]:
 
   261   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
 
   258   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
 
   262   by (simp add: append_rsp)
 
   259   by (simp add: append_rsp)
 
   263 
   260 
   264 lemma map_rsp:
 
   261 lemma map_rsp:
 
   265   assumes a: "a \<approx> b"
 
   262   assumes a: "a \<approx> b"
 
   267   using a
 
   264   using a
 
   268   apply (induct)
 
   265   apply (induct)
 
   269   apply(auto intro: list_eq.intros)
 
   266   apply(auto intro: list_eq.intros)
 
   270   done
 
   267   done
 
   271 
   268 
   272 lemma ho_map_rsp[quot_rsp]:
 
   269 lemma ho_map_rsp[quotient_rsp]:
 
   273   "(op = ===> op \<approx> ===> op \<approx>) map map"
 
   270   "(op = ===> op \<approx> ===> op \<approx>) map map"
 
   274   by (simp add: map_rsp)
 
   271   by (simp add: map_rsp)
 
   275 
   272 
   276 lemma map_append:
 
   273 lemma map_append:
 
   277   "(map f (a @ b)) \<approx> (map f a) @ (map f b)"
 
   274   "(map f (a @ b)) \<approx> (map f a) @ (map f b)"
 
   278  by simp (rule list_eq_refl)
 
   275  by simp (rule list_eq_refl)
 
   279 
   276 
   280 lemma ho_fold_rsp[quot_rsp]:
 
   277 lemma ho_fold_rsp[quotient_rsp]:
 
   281   "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
 
   278   "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
 
   282   apply (auto simp add: FUN_REL_EQ)
 
   279   apply (auto simp add: FUN_REL_EQ)
 
   283   apply (case_tac "rsp_fold x")
 
   280   apply (case_tac "rsp_fold x")
 
   284   prefer 2
 
   281   prefer 2
 
   285   apply (erule_tac list_eq.induct)
 
   282   apply (erule_tac list_eq.induct)
 
   295 ML {* val rsp_thms =
 
   292 ML {* val rsp_thms =
 
   296   @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *}
 
   293   @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *}
 
   297 
   294 
   298 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   295 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   299 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
 
   296 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
 
   300 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] [quot] *}
 
   297 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}
 
   301 
   298 
   302 lemma "IN x EMPTY = False"
 
   299 lemma "IN x EMPTY = False"
 
   303 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 
   300 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 
   304 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   301 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   305 apply(tactic {* all_inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   302 apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   306 apply(tactic {* clean_tac @{context} [quot] 1*})
 
   303 apply(tactic {* clean_tac @{context} 1*})
 
   307 done
 
   304 done
 
   308 
   305 
   309 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
 
   306 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
 
   310 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *})
 
   307 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *})
 
   311 
   308 
   328 lemma "FOLD f g (z::'b) (INSERT a x) =
 
   325 lemma "FOLD f g (z::'b) (INSERT a x) =
 
   329   (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
 
   326   (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
 
   330 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 
   327 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 
   331 done
 
   328 done
 
   332 
   329 
   333 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
 
   330 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
 
   334 
   331 
   335 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
 
   332 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
 
   336 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
 
   333 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
 
   337 done
 
   334 done
 
   338 
   335 
   346 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 
   343 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 
   347 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
 
   344 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
 
   348 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 
   345 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 
   349 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   346 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   350 prefer 2
 
   347 prefer 2
 
   351 apply(tactic {* clean_tac @{context} [quot] 1 *})
 
   348 apply(tactic {* clean_tac @{context} 1 *})
 
   352 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   349 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   353 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   350 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   354 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
 
   351 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
 
   355 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   352 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   356 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   353 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   402   apply (rule a)
 
   399   apply (rule a)
 
   403   apply (rule b)
 
   400   apply (rule b)
 
   404   apply (assumption)
 
   401   apply (assumption)
 
   405   done
 
   402   done
 
   406 
   403 
       
   404 ML {* quot *}
 
       
   405 thm quotient_thm
 
       
   406 
   407 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 
   407 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 
   408 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
 
   408 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
 
   409 done
 
   409 done
 
   410 
   410 
   411 lemma "P (x :: 'a fset) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 
   411 lemma "P (x :: 'a fset) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 
   429   INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
 
   429   INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
 
   430 where
 
   430 where
 
   431   "INSERT2 \<equiv> op #"
 
   431   "INSERT2 \<equiv> op #"
 
   432 
   432 
   433 ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *}
 
   433 ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *}
 
   434 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy quot [rel_refl] [trans2] *}
 
   434 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
 
   435 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot *}
 
   435 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}
 
   436 
   436 
   437 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 
   437 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 
   438 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
 
   438 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
 
   439 done
 
   439 done
 
   440 
   440 
   451   fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 
   451   fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 
   452 where
 
   452 where
 
   453   "fset_case \<equiv> list_case"
 
   453   "fset_case \<equiv> list_case"
 
   454 
   454 
   455 (* Probably not true without additional assumptions about the function *)
 
   455 (* Probably not true without additional assumptions about the function *)
 
   456 lemma list_rec_rsp[quot_rsp]:
 
   456 lemma list_rec_rsp[quotient_rsp]:
 
   457   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
 
   457   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
 
   458   apply (auto simp add: FUN_REL_EQ)
 
   458   apply (auto simp add: FUN_REL_EQ)
 
   459   apply (erule_tac list_eq.induct)
 
   459   apply (erule_tac list_eq.induct)
 
   460   apply (simp_all)
 
   460   apply (simp_all)
 
   461   sorry
 
   461   sorry
 
   462 
   462 
   463 lemma list_case_rsp[quot_rsp]:
 
   463 lemma list_case_rsp[quotient_rsp]:
 
   464   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
 
   464   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
 
   465   apply (auto simp add: FUN_REL_EQ)
 
   465   apply (auto simp add: FUN_REL_EQ)
 
   466   sorry
 
   466   sorry
 
   467 
   467 
   468 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
 
   468 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
 
   469 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot *}
 
   469 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}
 
   470 
   470 
   471 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 
   471 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 
   472 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
 
   472 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
 
   473 done
 
   473 done
 
   474 
   474
nominal2