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 640 5cb44fe9ae8e
parent 639 820c64273ce0
parent 638 e472aa533a24
child 642 005e4edc65ef
equal deleted inserted replaced
639:820c64273ce0 640:5cb44fe9ae8e 
   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 
   355   apply (rule a)
 
   355   apply (rule a)
 
   356   apply (rule b)
 
   356   apply (rule b)
 
   357   apply (assumption)
 
   357   apply (assumption)
 
   358   done
 
   358   done
 
   359 
   359 
   360 thm quotient_thm
 
       
   361 
       
   362 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"
 
   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"
 
   363 apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *})
 
   361 apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *})
 
   364 done
 
   362 done
 
   365 
   363 
   366 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"
 
   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"
 
   402   fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 
   400   fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 
   403 where
 
   401 where
 
   404   "fset_case \<equiv> list_case"
 
   402   "fset_case \<equiv> list_case"
 
   405 
   403 
   406 (* Probably not true without additional assumptions about the function *)
 
   404 (* Probably not true without additional assumptions about the function *)
 
   407 lemma list_rec_rsp[quotient_rsp]:
 
   405 lemma list_rec_rsp[quot_respect]:
 
   408   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
 
   406   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
 
   409   apply (auto)
 
   407   apply (auto)
 
   410   apply (erule_tac list_eq.induct)
 
   408   apply (erule_tac list_eq.induct)
 
   411   apply (simp_all)
 
   409   apply (simp_all)
 
   412   sorry
 
   410   sorry
 
   413 
   411 
   414 lemma list_case_rsp[quotient_rsp]:
 
   412 lemma list_case_rsp[quot_respect]:
 
   415   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
 
   413   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
 
   416   apply (auto)
 
   414   apply (auto)
 
   417   sorry
 
   415   sorry
 
   418 
   416 
   419 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 
   417 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 
   432 
   430 
   433 lemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))"
 
   431 lemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))"
 
   434 sorry
 
   432 sorry
 
   435 
   433 
   436 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))"
 
   434 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))"
 
   437 apply(lifting_setup rule: ttt2)
 
   435 apply(lifting_setup ttt2)
 
   438 apply(regularize)
 
   436 apply(regularize)
 
   439 apply(rule impI)
 
   437 apply(rule impI)
 
   440 apply(simp)
 
   438 apply(simp)
 
   441 apply(rule allI)
 
   439 apply(rule allI)
 
   442 apply(rule list_eq_refl)
 
   440 apply(rule list_eq_refl)
 
   443 apply(injection)
 
   441 apply(injection)
 
   444 apply(tactic {* clean_tac @{context} 1 *})
 
   442 apply(tactic {* clean_tac @{context} 1 *}) (* This is an example that needs lambda_prs twice *)
 
   445 apply(tactic {* clean_tac @{context} 1 *}) (* TODO: needs lambda_prs twice *)
 
       
   446 done
 
   443 done
 
   447 
   444 
   448 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"
 
   445 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"
 
   449 sorry
 
   446 sorry
 
   450 
   447
nominal2