nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:e30997c88050
+:77ff9624cfd6
 *}
 section {* lifting of constants *}
 ML {*
-(* whether ty1 is an instance of ty2 *)
-fun matches (ty1, ty2) =
-Type.raw_instance (ty1, Logic.varifyT ty2)
 fun lookup_snd _ [] _ = NONE
 | lookup_snd eq ((value, key)::xs) key' =
 if eq (key', key) then SOME value
 else lookup_snd eq xs key';
 fun lookup_qenv qenv qty =
-(case (AList.lookup matches qenv qty) of
+(case (AList.lookup (op =) qenv qty) of
 SOME rty => SOME (qty, rty)
 | NONE => NONE)
 *}
 ML {*
 end
 fun mk_identity ty = Abs ("", ty, Bound 0)
 in
-if (AList.defined matches qenv ty)
+if (AList.defined (op =) qenv ty)
 then (get_const flag (the (lookup_qenv qenv ty)))
 else (case ty of
 TFree _ => (mk_identity ty, (ty, ty))
 | Type (_, []) => (mk_identity ty, (ty, ty))
 | Type ("fun" , [ty1, ty2]) =>
 in
 fns $ otrm
 end
 *}
-ML {* lookup_snd *}
 ML {*
 fun exchange_ty qenv ty =
-case (lookup_snd matches qenv ty) of
+case (lookup_snd (op =) qenv ty) of
 SOME qty => qty
 | NONE =>
 (case ty of
 Type (s, tys) => Type (s, map (exchange_ty qenv) tys)
 | _ => ty
 )
 *}
+ML {*
+fun ppair lthy (ty1, ty2) =
+"(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")"
+*}
+ML {*
+fun print_env qenv lthy =
+map (ppair lthy) qenv
+|> commas
+|> tracing
+*}
 ML {*
 fun make_const_def nconst_bname otrm mx qenv lthy =
 let
 val otrm_ty = fastype_of otrm
 val nconst_ty = exchange_ty qenv otrm_ty
 val nconst = Const (Binding.name_of nconst_bname, nconst_ty)
 val def_trm = get_const_def nconst otrm qenv lthy
+val _ = print_env qenv lthy
+val _ = Syntax.string_of_typ lthy otrm_ty |> tracing
+val _ = Syntax.string_of_typ lthy nconst_ty |> tracing
+val _ = Syntax.string_of_term lthy def_trm |> tracing
 in
 define (nconst_bname, mx, def_trm) lthy
 end
 *}
 ML {*
 fun build_qenv lthy qtys =
 let
 val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy)
+val tsig = Sign.tsig_of (ProofContext.theory_of lthy)
-fun find_assoc qty =
-case (AList.lookup matches qenv qty) of
+fun find_assoc ((qty', rty')::rest) qty =
-SOME rty => (qty, rty)
+let
-| NONE => error (implode
+val inst = Type.typ_match tsig (qty', qty) Vartab.empty
-["Quotient type ",
+in
-quote (Syntax.string_of_typ lthy qty),
+(Envir.norm_type inst qty, Envir.norm_type inst rty')
-" does not exists"])
+end
+| find_assoc [] qty =
+let
+val qtystr =  quote (Syntax.string_of_typ lthy qty)
+in
+error (implode ["Quotient type ", qtystr, " does not exists"])
+end
 in
-map find_assoc qtys
+map (find_assoc qenv) qtys
 end
-*}
-ML {*
-(* taken from isar_syn.ML *)
-val constdecl =
-OuterParse.binding --
-(OuterParse.where_ >> K (NONE, NoSyn) ||
-OuterParse.$$$ "::" |-- OuterParse.!!! ((OuterParse.typ >> SOME) --
-OuterParse.opt_mixfix' --| OuterParse.where_) ||
-Scan.ahead (OuterParse.$$$ "(") |--
-OuterParse.!!! (OuterParse.mixfix' --| OuterParse.where_ >> pair NONE))
 *}
 ML {*
 val qd_parser =
 (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) --
-(constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop))
+(SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop))
 *}
 ML {*
-fun pair lthy (ty1, ty2) =
+fun parse_qd_spec (qtystrs, ((bind, tystr, mx), (attr__, propstr))) lthy =
-"(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")"
-*}
-ML {*
-fun parse_qd_spec (qtystrs, ((bind, (typstr__, mx)), (attr__, propstr))) lthy =
 let
 val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystrs
 val qenv = build_qenv lthy qtys
+val qty = Syntax.parse_typ lthy (the tystr) |> Syntax.check_typ lthy
 val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy
 val (lhs, rhs) = Logic.dest_equals prop
 in
 make_const_def bind rhs mx qenv lthy |> snd
 end
 ML {*
 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
 OuterKeyword.thy_decl (qd_parser >> parse_qd_spec)
 *}
+(* ML {* show_all_types := true *} *)
 section {* ATOMIZE *}
 text {*
 Unabs_def converts a definition given as
 if (needs_lift rty T) then
 (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
 else
 Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t
 end
-| Const (@{const_name "op ="}, ty) $ t =>
-if needs_lift rty (fastype_of t) then
-(tyRel (fastype_of t) rty rel lthy) $ t
-else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t)
 | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)
 | _ => trm
 *}
 text {* Assumes that the given theorem is atomized *}
 Logic.mk_implies
 ((prop_of thm),
 (my_reg lthy rel rty (prop_of thm)))
 *}
-lemma universal_twice: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
+ML {*
-apply (auto)
+fun regularize thm rty rel rel_eqv lthy =
-done
-lemma implication_twice: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
-apply (auto)
-done
-ML {*
-fun regularize thm rty rel rel_eqv rel_refl lthy =
 let
 val g = build_regularize_goal thm rty rel lthy;
 fun tac ctxt =
-(ObjectLogic.full_atomize_tac) THEN'
+(asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
-REPEAT_ALL_NEW (FIRST' [
-rtac rel_refl,
-atac,
-rtac @{thm universal_twice},
-rtac @{thm implication_twice},
-(fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
 [(@{thm equiv_res_forall} OF [rel_eqv]),
-(@{thm equiv_res_exists} OF [rel_eqv])]) i)),
+(@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW
-(rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
+(((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN'
-(rtac @{thm RIGHT_RES_FORALL_REGULAR})
+(MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt []));
-]);
 val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);
 in
 cthm OF [thm]
 end
 *}
 Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys)
 | _ => ty
 )
 *}
+ML {* make_const_def *}
 ML {*
 fun old_get_fun flag rty qty lthy ty =
 get_fun flag [(qty, rty)] lthy ty
+*}
+ML {*
 fun old_make_const_def nconst_bname otrm mx rty qty lthy =
 make_const_def nconst_bname otrm mx [(qty, rty)] lthy
 *}
 text {* Does the same as 'subst' in a given prop or theorem *}
 fun lift_thm lthy qty qty_name rsp_thms defs t = let
 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;
 val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name;
 val consts = lookup_quot_consts defs;
 val t_a = atomize_thm t;
-val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
+val t_r = regularize t_a rty rel rel_eqv lthy;
 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
 val abs = findabs rty (prop_of t_a);
 val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs;
 val t_l = repeat_eqsubst_thm lthy simp_lam_prs_thms t_t;
 val t_a = simp_allex_prs lthy quot t_l;

changeset 254	77ff9624cfd6
parent 252	e30997c88050
child 255	264c7b9d19f4