476 term LM' |
476 term LM' |
477 term VR' |
477 term VR' |
478 term AP' |
478 term AP' |
479 |
479 |
480 text {* finite set example *} |
480 text {* finite set example *} |
481 |
481 print_syntax |
482 inductive |
482 inductive |
483 list_eq ("_ \<approx> _") |
483 list_eq (infix "\<approx>" 50) |
484 where |
484 where |
485 "a#b#xs \<approx> b#a#xs" |
485 "a#b#xs \<approx> b#a#xs" |
486 | "[] \<approx> []" |
486 | "[] \<approx> []" |
487 | "xs \<approx> ys \<Longrightarrow> ys \<approx> xs" |
487 | "xs \<approx> ys \<Longrightarrow> ys \<approx> xs" |
488 | "a#a#xs \<approx> a#xs" |
488 | "a#a#xs \<approx> a#xs" |
489 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys" |
489 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys" |
490 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3" |
490 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3" |
491 |
491 |
492 lemma list_eq_sym: |
492 lemma list_eq_sym: |
493 shows "xs \<approx> xs" |
493 shows "xs \<approx> xs" |
494 apply(induct xs) |
494 apply (induct xs) |
495 apply(auto intro: list_eq.intros) |
495 apply (auto intro: list_eq.intros) |
496 done |
496 done |
497 |
497 |
498 lemma equiv_list_eq: |
498 lemma equiv_list_eq: |
499 shows "EQUIV list_eq" |
499 shows "EQUIV list_eq" |
500 unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def |
500 unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def |
501 apply(auto intro: list_eq.intros list_eq_sym) |
501 apply(auto intro: list_eq.intros list_eq_sym) |
502 done |
502 done |
503 |
503 |
504 local_setup {* |
504 local_setup {* |
505 typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd |
505 typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd |
506 *} |
506 *} |
507 |
507 |
545 |
545 |
546 (* This code builds the interpretation from ML level, currently only |
546 (* This code builds the interpretation from ML level, currently only |
547 for fset *) |
547 for fset *) |
548 |
548 |
549 ML {* val mthd = Method.SIMPLE_METHOD (rtac @{thm QUOT_TYPE_fset} 1 THEN |
549 ML {* val mthd = Method.SIMPLE_METHOD (rtac @{thm QUOT_TYPE_fset} 1 THEN |
550 simp_tac (HOL_basic_ss addsimps @{thms REP_fset_def[symmetric]}) 1 THEN |
550 simp_tac (HOL_basic_ss addsimps @{thms REP_fset_def [symmetric]}) 1 THEN |
551 simp_tac (HOL_basic_ss addsimps @{thms ABS_fset_def[symmetric]}) 1) *} |
551 simp_tac (HOL_basic_ss addsimps @{thms ABS_fset_def [symmetric]}) 1) *} |
552 ML {* val mthdt = Method.Basic (fn _ => mthd) *} |
552 ML {* val mthdt = Method.Basic (fn _ => mthd) *} |
553 ML {* val bymt = Proof.global_terminal_proof (mthdt, NONE) *} |
553 ML {* val bymt = Proof.global_terminal_proof (mthdt, NONE) *} |
554 ML {* val exp_i = [((Locale.intern @{theory} "QUOT_TYPE"),(("QUOT_TYPE_fset_i", true), |
554 ML {* val exp_i = [((Locale.intern @{theory} "QUOT_TYPE"),(("QUOT_TYPE_fset_i", true), |
555 Expression.Named [ |
555 Expression.Named [ |
556 ("R",@{term list_eq}), |
556 ("R",@{term list_eq}), |
575 done |
575 done |
576 *) |
576 *) |
577 |
577 |
578 |
578 |
579 |
579 |
580 fun |
580 fun |
581 membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" ("_ memb _") |
581 membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100) |
582 where |
582 where |
583 m1: "(x memb []) = False" |
583 m1: "(x memb []) = False" |
584 | m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))" |
584 | m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))" |
585 |
585 |
586 lemma mem_respects: |
586 lemma mem_respects: |
587 fixes z |
587 fixes z |
588 assumes a: "list_eq x y" |
588 assumes a: "list_eq x y" |
589 shows "(z memb x) = (z memb y)" |
589 shows "(z memb x) = (z memb y)" |
590 using a |
590 using a by induct auto |
591 apply(induct) |
591 |
592 apply(auto) |
|
593 done |
|
594 |
592 |
595 lemma cons_preserves: |
593 lemma cons_preserves: |
596 fixes z |
594 fixes z |
597 assumes a: "xs \<approx> ys" |
595 assumes a: "xs \<approx> ys" |
598 shows "(z # xs) \<approx> (z # ys)" |
596 shows "(z # xs) \<approx> (z # ys)" |
599 using a |
597 using a by (rule QuotMain.list_eq.intros(5)) |
600 apply (rule QuotMain.list_eq.intros(5)) |
|
601 done |
|
602 |
598 |
603 ML {* |
599 ML {* |
604 fun unlam_def orig_ctxt ctxt t = |
600 fun unlam_def orig_ctxt ctxt t = |
605 let |
601 let val rhs = Thm.rhs_of t in |
606 val (v, rest) = Thm.dest_abs NONE (Thm.rhs_of t) |
602 (case try (Thm.dest_abs NONE) rhs of |
607 val (vname, vt) = Term.dest_Free (Thm.term_of v) |
603 SOME (v, vt) => |
608 val ([vnname], ctxt) = Variable.variant_fixes [vname] ctxt |
604 let |
609 val nv = Free(vnname, vt) |
605 val (vname, vt) = Term.dest_Free (Thm.term_of v) |
610 val t2 = Drule.fun_cong_rule t (Thm.cterm_of @{theory} nv) |
606 val ([vnname], ctxt) = Variable.variant_fixes [vname] ctxt |
611 val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2 |
607 val nv = Free(vnname, vt) |
612 in unlam_def orig_ctxt ctxt tnorm end |
608 val t2 = Drule.fun_cong_rule t (Thm.cterm_of (ProofContext.theory_of ctxt) nv) |
613 handle CTERM _ => singleton (ProofContext.export ctxt orig_ctxt) t |
609 val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2 |
|
610 in unlam_def orig_ctxt ctxt tnorm end |
|
611 | NONE => singleton (ProofContext.export ctxt orig_ctxt) t) |
|
612 end |
614 *} |
613 *} |
615 |
614 |
616 local_setup {* |
615 local_setup {* |
617 make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
616 make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
618 *} |
617 *} |