# HG changeset patch # User Cezary Kaliszyk # Date 1257410314 -3600 # Node ID 8ebdef196fd5113bd62c03aa97ff25c04fad9ba7 # Parent 78bc4d9d7975bfd4a6a921c6db17bf01eff38662 Infrastructure for polymorphic types diff -r 78bc4d9d7975 -r 8ebdef196fd5 FSet.thy --- a/FSet.thy Wed Nov 04 16:10:39 2009 +0100 +++ b/FSet.thy Thu Nov 05 09:38:34 2009 +0100 @@ -317,9 +317,6 @@ ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} (* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *) - - - ML {* lift_thm_fset @{context} @{thm m1} *} ML {* lift_thm_fset @{context} @{thm m2} *} ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} @@ -351,49 +348,59 @@ ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} -ML {* val ind_r_a = atomize_thm @{thm map_append} *} - prove {* build_regularize_goal ind_r_a rty rel @{context} *} - ML_prf {* fun tac ctxt = - (FIRST' [ +ML {* val t_a = atomize_thm @{thm map_append} *} +(* prove {* build_regularize_goal t_a rty rel @{context} *} + ML_prf {* fun tac ctxt = FIRST' [ rtac rel_refl, atac, - rtac @{thm get_rid}, - rtac @{thm get_rid2}, - (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps + rtac @{thm universal_twice}, + (rtac @{thm impI} THEN' atac), + rtac @{thm implication_twice}, + (*rtac @{thm equality_twice},*) + EqSubst.eqsubst_tac ctxt [0] [(@{thm equiv_res_forall} OF [rel_eqv]), - (@{thm equiv_res_exists} OF [rel_eqv])]) i)), + (@{thm equiv_res_exists} OF [rel_eqv])], (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), (rtac @{thm RIGHT_RES_FORALL_REGULAR}) - ]); - *} + ]; *} apply (atomize(full)) - apply (tactic {* tac @{context} 1 *}) *) -ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv rel_refl @{context} *} + apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) + done*) + +ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} ML {* - val rt = build_repabs_term @{context} ind_r_r consts rty qty - val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); + val rt = build_repabs_term @{context} t_r consts rty qty + val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); *} + +ML {* val ttt = snd (dest_Free (term_of @{cpat "f :: ?'a list \ ?'a list"})) *} +ML {* old_get_fun repF @{typ "'a list"} @{typ "'a fset"} @{context} @{typ "'a list \ 'a list"} *} + prove rg apply(atomize(full)) ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) done -ML {* val ind_r_t = +ML {* val t_t = Toplevel.program (fn () => - repabs @{context} ind_r_r consts rty qty quot rel_refl trans2 rsp_thms + repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms ) *} ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} -ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} -ML {* val ind_r_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) ind_r_t *} -ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]]} *} -ML {* val ind_r_a = simp_allex_prs quot [thm] ind_r_l *} +ML {* val lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} +ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} +ML {* val app_prs_thms = map Thm.freezeT app_prs_thms *} +ML {* val t_l = repeat_eqsubst_thm @{context} (app_prs_thms @ lam_prs_thms) t_t *} +ML {* val (alls, exs) = findallex rty qty (prop_of t_a); *} +ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} +ML {* val allthmsv = map Thm.varifyT allthms *} +ML {* val t_a = MetaSimplifier.rewrite_rule (allthmsv) t_l *} ML {* val defs_sym = add_lower_defs @{context} defs *} -ML {* val ind_r_d = repeat_eqsubst_thm @{context} defs_sym ind_r_a *} -ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} -ML {* ObjectLogic.rulify ind_r_s *} +ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a *} +ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_d *} +ML {* ObjectLogic.rulify t_s *} ML {* fun lift_thm_fset_note name thm lthy = diff -r 78bc4d9d7975 -r 8ebdef196fd5 LamEx.thy --- a/LamEx.thy Wed Nov 04 16:10:39 2009 +0100 +++ b/LamEx.thy Thu Nov 05 09:38:34 2009 +0100 @@ -165,6 +165,12 @@ lemma rfv_rsp: "(alpha ===> op =) rfv rfv" sorry +lemma rvar_inject: "rVar a \ rVar b = (a = b)" +apply (auto) +apply (erule alpha.cases) +apply (simp_all add: rlam.inject alpha_refl) +done + ML {* val qty = @{typ "lam"} *} ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *} ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @ @@ -187,6 +193,8 @@ ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *} ML {* val alpha_induct = lift_thm_lam @{context} @{thm alpha.induct} *} +ML {* val var_inject = lift_thm_lam @{context} @{thm rvar_inject} *} + local_setup {* Quotient.note (@{binding "pi_var"}, pi_var) #> snd #> Quotient.note (@{binding "pi_app"}, pi_app) #> snd #> @@ -195,7 +203,8 @@ Quotient.note (@{binding "a2"}, a2) #> snd #> Quotient.note (@{binding "a3"}, a3) #> snd #> Quotient.note (@{binding "alpha_cases"}, alpha_cases) #> snd #> - Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd + Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd #> + Quotient.note (@{binding "var_inject"}, var_inject) #> snd *} thm alpha.cases @@ -203,18 +212,6 @@ thm alpha.induct thm alpha_induct -lemma rvar_inject: "rVar a \ rVar b = (a = b)" -apply (auto) -apply (erule alpha.cases) -apply (simp_all add: rlam.inject alpha_refl) -done - -ML {* val var_inject = Toplevel.program (fn () => lift_thm_lam @{context} @{thm rvar_inject}) *} - -local_setup {* - Quotient.note (@{binding "var_inject"}, var_inject) #> snd -*} - lemma var_supp: shows "supp (Var a) = ((supp a)::name set)" apply(simp add: supp_def) diff -r 78bc4d9d7975 -r 8ebdef196fd5 QuotMain.thy --- a/QuotMain.thy Wed Nov 04 16:10:39 2009 +0100 +++ b/QuotMain.thy Thu Nov 05 09:38:34 2009 +0100 @@ -376,7 +376,7 @@ fun my_reg_inst lthy rel rty trm = case rel of Const (n, _) => Syntax.check_term lthy - (my_reg lthy (Const (n, dummyT)) rty trm) + (my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm) *} (*ML {* @@ -448,14 +448,127 @@ ) *} +(* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \ bool) to (int 'b quo \ bool) *) +ML {* fun exchange_ty rty (qty as (Type (qtys, _))) ty = + let val (s, tys) = dest_Type ty in + if Type.raw_instance (Logic.varifyT ty, rty) + then Type (qtys, tys) + else Type (s, map (exchange_ty rty qty) tys) + end + handle _ => ty +*} + +ML {* +fun negF absF = repF + | negF repF = absF + +fun get_fun_noexchange flag (rty, qty) lthy ty = +let + fun get_fun_aux s fs_tys = + let + val (fs, tys) = split_list fs_tys + val (otys, ntys) = split_list tys + val oty = Type (s, otys) + val nty = Type (s, ntys) + val ftys = map (op -->) tys + in + (case (maps_lookup (ProofContext.theory_of lthy) s) of + SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty)) + | NONE => error ("no map association for type " ^ s)) + end + + fun get_fun_fun fs_tys = + let + val (fs, tys) = split_list fs_tys + val ([oty1, oty2], [nty1, nty2]) = split_list tys + val oty = nty1 --> oty2 + val nty = oty1 --> nty2 + val ftys = map (op -->) tys + in + (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty)) + end + + fun get_const flag (rty, qty) = + let + val thy = ProofContext.theory_of lthy + val qty_name = Long_Name.base_name (fst (dest_Type qty)) + in + case flag of + absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty)) + | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty)) + end + + fun mk_identity ty = Abs ("", ty, Bound 0) + +in + if (Type.raw_instance (Logic.varifyT ty, rty)) + then (get_const flag (ty, (exchange_ty rty qty ty))) + else (case ty of + TFree _ => (mk_identity ty, (ty, ty)) + | Type (_, []) => (mk_identity ty, (ty, ty)) + | Type ("fun" , [ty1, ty2]) => + get_fun_fun [get_fun_noexchange (negF flag) (rty,qty) lthy ty1, get_fun_noexchange flag (rty,qty) lthy ty2] + | Type (s, tys) => get_fun_aux s (map (get_fun_noexchange flag (rty, qty) lthy) tys) + | _ => raise ERROR ("no type variables")) +end +*} ML {* fun old_get_fun flag rty qty lthy ty = - get_fun flag [(qty, rty)] lthy ty + get_fun_noexchange flag (rty, qty) lthy ty +*} + +ML {* +fun find_matching_types rty ty = + let val (s, tys) = dest_Type ty in + if Type.raw_instance (Logic.varifyT ty, rty) + then [ty] + else flat (map (find_matching_types rty) tys) + end +*} + +ML {* +fun get_fun_new flag rty qty lthy ty = + let + val tys = find_matching_types rty ty; + val qenv = map (fn t => (exchange_ty rty qty t, t)) tys; + val xchg_ty = exchange_ty rty qty ty + in + get_fun flag qenv lthy xchg_ty + end +*} + +(* +consts Rl :: "'a list \ 'a list \ bool" +axioms Rl_eq: "EQUIV Rl" -fun old_make_const_def nconst_bname otrm mx rty qty lthy = - make_def nconst_bname otrm qty mx Attrib.empty_binding [(qty, rty)] lthy +quotient ql = "'a list" / "Rl" + by (rule Rl_eq) + +ML {* val al = snd (dest_Free (term_of @{cpat "f :: ?'a list"})) *} +ML {* val aq = snd (dest_Free (term_of @{cpat "f :: ?'a ql"})) *} +ML {* val ttt = term_of @{cterm "f :: bool list \ nat list"} *} + +ML {* + fst (get_fun_noexchange absF (al, aq) @{context} (fastype_of ttt)) +*} +ML {* + fst (get_fun_new absF al aq @{context} (fastype_of ttt)) *} +ML {* + fun mk_abs tm = + let + val ty = fastype_of tm + in fst (get_fun_noexchange absF (al, aq) @{context} ty) $ tm end + fun mk_repabs tm = + let + val ty = fastype_of tm + in fst (get_fun_noexchange repF (al, aq) @{context} ty) $ (mk_abs tm) end +*} +ML {* + cterm_of @{theory} (mk_repabs ttt) +*} +*) text {* Does the same as 'subst' in a given prop or theorem *} ML {* @@ -499,15 +612,17 @@ ML {* fun build_repabs_term lthy thm constructors rty qty = let - fun mk_rep tm = - let - val ty = old_exchange_ty rty qty (fastype_of tm) - in fst (old_get_fun repF rty qty lthy ty) $ tm end + val rty = Logic.varifyT rty; + val qty = Logic.varifyT qty; - fun mk_abs tm = - let - val ty = old_exchange_ty rty qty (fastype_of tm) in - fst (old_get_fun absF rty qty lthy ty) $ tm end + fun mk_abs tm = + let + val ty = fastype_of tm + in fst (get_fun_noexchange absF (rty, qty) lthy ty) $ tm end + fun mk_repabs tm = + let + val ty = fastype_of tm + in fst (get_fun_noexchange repF (rty, qty) lthy ty) $ (mk_abs tm) end fun is_constructor (Const (x, _)) = member (op =) constructors x | is_constructor _ = false; @@ -521,16 +636,16 @@ val t' = lambda v (build_aux lthy t) in if (not (needs_lift rty (fastype_of tm))) then t' - else mk_rep (mk_abs ( + else mk_repabs ( if not (needs_lift rty vty) then t' else let - val v' = mk_rep (mk_abs v); + val v' = mk_repabs v; val t1 = Envir.beta_norm (t' $ v') in lambda v t1 end - )) + ) end | x => let @@ -541,9 +656,9 @@ if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false) then (list_comb (opp, (hd tms0) :: (tl tms))) else if (is_constructor opp andalso needs_lift rty ty) then - mk_rep (mk_abs (list_comb (opp,tms))) + mk_repabs (list_comb (opp,tms)) else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then - mk_rep(mk_abs(list_comb(opp,tms))) + mk_repabs(list_comb(opp,tms)) else if tms = [] then opp else list_comb(opp, tms) end @@ -824,16 +939,18 @@ ML {* fun applic_prs lthy rty qty absrep ty = let + val rty = Logic.varifyT rty; + val qty = Logic.varifyT qty; fun absty ty = - old_exchange_ty rty qty ty + exchange_ty rty qty ty fun mk_rep tm = let - val ty = old_exchange_ty rty qty (fastype_of tm) - in fst (old_get_fun repF rty qty lthy ty) $ tm end; + val ty = exchange_ty qty rty (fastype_of tm) + in fst (get_fun_noexchange repF (rty, qty) lthy ty) $ tm end; fun mk_abs tm = - let - val ty = old_exchange_ty rty qty (fastype_of tm) in - fst (old_get_fun absF rty qty lthy ty) $ tm end; + let + val ty = fastype_of tm + in fst (get_fun_noexchange absF (rty, qty) lthy ty) $ tm end val (l, ltl) = Term.strip_type ty; val nl = map absty l; val vs = map (fn _ => "x") l; diff -r 78bc4d9d7975 -r 8ebdef196fd5 QuotTest.thy --- a/QuotTest.thy Wed Nov 04 16:10:39 2009 +0100 +++ b/QuotTest.thy Thu Nov 05 09:38:34 2009 +0100 @@ -120,25 +120,18 @@ ML {* val al = snd (dest_Free (term_of @{cpat "f :: ?'a list"})) *} ML {* val aq = snd (dest_Free (term_of @{cpat "f :: ?'a ql"})) *} -ML {* val ttt = snd (dest_Free (term_of @{cpat "f :: ?'a list \ ?'a list"})) *} +ML {* val ttt = snd (dest_Free (term_of @{cpat "f :: ?'a ql \ ?'a ql"})) *} ML {* - get_fun absF [(al, aq)] @{context} ttt - |> fst - |> Syntax.pretty_term @{context} - |> Pretty.string_of - |> writeln + fst (get_fun absF [(aq, al)] @{context} ttt) + |> cterm_of @{theory} *} - -ML {* val ttt2 = snd (dest_Free (term_of @{cpat "f :: nat list \ nat list"})) *} +ML {* val ttt2 = snd (dest_Free (term_of @{cpat "f :: nat ql \ bool ql \ 'a ql"})) *} ML {* - get_fun absF [(al, aq)] @{context} ttt2 - |> fst - |> Syntax.pretty_term @{context} - |> Pretty.string_of - |> writeln + fst (get_fun absF [(aq, al), (@{typ "nat ql"}, @{typ "nat list"}), (@{typ "bool ql"}, @{typ "bool list"})] @{context} ttt2) + |> cterm_of @{theory} *} quotient_def (for qt)