--- a/QuotMainNew.thy Sun Nov 29 19:48:55 2009 +0100
+++ b/QuotMainNew.thy Sun Nov 29 23:59:37 2009 +0100
@@ -1,4 +1,4 @@
-theory QuotMain
+theory QuotMainNew
imports QuotScript QuotList Prove
uses ("quotient_info.ML")
("quotient.ML")
@@ -259,90 +259,6 @@
*}
-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\<dots>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
@@ -366,41 +282,87 @@
*}
ML {*
-fun insertion_aux rtrm qtrm =
+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')
+ 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'
+ val qty = fastype_of qtrm
+ val (rhead, rargs) = strip_comb rtrm
+ val (qhead, qargs) = strip_comb qtrm
+ val rargs' = map insertion_aux (rargs ~~ qargs)
+ val rhead' = insertion_aux (rhead, qhead)
+ val result = list_comb (rhead', rargs')
in
if rty = qty
- then subtrm1 $ subtrm2
- else mk_qid (rty, qty, subtrm1 $ subtrm2)
+ then result
+ else mk_qid (rty, qty, result)
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'
+ if s = s'
then rtrm
else mk_qid (ty, ty', rtrm)
| (_, _) => raise (LIFT_MATCH "insertion")
*}
+ML {*
+fun insertion ctxt rtrm qtrm =
+ Syntax.check_term ctxt (insertion_aux (rtrm, qtrm))
+*}
+
+
+fun
+ intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
+where
+ "intrel (x, y) (u, v) = (x + v = u + y)"
+
+quotient my_int = "nat \<times> nat" / intrel
+ apply(unfold EQUIV_def)
+ apply(auto simp add: mem_def expand_fun_eq)
+ done
+
+fun
+ my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+ "my_plus (x, y) (u, v) = (x + u, y + v)"
+
+quotient_def
+ PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
+where
+ "PLUS \<equiv> my_plus"
+
+thm PLUS_def
+
+ML {* MetaSimplifier.rewrite_term *}
+
+ML {*
+let
+ val rtrm = @{term "\<forall>a b. my_plus a b \<approx> my_plus b a"}
+ val qtrm = @{term "\<forall>a b. PLUS a b = PLUS b a"}
+ val ctxt = @{context}
+in
+ insertion ctxt rtrm qtrm
+ (*|> Drule.term_rule @{theory} (MetaSimplifier.rewrite_rule [@{thm "qid_def"}])*)
+ |> Syntax.string_of_term ctxt
+ |> writeln
+end
+*}
+
section {* Regularization *}
(*
@@ -554,188 +516,6 @@
*)
-(* FIXME: they should be in in the new Isabelle *)
-lemma [mono]:
- "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
-by blast
-
-lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>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 \<Longrightarrow> a = b \<longrightarrow> 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 *}
(*
@@ -824,332 +604,6 @@
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: "\<And>x y. R1 x y \<Longrightarrow> 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) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
- NDT ctxt "1" (resolve_tac trans2),
-
- (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
- NDT ctxt "2" (lambda_res_tac ctxt),
-
- (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
- NDT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
-
- (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
- NDT ctxt "4" (ball_rsp_tac ctxt),
-
- (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
- NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
-
- (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>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 (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
- (* observe ---> *)
- NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt
- THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
-
- (* R (t $ \<dots>) (t' $ \<dots>) ----> 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 $ \<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}),
-
- (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
- NDT ctxt "C" (rtac @{thm ext}),
-
- (* reflexivity of the basic relations *)
- (* R \<dots> \<dots> *)
- 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) (\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
- (* (R1 ===> R2) (\<lambda>x\<dots>) (\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
- (*NDT ctxt "G" (weak_lambda_res_tac ctxt),*)
-
- (* (op =) ===> (op =) \<Longrightarrow> (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) (\<lambda>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 {*
@@ -1260,11 +714,7 @@
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]]
+ [rtac rule, rtac rthm']
end) lthy
*}