diff -r a840c232e04e -r 991b0e53f9dc QuotMain.thy --- a/QuotMain.thy Mon Nov 09 15:40:43 2009 +0100 +++ b/QuotMain.thy Tue Nov 10 09:32:16 2009 +0100 @@ -202,7 +202,7 @@ bounded quantifiers, for example: \x. P \ \x\(Respects R). P - Abstractions over a type that needs lifting are replaced - by bounded abstactions: + by bounded abstractions: \x. P \ Ball (Respects R) (\x. P) - Equalities over the type being lifted are replaced by @@ -241,7 +241,8 @@ val tys_out = tys_rel ---> ty_out; in (case (maps_lookup (ProofContext.theory_of lthy) s) of - SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys) + SOME (info) => list_comb (Const (#relfun info, tys_out), + map (fn ty => tyRel ty rty rel lthy) tys) | NONE => HOLogic.eq_const ty ) end @@ -341,12 +342,12 @@ (* ML {* - text {*val r = term_of @{cpat "R::?'a list \ ?'a list \ bool"};*} val r = Free ("R", dummyT); - val t = (my_reg @{context} r @{typ "'a list"} @{term "\(x::'b list). P x"}); + val t = (my_reg_inst @{context} r @{typ "'a list"} @{term "\(x::'b list). P x"}); val t2 = Syntax.check_term @{context} t; - Toplevel.program (fn () => cterm_of @{theory} t2) -*}*) + cterm_of @{theory} t2 +*} +*) text {* Assumes that the given theorem is atomized *} ML {* @@ -356,17 +357,16 @@ (my_reg_inst lthy rel rty (prop_of thm))) *} -lemma universal_twice: - "(\x. (P x \ Q x)) \ ((\x. P x) \ (\x. Q x))" -by auto +lemma universal_twice: + assumes *: "\x. (P x \ Q x)" + shows "(\x. P x) \ (\x. Q x)" +using * by auto -lemma implication_twice: - "(c \ a) \ (a \ b \ d) \ (a \ b) \ (c \ d)" -by auto - -(*lemma equality_twice: - "a = c \ b = d \ (a = b \ c = d)" -by auto*) +lemma implication_twice: + assumes a: "c \ a" + assumes b: "a \ b \ d" + shows "(a \ b) \ (c \ d)" +using a b by auto ML {* fun regularize thm rty rel rel_eqv rel_refl lthy = @@ -383,6 +383,7 @@ EqSubst.eqsubst_tac ctxt [0] [(@{thm equiv_res_forall} OF [rel_eqv]), (@{thm equiv_res_exists} OF [rel_eqv])], + (* For a = b \ a \ b *) (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), (rtac @{thm RIGHT_RES_FORALL_REGULAR}) ]); @@ -396,7 +397,12 @@ section {* RepAbs injection *} (* -Injecting RepAbs means: +RepAbs injection is done in the following phases: + 1) build_repabs_term inserts rep-abs pairs in the term + 2) we prove the equality between the original theorem and this one + 3) we use Pure.equal_elim_rule1 to get the new theorem. + +build_repabs_term does: For abstractions: * If the type of the abstraction doesn't need lifting we recurse. @@ -404,7 +410,9 @@ variable needs lifting. * If it doesn't then we recurse * If it does we recurse and put 'RepAbs' around all occurences - of the variable in the obtained subterm. + of the variable in the obtained subterm. This in combination + with the RepAbs above will let us change the type of the + abstraction with rewriting. For applications: * If the term is 'Respects' applied to anything we leave it unchanged * If the term needs lifting and the head is a constant that we know @@ -414,27 +422,24 @@ put RepAbs and recurse * Otherwise just recurse. -The injection is done in the following phases: - 1) build_repabs_term inserts rep-abs pairs in the term - 2) we prove the equality between the original theorem and this one - 3) we use Pure.equal_elim_rule1 to get the new theorem. To prove that the old theorem implies the new one, we first atomize it and then try: - 1) theorems 'trans2' from the QUOT_TYPE + 1) theorems 'trans2' from the appropriate QUOT_TYPE 2) remove lambdas from both sides (LAMBDA_RES_TAC) - 3) remove Ball/Bex - 4) use RSP theorems - 5) remove rep_abs from right side - 6) reflexivity + 3) remove Ball/Bex from the right hand side + 4) use user-supplied RSP theorems + 5) remove rep_abs from the right side + 6) reflexivity of equality 7) split applications of lifted type (apply_rsp) 8) split applications of non-lifted type (cong_tac) 9) apply extentionality -10) relation reflexive +10) reflexivity of the relation 11) assumption + (Lambdas under respects may have left us some assumptions) 12) proving obvious higher order equalities by simplifying fun_rel - (not sure if still needed?) + (not sure if it is still needed?) 13) unfolding lambda on one side 14) simplifying (= ===> =) for simpler respectfullness @@ -632,9 +637,14 @@ lemma id_def_sym: "(\x. x) \ id" by (simp add: id_def) +(* TODO: can be also obtained with: *) +ML {* symmetric (eq_reflection OF @{thms id_def}) *} + ML {* fun build_repabs_term lthy thm consts rty qty = let + (* TODO: The rty and qty stored in the quotient_info should + be varified, so this will soon not be needed *) val rty = Logic.varifyT rty; val qty = Logic.varifyT qty; @@ -664,8 +674,8 @@ else let val v' = mk_repabs v; - (* TODO: I believe this is not needed any more *) - val t1 = Envir.beta_norm (t' $ v') + (* TODO: I believe 'beta' is not needed any more *) + val t1 = (* Envir.beta_norm *) (t' $ v') in lambda v t1 end) @@ -691,7 +701,7 @@ end *} -text {* Assumes that it is given a regularized theorem *} +text {* Builds provable goals for regularized theorems *} ML {* fun build_repabs_goal ctxt thm cons rty qty = Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty)) @@ -699,14 +709,17 @@ ML {* fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} => -let - val pat = Drule.strip_imp_concl (cprop_of thm) - val insts = Thm.match (pat, concl) -in - rtac (Drule.instantiate insts thm) 1 -end -handle _ => no_tac -) + let + val pat = Drule.strip_imp_concl (cprop_of thm) + val insts = Thm.match (pat, concl) + in + rtac (Drule.instantiate insts thm) 1 + end + handle _ => no_tac) +*} + +ML {* +fun CHANGED' tac = (fn i => CHANGED (tac i)) *} ML {* @@ -715,9 +728,10 @@ rtac @{thm FUN_QUOTIENT}, rtac quot_thm, rtac @{thm IDENTITY_QUOTIENT}, - ( - fn i => CHANGED (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I}) i) THEN - rtac @{thm IDENTITY_QUOTIENT} i + (* For functional identity quotients, (op = ---> op =) *) + CHANGED' ( + (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I})) THEN' + rtac @{thm IDENTITY_QUOTIENT} ) ]) *} @@ -725,7 +739,7 @@ ML {* fun LAMBDA_RES_TAC ctxt i st = (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of - (_ $ (_ $ (Abs(_, _, _))$(Abs(_, _, _)))) => + (_ $ (_ $ (Abs(_, _, _)) $ (Abs(_, _, _)))) => (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) | _ => fn _ => no_tac) i st @@ -749,12 +763,12 @@ val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl; val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); val insts = Thm.match (pat, concl) -in - if needs_lift rty (type_of f) then - rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 - else no_tac -end -handle _ => no_tac) + in + if needs_lift rty (type_of f) then + rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 + else no_tac + end + handle _ => no_tac) *} ML {* @@ -768,8 +782,7 @@ THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 end - handle _ => no_tac - ) + handle _ => no_tac) *} ML {* @@ -783,8 +796,11 @@ THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 end - handle _ => no_tac - ) + handle _ => no_tac) +*} + +ML {* +fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) *} ML {* @@ -797,18 +813,14 @@ FIRST' (map rtac rsp_thms), (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), rtac refl, -(* rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*) (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), Cong_Tac.cong_tac @{thm cong}, rtac @{thm ext}, rtac reflex_thm, atac, - ( - (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) - THEN_ALL_NEW (fn _ => no_tac) - ), + SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), WEAK_LAMBDA_RES_TAC ctxt, - (fn i => CHANGED (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}) i)) + CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})) ]) *} @@ -828,12 +840,10 @@ section {* Cleaning the goal *} lemma prod_fun_id: "prod_fun id id = id" - apply (simp add: prod_fun_def) -done +by (simp add: prod_fun_def) + lemma map_id: "map id x = x" - apply (induct x) - apply (simp_all add: map.simps) -done +by (induct x) (simp_all) ML {* fun simp_ids lthy thm = @@ -866,6 +876,7 @@ end *} +(* TODO: Check if it behaves properly with varifyed rty *) ML {* fun findabs_all rty tm = case tm of @@ -881,7 +892,6 @@ fun findabs rty tm = distinct (op =) (findabs_all rty tm) *} - ML {* fun findaps_all rty tm = case tm of @@ -894,6 +904,7 @@ fun findaps rty tm = distinct (op =) (findaps_all rty tm) *} +(* Currently useful only for LAMBDA_PRS *) ML {* fun make_simp_prs_thm lthy quot_thm thm typ = let @@ -936,6 +947,7 @@ in (a1 @ a2, e1 @ e2) end | _ => ([], []); *} + ML {* fun findallex lthy rty qty tm = let @@ -1005,12 +1017,12 @@ *} ML {* -fun matches (ty1, ty2) = - Type.raw_instance (ty1, Logic.varifyT ty2); - fun lookup_quot_data lthy qty = let + fun matches (ty1, ty2) = + Type.raw_instance (ty1, Logic.varifyT ty2); val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy) + (* TODO: Should no longer be needed *) val rty = Logic.unvarifyT (#rtyp quotdata) val rel = #rel quotdata val rel_eqv = #equiv_thm quotdata