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.
Quot/Examples/FSet.thy
changeset 636 520a4084d064
parent 631 e26e3dac3bf0
child 638 e472aa533a24
equal deleted inserted replaced
633:2e51e1315839 636:520a4084d064 
   175   fixes z
 
   175   fixes z
 
   176   assumes a: "x \<approx> y"
 
   176   assumes a: "x \<approx> y"
 
   177   shows "(z memb x) = (z memb y)"
 
   177   shows "(z memb x) = (z memb y)"
 
   178   using a by induct auto
 
   178   using a by induct auto
 
   179 
   179 
   180 lemma ho_memb_rsp[quotient_rsp]:
 
   180 lemma ho_memb_rsp[quot_respect]:
 
   181   "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
 
   181   "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
 
   182   by (simp add: memb_rsp)
 
   182   by (simp add: memb_rsp)
 
   183 
   183 
   184 lemma card1_rsp:
 
   184 lemma card1_rsp:
 
   185   fixes a b :: "'a list"
 
   185   fixes a b :: "'a list"
 
   186   assumes e: "a \<approx> b"
 
   186   assumes e: "a \<approx> b"
 
   187   shows "card1 a = card1 b"
 
   187   shows "card1 a = card1 b"
 
   188   using e by induct (simp_all add:memb_rsp)
 
   188   using e by induct (simp_all add:memb_rsp)
 
   189 
   189 
   190 lemma ho_card1_rsp[quotient_rsp]: 
   190 lemma ho_card1_rsp[quot_respect]: 
   191   "(op \<approx> ===> op =) card1 card1"
 
   191   "(op \<approx> ===> op =) card1 card1"
 
   192   by (simp add: card1_rsp)
 
   192   by (simp add: card1_rsp)
 
   193 
   193 
   194 lemma cons_rsp[quotient_rsp]:
 
   194 lemma cons_rsp[quot_respect]:
 
   195   fixes z
 
   195   fixes z
 
   196   assumes a: "xs \<approx> ys"
 
   196   assumes a: "xs \<approx> ys"
 
   197   shows "(z # xs) \<approx> (z # ys)"
 
   197   shows "(z # xs) \<approx> (z # ys)"
 
   198   using a by (rule list_eq.intros(5))
 
   198   using a by (rule list_eq.intros(5))
 
   199 
   199 
   200 lemma ho_cons_rsp[quotient_rsp]:
 
   200 lemma ho_cons_rsp[quot_respect]:
 
   201   "(op = ===> op \<approx> ===> op \<approx>) op # op #"
 
   201   "(op = ===> op \<approx> ===> op \<approx>) op # op #"
 
   202   by (simp add: cons_rsp)
 
   202   by (simp add: cons_rsp)
 
   203 
   203 
   204 lemma append_rsp_fst:
 
   204 lemma append_rsp_fst:
 
   205   assumes a : "l1 \<approx> l2"
 
   205   assumes a : "l1 \<approx> l2"
 
   252   apply (rule append_rsp_fst)
 
   252   apply (rule append_rsp_fst)
 
   253   using b apply (assumption)
 
   253   using b apply (assumption)
 
   254   apply (rule append_sym_rsp)
 
   254   apply (rule append_sym_rsp)
 
   255   done
 
   255   done
 
   256 
   256 
   257 lemma ho_append_rsp[quotient_rsp]:
 
   257 lemma ho_append_rsp[quot_respect]:
 
   258   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
 
   258   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
 
   259   by (simp add: append_rsp)
 
   259   by (simp add: append_rsp)
 
   260 
   260 
   261 lemma map_rsp:
 
   261 lemma map_rsp:
 
   262   assumes a: "a \<approx> b"
 
   262   assumes a: "a \<approx> b"
 
   264   using a
 
   264   using a
 
   265   apply (induct)
 
   265   apply (induct)
 
   266   apply(auto intro: list_eq.intros)
 
   266   apply(auto intro: list_eq.intros)
 
   267   done
 
   267   done
 
   268 
   268 
   269 lemma ho_map_rsp[quotient_rsp]:
 
   269 lemma ho_map_rsp[quot_respect]:
 
   270   "(op = ===> op \<approx> ===> op \<approx>) map map"
 
   270   "(op = ===> op \<approx> ===> op \<approx>) map map"
 
   271   by (simp add: map_rsp)
 
   271   by (simp add: map_rsp)
 
   272 
   272 
   273 lemma map_append:
 
   273 lemma map_append:
 
   274   "(map f (a @ b)) \<approx> (map f a) @ (map f b)"
 
   274   "(map f (a @ b)) \<approx> (map f a) @ (map f b)"
 
   275  by simp (rule list_eq_refl)
 
   275  by simp (rule list_eq_refl)
 
   276 
   276 
   277 lemma ho_fold_rsp[quotient_rsp]:
 
   277 lemma ho_fold_rsp[quot_respect]:
 
   278   "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
 
   278   "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
 
   279   apply (auto)
 
   279   apply (auto)
 
   280   apply (case_tac "rsp_fold x")
 
   280   apply (case_tac "rsp_fold x")
 
   281   prefer 2
 
   281   prefer 2
 
   282   apply (erule_tac list_eq.induct)
 
   282   apply (erule_tac list_eq.induct)
 
   284   apply (erule_tac list_eq.induct)
 
   284   apply (erule_tac list_eq.induct)
 
   285   apply (simp_all)
 
   285   apply (simp_all)
 
   286   apply (auto simp add: memb_rsp rsp_fold_def)
 
   286   apply (auto simp add: memb_rsp rsp_fold_def)
 
   287 done
 
   287 done
 
   288 
   288 
   289 lemma list_equiv_rsp[quotient_rsp]:
 
   289 lemma list_equiv_rsp[quot_respect]:
 
   290   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
 
   290   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
 
   291 by (auto intro: list_eq.intros)
 
   291 by (auto intro: list_eq.intros)
 
   292 
   292 
   293 print_quotients
 
   293 print_quotients
 
   294 
   294 
   353   apply (rule a)
 
   353   apply (rule a)
 
   354   apply (rule b)
 
   354   apply (rule b)
 
   355   apply (assumption)
 
   355   apply (assumption)
 
   356   done
 
   356   done
 
   357 
   357 
   358 thm quotient_thm
 
       
   359 
       
   360 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"
 
   358 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"
 
   361 apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *})
 
   359 apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *})
 
   362 done
 
   360 done
 
   363 
   361 
   364 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"
 
   362 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"
 
   400   fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 
   398   fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 
   401 where
 
   399 where
 
   402   "fset_case \<equiv> list_case"
 
   400   "fset_case \<equiv> list_case"
 
   403 
   401 
   404 (* Probably not true without additional assumptions about the function *)
 
   402 (* Probably not true without additional assumptions about the function *)
 
   405 lemma list_rec_rsp[quotient_rsp]:
 
   403 lemma list_rec_rsp[quot_respect]:
 
   406   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
 
   404   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
 
   407   apply (auto)
 
   405   apply (auto)
 
   408   apply (erule_tac list_eq.induct)
 
   406   apply (erule_tac list_eq.induct)
 
   409   apply (simp_all)
 
   407   apply (simp_all)
 
   410   sorry
 
   408   sorry
 
   411 
   409 
   412 lemma list_case_rsp[quotient_rsp]:
 
   410 lemma list_case_rsp[quot_respect]:
 
   413   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
 
   411   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
 
   414   apply (auto)
 
   412   apply (auto)
 
   415   sorry
 
   413   sorry
 
   416 
   414 
   417 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 
   415 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
nominal2