--- a/QuotMain.thy Tue Dec 01 19:18:43 2009 +0100
+++ b/QuotMain.thy Wed Dec 02 07:21:10 2009 +0100
@@ -798,7 +798,7 @@
using a by simp
ML {*
-val lambda_res_tac =
+val lambda_rsp_tac =
SUBGOAL (fn (goal, i) =>
case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
(_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} i
@@ -806,7 +806,7 @@
*}
ML {*
-val weak_lambda_res_tac =
+val weak_lambda_rsp_tac =
SUBGOAL (fn (goal, i) =>
case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
(_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} i
@@ -868,7 +868,7 @@
we try:
1) theorems 'trans2' from the appropriate QUOT_TYPE
- 2) remove lambdas from both sides: lambda_res_tac
+ 2) remove lambdas from both sides: lambda_rsp_tac
3) remove Ball/Bex from the right hand side
4) use user-supplied RSP theorems
5) remove rep_abs from the right side
@@ -891,22 +891,23 @@
lemma quot_true_dests:
shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
- and QT_appL: "QUOT_TRUE (A B) \<Longrightarrow> QUOT_TRUE A"
- and QT_appR: "QUOT_TRUE (A B) \<Longrightarrow> QUOT_TRUE B"
+ and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))"
-apply(simp_all add: QUOT_TRUE_def)
+ and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"
+apply(simp_all add: QUOT_TRUE_def ext)
done
-lemma QUOT_TRUE_i: "(QUOT_TRUE a \<Longrightarrow> P) \<Longrightarrow> P"
+lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P"
by (simp add: QUOT_TRUE_def)
-lemma QUOT_TRUE_imp: "QUOT_TRUE a \<Longrightarrow> QUOT_TRUE b"
+lemma QUOT_TRUE_imp: "QUOT_TRUE a"
by (simp add: QUOT_TRUE_def)
ML {*
fun quot_true_tac ctxt fnctn =
- SUBGOAL (fn (gl, i) =>
+ CSUBGOAL (fn (cgl, i) =>
let
+ val gl = term_of cgl;
val thy = ProofContext.theory_of ctxt;
fun find_fun trm =
case trm of
@@ -916,20 +917,27 @@
case find_first find_fun (Logic.strip_assums_hyp gl) of
SOME (_ $ (_ $ x)) =>
let
+ val thm' = Thm.lift_rule cgl @{thm QUOT_TRUE_imp}
+ val ps = Logic.strip_params (Thm.concl_of thm');
val fx = fnctn x;
- val ctrm1 = cterm_of thy x;
- val cty1 = ctyp_of thy (fastype_of x);
- val ctrm2 = cterm_of thy fx;
- val cty2 = ctyp_of thy (fastype_of fx);
- val thm = Drule.instantiate' [SOME cty1, SOME cty2] [SOME ctrm1, SOME ctrm2] @{thm QUOT_TRUE_imp}
+ val (_ $ (_ $ fx')) = Logic.strip_assums_concl (prop_of thm');
+ val insts = [(fx', fx)]
+ |> map (fn (t, u) => (cterm_of thy (Term.head_of t), cterm_of thy (Term.list_abs (ps, u))));
+ val thm_i = Drule.cterm_instantiate insts thm'
+ val thm_j = Thm.forall_elim_vars 1 thm_i
in
- dtac thm i
+ dtac thm_j i
end
| NONE => error "quot_true_tac!"
| _ => error "quot_true_tac!!"
end)
*}
+
+ML {* fun dest_comb (f $ a) = (f, a) *}
+ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *}
+ML {* fun unlam (Abs a) = snd (Term.dest_abs a) *}
+
ML {*
fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
(FIRST' [
@@ -938,7 +946,7 @@
DT ctxt "1" (resolve_tac trans2),
(* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
- NDT ctxt "2" (lambda_res_tac),
+ NDT ctxt "2" (lambda_rsp_tac),
(* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
NDT ctxt "3" (rtac @{thm ball_rsp}),
@@ -987,11 +995,69 @@
*}
ML {*
+fun inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 =
+ (FIRST' [
+ (* "cong" rule of the of the relation / transitivity*)
+ (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
+ DT ctxt "1" (resolve_tac trans2),
+
+ (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
+ NDT ctxt "2" (lambda_rsp_tac THEN' quot_true_tac ctxt unlam),
+
+ (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
+ NDT ctxt "3" (rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}),
+
+ (* R2 is always equality *)
+ (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
+ NDT ctxt "4" (ball_rsp_tac THEN' quot_true_tac ctxt unlam),
+
+ (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
+ NDT ctxt "5" (rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}),
+
+ (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
+ NDT ctxt "6" (bex_rsp_tac THEN' dtac @{thm QT_ext}),
+
+ (* respectfulness of constants *)
+ NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),
+
+ (* reflexivity of operators arising from Cong_tac *)
+ NDT ctxt "8" (rtac @{thm refl}),
+
+ (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
+ (* observe ---> *)
+ NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt
+ THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))),
+
+ (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *)
+ NDT ctxt "A" (APPLY_RSP_TAC rty ctxt THEN'
+ (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms),
+ quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
+
+ (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *)
+ (* merge with previous tactic *)
+ NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'
+ (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
+
+ (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
+ NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
+
+ (* reflexivity of the basic relations *)
+ (* R \<dots> \<dots> *)
+ NDT ctxt "D" (resolve_tac rel_refl),
+
+ (* resolving with R x y assumptions *)
+ NDT ctxt "E" (atac),
+
+ (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)
+ (* global simplification *)
+ NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])
+*}
+
+ML {*
fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2)
*}
-
section {* Cleaning of the theorem *}
@@ -1206,14 +1272,12 @@
let
val rthm' = atomize_thm rthm
val rule = procedure_inst context (prop_of rthm') (term_of concl)
+ val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i}
in
- EVERY1 [rtac rule, rtac rthm']
+ EVERY1 [rtac rule, rtac rthm'] THEN RANGE [(fn _ => all_tac), rtac thm] 1
end) lthy
*}
-thm EQUIV_REFL
-thm equiv_trans2
-
ML {*
(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
fun lift_tac lthy rthm rel_eqv rty quot defs =
@@ -1225,12 +1289,13 @@
val rule = procedure_inst context (prop_of rthm') (term_of concl)
val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv
+ val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i}
in
EVERY1
[rtac rule,
RANGE [rtac rthm',
regularize_tac lthy rel_eqv,
- all_inj_repabs_tac lthy rty quot rel_refl trans2,
+ rtac thm THEN' all_inj_repabs_tac lthy rty quot rel_refl trans2,
clean_tac lthy quot defs]]
end) lthy
*}