# HG changeset patch # User Christian Urban # Date 1259412888 -3600 # Node ID 7beed9b75ea28e7fe1cb5e601a6339c6fd463d08 # Parent 42e7f323913a60c12d2f2eb198a5980f9f37502a renamed LAMBDA_RES_TAC and WEAK_LAMBDA_RES_TAC to lower case names diff -r 42e7f323913a -r 7beed9b75ea2 FSet.thy --- a/FSet.thy Sat Nov 28 08:46:24 2009 +0100 +++ b/FSet.thy Sat Nov 28 13:54:48 2009 +0100 @@ -328,9 +328,11 @@ apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *}) done -lemma "\f g z a x. FOLD f g (z::'b) (INSERT a x) = +ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *} + +lemma "FOLD f g (z::'b) (INSERT a x) = (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)" -apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) +apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) done lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" @@ -341,8 +343,6 @@ apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) done -ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *} - lemma cheat: "P" sorry lemma "\P EMPTY; \a x. P x \ P (INSERT a x)\ \ P l" diff -r 42e7f323913a -r 7beed9b75ea2 QuotMain.thy --- a/QuotMain.thy Sat Nov 28 08:46:24 2009 +0100 +++ b/QuotMain.thy Sat Nov 28 13:54:48 2009 +0100 @@ -488,6 +488,7 @@ *) +(* FIXME: they should be in in the new Isabelle *) lemma [mono]: "(\x. P x \ Q x) \ (Ex P) \ (Ex Q)" by blast @@ -811,7 +812,7 @@ using a by (simp add: FUN_REL.simps) ML {* -val LAMBDA_RES_TAC = +val lambda_res_tac = Subgoal.FOCUS (fn {concl, ...} => case (term_of concl) of (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} 1 @@ -819,7 +820,7 @@ *} ML {* -val WEAK_LAMBDA_RES_TAC = +val weak_lambda_res_tac = Subgoal.FOCUS (fn {concl, ...} => case (term_of concl) of (_ $ (_ $ _ $ (Abs _))) => rtac @{thm FUN_REL_I} 1 @@ -831,7 +832,8 @@ val ball_rsp_tac = Subgoal.FOCUS (fn {concl, ...} => case (term_of concl) of - (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) => + (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) + $ (Const (@{const_name Ball}, _) $ _))) => rtac @{thm FUN_REL_I} 1 |_ => no_tac) *} @@ -840,7 +842,8 @@ val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => case (term_of concl) of - (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) => + (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) + $ (Const (@{const_name Bex}, _) $ _))) => rtac @{thm FUN_REL_I} 1 | _ => no_tac) *} @@ -877,7 +880,7 @@ ML {* fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = (FIRST' [resolve_tac trans2, - LAMBDA_RES_TAC ctxt, + lambda_res_tac ctxt, rtac @{thm RES_FORALL_RSP}, ball_rsp_tac ctxt, rtac @{thm RES_EXISTS_RSP}, @@ -892,8 +895,8 @@ rtac @{thm ext}, resolve_tac rel_refl, atac, - SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), - WEAK_LAMBDA_RES_TAC ctxt, + (*seems not necessary:: SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),*) + weak_lambda_res_tac ctxt, CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))]) fun all_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = @@ -905,7 +908,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_res_tac 3) remove Ball/Bex from the right hand side 4) use user-supplied RSP theorems 5) remove rep_abs from the right side @@ -929,11 +932,11 @@ (K (print_tac "start")) THEN' (K no_tac), (* "cong" rule of the of the relation *) - (* \a \ c; b \ d\ \ (a \ b) = (c \ d) *) + (* \a \ c; b \ d\ \ a \ b = c \ d *) DT ctxt "1" (resolve_tac trans2), (* (R1 ===> R2) (\x\) (\\) \ \R1 x y\ \ R2 (\x) (\y) *) - DT ctxt "2" (LAMBDA_RES_TAC ctxt), + DT ctxt "2" (lambda_res_tac ctxt), (* = (Ball\) (Ball\) \ = (\) (\) *) DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), @@ -947,7 +950,7 @@ (* (R1 ===> R2) (Bex\) (Bex\) \ \R1 x y\ \ R2 (Bex\x) (Bex\y) *) DT ctxt "6" (bex_rsp_tac ctxt), - (* respectfulness of ops *) + (* respectfulness of constants *) DT ctxt "7" (resolve_tac rsp_thms), (* reflexivity of operators arising from Cong_tac *) @@ -974,39 +977,17 @@ (* resolving with R x y assumptions *) DT ctxt "E" (atac), - DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), - DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt), + (* seems not necessay:: DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*) + DT ctxt "G" (weak_lambda_res_tac ctxt), + + (* (op =) ===> (op =) \ (op =), needed to apply respectfulness theorems *) + (* works globally *) DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms) *} -ML {* -fun get_inj_repabs_tac ctxt rel lhs rhs = -let - val _ = tracing "input" - val _ = tracing ("rel: " ^ Syntax.string_of_term ctxt rel) - val _ = tracing ("lhs: " ^ Syntax.string_of_term ctxt lhs) - val _ = tracing ("rhs: " ^ Syntax.string_of_term ctxt rhs) -in - case (rel, lhs, rhs) of - (_, l, Const _ $ (Const _ $ r)) (* FIXME: not right_match *) - => rtac @{thm REP_ABS_RSP(1)} - | (_, Const (@{const_name "Ball"}, _) $ _, - Const (@{const_name "Ball"}, _) $ _) - => rtac @{thm RES_FORALL_RSP} - | _ => K no_tac -end -*} - -ML {* -fun inj_repabs_tac ctxt = - SUBGOAL (fn (goal, i) => - (case (HOLogic.dest_Trueprop goal) of - (rel $ lhs $ rhs) => get_inj_repabs_tac ctxt rel lhs rhs - | _ => K no_tac) i) -*} section {* Cleaning of the theorem *}