--- a/IntEx.thy Thu Nov 19 14:17:10 2009 +0100
+++ b/IntEx.thy Fri Nov 20 13:03:01 2009 +0100
@@ -22,7 +22,6 @@
ML {* print_qconstinfo @{context} *}
-
term ZERO
thm ZERO_def
@@ -143,19 +142,20 @@
*}
print_quotients
+ML {* quotdata_lookup @{context} "IntEx.my_int" *}
+ML {* quotdata_lookup @{context} "my_int" *}
ML {*
val test = lift_thm_my_int @{context} @{thm plus_sym_pre}
*}
-ML {* my_lift (prop_of test) @{thm plus_sym_pre} @{context} *}
ML {*
- ObjectLogic.atomize_term @{theory} (prop_of test)
- |> Syntax.string_of_term @{context}
- |> writeln
+ val aqtrm = HOLogic.dest_Trueprop (prop_of (atomize_thm test))
+ val artrm = HOLogic.dest_Trueprop (prop_of (atomize_thm @{thm plus_sym_pre}))
*}
+
lemma plus_assoc_pre:
shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
apply (cases i)
--- a/QuotMain.thy Thu Nov 19 14:17:10 2009 +0100
+++ b/QuotMain.thy Fri Nov 20 13:03:01 2009 +0100
@@ -331,7 +331,7 @@
end
| Const (@{const_name "op ="}, ty) $ t =>
if needs_lift rty (fastype_of t) then
- (tyRel (fastype_of t) rty rel lthy) $ t
+ (tyRel (fastype_of t) rty rel lthy) $ t (* FIXME: t should be regularised too *)
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
@@ -1144,19 +1144,112 @@
end
*}
+(******************************************)
+(* version with explicit qtrm *)
+(******************************************)
+
+(* exception for when qtrm and rtrm do not match *)
+ML {* exception LIFT_MATCH of string *}
+
ML {*
-fun my_lift qtrm rthm lthy =
+fun mk_resp_arg lthy (rty, qty) =
let
val thy = ProofContext.theory_of lthy
+in
+ case (rty, qty) of
+ (Type (s, tys), Type (s', tys')) =>
+ if s = s'
+ then let
+ val SOME map_info = maps_lookup thy s
+ val args = map (mk_resp_arg lthy) (tys ~~tys')
+ in
+ list_comb (Const (#relfun map_info, dummyT), args)
+ end
+ else let
+ val SOME qinfo = quotdata_lookup_thy thy s'
+ in
+ #rel qinfo
+ end
+ | _ => HOLogic.eq_const dummyT
+end
+*}
- val a_rthm = atomize_thm rthm
- val a_qtrm = ObjectLogic.atomize_term thy qtrm
+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)
+val mk_resp = Const (@{const_name Respects}, dummyT)
+*}
+
+ML {*
+(* applies f to the subterm of an abstractions, otherwise to the given term *)
+(* abstracted variables do not have to be treated specially *)
+fun apply_subt f trm1 trm2 =
+ case (trm1, trm2) of
+ (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t')
+ | _ => f trm1 trm2
+
+fun qnt_typ ty = domain_type (domain_type ty)
+*}
- val _ = Syntax.string_of_term lthy (prop_of a_rthm) |> writeln
- val _ = Syntax.string_of_term lthy a_qtrm |> writeln
-in
- (a_rthm, a_qtrm)
-end
+ML {*
+fun REGULARIZE_aux lthy rtrm qtrm =
+ case (rtrm, qtrm) of
+ (Abs (x, T, t), Abs (x', T', t')) =>
+ let
+ val subtrm = REGULARIZE_aux lthy t t'
+ in
+ if T = T'
+ then Abs (x, T, subtrm)
+ else mk_babs $ (mk_resp $ mk_resp_arg lthy (T, T')) $ subtrm
+ end
+ | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
+ let
+ val subtrm = apply_subt (REGULARIZE_aux lthy) t t'
+ in
+ if ty = ty'
+ 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_aux lthy) t t'
+ in
+ if ty = ty'
+ 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: why is there a case for equality? is it correct? *)
+ | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>
+ let
+ val subtrm = REGULARIZE_aux lthy t t'
+ in
+ if ty = ty'
+ then Const (@{const_name "op ="}, ty) $ subtrm
+ else mk_resp_arg lthy (ty, ty') $ subtrm
+ end
+ | (t1 $ t2, t1' $ t2') =>
+ (REGULARIZE_aux lthy t1 t1') $ (REGULARIZE_aux lthy t2 t2')
+ | (Free (x, ty), Free (x', ty')) =>
+ if x = x'
+ then rtrm
+ else raise LIFT_MATCH "quotient and lifted theorem do not match"
+ | (Bound i, Bound i') =>
+ if i = i'
+ then rtrm
+ else raise LIFT_MATCH "quotient and lifted theorem do not match"
+ | (Const (s, ty), Const (s', ty')) =>
+ if s = s' andalso ty = ty'
+ then rtrm
+ else rtrm (* FIXME: check correspondence according to definitions *)
+ | _ => raise LIFT_MATCH "quotient and lifted theorem do not match"
+*}
+
+ML {*
+fun REGULARIZE_trm lthy rtrm qtrm =
+ REGULARIZE_aux lthy rtrm qtrm
+ |> Syntax.check_term lthy
+
*}
end
--- a/quotient.ML Thu Nov 19 14:17:10 2009 +0100
+++ b/quotient.ML Fri Nov 20 13:03:01 2009 +0100
@@ -146,10 +146,10 @@
val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
(* storing the quot-info *)
- val qty_str = fst (dest_Type abs_ty)
- val lthy3 = quotdata_update qty_str (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2
+ val qty_str = fst (Term.dest_Type abs_ty)
+ val _ = tracing ("storing under: " ^ qty_str)
+ val lthy3 = quotdata_update qty_str (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2
(* FIXME: varifyT should not be used *)
- (* the type name maybe should be calculated via qty_name and Sign.intern_type *)
(* interpretation *)
val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
--- a/quotient_info.ML Thu Nov 19 14:17:10 2009 +0100
+++ b/quotient_info.ML Fri Nov 20 13:03:01 2009 +0100
@@ -79,7 +79,9 @@
val extend = I
val merge = Symtab.merge (K true))
-val quotdata_lookup_thy = Symtab.lookup o QuotData.get
+fun quotdata_lookup_thy thy str =
+ Symtab.lookup (QuotData.get thy) (Sign.intern_type thy str)
+
val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of
fun quotdata_update_thy qty_name (qty, rty, rel, equiv_thm) =