--- a/QuotMain.thy Fri Sep 25 14:50:35 2009 +0200
+++ b/QuotMain.thy Fri Sep 25 16:50:11 2009 +0200
@@ -77,8 +77,8 @@
done
lemma R_trans:
- assumes ab: "R a b"
- and bc: "R b c"
+ assumes ab: "R a b"
+ and bc: "R b c"
shows "R a c"
proof -
have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
@@ -88,15 +88,15 @@
qed
lemma R_sym:
- assumes ab: "R a b"
+ assumes ab: "R a b"
shows "R b a"
proof -
have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
then show "R b a" using ab unfolding SYM_def by blast
qed
-lemma R_trans2:
- assumes ac: "R a c"
+lemma R_trans2:
+ assumes ac: "R a c"
and bd: "R b d"
shows "R a b = R c d"
proof
@@ -115,24 +115,27 @@
lemma REPS_same:
shows "R (REP a) (REP b) \<equiv> (a = b)"
- apply (rule eq_reflection)
-proof
- assume as: "R (REP a) (REP b)"
- from rep_prop
- obtain x y
- where eqs: "Rep a = R x" "Rep b = R y" by blast
- from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
- then have "R x (Eps (R y))" using lem9 by simp
- then have "R (Eps (R y)) x" using R_sym by blast
- then have "R y x" using lem9 by simp
- then have "R x y" using R_sym by blast
- then have "ABS x = ABS y" using thm11 by simp
- then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
- then show "a = b" using rep_inverse by simp
-next
- assume ab: "a = b"
- have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
- then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto
+proof -
+ have "R (REP a) (REP b) = (a = b)"
+ proof
+ assume as: "R (REP a) (REP b)"
+ from rep_prop
+ obtain x y
+ where eqs: "Rep a = R x" "Rep b = R y" by blast
+ from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
+ then have "R x (Eps (R y))" using lem9 by simp
+ then have "R (Eps (R y)) x" using R_sym by blast
+ then have "R y x" using lem9 by simp
+ then have "R x y" using R_sym by blast
+ then have "ABS x = ABS y" using thm11 by simp
+ then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
+ then show "a = b" using rep_inverse by simp
+ next
+ assume ab: "a = b"
+ have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
+ then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto
+ qed
+ then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
qed
end
@@ -156,11 +159,11 @@
ML {*
(* makes the new type definitions and proves non-emptyness*)
fun typedef_make (qty_name, rel, ty) lthy =
-let
+let
val typedef_tac =
EVERY1 [rewrite_goal_tac @{thms mem_def},
- rtac @{thm exI},
- rtac @{thm exI},
+ rtac @{thm exI},
+ rtac @{thm exI},
rtac @{thm refl}]
in
LocalTheory.theory_result
@@ -215,7 +218,7 @@
rtac @{thm QUOT_TYPE.QUOTIENT},
rtac quot_type_thm]
in
- Goal.prove lthy [] [] goal
+ Goal.prove lthy [] [] goal
(K typedef_quotient_thm_tac)
end
*}
@@ -322,8 +325,8 @@
| app "trm" "trm"
| lam "nat" "trm"
-axiomatization
- RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"
+axiomatization
+ RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"
where
r_eq: "EQUIV RR"
@@ -676,66 +679,21 @@
fixes xs :: "'a list"
assumes a : "x memb xs"
shows "x # xs \<approx> xs"
- using a apply (induct xs)
- apply (simp_all)
- apply (meson)
- apply (simp_all add: list_eq.intros(4))
- proof -
- fix a :: "'a"
- fix xs :: "'a list"
- assume a1 : "x # xs \<approx> xs"
- assume a2 : "x memb xs"
- have a3 : "x # a # xs \<approx> a # x # xs" using list_eq.intros(1)[of "x"] by blast
- have a4 : "a # x # xs \<approx> a # xs" using a1 list_eq.intros(5)[of "x # xs" "xs"] by simp
- then show "x # a # xs \<approx> a # xs" using a3 list_eq.intros(6) by blast
- qed
+ using a
+ apply (induct xs)
+ apply (auto intro: list_eq.intros)
+ done
lemma card1_suc:
fixes xs :: "'a list"
fixes n :: "nat"
assumes c: "card1 xs = Suc n"
shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)"
- using c apply (induct xs)
- apply (simp)
-(* apply (rule allI)*)
- proof -
- fix a :: "'a"
- fix xs :: "'a list"
- fix n :: "nat"
- assume a1: "card1 xs = Suc n \<Longrightarrow> \<exists>a ys. \<not> a memb ys \<and> xs \<approx> a # ys"
- assume a2: "card1 (a # xs) = Suc n"
- from a1 a2 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys"
- apply -
- apply (rule True_or_False [of "a memb xs", THEN disjE])
- apply (simp_all add: card1_cons if_True simp_thms)
- proof -
- assume a1: "\<exists>a ys. \<not> a memb ys \<and> xs \<approx> a # ys"
- assume a2: "card1 xs = Suc n"
- assume a3: "a memb xs"
- from a1 obtain b ys where a5: "\<not> b memb ys \<and> xs \<approx> b # ys" by blast
- from a2 a3 a5 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys"
- apply -
- apply (rule_tac x = "b" in exI)
- apply (rule_tac x = "ys" in exI)
- apply (simp_all)
- proof -
- assume a1: "a memb xs"
- assume a2: "\<not> b memb ys \<and> xs \<approx> b # ys"
- then have a3: "xs \<approx> b # ys" by simp
- have "a # xs \<approx> xs" using a1 mem_cons[of "a" "xs"] by simp
- then show "a # xs \<approx> b # ys" using a3 list_eq.intros(6) by blast
- qed
-next
- assume a2: "\<not> a memb xs"
- from a2 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys"
- apply -
- apply (rule_tac x = "a" in exI)
- apply (rule_tac x = "xs" in exI)
- apply (simp)
- apply (rule list_eq_sym)
- done
- qed
-qed
+ using c
+apply(induct xs)
+apply (metis Suc_neq_Zero card1_0)
+apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_sym mem_cons)
+done
lemma cons_preserves:
fixes z
@@ -859,8 +817,6 @@
val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}, @{const_name "card1"}]
*}
-ML lambda
-
ML {*
fun build_goal thm constructors lifted_type mk_rep_abs =
let
@@ -872,17 +828,8 @@
in
if type_of t = lifted_type then mk_rep_abs t else t
end
-(* handle TYPE _ => t*)
- fun build_aux (Abs (s, t, tr)) =
- let
- val [(fresh_s, _)] = Variable.variant_frees @{context} [] [(s, ())];
- val newv = Free (fresh_s, t);
- val str = subst_bound (newv, tr);
- val rec_term = build_aux str;
- val bound_term = lambda newv rec_term
- in
- bound_term
- end
+ handle TYPE _ => t
+ fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr))
| build_aux (f $ a) =
let
val (f, args) = strip_comb (f $ a)
@@ -898,8 +845,13 @@
Logic.mk_equals ((build_aux concl2), concl2)
end *}
+ML {* val emptyt = symmetric (unlam_def @{context} @{thm EMPTY_def}) *}
+ML {* val in_t = symmetric (unlam_def @{context} @{thm IN_def}) *}
+ML {* val uniont = symmetric (unlam_def @{context} @{thm UNION_def}) *}
+ML {* val cardt = symmetric (unlam_def @{context} @{thm card_def}) *}
+ML {* val insertt = symmetric (unlam_def @{context} @{thm INSERT_def}) *}
ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
-ML {* val fset_defs_sym = map (fn t => symmetric (unlam_def @{context} t)) fset_defs *}
+ML {* val fset_defs_sym = [emptyt, in_t, uniont, cardt, insertt] *}
ML {*
fun dest_cbinop t =
@@ -910,6 +862,7 @@
(bop, (lhs, rhs))
end
*}
+
ML {*
fun dest_ceq t =
let
@@ -919,58 +872,37 @@
if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))
end
*}
+
ML Thm.instantiate
ML {*@{thm arg_cong2}*}
ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *}
ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *}
ML {*
Toplevel.program (fn () =>
- Drule.instantiate' [SOME cT, SOME cT, SOME @{ctyp bool}] [NONE, NONE, NONE, NONE, SOME (@{cpat "op ="})] @{thm arg_cong2}
+ Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2}
)
*}
ML {*
- fun split_binop_conv t =
+ fun foo_conv t =
let
- val _ = tracing (Syntax.string_of_term @{context} (term_of t))
val (lhs, rhs) = dest_ceq t;
val (bop, _) = dest_cbinop lhs;
val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
val [cmT, crT] = Thm.dest_ctyp cr2;
in
- Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}
- end
-*}
-
-ML {*
- fun split_arg_conv t =
- let
- val (lhs, rhs) = dest_ceq t;
- val (lop, larg) = Thm.dest_comb lhs;
- val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
- in
- Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}
+ Drule.instantiate' [SOME clT,SOME cmT,SOME crT] [NONE,NONE,NONE,NONE,SOME bop] @{thm arg_cong2}
end
*}
ML {*
- fun split_binop_tac n thm =
+ fun foo_tac n thm =
let
val concl = Thm.cprem_of thm n;
val (_, cconcl) = Thm.dest_comb concl;
- val rewr = split_binop_conv cconcl;
- in
- rtac rewr n thm
- end
- handle CTERM _ => Seq.empty
-*}
-
-ML {*
- fun split_arg_tac n thm =
- let
- val concl = Thm.cprem_of thm n;
- val (_, cconcl) = Thm.dest_comb concl;
- val rewr = split_arg_conv cconcl;
+ val rewr = foo_conv cconcl;
+(* val _ = tracing (Display.string_of_thm @{context} rewr)
+ val _ = tracing (Display.string_of_thm @{context} thm)*)
in
rtac rewr n thm
end
@@ -990,18 +922,15 @@
rtac @{thm list_eq_sym},
rtac @{thm cons_preserves},
rtac @{thm mem_respects},
- rtac @{thm card1_rsp},
rtac @{thm QUOT_TYPE_I_fset.R_trans2},
CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
- DatatypeAux.cong_tac,
- rtac @{thm ext},
-(* rtac @{thm eq_reflection}*)
+ foo_tac,
CHANGED o (ObjectLogic.full_atomize_tac)
])
*}
ML {*
- val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
+ val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
val cgoal = cterm_of @{theory} goal
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
@@ -1017,7 +946,7 @@
thm length_append (* Not true but worth checking that the goal is correct *)
ML {*
- val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append}))
+ val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append}))
val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
val cgoal = cterm_of @{theory} goal
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
@@ -1029,7 +958,7 @@
thm m2
ML {*
- val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
+ val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2}))
val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
val cgoal = cterm_of @{theory} goal
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
@@ -1041,7 +970,7 @@
thm list_eq.intros(4)
ML {*
- val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))
+ val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(4)}))
val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
val cgoal = cterm_of @{theory} goal
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
@@ -1067,19 +996,33 @@
thm QUOT_TYPE_I_fset.REPS_same
ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}
+ML Drule.instantiate'
+ML {* zzz'' *}
+text {*
+ A variable export will still be necessary in the end, but this is already the final theorem.
+*}
+ML {*
+ Toplevel.program (fn () =>
+ MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
+ Drule.instantiate' [] [NONE,SOME (@{cpat "REP_fset x"})] zzz''
+ )
+ )
+*}
+
+
thm list_eq.intros(5)
ML {*
- val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
+ val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)}))
val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
*}
ML {*
- val cgoal =
+ val cgoal =
Toplevel.program (fn () =>
cterm_of @{theory} goal
)
*}
ML {*
- val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
+ val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
*}
prove {* Thm.term_of cgoal2 *}
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
@@ -1087,9 +1030,10 @@
done
thm list.induct
+ML {* Logic.list_implies ((Thm.prems_of @{thm list.induct}), (Thm.concl_of @{thm list.induct})) *}
ML {*
- val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct}))
+ val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list.induct}))
*}
ML {*
val goal =
@@ -1099,89 +1043,33 @@
*}
ML {*
val cgoal = cterm_of @{theory} goal
+ val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
*}
-ML {*
- val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
-*}
-
+ML fset_defs_sym
prove {* (Thm.term_of cgoal2) *}
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
- apply (tactic {* foo_tac' @{context} 1 *})
+ apply (atomize(full))
+ apply (rule_tac trueprop_cong)
+ apply (atomize(full))
+ apply (tactic {* foo_tac' @{context} 1 *})
+ apply (rule_tac f = "P" in arg_cong)
sorry
-ML {*
- fun lift_theorem_fset_aux thm lthy =
- let
- val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;
- val goal = build_goal novars consts @{typ "'a list"} mk_rep_abs;
- val cgoal = cterm_of @{theory} goal;
- val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);
- val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (foo_tac' @{context}) 1;
- val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac);
- val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm)))
- val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm;
- val [nthm3] = ProofContext.export lthy2 lthy [nthm2]
- in
- nthm3
- end
-*}
-
-ML {* lift_theorem_fset_aux @{thm m1} @{context} *}
-
-ML {*
- fun lift_theorem_fset name thm lthy =
- let
- val lifted_thm = lift_theorem_fset_aux thm lthy;
- val (_, lthy2) = note_thm (name, lifted_thm) lthy;
- in
- lthy2
- end;
-*}
-
-local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *}
-local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}
-local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
-local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}
-
-thm m1_lift
-thm leqi4_lift
-thm leqi5_lift
-thm m2_lift
-
-ML Drule.instantiate'
-text {*
- We lost the schematic variable again :(.
- Another variable export will still be necessary...
-*}
-ML {*
- Toplevel.program (fn () =>
- MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
- Drule.instantiate' [] [NONE, NONE, SOME (@{cpat "REP_fset x"})] @{thm m2_lift}
- )
- )
-*}
-
-
-
-
-ML {* MRS *}
thm card1_suc
ML {*
- val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm card1_suc}))
+ val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm card1_suc}))
*}
ML {*
val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
*}
ML {*
val cgoal = cterm_of @{theory} goal
- val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
+ val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
*}
-ML {* @{term "\<exists>x. P x"} *}
prove {* (Thm.term_of cgoal2) *}
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
- apply (tactic {* foo_tac' @{context} 1 *})
- done
+
(*