# HG changeset patch # User Christian Urban # Date 1259520535 -3600 # Node ID cc0b9cb367cd6c5b91dad784b1d7c687b56aa1f9 # Parent c22ab554a32da98e7e30245a971e828acbabcff9 added a new version of QuotMain to experiment with qids diff -r c22ab554a32d -r cc0b9cb367cd QuotMainNew.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/QuotMainNew.thy Sun Nov 29 19:48:55 2009 +0100 @@ -0,0 +1,1273 @@ +theory QuotMain +imports QuotScript QuotList Prove +uses ("quotient_info.ML") + ("quotient.ML") + ("quotient_def.ML") +begin + +locale QUOT_TYPE = + fixes R :: "'a \ 'a \ bool" + and Abs :: "('a \ bool) \ 'b" + and Rep :: "'b \ ('a \ bool)" + assumes equiv: "EQUIV R" + and rep_prop: "\y. \x. Rep y = R x" + and rep_inverse: "\x. Abs (Rep x) = x" + and abs_inverse: "\x. (Rep (Abs (R x))) = (R x)" + and rep_inject: "\x y. (Rep x = Rep y) = (x = y)" +begin + +definition + ABS::"'a \ 'b" +where + "ABS x \ Abs (R x)" + +definition + REP::"'b \ 'a" +where + "REP a = Eps (Rep a)" + +lemma lem9: + shows "R (Eps (R x)) = R x" +proof - + have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def) + then have "R x (Eps (R x))" by (rule someI) + then show "R (Eps (R x)) = R x" + using equiv unfolding EQUIV_def by simp +qed + +theorem thm10: + shows "ABS (REP a) \ a" + apply (rule eq_reflection) + unfolding ABS_def REP_def +proof - + from rep_prop + obtain x where eq: "Rep a = R x" by auto + have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp + also have "\ = Abs (R x)" using lem9 by simp + also have "\ = Abs (Rep a)" using eq by simp + also have "\ = a" using rep_inverse by simp + finally + show "Abs (R (Eps (Rep a))) = a" by simp +qed + +lemma REP_refl: + shows "R (REP a) (REP a)" +unfolding REP_def +by (simp add: equiv[simplified EQUIV_def]) + +lemma lem7: + shows "(R x = R y) = (Abs (R x) = Abs (R y))" +apply(rule iffI) +apply(simp) +apply(drule rep_inject[THEN iffD2]) +apply(simp add: abs_inverse) +done + +theorem thm11: + shows "R r r' = (ABS r = ABS r')" +unfolding ABS_def +by (simp only: equiv[simplified EQUIV_def] lem7) + + +lemma REP_ABS_rsp: + shows "R f (REP (ABS g)) = R f g" + and "R (REP (ABS g)) f = R g f" +by (simp_all add: thm10 thm11) + +lemma QUOTIENT: + "QUOTIENT R ABS REP" +apply(unfold QUOTIENT_def) +apply(simp add: thm10) +apply(simp add: REP_refl) +apply(subst thm11[symmetric]) +apply(simp add: equiv[simplified EQUIV_def]) +done + +lemma R_trans: + assumes ab: "R a b" + and bc: "R b c" + shows "R a c" +proof - + have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp + moreover have ab: "R a b" by fact + moreover have bc: "R b c" by fact + ultimately show "R a c" unfolding TRANS_def by blast +qed + +lemma R_sym: + assumes ab: "R a b" + shows "R b a" +proof - + have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp + then show "R b a" using ab unfolding SYM_def by blast +qed + +lemma R_trans2: + assumes ac: "R a c" + and bd: "R b d" + shows "R a b = R c d" +using ac bd +by (blast intro: R_trans R_sym) + +lemma REPS_same: + shows "R (REP a) (REP b) \ (a = b)" +proof - + have "R (REP a) (REP b) = (a = b)" + proof + assume as: "R (REP a) (REP b)" + from rep_prop + obtain x y + where eqs: "Rep a = R x" "Rep b = R y" by blast + from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp + then have "R x (Eps (R y))" using lem9 by simp + then have "R (Eps (R y)) x" using R_sym by blast + then have "R y x" using lem9 by simp + then have "R x y" using R_sym by blast + then have "ABS x = ABS y" using thm11 by simp + then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp + then show "a = b" using rep_inverse by simp + next + assume ab: "a = b" + have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp + then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto + qed + then show "R (REP a) (REP b) \ (a = b)" by simp +qed + +end + +lemma equiv_trans2: + assumes e: "EQUIV R" + and ac: "R a c" + and bd: "R b d" + shows "R a b = R c d" +using ac bd e +unfolding EQUIV_REFL_SYM_TRANS TRANS_def SYM_def +by (blast) + +section {* type definition for the quotient type *} + +(* the auxiliary data for the quotient types *) +use "quotient_info.ML" + +declare [[map list = (map, LIST_REL)]] +declare [[map * = (prod_fun, prod_rel)]] +declare [[map "fun" = (fun_map, FUN_REL)]] + +ML {* maps_lookup @{theory} "List.list" *} +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" + +(* TODO: Consider defining it with an "if"; sth like: + Babs p m = \x. if x \ p then m x else undefined +*) +definition + Babs :: "('a \ bool) \ ('a \ 'b) \ 'a \ 'b" +where + "(x \ p) \ (Babs p m x = m x)" + +section {* ATOMIZE *} + +lemma atomize_eqv[atomize]: + shows "(Trueprop A \ Trueprop B) \ (A \ B)" +proof + assume "A \ B" + then show "Trueprop A \ Trueprop B" by unfold +next + assume *: "Trueprop A \ Trueprop B" + have "A = B" + proof (cases A) + case True + have "A" by fact + then show "A = B" using * by simp + next + case False + have "\A" by fact + then show "A = B" using * by auto + qed + then show "A \ B" by (rule eq_reflection) +qed + +ML {* +fun atomize_thm thm = +let + val thm' = Thm.freezeT (forall_intr_vars thm) + val thm'' = ObjectLogic.atomize (cprop_of thm') +in + @{thm equal_elim_rule1} OF [thm'', thm'] +end +*} + +section {* infrastructure about id *} + +lemma prod_fun_id: "prod_fun id id \ id" + by (rule eq_reflection) (simp add: prod_fun_def) + +lemma map_id: "map id \ id" + apply (rule eq_reflection) + apply (rule ext) + apply (rule_tac list="x" in list.induct) + apply (simp_all) + done + +lemmas id_simps = + FUN_MAP_I[THEN eq_reflection] + id_apply[THEN eq_reflection] + id_def[THEN eq_reflection,symmetric] + prod_fun_id map_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 = +let + val prem_str = nth (prems_of thm) (i - 1) + |> Syntax.string_of_term ctxt + handle Subscript => "no subgoal" + val _ = tracing (s ^ "\n" ^ prem_str) +in + Seq.single thm +end *} + + +ML {* +fun DT ctxt s tac i thm = +let + val before_goal = nth (prems_of thm) (i - 1) + |> Syntax.string_of_term ctxt + val before_msg = ["before: " ^ s, before_goal, "after: " ^ s] + |> cat_lines +in + EVERY [tac i, my_print_tac ctxt before_msg i] thm +end + +fun NDT ctxt s tac thm = tac thm +*} + + +section {* Infrastructure about definitions *} + +(* Does the same as 'subst' in a given theorem *) +ML {* +fun eqsubst_thm ctxt thms thm = + let + val goalstate = Goal.init (Thm.cprop_of thm) + val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of + NONE => error "eqsubst_thm" + | SOME th => cprem_of th 1 + val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 + val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'); + val cgoal = cterm_of (ProofContext.theory_of ctxt) goal + val rt = Goal.prove_internal [] cgoal (fn _ => tac); + in + @{thm equal_elim_rule1} OF [rt, thm] + end +*} + +(* expects atomized definitions *) +ML {* +fun add_lower_defs_aux lthy thm = + let + val e1 = @{thm fun_cong} OF [thm]; + val f = eqsubst_thm lthy @{thms fun_map.simps} e1; + val g = simp_ids f + in + (simp_ids thm) :: (add_lower_defs_aux lthy g) + end + handle _ => [simp_ids thm] +*} + +ML {* +fun add_lower_defs lthy def = + let + val def_pre_sym = symmetric def + val def_atom = atomize_thm def_pre_sym + val defs_all = add_lower_defs_aux lthy def_atom + in + map Thm.varifyT defs_all + end +*} + +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 + (* cu: Changed the lookup\not sure whether this works *) + (* 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 EQUIV_REFL} 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 +*} + +ML {* +fun lookup_quot_consts defs = + let + fun dest_term (a $ b) = (a, b); + val def_terms = map (snd o Logic.dest_equals o concl_of) defs; + in + map (fst o dest_Const o snd o dest_term) def_terms + end +*} + +section {* Infrastructure for special quotient identity *} + +definition + "qid TYPE('a) TYPE('b) x \ x" + +ML {* +fun get_typ_aux (Type ("itself", [T])) = T +fun get_typ (Const ("TYPE", T)) = get_typ_aux T +fun get_tys (Const (@{const_name "qid"},_) $ ty1 $ ty2) = + (get_typ ty1, get_typ ty2) + +fun is_qid (Const (@{const_name "qid"},_) $ _ $ _) = true + | is_qid _ = false + + +fun mk_itself ty = Type ("itself", [ty]) +fun mk_TYPE ty = Const ("TYPE", mk_itself ty) +fun mk_qid (rty, qty, trm) = + Const (@{const_name "qid"}, [mk_itself rty, mk_itself qty, dummyT] ---> dummyT) + $ mk_TYPE rty $ mk_TYPE qty $ trm +*} + +ML {* +fun insertion_aux rtrm qtrm = + case (rtrm, qtrm) of + (Abs (x, ty, t), Abs (x', ty', t')) => + let + val (y, s) = Term.dest_abs (x, ty, t) + val (_, s') = Term.dest_abs (x', ty', t') + val yvar = Free (y, ty) + val result = Term.lambda_name (y, yvar) (insertion_aux s s') + in + if ty = ty' + then result + else mk_qid (ty, ty', result) + end + | (t1 $ t2, t1' $ t2') => + let + val rty = fastype_of rtrm + val qty = fastype_of qtrm + val subtrm1 = insertion_aux t1 t1' + val subtrm2 = insertion_aux t2 t2' + in + if rty = qty + then subtrm1 $ subtrm2 + else mk_qid (rty, qty, subtrm1 $ subtrm2) + end + | (Free (_, ty), Free (_, ty')) => + if ty = ty' + then rtrm + else mk_qid (ty, ty', rtrm) + | (Const (s, ty), Const (s', ty')) => + if s = s' andalso ty = ty' + then rtrm + else mk_qid (ty, ty', rtrm) + | (_, _) => raise (LIFT_MATCH "insertion") +*} + +section {* Regularization *} + +(* +Regularizing an rtrm means: + - quantifiers over a type that needs lifting are replaced by + bounded quantifiers, for example: + \x. P \ \x \ (Respects R). P / All (Respects R) P + + the relation R is given by the rty and qty; + + - abstractions over a type that needs lifting are replaced + by bounded abstractions: + \x. P \ Ball (Respects R) (\x. P) + + - equalities over the type being lifted are replaced by + corresponding relations: + A = B \ A \ B + + example with more complicated types of A, B: + A = B \ (op = \ op \) A B +*) + +ML {* +(* builds the relation that is the argument of respects *) +fun mk_resp_arg lthy (rty, qty) = +let + val thy = ProofContext.theory_of lthy +in + if rty = qty + then HOLogic.eq_const rty + else + case (rty, qty) of + (Type (s, tys), Type (s', tys')) => + if s = s' + then let + val SOME map_info = maps_lookup thy s + val args = map (mk_resp_arg lthy) (tys ~~ tys') + in + list_comb (Const (#relfun map_info, dummyT), args) + end + else let + val SOME qinfo = quotdata_lookup_thy thy s' + (* FIXME: check in this case that the rty and qty *) + (* FIXME: correspond to each other *) + val (s, _) = dest_Const (#rel qinfo) + (* FIXME: the relation should only be the string *) + (* FIXME: and the type needs to be calculated as below; *) + (* FIXME: maybe one should actually have a term *) + (* FIXME: and one needs to force it to have this type *) + in + Const (s, rty --> rty --> @{typ bool}) + end + | _ => HOLogic.eq_const dummyT + (* FIXME: check that the types correspond to each other? *) +end +*} + +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) +val mk_resp = Const (@{const_name Respects}, dummyT) +*} + +ML {* +(* - applies f to the subterm of an abstraction, *) +(* otherwise to the given term, *) +(* - used by regularize, therefore abstracted *) +(* variables do not have to be treated specially *) + +fun apply_subt f trm = + case trm of + (Abs (x, T, t)) => Abs (x, T, f t) + | _ => f trm + +(* the major type of All and Ex quantifiers *) +fun qnt_typ ty = domain_type (domain_type ty) +*} + +ML {* +(* produces a regularized version of trm *) +(* - the result is still not completely typed *) +(* - does not need any special treatment of *) +(* bound variables *) + +fun regularize_trm lthy trm = + case trm of + (Const (@{const_name "qid"},_) $ rty' $ qty' $ Abs (x, ty, t)) => + let + val rty = get_typ rty' + val qty = get_typ qty' + val subtrm = regularize_trm lthy t + in + mk_qid (rty, qty, mk_babs $ (mk_resp $ mk_resp_arg lthy (rty, qty)) $ subtrm) + end + | (Const (@{const_name "qid"},_) $ rty' $ qty' $ (Const (@{const_name "All"}, ty) $ t)) => + let + val subtrm = apply_subt (regularize_trm lthy) t + in + if ty = ty' + then Const (@{const_name "All"}, ty) $ subtrm + else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm + end + | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => + let + val subtrm = apply_subt (regularize_trm lthy) t t' + in + if ty = ty' + then Const (@{const_name "Ex"}, ty) $ subtrm + else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm + end + (* FIXME: Should = only be replaced, when fully applied? *) + (* Then there must be a 2nd argument *) + | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') => + let + val subtrm = regularize_trm lthy t t' + in + if ty = ty' + then Const (@{const_name "op ="}, ty) $ subtrm + else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm + end + | (t1 $ t2, t1' $ t2') => + (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') + | (Free (x, ty), Free (x', ty')) => + (* this case cannot arrise as we start with two fully atomized terms *) + raise (LIFT_MATCH "regularize (frees)") + | (Bound i, Bound i') => + if i = i' + then rtrm + else raise (LIFT_MATCH "regularize (bounds)") + | (Const (s, ty), Const (s', ty')) => + if s = s' andalso ty = ty' + then rtrm + else rtrm (* FIXME: check correspondence according to definitions *) + | (rt, qt) => + raise (LIFT_MATCH "regularize (default)") +*} + +(* +FIXME / TODO: needs to be adapted + +To prove that the raw theorem implies the regularised one, +we try in order: + + - 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 + +*) + +(* FIXME: they should be in in the new Isabelle *) +lemma [mono]: + "(\x. P x \ Q x) \ (Ex P) \ (Ex Q)" +by blast + +lemma [mono]: "P \ Q \ \Q \ \P" +by auto + +(* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *) +ML {* +fun equiv_tac rel_eqvs = + REPEAT_ALL_NEW (FIRST' + [resolve_tac rel_eqvs, + rtac @{thm IDENTITY_EQUIV}, + rtac @{thm LIST_EQUIV}]) +*} + +ML {* +fun ball_reg_eqv_simproc rel_eqvs ss redex = + let + val ctxt = Simplifier.the_context ss + val thy = ProofContext.theory_of ctxt + in + case redex of + (ogl as ((Const (@{const_name "Ball"}, _)) $ + ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) => + (let + val gl = Const (@{const_name "EQUIV"}, dummyT) $ R; + val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); + val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); + val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]); +(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) + in + SOME thm + end + handle _ => NONE + ) + | _ => NONE + end +*} + +ML {* +fun bex_reg_eqv_simproc rel_eqvs ss redex = + let + val ctxt = Simplifier.the_context ss + val thy = ProofContext.theory_of ctxt + in + case redex of + (ogl as ((Const (@{const_name "Bex"}, _)) $ + ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) => + (let + val gl = Const (@{const_name "EQUIV"}, dummyT) $ R; + val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); + val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); + val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]); +(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) + in + SOME thm + end + handle _ => NONE + ) + | _ => NONE + end +*} + +ML {* +fun prep_trm thy (x, (T, t)) = + (cterm_of thy (Var (x, T)), cterm_of thy t) + +fun prep_ty thy (x, (S, ty)) = + (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) +*} + +ML {* +fun matching_prs thy pat trm = +let + val univ = Unify.matchers thy [(pat, trm)] + val SOME (env, _) = Seq.pull univ + val tenv = Vartab.dest (Envir.term_env env) + val tyenv = Vartab.dest (Envir.type_env env) +in + (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) +end +*} + +ML {* +fun ball_reg_eqv_range_simproc rel_eqvs ss redex = + let + val ctxt = Simplifier.the_context ss + val thy = ProofContext.theory_of ctxt + in + case redex of + (ogl as ((Const (@{const_name "Ball"}, _)) $ + ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) => + (let + val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2; + val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); + val _ = tracing (Syntax.string_of_term ctxt glc); + val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); + val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]); + val R1c = cterm_of thy R1; + val thmi = Drule.instantiate' [] [SOME R1c] thm; +(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *) + val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl + val _ = tracing "AAA"; + val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); + val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); + in + SOME thm2 + end + handle _ => NONE + + ) + | _ => NONE + end +*} + +ML {* +fun bex_reg_eqv_range_simproc rel_eqvs ss redex = + let + val ctxt = Simplifier.the_context ss + val thy = ProofContext.theory_of ctxt + in + case redex of + (ogl as ((Const (@{const_name "Bex"}, _)) $ + ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) => + (let + val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2; + val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); + val _ = tracing (Syntax.string_of_term ctxt glc); + val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); + val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]); + val R1c = cterm_of thy R1; + val thmi = Drule.instantiate' [] [SOME R1c] thm; +(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *) + val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl + val _ = tracing "AAA"; + val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); + val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); + in + SOME thm2 + end + handle _ => NONE + + ) + | _ => NONE + end +*} + +lemma eq_imp_rel: "EQUIV R \ a = b \ R a b" +by (simp add: EQUIV_REFL) + +ML {* +fun regularize_tac ctxt rel_eqvs = + let + val pat1 = [@{term "Ball (Respects R) P"}]; + val pat2 = [@{term "Bex (Respects R) P"}]; + val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}]; + val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}]; + val thy = ProofContext.theory_of ctxt + val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs)) + val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc rel_eqvs)) + val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs)) + val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs)) + val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4] + (* TODO: Make sure that there are no LIST_REL, PAIR_REL etc involved *) + val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) rel_eqvs + in + ObjectLogic.full_atomize_tac THEN' + simp_tac simp_ctxt THEN' + REPEAT_ALL_NEW (FIRST' [ + rtac @{thm ball_reg_right}, + rtac @{thm bex_reg_left}, + resolve_tac (Inductive.get_monos ctxt), + rtac @{thm ball_all_comm}, + rtac @{thm bex_ex_comm}, + resolve_tac eq_eqvs, + simp_tac simp_ctxt + ]) + end +*} + +section {* Injections of REP and ABSes *} + +(* +Injecting REPABS means: + + For abstractions: + * If the type of the abstraction doesn't need lifting we recurse. + * If it does we add RepAbs around the whole term and check if the + 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. 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 + how to lift, we put a RepAbs and recurse + * If the term needs lifting and the head is a free applied to subterms + (if it is not applied we treated it in Abs branch) then we + put RepAbs and recurse + * Otherwise just recurse. +*) + +ML {* +fun mk_repabs lthy (T, T') trm = + Quotient_Def.get_fun repF lthy (T, T') + $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) +*} + +ML {* +(* bound variables need to be treated properly, *) +(* as the type of subterms need to be calculated *) + +fun inj_repabs_trm lthy (rtrm, qtrm) = +let + val rty = fastype_of rtrm + val qty = fastype_of qtrm +in + case (rtrm, qtrm) of + (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => + Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t')) + | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => + Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t')) + | (Const (@{const_name "Babs"}, T) $ r $ t, t') => + Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')) + | (Abs (x, T, t), Abs (x', T', t')) => + 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 + then result + else mk_repabs lthy (rty, qty) result + end + | _ => + (* FIXME / TODO: this is a case that needs to be looked at *) + (* - variables get a rep-abs insde and outside an application *) + (* - constants only get a rep-abs on the outside of the application *) + (* - applications get a rep-abs insde and outside an application *) + let + val (rhead, rargs) = strip_comb rtrm + val (qhead, qargs) = strip_comb qtrm + val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) + in + if rty = qty + then + case (rhead, qhead) of + (Free (_, T), Free (_, T')) => + if T = T' then list_comb (rhead, rargs') + else list_comb (mk_repabs lthy (T, T') rhead, rargs') + | _ => list_comb (rhead, rargs') + else + case (rhead, qhead, length rargs') of + (Const _, Const _, 0) => mk_repabs lthy (rty, qty) rhead + | (Free (_, T), Free (_, T'), 0) => mk_repabs lthy (T, T') rhead + | (Const _, Const _, _) => mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) + | (Free (x, T), Free (x', T'), _) => + mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs')) + | (Abs _, Abs _, _ ) => + mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')) + | _ => raise (LIFT_MATCH "injection") + end +end +*} + +section {* RepAbs Injection Tactic *} + +ML {* +fun stripped_term_of ct = + ct |> term_of |> HOLogic.dest_Trueprop +*} + +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) +*} + +ML {* +fun quotient_tac quot_thms = + REPEAT_ALL_NEW (FIRST' + [rtac @{thm FUN_QUOTIENT}, + resolve_tac quot_thms, + rtac @{thm IDENTITY_QUOTIENT}, + (* For functional identity quotients, (op = ---> op =) *) + (* TODO: think about the other way around, if we need to shorten the relation *) + CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))]) +*} + +lemma FUN_REL_I: + assumes a: "\x y. R1 x y \ R2 (f x) (g y)" + shows "(R1 ===> R2) f g" +using a by (simp add: FUN_REL.simps) + +ML {* +val lambda_res_tac = + Subgoal.FOCUS (fn {concl, ...} => + case (stripped_term_of concl) of + (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} 1 + | _ => no_tac) +*} + +ML {* +val weak_lambda_res_tac = + Subgoal.FOCUS (fn {concl, ...} => + case (stripped_term_of concl) of + (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} 1 + | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} 1 + | _ => no_tac) +*} + +ML {* +val ball_rsp_tac = + Subgoal.FOCUS (fn {concl, ...} => + case (stripped_term_of concl) of + (_ $ (Const (@{const_name Ball}, _) $ _) + $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} 1 + |_ => no_tac) +*} + +ML {* +val bex_rsp_tac = + Subgoal.FOCUS (fn {concl, context = ctxt, ...} => + case (stripped_term_of concl) of + (_ $ (Const (@{const_name Bex}, _) $ _) + $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} 1 + | _ => no_tac) +*} + +ML {* (* Legacy *) +fun needs_lift (rty as Type (rty_s, _)) ty = + case ty of + Type (s, tys) => (s = rty_s) orelse (exists (needs_lift rty) tys) + | _ => false + +*} + +ML {* +fun APPLY_RSP_TAC rty = + Subgoal.FOCUS (fn {concl, ...} => + case (stripped_term_of concl) of + (_ $ (f $ _) $ (_ $ _)) => + let + val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); + val insts = Thm.match (pat, concl) + in + if needs_lift rty (fastype_of f) + then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 + else no_tac + end + | _ => 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: + + 1) theorems 'trans2' from the appropriate QUOT_TYPE + 2) remove lambdas from both sides: lambda_res_tac + 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 + A) reflexivity of the relation + B) assumption + (Lambdas under respects may have left us some assumptions) + C) proving obvious higher order equalities by simplifying fun_rel + (not sure if it is still needed?) + D) unfolding lambda on one side + E) simplifying (= ===> =) for simpler respectfulness + +*) + +ML {* +fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = + (FIRST' [ + (* "cong" rule of the of the relation / transitivity*) + (* (op =) (R a b) (R c d) ----> \R a c; R b d\ *) + NDT ctxt "1" (resolve_tac trans2), + + (* (R1 ===> R2) (\x\) (\y\) ----> \R1 x y\ \ R2 (\x) (\y) *) + NDT ctxt "2" (lambda_res_tac ctxt), + + (* (op =) (Ball\) (Ball\) ----> (op =) (\) (\) *) + NDT ctxt "3" (rtac @{thm RES_FORALL_RSP}), + + (* (R1 ===> R2) (Ball\) (Ball\) ----> \R1 x y\ \ R2 (Ball\x) (Ball\y) *) + NDT ctxt "4" (ball_rsp_tac ctxt), + + (* (op =) (Bex\) (Bex\) ----> (op =) (\) (\) *) + NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), + + (* (R1 ===> R2) (Bex\) (Bex\) ----> \R1 x y\ \ R2 (Bex\x) (Bex\y) *) + NDT ctxt "6" (bex_rsp_tac ctxt), + + (* respectfulness of constants *) + NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)), + + (* reflexivity of operators arising from Cong_tac *) + NDT ctxt "8" (rtac @{thm refl}), + + (* R (\) (Rep (Abs \)) ----> R (\) (\) *) + (* observe ---> *) + NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt + THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), + + (* R (t $ \) (t' $ \) ----> APPLY_RSP provided type of t needs lifting *) + NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' + (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), + + (* (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}), + + (* (op =) (\x\) (\x\) ----> (op =) (\) (\) *) + NDT ctxt "C" (rtac @{thm ext}), + + (* reflexivity of the basic relations *) + (* R \ \ *) + NDT ctxt "D" (resolve_tac rel_refl), + + (* resolving with R x y assumptions *) + NDT ctxt "E" (atac), + + (* seems not necessay:: NDT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*) + + (* (R1 ===> R2) (\) (\y\) ----> \R1 x y\ \ R2 (\x) (\y) *) + (* (R1 ===> R2) (\x\) (\) ----> \R1 x y\ \ R2 (\x) (\y) *) + (*NDT ctxt "G" (weak_lambda_res_tac ctxt),*) + + (* (op =) ===> (op =) \ (op =), needed in order to apply respectfulness theorems *) + (* global simplification *) + NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))]) +*} + +ML {* +fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = + REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2) +*} + + +section {* Cleaning of the theorem *} + +ML {* +fun applic_prs lthy absrep (rty, qty) = + let + fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm; + fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm; + val (raty, rgty) = Term.strip_type rty; + val (qaty, qgty) = Term.strip_type qty; + val vs = map (fn _ => "x") qaty; + val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy; + val f = Free (fname, qaty ---> qgty); + val args = map Free (vfs ~~ qaty); + val rhs = list_comb(f, args); + val largs = map2 mk_rep (raty ~~ qaty) args; + val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs)); + val llhs = Syntax.check_term lthy lhs; + val eq = Logic.mk_equals (llhs, rhs); + val ceq = cterm_of (ProofContext.theory_of lthy') eq; + val sctxt = HOL_ss addsimps (@{thms fun_map.simps id_simps} @ absrep); + val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1) + val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t; + in + singleton (ProofContext.export lthy' lthy) t_id + end +*} + +ML {* +fun find_aps_all rtm qtm = + case (rtm, qtm) of + (Abs(_, T1, s1), Abs(_, T2, s2)) => + find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2)) + | (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) => + let + val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2) + in + if T1 = T2 then sub else (T1, T2) :: sub + end + | ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2) + | _ => []; + +fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm) +*} + +ML {* +fun allex_prs_tac lthy quot = + (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) + THEN' (quotient_tac quot) +*} + +(* Rewrites the term with LAMBDA_PRS thm. + +Replaces: (Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) + with: f + +It proves the QUOTIENT assumptions by calling quotient_tac + *) +ML {* +fun make_inst lhs t = + let + val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; + val _ $ (Abs (_, _, g)) = t; + fun mk_abs i t = + if incr_boundvars i u aconv t then Bound i + else (case t of + t1 $ t2 => mk_abs i t1 $ mk_abs i t2 + | Abs (s, T, t') => Abs (s, T, mk_abs (i+1) t') + | Bound j => if i = j then error "make_inst" else t + | _ => t); + in (f, Abs ("x", T, mk_abs 0 g)) end; + +fun lambda_prs_conv1 ctxt quot_thms ctrm = + case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => + let + val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); + val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2); + val thy = ProofContext.theory_of ctxt; + val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d] + val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d]; + val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] + val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS}; + val tac = + (compose_tac (false, lpi, 2)) THEN_ALL_NEW + (quotient_tac quot_thms); + val gc = Drule.strip_imp_concl (cprop_of lpi); + val t = Goal.prove_internal [] gc (fn _ => tac 1) + val te = @{thm eq_reflection} OF [t] + val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te + val tl = Thm.lhs_of ts; + val (insp, inst) = make_inst (term_of tl) (term_of ctrm); + val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; +(* val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*) + in + Conv.rewr_conv ti ctrm + end +*} + +(* quot stands for the QUOTIENT theorems: *) +(* could be potentially all of them *) +ML {* +fun lambda_prs_conv ctxt quot ctrm = + case (term_of ctrm) of + (Const (@{const_name "fun_map"}, _) $ _ $ _) $ (Abs _) => + (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt) + then_conv (lambda_prs_conv1 ctxt quot)) ctrm + | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm + | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm + | _ => Conv.all_conv ctrm +*} + +ML {* +fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) => + CONVERSION + (Conv.params_conv ~1 (fn ctxt => + (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv + Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) +*} + +ML {* +fun clean_tac lthy quot defs aps = + let + val lower = flat (map (add_lower_defs lthy) defs) + val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower + val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot + val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot + val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same + val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps (meta_reps_same @ meta_lower) + val aps_thms = map (applic_prs lthy absrep) aps + in + EVERY' [lambda_prs_tac lthy quot, + TRY o simp_tac simp_ctxt, + TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), + TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms), + TRY o rtac refl] + end +*} + +section {* Genralisation of free variables in a goal *} + +ML {* +fun inst_spec ctrm = + Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} + +fun inst_spec_tac ctrms = + EVERY' (map (dtac o inst_spec) ctrms) + +fun all_list xs trm = + fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm + +fun apply_under_Trueprop f = + HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop + +fun gen_frees_tac ctxt = + SUBGOAL (fn (concl, i) => + let + val thy = ProofContext.theory_of ctxt + val vrs = Term.add_frees concl [] + val cvrs = map (cterm_of thy o Free) vrs + val concl' = apply_under_Trueprop (all_list vrs) concl + val goal = Logic.mk_implies (concl', concl) + val rule = Goal.prove ctxt [] [] goal + (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) + in + rtac rule i + end) +*} + +section {* General outline 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 *) +(* *) +(* - b is the regularization step *) +(* - c is the rep/abs injection step *) +(* - d is the cleaning part *) + +lemma lifting_procedure: + assumes a: "A" + and b: "A \ 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 qtrm_str = Syntax.string_of_term ctxt qtrm + val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str, + "and the lifted theorem\n", rtrm_str, "do not match"] +in + error (space_implode " " msg) +end +*} + +ML {* +fun procedure_inst ctxt rtrm qtrm = +let + val thy = ProofContext.theory_of ctxt + 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 inj_goal = + Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) + handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm +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 {* +fun procedure_tac lthy rthm = + ObjectLogic.full_atomize_tac + THEN' gen_frees_tac lthy + THEN' Subgoal.FOCUS (fn {context, concl, ...} => + let + val rthm' = atomize_thm rthm + val rule = procedure_inst context (prop_of rthm') (term_of concl) + in + EVERY1 [rtac rule, rtac rthm'] + end) lthy +*} + +ML {* +(* FIXME/TODO should only get as arguments the rthm like procedure_tac *) +fun lift_tac lthy rthm rel_eqv rty quot defs = + ObjectLogic.full_atomize_tac + THEN' gen_frees_tac lthy + THEN' Subgoal.FOCUS (fn {context, concl, ...} => + let + val rthm' = atomize_thm rthm + val rule = procedure_inst context (prop_of rthm') (term_of concl) + val aps = find_aps (prop_of rthm') (term_of concl) + val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv + val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv + in + EVERY1 + [rtac rule, + RANGE [rtac rthm', + regularize_tac lthy rel_eqv, + all_inj_repabs_tac lthy rty quot rel_refl trans2, + clean_tac lthy quot defs aps]] + end) lthy +*} + +end + +