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 506 91c374abde06
parent 498 e7bb6bbe7576
child 507 f7569f994195
child 508 fac6069d8e80
equal deleted inserted replaced
505:6cdba30c6d66 506:91c374abde06 
   178   fixes z
 
   178   fixes z
 
   179   assumes a: "x \<approx> y"
 
   179   assumes a: "x \<approx> y"
 
   180   shows "(z memb x) = (z memb y)"
 
   180   shows "(z memb x) = (z memb y)"
 
   181   using a by induct auto
 
   181   using a by induct auto
 
   182 
   182 
   183 lemma ho_memb_rsp[quot_rsp]:
 
   183 lemma ho_memb_rsp[quotient_rsp]:
 
   184   "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
 
   184   "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
 
   185   by (simp add: memb_rsp)
 
   185   by (simp add: memb_rsp)
 
   186 
   186 
   187 lemma card1_rsp:
 
   187 lemma card1_rsp:
 
   188   fixes a b :: "'a list"
 
   188   fixes a b :: "'a list"
 
   189   assumes e: "a \<approx> b"
 
   189   assumes e: "a \<approx> b"
 
   190   shows "card1 a = card1 b"
 
   190   shows "card1 a = card1 b"
 
   191   using e by induct (simp_all add:memb_rsp)
 
   191   using e by induct (simp_all add:memb_rsp)
 
   192 
   192 
   193 lemma ho_card1_rsp[quot_rsp]: 
   193 lemma ho_card1_rsp[quotient_rsp]: 
   194   "(op \<approx> ===> op =) card1 card1"
 
   194   "(op \<approx> ===> op =) card1 card1"
 
   195   by (simp add: card1_rsp)
 
   195   by (simp add: card1_rsp)
 
   196 
   196 
   197 lemma cons_rsp[quot_rsp]:
 
   197 lemma cons_rsp[quotient_rsp]:
 
   198   fixes z
 
   198   fixes z
 
   199   assumes a: "xs \<approx> ys"
 
   199   assumes a: "xs \<approx> ys"
 
   200   shows "(z # xs) \<approx> (z # ys)"
 
   200   shows "(z # xs) \<approx> (z # ys)"
 
   201   using a by (rule list_eq.intros(5))
 
   201   using a by (rule list_eq.intros(5))
 
   202 
   202 
   203 lemma ho_cons_rsp[quot_rsp]:
 
   203 lemma ho_cons_rsp[quotient_rsp]:
 
   204   "(op = ===> op \<approx> ===> op \<approx>) op # op #"
 
   204   "(op = ===> op \<approx> ===> op \<approx>) op # op #"
 
   205   by (simp add: cons_rsp)
 
   205   by (simp add: cons_rsp)
 
   206 
   206 
   207 lemma append_rsp_fst:
 
   207 lemma append_rsp_fst:
 
   208   assumes a : "l1 \<approx> l2"
 
   208   assumes a : "l1 \<approx> l2"
 
   255   apply (rule append_rsp_fst)
 
   255   apply (rule append_rsp_fst)
 
   256   using b apply (assumption)
 
   256   using b apply (assumption)
 
   257   apply (rule append_sym_rsp)
 
   257   apply (rule append_sym_rsp)
 
   258   done
 
   258   done
 
   259 
   259 
   260 lemma ho_append_rsp[quot_rsp]:
 
   260 lemma ho_append_rsp[quotient_rsp]:
 
   261   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
 
   261   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
 
   262   by (simp add: append_rsp)
 
   262   by (simp add: append_rsp)
 
   263 
   263 
   264 lemma map_rsp:
 
   264 lemma map_rsp:
 
   265   assumes a: "a \<approx> b"
 
   265   assumes a: "a \<approx> b"
 
   267   using a
 
   267   using a
 
   268   apply (induct)
 
   268   apply (induct)
 
   269   apply(auto intro: list_eq.intros)
 
   269   apply(auto intro: list_eq.intros)
 
   270   done
 
   270   done
 
   271 
   271 
   272 lemma ho_map_rsp[quot_rsp]:
 
   272 lemma ho_map_rsp[quotient_rsp]:
 
   273   "(op = ===> op \<approx> ===> op \<approx>) map map"
 
   273   "(op = ===> op \<approx> ===> op \<approx>) map map"
 
   274   by (simp add: map_rsp)
 
   274   by (simp add: map_rsp)
 
   275 
   275 
   276 lemma map_append:
 
   276 lemma map_append:
 
   277   "(map f (a @ b)) \<approx> (map f a) @ (map f b)"
 
   277   "(map f (a @ b)) \<approx> (map f a) @ (map f b)"
 
   278  by simp (rule list_eq_refl)
 
   278  by simp (rule list_eq_refl)
 
   279 
   279 
   280 lemma ho_fold_rsp[quot_rsp]:
 
   280 lemma ho_fold_rsp[quotient_rsp]:
 
   281   "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
 
   281   "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
 
   282   apply (auto simp add: FUN_REL_EQ)
 
   282   apply (auto simp add: FUN_REL_EQ)
 
   283   apply (case_tac "rsp_fold x")
 
   283   apply (case_tac "rsp_fold x")
 
   284   prefer 2
 
   284   prefer 2
 
   285   apply (erule_tac list_eq.induct)
 
   285   apply (erule_tac list_eq.induct)
 
   295 ML {* val rsp_thms =
 
   295 ML {* val rsp_thms =
 
   296   @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *}
 
   296   @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *}
 
   297 
   297 
   298 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   298 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"; *}
 
   299 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] *}
 
   300 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}
 
   301 
   301 
   302 lemma "IN x EMPTY = False"
 
   302 lemma "IN x EMPTY = False"
 
   303 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 
   303 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 
   304 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   304 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   305 apply(tactic {* all_inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 
   305 apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
   306 apply(tactic {* clean_tac @{context} [quot] 1*})
 
   306 apply(tactic {* clean_tac @{context} 1*})
 
   307 done
 
   307 done
 
   308 
   308 
   309 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
 
   309 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
 
   310 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *})
 
   310 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *})
 
   311 
   311 
   328 lemma "FOLD f g (z::'b) (INSERT a x) =
 
   328 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)"
 
   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)"
 
   330 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 
   330 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 
   331 done
 
   331 done
 
   332 
   332 
   333 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
 
   333 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
 
   334 
   334 
   335 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
 
   335 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 *})
 
   336 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
 
   337 done
 
   337 done
 
   338 
   338 
   346 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 
   346 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 *})
 
   347 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
 
   348 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 
   348 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 
   349 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   349 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   350 prefer 2
 
   350 prefer 2
 
   351 apply(tactic {* clean_tac @{context} [quot] 1 *})
 
   351 apply(tactic {* clean_tac @{context} 1 *})
 
   352 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   352 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 *)
 
   353 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 = (===>) *)
 
   354 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 *)
 
   355 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 *)
 
   356 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   402   apply (rule a)
 
   402   apply (rule a)
 
   403   apply (rule b)
 
   403   apply (rule b)
 
   404   apply (assumption)
 
   404   apply (assumption)
 
   405   done
 
   405   done
 
   406 
   406 
       
   407 ML {* quot *}
 
       
   408 thm quotient_thm
 
       
   409 
   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"
 
   410 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 *})
 
   411 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
 
   409 done
 
   412 done
 
   410 
   413 
   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"
 
   414 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"
 
   451   fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 
   454   fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 
   452 where
 
   455 where
 
   453   "fset_case \<equiv> list_case"
 
   456   "fset_case \<equiv> list_case"
 
   454 
   457 
   455 (* Probably not true without additional assumptions about the function *)
 
   458 (* Probably not true without additional assumptions about the function *)
 
   456 lemma list_rec_rsp[quot_rsp]:
 
   459 lemma list_rec_rsp[quotient_rsp]:
 
   457   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
 
   460   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
 
   458   apply (auto simp add: FUN_REL_EQ)
 
   461   apply (auto simp add: FUN_REL_EQ)
 
   459   apply (erule_tac list_eq.induct)
 
   462   apply (erule_tac list_eq.induct)
 
   460   apply (simp_all)
 
   463   apply (simp_all)
 
   461   sorry
 
   464   sorry
 
   462 
   465 
   463 lemma list_case_rsp[quot_rsp]:
 
   466 lemma list_case_rsp[quotient_rsp]:
 
   464   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
 
   467   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
 
   465   apply (auto simp add: FUN_REL_EQ)
 
   468   apply (auto simp add: FUN_REL_EQ)
 
   466   sorry
 
   469   sorry
 
   467 
   470 
   468 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
 
   471 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
nominal2