nominal2: comparison Quot/QuotMain.thy

equal deleted inserted replaced

-:ca37f4b6457c
+:8dfae5d97387
 (* the auxiliary data for the quotient types *)
 use "quotient_info.ML"
 declare [[map * = (prod_fun, prod_rel)]]
 declare [[map "fun" = (fun_map, fun_rel)]]
-(* FIXME: This should throw an exception:
-declare [[map "option" = (bla, blu)]]
+(* Throws now an exception:              *)
-*)
+(* declare [[map "option" = (bla, blu)]] *)
-(* identity quotient is not here as it has to be applied first *)
 lemmas [quotient_thm] =
 fun_quotient prod_quotient
 lemmas [quotient_rsp] =
 quot_rel_rsp pair_rsp
 (* fun_map is not here since equivp is not true *)
 (* TODO: option, ... *)
 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 *)
+(* Since HOL_basic_ss is too "big" for us, *)
-(* our own minimal simpset                            *)
+(* we set up our own minimal simpset.      *)
 ML {*
 fun  mk_minimal_ss ctxt =
 Simplifier.context ctxt empty_ss
 setsubgoaler asm_simp_tac
 setmksimps (mksimps [])
 *}
 ML {*
-(* TODO/FIXME not needed anymore? *)
+fun OF1 thm1 thm2 = thm2 RS thm1
-fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+*}
-*}
+section {* Atomize Infrastructure *}
-section {* atomize *}
 lemma atomize_eqv[atomize]:
 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
 proof
 assume "A \<equiv> B"
 in
 @{thm equal_elim_rule1} OF [thm'', thm']
 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 \<equiv> 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 {*
 fun my_print_tac ctxt s i thm =
 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')
 | (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 *}
+section {* Computation of the Regularize Goal *}
-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 *}
 (*
 Regularizing an rtrm means:
 - quantifiers over a type that needs lifting are replaced by
 bounded quantifiers, for example:
 | (rt, qt) =>
 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
 *}
 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
 lemma eq_imp_rel:
 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
 by (simp add: equivp_reflp)
-(* FIXME/TODO: How does regularizing work? *)
-(* FIXME/TODO: needs to be adapted
+(* Regularize Tactic *)
-To prove that the raw theorem implies the regularised one,
+(* 0. preliminary simplification step according to *)
-we try in order:
+thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *)
+ball_reg_eqv_range bex_reg_eqv_range
-- Reflexivity of the relation
+(* 1. eliminating simple Ball/Bex instances*)
-- Assumption
+thm ball_reg_right bex_reg_left
-- Elimnating quantifiers on both sides of toplevel implication
+(* 2. monos *)
-- Simplifying implications on both sides of toplevel implication
+(* 3. commutation rules for ball and bex *)
-- Ball (Respects ?E) ?P = All ?P
+thm ball_all_comm bex_ex_comm
-- (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
+(* 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
 val thy = ProofContext.theory_of ctxt
 val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"}
 val simpset = (mk_minimal_ss ctxt)
 addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv}
 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},
+resolve_tac @{thms ball_reg_right bex_reg_left},
-rtac @{thm bex_reg_left},
 resolve_tac (Inductive.get_monos ctxt),
-rtac @{thm ball_all_comm},
+resolve_tac @{thms ball_all_comm bex_ex_comm},
-rtac @{thm 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:
 For abstractions:
 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")
 *}
-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
+let
-thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)]
+val goal = hd (Drule.strip_imp_prems (cprop_of thm))
-end
+in
-handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"
+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 *)
 (* It proves the Quotient assumptions by calling quotient_tac *)
 ML {*
 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
 => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
 (* 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}, _) $ _ $ _) $
 (Const (@{const_name fun_rel}, _) $ _ $ _) $
 (Const (@{const_name fun_rel}, _) $ _ $ _)
 | _ => error "inj_repabs_tac not a relation"
 ) i)
 *}
 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 $ \<dots>) (t' $ \<dots>) ----> 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 $ \<dots>) (t' $ \<dots>) ----> 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 =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-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 \<dots> \<dots> *)
-NDT ctxt "D" (resolve_tac rel_refl)
+NDT ctxt "F" (resolve_tac rel_refl)
 ])
 *}
 ML {*
-fun all_inj_repabs_tac ctxt rel_refl trans2 =
+fun inj_repabs_tac ctxt =
-REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
+let
-*}
+val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
+val trans2 = map (OF1 @{thm equals_rsp}) (quotient_rules_get ctxt)
-section {* Cleaning of the theorem *}
+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 *}
 ML {*
 fun make_inst lhs t =
 let
 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}
 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
 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
 end handle _ => (* TODO handle only Bind | Error "make_inst" *)
 let
 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";
 tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
 tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi)));
 More_Conv.top_conv lambda_prs_simple_conv
 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
 *}
-(*
+(* 1. conversion (is not a pattern) *)
-Cleaning the theorem consists of three rewriting steps.
+thm lambda_prs
-The first two need to be done before fun_map is unfolded
+(* 2. folding of definitions: (rep ---> abs) oldConst == newconst *)
+(*    and simplification with                                     *)
-1) lambda_prs:
+thm all_prs ex_prs
-(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))  ---->  f
+(* 3. simplification with *)
+thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps
-Implemented as conversion since it is not a pattern.
+(* 4. Test for refl *)
-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
-*)
 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]}
+val thms2 = @{thms eq_reflection[OF fun_map.simps]} @ (id_simps_get lthy)
-@ @{thms id_simps Quotient_abs_rep Quotient_rel_rep}
+@ @{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,
 simp_tac (simps thms1),
 simp_tac (simps thms2),
 TRY o rtac refl]
 end
 *}
-section {* Genralisation of free variables in a goal *}
+section {* Tactic for genralisation of free variables in a goal *}
 ML {*
 fun inst_spec ctrm =
 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
 in
 rtac rule i
 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           *)
 (* - C is the rep/abs injected version of B *)
 (* - D is the lifted theorem                *)
 assumes a: "A"
 and     b: "A \<longrightarrow> B"
 and     c: "B = C"
 and     d: "C = D"
 shows   "D"
 using a b c d
 by simp
 ML {*
 fun lift_match_error ctxt fun_str rtrm qtrm =
 let
 val rtrm_str = Syntax.string_of_term ctxt rtrm
 val rtrm' = HOLogic.dest_Trueprop rtrm
 val qtrm' = HOLogic.dest_Trueprop qtrm
 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'),
 SOME (cterm_of thy reg_goal),
 SOME (cterm_of thy inj_goal)] @{thm lifting_procedure}
 end
 *}
-(* Left for debugging *)
+ML {*
-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 rule = procedure_inst ctxt (prop_of rthm') (term_of goal)
-val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i}
+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)
 *}
-ML {*
+(* automatic proofs *)
-(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
+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 {*
 fun lift_tac ctxt rthm =
-ObjectLogic.full_atomize_tac
+procedure_tac ctxt rthm
-THEN' gen_frees_tac ctxt
+THEN' RANGE_WARN [(regularize_tac ctxt,     "Regularize proof failed."),
-THEN' CSUBGOAL (fn (gl, i) =>
+(all_inj_repabs_tac ctxt, "Injection proof failed."),
-let
+(clean_tac ctxt,          "Cleaning proof failed.")]
-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)
+end
-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)
-*}
-end

changeset 618	8dfae5d97387
parent 616	20b8585ad1e0
child 621	c10a46fa0de9