# HG changeset patch # User Christian Urban # Date 1259959409 -3600 # Node ID 51a1d1aba9fd93b8e2b93512920e6b1dc824387e # Parent f178958d3d816a671030c031e89cf8cb02a03cca# Parent 9fb773ec083c0dbf16f14df0ea46112d8bacbee6 merged diff -r 9fb773ec083c -r 51a1d1aba9fd FSet.thy --- a/FSet.thy Fri Dec 04 19:47:58 2009 +0100 +++ b/FSet.thy Fri Dec 04 21:43:29 2009 +0100 @@ -286,6 +286,10 @@ apply (auto simp add: memb_rsp rsp_fold_def) done +lemma list_equiv_rsp[quotient_rsp]: + shows "(op \ ===> op \ ===> op =) op \ op \" +by (auto intro: list_eq.intros) + print_quotients ML {* val qty = @{typ "'a fset"} *} @@ -342,54 +346,9 @@ apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) -prefer 2 +defer apply(tactic {* clean_tac @{context} 1 *}) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* D *) (* reflexivity of basic relations *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* C *) (* = and extensionality *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) -apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) +apply(tactic {* inj_repabs_tac_fset @{context} 1*})+ done lemma list_induct_part: diff -r 9fb773ec083c -r 51a1d1aba9fd IntEx.thy --- a/IntEx.thy Fri Dec 04 19:47:58 2009 +0100 +++ b/IntEx.thy Fri Dec 04 21:43:29 2009 +0100 @@ -130,6 +130,10 @@ apply(auto) done +lemma list_equiv_rsp[quotient_rsp]: + shows "(op \ ===> op \ ===> op =) op \ op \" +by auto + lemma ho_plus_rsp[quotient_rsp]: shows "(intrel ===> intrel ===> intrel) my_plus my_plus" by (simp) @@ -149,8 +153,9 @@ lemma "PLUS a b = PLUS b a" apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) -prefer 2 -apply(tactic {* clean_tac @{context} 1 *}) +apply(tactic {* inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* inj_repabs_tac_intex @{context} 1*}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) @@ -174,6 +179,7 @@ apply(tactic {* inj_repabs_tac_intex @{context} 1*}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* clean_tac @{context} 1 *}) done lemma plus_assoc_pre: @@ -195,11 +201,6 @@ apply simp done - - - - - (* I believe it's true. *) lemma foldl_rsp[quotient_rsp]: "((op \ ===> op \ ===> op \) ===> op \ ===> list_rel op \ ===> op \) foldl foldl" @@ -222,10 +223,12 @@ apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) apply(rule nil_rsp) apply(tactic {* quotient_tac @{context} 1*}) +apply(simp only: fun_map.simps id_simps) +apply(simp only: Quotient_abs_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]]) +apply(simp only: Quotient_abs_rep[OF list_quotient[OF Quotient_my_int]]) apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int]) -apply(simp only: nil_prs[OF Quotient_my_int]) apply(tactic {* clean_tac @{context} 1 *}) -done +sorry lemma ho_tst2: "foldl my_plus x (h # t) \ my_plus h (foldl my_plus x t)" sorry @@ -236,6 +239,9 @@ apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) apply(rule cons_rsp) apply(tactic {* quotient_tac @{context} 1 *}) +apply(simp only: fun_map.simps id_simps) +apply(simp only: Quotient_abs_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]]) +apply(simp only: Quotient_abs_rep[OF list_quotient[OF Quotient_my_int]]) apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int]) apply(simp only: cons_prs[OF Quotient_my_int]) apply(tactic {* clean_tac @{context} 1 *}) diff -r 9fb773ec083c -r 51a1d1aba9fd Prove.thy --- a/Prove.thy Fri Dec 04 19:47:58 2009 +0100 +++ b/Prove.thy Fri Dec 04 21:43:29 2009 +0100 @@ -1,5 +1,5 @@ theory Prove -imports Main +imports Plain begin ML {* diff -r 9fb773ec083c -r 51a1d1aba9fd QuotMain.thy --- a/QuotMain.thy Fri Dec 04 19:47:58 2009 +0100 +++ b/QuotMain.thy Fri Dec 04 21:43:29 2009 +0100 @@ -351,6 +351,30 @@ *} ML {* +fun matches_typ (ty, ty') = + case (ty, ty') of + (_, TVar _) => true + | (TFree x, TFree x') => x = x' + | (Type (s, tys), Type (s', tys')) => + 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') + | (Bound i, Bound j) => i = j + | (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 +*} + +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) @@ -388,6 +412,7 @@ then Abs (x, ty, subtrm) else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm end + | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => let val subtrm = apply_subt (regularize_trm lthy) t t' @@ -396,6 +421,7 @@ 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' @@ -404,30 +430,59 @@ 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' + + | (* equalities need to be replaced by appropriate equivalence relations *) + (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => + if ty = ty' + then rtrm + else mk_resp_arg lthy (domain_type ty, domain_type ty') + + | (* in this case we check whether the given equivalence relation is correct *) + (rel, Const (@{const_name "op ="}, ty')) => + let + val exc = LIFT_MATCH "regularise (relation mismatch)" + val rel_ty = (fastype_of rel) handle TERM _ => raise exc + val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') + in + if rel' = rel + then rtrm + else raise exc + end + | (_, Const (s, _)) => + let + fun same_name (Const (s, _)) (Const (s', _)) = (s = s') + | same_name _ _ = false in - if ty = ty' - then Const (@{const_name "op ="}, ty) $ subtrm - else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm + if same_name rtrm qtrm + then rtrm + else + let + fun exc1 s = LIFT_MATCH ("regularize (constant " ^ s ^ " not found)") + val exc2 = LIFT_MATCH ("regularize (constant mismatch)") + val thy = ProofContext.theory_of lthy + val rtrm' = (#rconst (qconsts_lookup thy s)) handle NotFound => raise (exc1 s) + in + if matches_term (rtrm, rtrm') + then rtrm + else raise exc2 + end 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) => + else raise (LIFT_MATCH "regularize (bounds mismatch)") + + + + | (rt, qt) => raise (LIFT_MATCH "regularize (default)") *} @@ -690,10 +745,10 @@ val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) in case (rhead, qhead) of - (Const _, Const _) => - if rty = qty + (Const (s, T), Const (s', T')) => + if T = T' then list_comb (rhead, rargs') - else mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) + else list_comb (mk_repabs lthy (T, T') rhead, rargs') | (Free (x, T), Free (x', T')) => if T = T' then list_comb (rhead, rargs') diff -r 9fb773ec083c -r 51a1d1aba9fd quotient_def.ML --- a/quotient_def.ML Fri Dec 04 19:47:58 2009 +0100 +++ b/quotient_def.ML Fri Dec 04 21:43:29 2009 +0100 @@ -96,10 +96,14 @@ val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy - val qconst_str = Binding.name_of qconst_bname fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm} val lthy'' = Local_Theory.declaration true - (fn phi => qconsts_update_gen qconst_str (qcinfo phi)) lthy' + (fn phi => + let + val qconst_str = fst (Term.dest_Const (Morphism.term phi trm)) + in + qconsts_update_gen qconst_str (qcinfo phi) + end) lthy' in ((trm, thm), lthy'') end diff -r 9fb773ec083c -r 51a1d1aba9fd quotient_info.ML --- a/quotient_info.ML Fri Dec 04 19:47:58 2009 +0100 +++ b/quotient_info.ML Fri Dec 04 21:43:29 2009 +0100 @@ -1,5 +1,7 @@ signature QUOTIENT_INFO = sig + exception NotFound + type maps_info = {mapfun: string, relfun: string} val maps_lookup: theory -> string -> maps_info option val maps_update_thy: string -> maps_info -> theory -> theory @@ -15,7 +17,7 @@ type qconsts_info = {qconst: term, rconst: term, def: thm} val qconsts_transfer: morphism -> qconsts_info -> qconsts_info - val qconsts_lookup: theory -> string -> qconsts_info option + val qconsts_lookup: theory -> string -> qconsts_info val qconsts_update_thy: string -> qconsts_info -> theory -> theory val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic val qconsts_dest: theory -> qconsts_info list @@ -29,6 +31,7 @@ structure Quotient_Info: QUOTIENT_INFO = struct +exception NotFound (* data containers *) (*******************) @@ -134,7 +137,10 @@ rconst = Morphism.term phi rconst, def = Morphism.thm phi def} -val qconsts_lookup = Symtab.lookup o QConstsData.get +fun qconsts_lookup thy str = + case Symtab.lookup (QConstsData.get thy) str of + SOME info => info + | NONE => raise NotFound fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I