nominal2: comparison Quot/QuotMain.thy

equal deleted inserted replaced

-:51a4208162ed
+:386a6b1a5203
 (* the auxiliary data for the quotient types *)
 use "quotient_info.ML"
 declare [[map * = (prod_fun, prod_rel)]]
 declare [[map "fun" = (fun_map, fun_rel)]]
 (* Throws now an exception:              *)
 (* declare [[map "option" = (bla, blu)]] *)
 lemmas [quotient_thm] =
 fun_quotient prod_quotient
 end
 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') =
 case (ty, ty') of
 (_, TVar _) => true
 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')
 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
 *}
 ML {*
 val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi)
 in
 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 {*
 fun ball_bex_range_simproc ss redex =
 let
 val (y, s) = Term.dest_abs (x, T, t)
 val (_, s') = Term.dest_abs (x', T', t')
 val yvar = Free (y, T)
 val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))
 in
-if rty = qty
+if rty = qty then result
-then result
 else mk_repabs lthy (rty, qty) result
 end
 | (t $ s, t' $ s') =>
 (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))
 | (Free (_, T), Free (_, T')) =>
-if T = T'
+if T = T' then rtrm
-then rtrm
 else mk_repabs lthy (T, T') rtrm
 | (_, Const (@{const_name "op ="}, _)) => rtrm
 (* FIXME: check here that rtrm is the corresponding definition for the const *)
 | (_, Const (_, T')) =>
 let
 val rty = fastype_of rtrm
 in
-if rty = T'
+if rty = T' then rtrm
-then rtrm
 else mk_repabs lthy (rty, T') rtrm
 end
 | _ => raise (LIFT_MATCH "injection")
 *}
 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 {*
 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
-*}
-ML {*
 fun all_inj_repabs_tac ctxt =
 REPEAT_ALL_NEW (inj_repabs_tac ctxt)
-(* if this is too slow we can inline the code above *)
+*}
-*}
+section {* Cleaning of the Theorem *}
-section {* Cleaning of the theorem *}
 ML {*
 fun make_inst lhs t =
 let
 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
 (* 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 id_simps and *)
+(* 3. simplification with *)
-thm fun_map.simps Quotient_abs_rep Quotient_rel_rep
+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]} @ (id_simps_get lthy)
 @ @{thms Quotient_abs_rep Quotient_rel_rep}
 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
 in
 (rtac rule THEN' RANGE [rtac rthm', K all_tac, rtac quot_weak]) i
 end)
 *}
 ML {*
-(* automated tactics *)
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => 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 {*
 fun lift_tac ctxt rthm =
 procedure_tac ctxt rthm
-THEN' RANGE [regularize_tac ctxt,
+THEN' RANGE_WARN [(regularize_tac ctxt,     "Regularize proof failed."),
-all_inj_repabs_tac ctxt,
+(all_inj_repabs_tac ctxt, "Injection proof failed."),
-clean_tac ctxt]
+(clean_tac ctxt,          "Cleaning proof failed.")]
 *}
 end

changeset 615	386a6b1a5203
parent 614	51a4208162ed
child 616	20b8585ad1e0