# HG changeset patch # User Cezary Kaliszyk # Date 1259734870 -3600 # Node ID 325d6e9a7515354a4273f9cf9cbfba208bc3fb75 # Parent 1eeacabe5ffe6d640ef33c486df488b346cfe335 Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE. diff -r 1eeacabe5ffe -r 325d6e9a7515 QuotMain.thy --- 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) \ QUOT_TRUE P" - and QT_appL: "QUOT_TRUE (A B) \ QUOT_TRUE A" - and QT_appR: "QUOT_TRUE (A B) \ QUOT_TRUE B" + and QT_ex: "QUOT_TRUE (Ex P) \ QUOT_TRUE P" and QT_lam: "QUOT_TRUE (\x. P x) \ (\x. QUOT_TRUE (P x))" -apply(simp_all add: QUOT_TRUE_def) + and QT_ext: "(\x. QUOT_TRUE (a x) \ f x = g x) \ (QUOT_TRUE a \ f = g)" +apply(simp_all add: QUOT_TRUE_def ext) done -lemma QUOT_TRUE_i: "(QUOT_TRUE a \ P) \ P" +lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \ P) \ P" by (simp add: QUOT_TRUE_def) -lemma QUOT_TRUE_imp: "QUOT_TRUE a \ 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) (\x\) (\y\) ----> \R1 x y\ \ R2 (\x) (\y) *) - NDT ctxt "2" (lambda_res_tac), + NDT ctxt "2" (lambda_rsp_tac), (* (op =) (Ball\) (Ball\) ----> (op =) (\) (\) *) 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) ----> \R a c; R b d\ *) + DT ctxt "1" (resolve_tac trans2), + + (* (R1 ===> R2) (\x\) (\y\) ----> \R1 x y\ \ R2 (\x) (\y) *) + NDT ctxt "2" (lambda_rsp_tac THEN' quot_true_tac ctxt unlam), + + (* (op =) (Ball\) (Ball\) ----> (op =) (\) (\) *) + NDT ctxt "3" (rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}), + + (* R2 is always equality *) + (* (R1 ===> R2) (Ball\) (Ball\) ----> \R1 x y\ \ R2 (Ball\x) (Ball\y) *) + NDT ctxt "4" (ball_rsp_tac THEN' quot_true_tac ctxt unlam), + + (* (op =) (Bex\) (Bex\) ----> (op =) (\) (\) *) + NDT ctxt "5" (rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}), + + (* (R1 ===> R2) (Bex\) (Bex\) ----> \R1 x y\ \ R2 (Bex\x) (Bex\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 (\) (Rep (Abs \)) ----> R (\) (\) *) + (* observe ---> *) + NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt + THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))), + + (* R (t $ \) (t' $ \) ----> 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 $ \) (t' $ \) ----> 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 =) (\x\) (\x\) ----> (op =) (\) (\) *) + NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), + + (* reflexivity of the basic relations *) + (* R \ \ *) + NDT ctxt "D" (resolve_tac rel_refl), + + (* resolving with R x y assumptions *) + NDT ctxt "E" (atac), + + (* (op =) ===> (op =) \ (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 *}