--- a/FSet.thy Fri Dec 04 18:32:19 2009 +0100
+++ b/FSet.thy Fri Dec 04 21:42:55 2009 +0100
@@ -286,6 +286,10 @@
apply (auto simp add: memb_rsp rsp_fold_def)
done
+lemma list_equiv_rsp[quotient_rsp]:
+ shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
+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:
--- a/IntEx.thy Fri Dec 04 18:32:19 2009 +0100
+++ b/IntEx.thy Fri Dec 04 21:42:55 2009 +0100
@@ -130,6 +130,10 @@
apply(auto)
done
+lemma list_equiv_rsp[quotient_rsp]:
+ shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
+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 \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> list_rel op \<approx> ===> op \<approx>) 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) \<approx> 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 *})
--- a/Prove.thy Fri Dec 04 18:32:19 2009 +0100
+++ b/Prove.thy Fri Dec 04 21:42:55 2009 +0100
@@ -1,5 +1,5 @@
theory Prove
-imports Main
+imports Plain
begin
ML {*
--- a/QuotMain.thy Fri Dec 04 18:32:19 2009 +0100
+++ b/QuotMain.thy Fri Dec 04 21:42:55 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')
--- a/quotient_def.ML Fri Dec 04 18:32:19 2009 +0100
+++ b/quotient_def.ML Fri Dec 04 21:42:55 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
--- a/quotient_info.ML Fri Dec 04 18:32:19 2009 +0100
+++ b/quotient_info.ML Fri Dec 04 21:42:55 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