75 apply(subst thm11[symmetric]) |
75 apply(subst thm11[symmetric]) |
76 apply(simp add: equiv[simplified EQUIV_def]) |
76 apply(simp add: equiv[simplified EQUIV_def]) |
77 done |
77 done |
78 |
78 |
79 lemma R_trans: |
79 lemma R_trans: |
80 assumes ab: "R a b" |
80 assumes ab: "R a b" |
81 and bc: "R b c" |
81 and bc: "R b c" |
82 shows "R a c" |
82 shows "R a c" |
83 proof - |
83 proof - |
84 have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
84 have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
85 moreover have ab: "R a b" by fact |
85 moreover have ab: "R a b" by fact |
86 moreover have bc: "R b c" by fact |
86 moreover have bc: "R b c" by fact |
87 ultimately show "R a c" unfolding TRANS_def by blast |
87 ultimately show "R a c" unfolding TRANS_def by blast |
88 qed |
88 qed |
89 |
89 |
90 lemma R_sym: |
90 lemma R_sym: |
91 assumes ab: "R a b" |
91 assumes ab: "R a b" |
92 shows "R b a" |
92 shows "R b a" |
93 proof - |
93 proof - |
94 have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
94 have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
95 then show "R b a" using ab unfolding SYM_def by blast |
95 then show "R b a" using ab unfolding SYM_def by blast |
96 qed |
96 qed |
97 |
97 |
98 lemma R_trans2: |
98 lemma R_trans2: |
99 assumes ac: "R a c" |
99 assumes ac: "R a c" |
100 and bd: "R b d" |
100 and bd: "R b d" |
101 shows "R a b = R c d" |
101 shows "R a b = R c d" |
102 proof |
102 proof |
103 assume "R a b" |
103 assume "R a b" |
104 then have "R b a" using R_sym by blast |
104 then have "R b a" using R_sym by blast |
154 *} |
154 *} |
155 |
155 |
156 ML {* |
156 ML {* |
157 (* makes the new type definitions and proves non-emptyness*) |
157 (* makes the new type definitions and proves non-emptyness*) |
158 fun typedef_make (qty_name, rel, ty) lthy = |
158 fun typedef_make (qty_name, rel, ty) lthy = |
159 let |
159 let |
160 val typedef_tac = |
160 val typedef_tac = |
161 EVERY1 [rewrite_goal_tac @{thms mem_def}, |
161 EVERY1 [rewrite_goal_tac @{thms mem_def}, |
162 rtac @{thm exI}, |
162 rtac @{thm exI}, |
163 rtac @{thm exI}, |
163 rtac @{thm exI}, |
164 rtac @{thm refl}] |
164 rtac @{thm refl}] |
165 in |
165 in |
166 LocalTheory.theory_result |
166 LocalTheory.theory_result |
167 (Typedef.add_typedef false NONE |
167 (Typedef.add_typedef false NONE |
168 (qty_name, map fst (Term.add_tfreesT ty []), NoSyn) |
168 (qty_name, map fst (Term.add_tfreesT ty []), NoSyn) |
213 val typedef_quotient_thm_tac = |
213 val typedef_quotient_thm_tac = |
214 EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]), |
214 EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]), |
215 rtac @{thm QUOT_TYPE.QUOTIENT}, |
215 rtac @{thm QUOT_TYPE.QUOTIENT}, |
216 rtac quot_type_thm] |
216 rtac quot_type_thm] |
217 in |
217 in |
218 Goal.prove lthy [] [] goal |
218 Goal.prove lthy [] [] goal |
219 (K typedef_quotient_thm_tac) |
219 (K typedef_quotient_thm_tac) |
220 end |
220 end |
221 *} |
221 *} |
222 |
222 |
223 text {* two wrappers for define and note *} |
223 text {* two wrappers for define and note *} |
923 ML {*@{thm arg_cong2}*} |
923 ML {*@{thm arg_cong2}*} |
924 ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *} |
924 ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *} |
925 ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *} |
925 ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *} |
926 ML {* |
926 ML {* |
927 Toplevel.program (fn () => |
927 Toplevel.program (fn () => |
928 Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2} |
928 Drule.instantiate' [SOME cT, SOME cT, SOME @{ctyp bool}] [NONE, NONE, NONE, NONE, SOME (@{cpat "op ="})] @{thm arg_cong2} |
929 ) |
929 ) |
930 *} |
930 *} |
931 |
931 |
932 ML {* |
932 ML {* |
933 fun split_binop_conv t = |
933 fun split_binop_conv t = |
936 val (lhs, rhs) = dest_ceq t; |
936 val (lhs, rhs) = dest_ceq t; |
937 val (bop, _) = dest_cbinop lhs; |
937 val (bop, _) = dest_cbinop lhs; |
938 val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp; |
938 val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp; |
939 val [cmT, crT] = Thm.dest_ctyp cr2; |
939 val [cmT, crT] = Thm.dest_ctyp cr2; |
940 in |
940 in |
941 Drule.instantiate' [SOME clT,SOME cmT,SOME crT] [NONE,NONE,NONE,NONE,SOME bop] @{thm arg_cong2} |
941 Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2} |
942 end |
942 end |
943 *} |
943 *} |
944 |
944 |
945 ML {* |
945 ML {* |
946 fun split_arg_conv t = |
946 fun split_arg_conv t = |
947 let |
947 let |
948 val (lhs, rhs) = dest_ceq t; |
948 val (lhs, rhs) = dest_ceq t; |
949 val (lop, larg) = Thm.dest_comb lhs; |
949 val (lop, larg) = Thm.dest_comb lhs; |
950 val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp; |
950 val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp; |
951 in |
951 in |
952 Drule.instantiate' [SOME caT,SOME crT] [NONE,NONE,SOME lop] @{thm arg_cong} |
952 Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong} |
953 end |
953 end |
954 *} |
954 *} |
955 |
955 |
956 ML {* |
956 ML {* |
957 fun split_binop_tac n thm = |
957 fun split_binop_tac n thm = |
999 CHANGED o (ObjectLogic.full_atomize_tac) |
999 CHANGED o (ObjectLogic.full_atomize_tac) |
1000 ]) |
1000 ]) |
1001 *} |
1001 *} |
1002 |
1002 |
1003 ML {* |
1003 ML {* |
1004 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1})) |
1004 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) |
1005 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1005 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1006 val cgoal = cterm_of @{theory} goal |
1006 val cgoal = cterm_of @{theory} goal |
1007 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1007 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1008 *} |
1008 *} |
1009 |
1009 |
1015 apply (tactic {* foo_tac' @{context} 1 *}) |
1015 apply (tactic {* foo_tac' @{context} 1 *}) |
1016 done |
1016 done |
1017 |
1017 |
1018 thm length_append (* Not true but worth checking that the goal is correct *) |
1018 thm length_append (* Not true but worth checking that the goal is correct *) |
1019 ML {* |
1019 ML {* |
1020 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append})) |
1020 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append})) |
1021 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1021 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1022 val cgoal = cterm_of @{theory} goal |
1022 val cgoal = cterm_of @{theory} goal |
1023 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1023 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1024 *} |
1024 *} |
1025 prove {* Thm.term_of cgoal2 *} |
1025 prove {* Thm.term_of cgoal2 *} |
1027 apply (tactic {* foo_tac' @{context} 1 *}) |
1027 apply (tactic {* foo_tac' @{context} 1 *}) |
1028 sorry |
1028 sorry |
1029 |
1029 |
1030 thm m2 |
1030 thm m2 |
1031 ML {* |
1031 ML {* |
1032 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2})) |
1032 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) |
1033 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1033 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1034 val cgoal = cterm_of @{theory} goal |
1034 val cgoal = cterm_of @{theory} goal |
1035 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1035 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1036 *} |
1036 *} |
1037 prove {* Thm.term_of cgoal2 *} |
1037 prove {* Thm.term_of cgoal2 *} |
1039 apply (tactic {* foo_tac' @{context} 1 *}) |
1039 apply (tactic {* foo_tac' @{context} 1 *}) |
1040 done |
1040 done |
1041 |
1041 |
1042 thm list_eq.intros(4) |
1042 thm list_eq.intros(4) |
1043 ML {* |
1043 ML {* |
1044 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(4)})) |
1044 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)})) |
1045 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1045 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1046 val cgoal = cterm_of @{theory} goal |
1046 val cgoal = cterm_of @{theory} goal |
1047 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1047 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1048 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
1048 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
1049 *} |
1049 *} |
1073 A variable export will still be necessary in the end, but this is already the final theorem. |
1073 A variable export will still be necessary in the end, but this is already the final theorem. |
1074 *} |
1074 *} |
1075 ML {* |
1075 ML {* |
1076 Toplevel.program (fn () => |
1076 Toplevel.program (fn () => |
1077 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
1077 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
1078 Drule.instantiate' [] [NONE,SOME (@{cpat "REP_fset x"})] zzz'' |
1078 Drule.instantiate' [] [NONE, SOME (@{cpat "REP_fset x"})] zzz'' |
1079 ) |
1079 ) |
1080 ) |
1080 ) |
1081 *} |
1081 *} |
1082 |
1082 |
1083 |
1083 |
1084 thm list_eq.intros(5) |
1084 thm list_eq.intros(5) |
1085 ML {* |
1085 ML {* |
1086 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)})) |
1086 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)})) |
1087 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1087 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1088 *} |
1088 *} |
1089 ML {* |
1089 ML {* |
1090 val cgoal = |
1090 val cgoal = |
1091 Toplevel.program (fn () => |
1091 Toplevel.program (fn () => |
1092 cterm_of @{theory} goal |
1092 cterm_of @{theory} goal |
1093 ) |
1093 ) |
1094 *} |
1094 *} |
1095 ML {* |
1095 ML {* |