equal
deleted
inserted
replaced
14 |
14 |
15 lemma list_eq_refl: |
15 lemma list_eq_refl: |
16 shows "xs \<approx> xs" |
16 shows "xs \<approx> xs" |
17 by (induct xs) (auto intro: list_eq.intros) |
17 by (induct xs) (auto intro: list_eq.intros) |
18 |
18 |
19 lemma equiv_list_eq: |
19 lemma equivp_list_eq: |
20 shows "EQUIV list_eq" |
20 shows "equivp list_eq" |
21 unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def |
21 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
22 apply(auto intro: list_eq.intros list_eq_refl) |
22 apply(auto intro: list_eq.intros list_eq_refl) |
23 done |
23 done |
24 |
24 |
25 quotient fset = "'a list" / "list_eq" |
25 quotient fset = "'a list" / "list_eq" |
26 apply(rule equiv_list_eq) |
26 apply(rule equivp_list_eq) |
27 done |
27 done |
28 |
28 |
29 print_theorems |
29 print_theorems |
30 |
30 |
31 typ "'a fset" |
31 typ "'a fset" |
57 |
57 |
58 term append |
58 term append |
59 term FUNION |
59 term FUNION |
60 thm FUNION_def |
60 thm FUNION_def |
61 |
61 |
62 thm QUOTIENT_fset |
62 thm Quotient_fset |
63 |
63 |
64 thm QUOT_TYPE_I_fset.thm11 |
64 thm QUOT_TYPE_I_fset.thm11 |
65 |
65 |
66 |
66 |
67 fun |
67 fun |
416 lemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l" |
416 lemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l" |
417 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) |
417 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) |
418 done |
418 done |
419 |
419 |
420 quotient fset2 = "'a list" / "list_eq" |
420 quotient fset2 = "'a list" / "list_eq" |
421 apply(rule equiv_list_eq) |
421 apply(rule equivp_list_eq) |
422 done |
422 done |
423 |
423 |
424 quotient_def |
424 quotient_def |
425 EMPTY2 :: "'a fset2" |
425 EMPTY2 :: "'a fset2" |
426 where |
426 where |
429 quotient_def |
429 quotient_def |
430 INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2" |
430 INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2" |
431 where |
431 where |
432 "INSERT2 \<equiv> op #" |
432 "INSERT2 \<equiv> op #" |
433 |
433 |
434 ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *} |
434 ML {* val quot = @{thms Quotient_fset Quotient_fset2} *} |
435 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} |
435 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} |
436 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *} |
436 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *} |
437 |
437 |
438 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 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" |
439 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) |
439 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) |