diff -r 334b3e9ea3e0 -r 33ff4b5f1806 QuotMain.thy --- a/QuotMain.thy Sun Dec 06 06:58:24 2009 +0100 +++ b/QuotMain.thy Sun Dec 06 11:09:51 2009 +0100 @@ -255,6 +255,31 @@ fun NDT ctxt s tac thm = tac thm *} +section {* Matching of terms and types *} + +ML {* +fun matches_typ (ty, ty') = + case (ty, ty') of + (_, TVar _) => true + | (TFree x, TFree x') => x = x' + | (Type (s, tys), Type (s', tys')) => + s = s' andalso + if (length tys = length tys') + then (List.all matches_typ (tys ~~ tys')) + else false + | _ => false +*} +ML {* +fun matches_term (trm, trm') = + case (trm, trm') of + (_, Var _) => true + | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty') + | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty') + | (Bound i, Bound j) => i = j + | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t') + | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s') + | _ => false +*} section {* Infrastructure for collecting theorems for starting the lifting *} @@ -344,30 +369,6 @@ *} ML {* -fun matches_typ (ty, ty') = - case (ty, ty') of - (_, TVar _) => true - | (TFree x, TFree x') => x = x' - | (Type (s, tys), Type (s', tys')) => - s = s' andalso - if (length tys = length tys') - then (List.all matches_typ (tys ~~ tys')) - else false - | _ => false -*} -ML {* -fun matches_term (trm, trm') = - case (trm, trm') of - (_, Var _) => true - | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty') - | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty') - | (Bound i, Bound j) => i = j - | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t') - | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s') - | _ => false -*} - -ML {* val mk_babs = Const (@{const_name Babs}, dummyT) val mk_ball = Const (@{const_name Ball}, dummyT) val mk_bex = Const (@{const_name Bex}, dummyT) @@ -742,7 +743,7 @@ | (_, Const (@{const_name "op ="}, _)) => rtrm - (* FIXME: check here that rtrm is the corresponding definition for teh const *) + (* FIXME: check here that rtrm is the corresponding definition for the const *) | (_, Const (_, T')) => let val rty = fastype_of rtrm @@ -757,20 +758,6 @@ section {* RepAbs Injection Tactic *} -(* Not used anymore *) -(* FIXME/TODO: do not handle everything *) -ML {* -fun instantiate_tac thm = - Subgoal.FOCUS (fn {concl, ...} => - let - val pat = Drule.strip_imp_concl (cprop_of thm) - val insts = Thm.first_order_match (pat, concl) - in - rtac (Drule.instantiate insts thm) 1 - end - handle _ => no_tac) -*} - ML {* fun quotient_tac ctxt = REPEAT_ALL_NEW (FIRST' @@ -784,6 +771,28 @@ val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac *} +ML {* +fun solve_quotient_assums ctxt thm = + let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in + thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)] + end + handle _ => error "solve_quotient_assums" +*} + +(* It proves the Quotient assumptions by calling quotient_tac *) +ML {* +fun solve_quotient_assum i ctxt thm = + let + val tac = + (compose_tac (false, thm, i)) THEN_ALL_NEW + (quotient_tac ctxt); + val gc = Drule.strip_imp_concl (cprop_of thm); + in + Goal.prove_internal [] gc (fn _ => tac 1) + end + handle _ => error "solve_quotient_assum" +*} + definition "QUOT_TRUE x \ True" @@ -802,58 +811,6 @@ end *} -(* It proves the Quotient assumptions by calling quotient_tac *) -ML {* -fun solve_quotient_assum i ctxt thm = - let - val tac = - (compose_tac (false, thm, i)) THEN_ALL_NEW - (quotient_tac ctxt); - val gc = Drule.strip_imp_concl (cprop_of thm); - in - Goal.prove_internal [] gc (fn _ => tac 1) - end - handle _ => error "solve_quotient_assum" -*} - -ML {* -fun solve_quotient_assums ctxt thm = - let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in - thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)] - end - handle _ => error "solve_quotient_assums" -*} - -ML {* -val apply_rsp_tac = - Subgoal.FOCUS (fn {concl, asms, context,...} => - case ((HOLogic.dest_Trueprop (term_of concl))) of - ((R2 $ (f $ x) $ (g $ y))) => - (let - val (asmf, asma) = find_qt_asm (map term_of asms); - in - if (fastype_of asmf) = (fastype_of f) then no_tac else let - val ty_a = fastype_of x; - val ty_b = fastype_of asma; - val ty_c = range_type (type_of f); - val thy = ProofContext.theory_of context; - val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c]; - val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp} - val te = solve_quotient_assums context thm - val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; - val thm = Drule.instantiate' [] t_inst te - in - compose_tac (false, thm, 2) 1 - end - end - handle ERROR "find_qt_asm: no pair" => no_tac) - | _ => no_tac) -*} - -ML {* -fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) -*} - (* To prove that the regularised theorem implies the abs/rep injected, we try: @@ -944,6 +901,35 @@ *} ML {* +val apply_rsp_tac = + Subgoal.FOCUS (fn {concl, asms, context,...} => + case ((HOLogic.dest_Trueprop (term_of concl))) of + ((R2 $ (f $ x) $ (g $ y))) => + (let + val (asmf, asma) = find_qt_asm (map term_of asms); + in + if (fastype_of asmf) = (fastype_of f) then no_tac else let + val ty_a = fastype_of x; + val ty_b = fastype_of asma; + val ty_c = range_type (type_of f); + val thy = ProofContext.theory_of context; + val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c]; + val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp} + val te = solve_quotient_assums context thm + val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; + val thm = Drule.instantiate' [] t_inst te + in + compose_tac (false, thm, 2) 1 + end + end + handle ERROR "find_qt_asm: no pair" => no_tac) + | _ => no_tac) +*} +ML {* +fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) +*} + +ML {* fun rep_abs_rsp_tac ctxt = SUBGOAL (fn (goal, i) => case (bare_concl goal) of @@ -1034,8 +1020,6 @@ REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2) *} - - section {* Cleaning of the theorem *} ML {*