diff -r ca37f4b6457c -r 8dfae5d97387 Quot/QuotMain.thy --- a/Quot/QuotMain.thy Tue Dec 08 11:17:56 2009 +0100 +++ b/Quot/QuotMain.thy Tue Dec 08 11:20:01 2009 +0100 @@ -144,11 +144,10 @@ declare [[map * = (prod_fun, prod_rel)]] declare [[map "fun" = (fun_map, fun_rel)]] -(* FIXME: This should throw an exception: -declare [[map "option" = (bla, blu)]] -*) -(* identity quotient is not here as it has to be applied first *) +(* Throws now an exception: *) +(* declare [[map "option" = (bla, blu)]] *) + lemmas [quotient_thm] = fun_quotient prod_quotient @@ -160,22 +159,17 @@ lemmas [quotient_equiv] = identity_equivp prod_equivp -ML {* maps_lookup @{theory} "*" *} -ML {* maps_lookup @{theory} "fun" *} - - (* definition of the quotient types *) (* FIXME: should be called quotient_typ.ML *) use "quotient.ML" - (* lifting of constants *) use "quotient_def.ML" section {* Simset setup *} -(* since HOL_basic_ss is too "big", we need to set up *) -(* our own minimal simpset *) +(* Since HOL_basic_ss is too "big" for us, *) +(* we set up our own minimal simpset. *) ML {* fun mk_minimal_ss ctxt = Simplifier.context ctxt empty_ss @@ -184,11 +178,10 @@ *} ML {* -(* TODO/FIXME not needed anymore? *) -fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) +fun OF1 thm1 thm2 = thm2 RS thm1 *} -section {* atomize *} +section {* Atomize Infrastructure *} lemma atomize_eqv[atomize]: shows "(Trueprop A \ Trueprop B) \ (A \ B)" @@ -220,24 +213,20 @@ end *} -section {* infrastructure about id *} +section {* Infrastructure about id *} + +print_attributes (* TODO: think where should this be *) lemma prod_fun_id: "prod_fun id id \ id" by (rule eq_reflection) (simp add: prod_fun_def) -(* FIXME: make it a list and add map_id to it *) -lemmas id_simps = +lemmas [id_simps] = fun_map_id[THEN eq_reflection] id_apply[THEN eq_reflection] id_def[THEN eq_reflection,symmetric] prod_fun_id -ML {* -fun simp_ids thm = - MetaSimplifier.rewrite_rule @{thms id_simps} thm -*} - section {* Debugging infrastructure for testing tactics *} ML {* @@ -265,7 +254,7 @@ fun NDT ctxt s tac thm = tac thm *} -section {* Matching of terms and types *} +section {* Matching of Terms and Types *} ML {* fun matches_typ (ty, ty') = @@ -278,9 +267,7 @@ then (List.all matches_typ (tys ~~ tys')) else false | _ => false -*} -ML {* fun matches_term (trm, trm') = case (trm, trm') of (_, Var _) => true @@ -292,37 +279,7 @@ | _ => false *} -section {* Infrastructure for collecting theorems for starting the lifting *} - -ML {* -fun lookup_quot_data lthy qty = - let - val qty_name = fst (dest_Type qty) - val SOME quotdata = quotdata_lookup lthy qty_name - (* TODO: Should no longer be needed *) - val rty = Logic.unvarifyT (#rtyp quotdata) - val rel = #rel quotdata - val rel_eqv = #equiv_thm quotdata - val rel_refl = @{thm equivp_reflp} OF [rel_eqv] - in - (rty, rel, rel_refl, rel_eqv) - end -*} - -ML {* -fun lookup_quot_thms lthy qty_name = - let - val thy = ProofContext.theory_of lthy; - val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2") - val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same") - val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10") - val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name) - in - (trans2, reps_same, absrep, quot) - end -*} - -section {* Regularization *} +section {* Computation of the Regularize Goal *} (* Regularizing an rtrm means: @@ -489,13 +446,13 @@ raise (LIFT_MATCH "regularize (default)") *} +section {* Regularize Tactic *} + ML {* fun equiv_tac ctxt = (K (print_tac "equiv tac")) THEN' REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) -*} -ML {* fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac *} @@ -537,7 +494,7 @@ SOME thm2 end handle _ => NONE -(* FIXME/TODO: what is the place where the exception can be raised: matching_prs? *) +(* FIXME/TODO: what is the place where the exception is raised: matching_prs? *) *} ML {* @@ -560,20 +517,23 @@ shows "equivp R \ a = b \ R a b" by (simp add: equivp_reflp) -(* FIXME/TODO: How does regularizing work? *) -(* FIXME/TODO: needs to be adapted -To prove that the raw theorem implies the regularised one, -we try in order: +(* Regularize Tactic *) - - Reflexivity of the relation - - Assumption - - Elimnating quantifiers on both sides of toplevel implication - - Simplifying implications on both sides of toplevel implication - - Ball (Respects ?E) ?P = All ?P - - (\x. ?R x \ ?P x \ ?Q x) \ All ?P \ Ball ?R ?Q +(* 0. preliminary simplification step according to *) +thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *) + ball_reg_eqv_range bex_reg_eqv_range +(* 1. eliminating simple Ball/Bex instances*) +thm ball_reg_right bex_reg_left +(* 2. monos *) +(* 3. commutation rules for ball and bex *) +thm ball_all_comm bex_ex_comm +(* 4. then rel-equality (which need to be instantiated to avoid loops *) +thm eq_imp_rel +(* 5. then simplification like 0 *) +(* finally jump back to 1 *) -*) + ML {* fun regularize_tac ctxt = let @@ -586,24 +546,19 @@ addsimprocs [simproc] addSolver equiv_solver (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) (* can this cause loops in equiv_tac ? *) - val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt) + val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) in simp_tac simpset THEN' REPEAT_ALL_NEW (CHANGED o FIRST' [ - rtac @{thm ball_reg_right}, - rtac @{thm bex_reg_left}, + resolve_tac @{thms ball_reg_right bex_reg_left}, resolve_tac (Inductive.get_monos ctxt), - rtac @{thm ball_all_comm}, - rtac @{thm bex_ex_comm}, + resolve_tac @{thms ball_all_comm bex_ex_comm}, resolve_tac eq_eqvs, - (* should be equivalent to the above, but causes loops: *) - (* rtac @{thm eq_imp_rel} THEN' SOLVES' (equiv_tac ctxt), *) - (* the culprit is aslread rtac @{thm eq_imp_rel} *) simp_tac simpset]) end *} -section {* Injections of rep and abses *} +section {* Calculation of the Injected Goal *} (* Injecting repabs means: @@ -658,8 +613,7 @@ val yvar = Free (y, T) val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s')) in - if rty = qty - then result + if rty = qty then result else mk_repabs lthy (rty, qty) result end @@ -667,8 +621,7 @@ (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s')) | (Free (_, T), Free (_, T')) => - if T = T' - then rtrm + if T = T' then rtrm else mk_repabs lthy (T, T') rtrm | (_, Const (@{const_name "op ="}, _)) => rtrm @@ -678,35 +631,33 @@ let val rty = fastype_of rtrm in - if rty = T' - then rtrm + if rty = T' then rtrm else mk_repabs lthy (rty, T') rtrm end | _ => raise (LIFT_MATCH "injection") *} -section {* RepAbs Injection Tactic *} +section {* Injection Tactic *} ML {* fun quotient_tac ctxt = REPEAT_ALL_NEW (FIRST' [rtac @{thm identity_quotient}, resolve_tac (quotient_rules_get ctxt)]) -*} -(* solver for the simplifier *) -ML {* fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) 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 failed. Maybe a quotient_thm is missing" +let + val goal = hd (Drule.strip_imp_prems (cprop_of thm)) +in + thm OF [Goal.prove_internal [] goal (fn _ => quotient_tac ctxt 1)] +end +handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing" *} (* Not used *) @@ -914,9 +865,9 @@ (* reflexivity of operators arising from Cong_tac *) | Const (@{const_name "op ="},_) $ _ $ _ - => rtac @{thm refl} ORELSE' + => rtac @{thm refl} (*ORELSE' (resolve_tac trans2 THEN' RANGE [ - quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) + quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])*) (* TODO: These patterns should should be somehow combined and generalized... *) | (Const (@{const_name fun_rel}, _) $ _ $ _) $ @@ -943,32 +894,49 @@ *} ML {* -fun inj_repabs_tac ctxt rel_refl trans2 = +fun inj_repabs_step_tac ctxt rel_refl trans2 = (FIRST' [ - inj_repabs_tac_match ctxt trans2, + NDT ctxt "0" (inj_repabs_tac_match ctxt trans2), (* R (t $ \) (t' $ \) ----> apply_rsp provided type of t needs lifting *) + NDT ctxt "A" (apply_rsp_tac ctxt THEN' - (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), + RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)]), + + (* TODO/FIXME: I had to move this after the apply_rsp_tac - is this right *) + NDT ctxt "B" (resolve_tac trans2 THEN' + RANGE [quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]), + (* (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' + NDT ctxt "C" (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), + NDT ctxt "D" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), + (* resolving with R x y assumptions *) NDT ctxt "E" (atac), + (* reflexivity of the basic relations *) (* R \ \ *) - NDT ctxt "D" (resolve_tac rel_refl) + NDT ctxt "F" (resolve_tac rel_refl) ]) *} ML {* -fun all_inj_repabs_tac ctxt rel_refl trans2 = - REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2) +fun inj_repabs_tac ctxt = +let + val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) + val trans2 = map (OF1 @{thm equals_rsp}) (quotient_rules_get ctxt) +in + inj_repabs_step_tac ctxt rel_refl trans2 +end + +fun all_inj_repabs_tac ctxt = + REPEAT_ALL_NEW (inj_repabs_tac ctxt) *} -section {* Cleaning of the theorem *} +section {* Cleaning of the Theorem *} ML {* fun make_inst lhs t = @@ -1017,7 +985,7 @@ val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); val ti = (let - val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te + val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) in Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts @@ -1026,7 +994,7 @@ val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm) val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te in - MetaSimplifier.rewrite_rule @{thms id_simps} td + MetaSimplifier.rewrite_rule (id_simps_get ctxt) td end); val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then (tracing "lambda_prs"; @@ -1049,39 +1017,24 @@ fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) *} -(* - Cleaning the theorem consists of three rewriting steps. - The first two need to be done before fun_map is unfolded - - 1) lambda_prs: - (Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) ----> f - - Implemented as conversion since it is not a pattern. - - 2) all_prs (the same for exists): - Ball (Respects R) ((abs ---> id) f) ----> All f - - Rewriting with definitions from the argument defs - (rep ---> abs) oldConst ----> newconst - - 3) Quotient_rel_rep: - Rel (Rep x) (Rep y) ----> x = y - - Quotient_abs_rep: - Abs (Rep x) ----> x - - id_simps; fun_map.simps -*) +(* 1. conversion (is not a pattern) *) +thm lambda_prs +(* 2. folding of definitions: (rep ---> abs) oldConst == newconst *) +(* and simplification with *) +thm all_prs ex_prs +(* 3. simplification with *) +thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps +(* 4. Test for refl *) ML {* fun clean_tac lthy = let val thy = ProofContext.theory_of lthy; val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) - (* FIXME: shouldn't the definitions already be varified? *) + (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) val thms1 = @{thms all_prs ex_prs} @ defs - val thms2 = @{thms eq_reflection[OF fun_map.simps]} - @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} + val thms2 = @{thms eq_reflection[OF fun_map.simps]} @ (id_simps_get lthy) + @ @{thms Quotient_abs_rep Quotient_rel_rep} fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver in EVERY' [lambda_prs_tac lthy, @@ -1091,7 +1044,7 @@ end *} -section {* Genralisation of free variables in a goal *} +section {* Tactic for genralisation of free variables in a goal *} ML {* fun inst_spec ctrm = @@ -1121,7 +1074,7 @@ end) *} -section {* General outline of the lifting procedure *} +section {* General Shape of the Lifting Procedure *} (* - A is the original raw theorem *) (* - B is the regularized theorem *) @@ -1138,8 +1091,8 @@ and c: "B = C" and d: "C = D" shows "D" - using a b c d - by simp +using a b c d +by simp ML {* fun lift_match_error ctxt fun_str rtrm qtrm = @@ -1162,11 +1115,9 @@ val reg_goal = Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm - val _ = warning "Regularization done." val inj_goal = Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm - val _ = warning "RepAbs Injection done." in Drule.instantiate' [] [SOME (cterm_of thy rtrm'), @@ -1175,42 +1126,40 @@ end *} -(* Left for debugging *) ML {* +(* the tactic leaves three subgoals to be proved *) fun procedure_tac ctxt rthm = ObjectLogic.full_atomize_tac THEN' gen_frees_tac ctxt - THEN' CSUBGOAL (fn (gl, i) => + THEN' CSUBGOAL (fn (goal, i) => let val rthm' = atomize_thm rthm - val rule = procedure_inst ctxt (prop_of rthm') (term_of gl) - val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i} + val rule = procedure_inst ctxt (prop_of rthm') (term_of goal) + val bare_goal = snd (Thm.dest_comb goal) + val quot_weak = Drule.instantiate' [] [SOME bare_goal] @{thm QUOT_TRUE_i} in - (rtac rule THEN' RANGE [rtac rthm', (fn _ => all_tac), rtac thm]) i + (rtac rule THEN' RANGE [rtac rthm', K all_tac, rtac quot_weak]) i end) *} +(* automatic proofs *) +ML {* +fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) + +fun WARN (tac, msg) i st = + case Seq.pull ((SOLVES' tac) i st) of + NONE => (warning msg; Seq.single st) + | seqcell => Seq.make (fn () => seqcell) + +fun RANGE_WARN xs = RANGE (map WARN xs) +*} + ML {* -(* FIXME/TODO should only get as arguments the rthm like procedure_tac *) - fun lift_tac ctxt rthm = - ObjectLogic.full_atomize_tac - THEN' gen_frees_tac ctxt - THEN' CSUBGOAL (fn (gl, i) => - let - val rthm' = atomize_thm rthm - val rule = procedure_inst ctxt (prop_of rthm') (term_of gl) - val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt) - val quotients = quotient_rules_get ctxt - val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients - val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i} - in - (rtac rule THEN' - RANGE [rtac rthm', - regularize_tac ctxt, - rtac thm THEN' all_inj_repabs_tac ctxt rel_refl trans2, - clean_tac ctxt]) i - end) + procedure_tac ctxt rthm + THEN' RANGE_WARN [(regularize_tac ctxt, "Regularize proof failed."), + (all_inj_repabs_tac ctxt, "Injection proof failed."), + (clean_tac ctxt, "Cleaning proof failed.")] *} end