27 then show "R (Eps (R x)) = R x" |
27 then show "R (Eps (R x)) = R x" |
28 using equiv unfolding EQUIV_def by simp |
28 using equiv unfolding EQUIV_def by simp |
29 qed |
29 qed |
30 |
30 |
31 theorem thm10: |
31 theorem thm10: |
32 shows "ABS (REP a) = a" |
32 shows "ABS (REP a) \<equiv> a" |
33 unfolding ABS_def REP_def |
33 apply (rule eq_reflection) |
|
34 unfolding ABS_def REP_def |
34 proof - |
35 proof - |
35 from rep_prop |
36 from rep_prop |
36 obtain x where eq: "Rep a = R x" by auto |
37 obtain x where eq: "Rep a = R x" by auto |
37 have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp |
38 have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp |
38 also have "\<dots> = Abs (R x)" using lem9 by simp |
39 also have "\<dots> = Abs (R x)" using lem9 by simp |
759 lemma |
760 lemma |
760 shows " |
761 shows " |
761 (UNION EMPTY s = s) & |
762 (UNION EMPTY s = s) & |
762 ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))" |
763 ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))" |
763 apply (simp add: yyy) |
764 apply (simp add: yyy) |
764 apply (rule QUOT_TYPE_I_fset.thm10) |
765 apply (simp add: QUOT_TYPE_I_fset.thm10) |
765 done |
766 done |
766 |
767 |
767 ML {* |
768 ML {* |
768 fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x) |
769 fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x) |
769 val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}] |
770 val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}] |
933 ML {* |
934 ML {* |
934 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(4)})) |
935 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(4)})) |
935 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
936 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
936 val cgoal = cterm_of @{theory} goal |
937 val cgoal = cterm_of @{theory} goal |
937 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
938 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
938 (* Why doesn't this work? *) |
939 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
939 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10 QUOT_TYPE_I_fset.REPS_same} cgoal2) |
940 *} |
940 *} |
941 |
941 thm QUOT_TYPE_I_fset.thm10 |
942 (* It is the same, but we need a name for it. *) |
942 thm QUOT_TYPE_I_fset.REPS_same |
943 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} sorry |
943 |
944 lemma zzz : |
944 (* keep it commented out, until we get a proving mechanism *) |
945 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> |
945 (*prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *}*) |
|
946 lemma zzz : |
|
947 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> |
|
948 REP_fset (INSERT a (ABS_fset xs))) = (a # a # xs \<approx> a # xs)" |
946 REP_fset (INSERT a (ABS_fset xs))) = (a # a # xs \<approx> a # xs)" |
949 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
947 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
950 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
948 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
951 (* apply (simp only: QUOT_TYPE_I_fset.thm10)*) |
|
952 apply (rule QUOT_TYPE_I_fset.R_trans2) |
949 apply (rule QUOT_TYPE_I_fset.R_trans2) |
953 apply (tactic {* foo_tac' 1 *}) |
950 apply (tactic {* foo_tac' 1 *}) |
954 apply (tactic {* foo_tac' 1 *}) |
951 apply (tactic {* foo_tac' 1 *}) |
955 apply (tactic {* foo_tac' 1 *}) |
952 apply (tactic {* foo_tac' 1 *}) |
956 apply (tactic {* foo_tac' 1 *}) |
953 apply (tactic {* foo_tac' 1 *}) |
957 apply (tactic {* foo_tac' 1 *}) |
954 apply (tactic {* foo_tac' 1 *}) |
958 apply (tactic {* foo_tac' 1 *}) |
955 apply (tactic {* foo_tac' 1 *}) |
959 apply (tactic {* foo_tac' 1 *}) |
956 apply (tactic {* foo_tac' 1 *}) |
960 apply (tactic {* foo_tac' 1 *}) |
957 apply (tactic {* foo_tac' 1 *}) |
961 done |
958 done |
|
959 |
|
960 lemma zzz' : |
|
961 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))" |
|
962 using list_eq.intros(4) by (simp only: zzz) |
|
963 |
|
964 thm QUOT_TYPE_I_fset.REPS_same |
|
965 ML {* MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *} |
962 |
966 |
963 thm list_eq.intros(5) |
967 thm list_eq.intros(5) |
964 ML {* |
968 ML {* |
965 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)})) |
969 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)})) |
966 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
970 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |