--- a/QuotMain.thy Wed Oct 21 11:50:53 2009 +0200
+++ b/QuotMain.thy Wed Oct 21 13:47:39 2009 +0200
@@ -411,6 +411,368 @@
term VR'
term AP'
+section {* ATOMIZE *}
+
+text {*
+ Unabs_def converts a definition given as
+
+ c \<equiv> %x. %y. f x y
+
+ to a theorem of the form
+
+ c x y \<equiv> f x y
+
+ This function is needed to rewrite the right-hand
+ side to the left-hand side.
+*}
+
+ML {*
+fun unabs_def ctxt def =
+let
+ val (lhs, rhs) = Thm.dest_equals (cprop_of def)
+ val xs = strip_abs_vars (term_of rhs)
+ val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
+
+ val thy = ProofContext.theory_of ctxt'
+ val cxs = map (cterm_of thy o Free) xs
+ val new_lhs = Drule.list_comb (lhs, cxs)
+
+ fun get_conv [] = Conv.rewr_conv def
+ | get_conv (x::xs) = Conv.fun_conv (get_conv xs)
+in
+ get_conv xs new_lhs |>
+ singleton (ProofContext.export ctxt' ctxt)
+end
+*}
+
+lemma atomize_eqv[atomize]:
+ shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
+proof
+ assume "A \<equiv> B"
+ then show "Trueprop A \<equiv> Trueprop B" by unfold
+next
+ assume *: "Trueprop A \<equiv> Trueprop B"
+ have "A = B"
+ proof (cases A)
+ case True
+ have "A" by fact
+ then show "A = B" using * by simp
+ next
+ case False
+ have "\<not>A" by fact
+ then show "A = B" using * by auto
+ qed
+ then show "A \<equiv> B" by (rule eq_reflection)
+qed
+
+ML {*
+fun atomize_thm thm =
+let
+ val thm' = forall_intr_vars thm
+ val thm'' = ObjectLogic.atomize (cprop_of thm')
+in
+ Simplifier.rewrite_rule [thm''] thm'
+end
+*}
+
+
+section {* REGULARIZE *}
+
+text {* tyRel takes a type and builds a relation that a quantifier over this
+ type needs to respect. *}
+ML {*
+fun tyRel ty rty rel lthy =
+ if ty = rty
+ then rel
+ else (case ty of
+ Type (s, tys) =>
+ let
+ val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
+ val ty_out = ty --> ty --> @{typ bool};
+ val tys_out = tys_rel ---> ty_out;
+ in
+ (case (maps_lookup (ProofContext.theory_of lthy) s) of
+ SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
+ | NONE => HOLogic.eq_const ty
+ )
+ end
+ | _ => HOLogic.eq_const ty)
+*}
+
+ML {*
+ cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context})
+*}
+
+definition
+ Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+where
+ "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
+(* TODO: Consider defining it with an "if"; sth like:
+ Babs p m = \<lambda>x. if x \<in> p then m x else undefined
+*)
+
+ML {*
+fun needs_lift (rty as Type (rty_s, _)) ty =
+ case ty of
+ Type (s, tys) =>
+ (s = rty_s) orelse (exists (needs_lift rty) tys)
+ | _ => false
+
+*}
+
+ML {*
+(* trm \<Rightarrow> new_trm *)
+fun regularise trm rty rel lthy =
+ case trm of
+ Abs (x, T, t) =>
+ if (needs_lift rty T) then let
+ val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
+ val v = Free (x', T);
+ val t' = subst_bound (v, t);
+ val rec_term = regularise t' rty rel lthy2;
+ val lam_term = Term.lambda_name (x, v) rec_term;
+ val sub_res_term = tyRel T rty rel lthy;
+ val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
+ val res_term = respects $ sub_res_term;
+ val ty = fastype_of trm;
+ val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty);
+ val rabs_term = (rabs $ res_term) $ lam_term;
+ in
+ rabs_term
+ end else let
+ val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
+ val v = Free (x', T);
+ val t' = subst_bound (v, t);
+ val rec_term = regularise t' rty rel lthy2;
+ in
+ Term.lambda_name (x, v) rec_term
+ end
+ | ((Const (@{const_name "All"}, at)) $ (Abs (x, T, t))) =>
+ if (needs_lift rty T) then let
+ val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
+ val v = Free (x', T);
+ val t' = subst_bound (v, t);
+ val rec_term = regularise t' rty rel lthy2;
+ val lam_term = Term.lambda_name (x, v) rec_term;
+ val sub_res_term = tyRel T rty rel lthy;
+ val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
+ val res_term = respects $ sub_res_term;
+ val ty = fastype_of lam_term;
+ val rall = Const (@{const_name Ball}, (fastype_of res_term) --> ty --> @{typ bool});
+ val rall_term = (rall $ res_term) $ lam_term;
+ in
+ rall_term
+ end else let
+ val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
+ val v = Free (x', T);
+ val t' = subst_bound (v, t);
+ val rec_term = regularise t' rty rel lthy2;
+ val lam_term = Term.lambda_name (x, v) rec_term
+ in
+ Const(@{const_name "All"}, at) $ lam_term
+ end
+ | ((Const (@{const_name "All"}, at)) $ P) =>
+ let
+ val (_, [al, _]) = dest_Type (fastype_of P);
+ val ([x], lthy2) = Variable.variant_fixes [""] lthy;
+ val v = (Free (x, al));
+ val abs = Term.lambda_name (x, v) (P $ v);
+ in regularise ((Const (@{const_name "All"}, at)) $ abs) rty rel lthy2 end
+ | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) =>
+ if (needs_lift rty T) then let
+ val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
+ val v = Free (x', T);
+ val t' = subst_bound (v, t);
+ val rec_term = regularise t' rty rel lthy2;
+ val lam_term = Term.lambda_name (x, v) rec_term;
+ val sub_res_term = tyRel T rty rel lthy;
+ val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
+ val res_term = respects $ sub_res_term;
+ val ty = fastype_of lam_term;
+ val rall = Const (@{const_name Bex}, (fastype_of res_term) --> ty --> @{typ bool});
+ val rall_term = (rall $ res_term) $ lam_term;
+ in
+ rall_term
+ end else let
+ val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
+ val v = Free (x', T);
+ val t' = subst_bound (v, t);
+ val rec_term = regularise t' rty rel lthy2;
+ val lam_term = Term.lambda_name (x, v) rec_term
+ in
+ Const(@{const_name "Ex"}, at) $ lam_term
+ end
+ | ((Const (@{const_name "Ex"}, at)) $ P) =>
+ let
+ val (_, [al, _]) = dest_Type (fastype_of P);
+ val ([x], lthy2) = Variable.variant_fixes [""] lthy;
+ val v = (Free (x, al));
+ val abs = Term.lambda_name (x, v) (P $ v);
+ in regularise ((Const (@{const_name "Ex"}, at)) $ abs) rty rel lthy2 end
+ | a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy)
+ | _ => trm
+
+*}
+
+ML {*
+ cterm_of @{theory} (regularise @{term "\<lambda>x :: int. x"} @{typ "trm"} @{term "RR"} @{context});
+ cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
+ cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+ cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+ cterm_of @{theory} (regularise @{term "All (P :: trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
+*}
+
+(* my version of regularise *)
+(****************************)
+
+(* some helper functions *)
+
+
+ML {*
+fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)
+fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
+fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
+fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})
+*}
+
+(* applies f to the subterm of an abstractions, otherwise to the given term *)
+ML {*
+fun apply_subt f trm =
+ case trm of
+ Abs (x, T, t) => Abs (x, T, f t)
+ | _ => f trm
+*}
+
+
+(* FIXME: assumes always the typ is qty! *)
+(* FIXME: if there are more than one quotient, then you have to look up the relation *)
+ML {*
+fun my_reg rel trm =
+ case trm of
+ Abs (x, T, t) =>
+ let
+ val ty1 = fastype_of trm
+ in
+ (mk_babs ty1 T) $ (mk_resp T $ rel) $ (Abs (x, T, my_reg rel t))
+ end
+ | Const (@{const_name "All"}, ty) $ t =>
+ let
+ val ty1 = domain_type ty
+ val ty2 = domain_type ty1
+ in
+ (mk_ball ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)
+ end
+ | Const (@{const_name "Ex"}, ty) $ t =>
+ let
+ val ty1 = domain_type ty
+ val ty2 = domain_type ty1
+ in
+ (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)
+ end
+ | t1 $ t2 => (my_reg rel t1) $ (my_reg rel t2)
+ | _ => trm
+*}
+
+ML {*
+ cterm_of @{theory} (regularise @{term "\<lambda>x::trm. x"} @{typ "trm"} @{term "RR"} @{context});
+ cterm_of @{theory} (my_reg @{term "RR"} @{term "\<lambda>x::trm. x"})
+*}
+
+ML {*
+ cterm_of @{theory} (regularise @{term "\<forall>(x::trm) (y::trm). P x y"} @{typ "trm"} @{term "RR"} @{context});
+ cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>(x::trm) (y::trm). P x y"})
+*}
+
+ML {*
+ cterm_of @{theory} (regularise @{term "\<forall>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+ cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>x::trm. P x"})
+*}
+
+ML {*
+ cterm_of @{theory} (regularise @{term "\<exists>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+ cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>x::trm. P x"})
+*}
+
+(* my version is not eta-expanded, but that should be OK *)
+ML {*
+ cterm_of @{theory} (regularise @{term "All (P::trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
+ cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm \<Rightarrow> bool)"})
+*}
+
+(*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
+ trm == new_trm
+*)
+
+section {* TRANSCONV *}
+
+
+ML {*
+fun build_goal_term lthy thm constructors rty qty =
+ let
+ fun mk_rep tm =
+ let
+ val ty = exchange_ty rty qty (fastype_of tm)
+ in fst (get_fun repF rty qty lthy ty) $ tm end
+
+ fun mk_abs tm =
+ let
+ val _ = tracing (Syntax.string_of_term @{context} tm)
+ val _ = tracing (Syntax.string_of_typ @{context} (fastype_of tm))
+ val ty = exchange_ty rty qty (fastype_of tm) in
+ fst (get_fun absF rty qty lthy ty) $ tm end
+
+ fun is_constructor (Const (x, _)) = member (op =) constructors x
+ | is_constructor _ = false;
+
+ fun build_aux lthy tm =
+ case tm of
+ Abs (a as (_, vty, _)) =>
+ let
+ val (vs, t) = Term.dest_abs a;
+ val v = Free(vs, vty);
+ val t' = lambda v (build_aux lthy t)
+ in
+ if (not (needs_lift rty (fastype_of tm))) then t'
+ else mk_rep (mk_abs (
+ if not (needs_lift rty vty) then t'
+ else
+ let
+ val v' = mk_rep (mk_abs v);
+ val t1 = Envir.beta_norm (t' $ v')
+ in
+ lambda v t1
+ end
+ ))
+ end
+ | x =>
+ let
+ val _ = tracing (">>" ^ Syntax.string_of_term @{context} tm)
+ val (opp, tms0) = Term.strip_comb tm
+ val tms = map (build_aux lthy) tms0
+ val ty = fastype_of tm
+ in
+ 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)))
+ else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
+ mk_rep(mk_abs(list_comb(opp,tms)))
+ else if tms = [] then opp
+ else list_comb(opp, tms)
+ end
+ in
+ build_aux lthy (Thm.prop_of thm)
+ end
+*}
+
+ML {*
+fun build_goal ctxt thm cons rty qty =
+ Logic.mk_equals ((Thm.prop_of thm), (build_goal_term ctxt thm cons rty qty))
+*}
+
+
+
+
text {* finite set example *}
print_syntax
@@ -685,138 +1047,10 @@
ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *}
ML {* val fall = Const(@{const_name all}, dummyT) *}
-ML {*
-fun needs_lift (rty as Type (rty_s, _)) ty =
- case ty of
- Type (s, tys) =>
- (s = rty_s) orelse (exists (needs_lift rty) tys)
- | _ => false
-
-*}
-
-ML {*
-fun build_goal_term lthy thm constructors rty qty =
- let
- fun mk_rep tm =
- let
- val ty = exchange_ty rty qty (fastype_of tm)
- in fst (get_fun repF rty qty lthy ty) $ tm end
-
- fun mk_abs tm =
- let
- val _ = tracing (Syntax.string_of_term @{context} tm)
- val _ = tracing (Syntax.string_of_typ @{context} (fastype_of tm))
- val ty = exchange_ty rty qty (fastype_of tm) in
- fst (get_fun absF rty qty lthy ty) $ tm end
-
- fun is_constructor (Const (x, _)) = member (op =) constructors x
- | is_constructor _ = false;
+ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
+ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}
- fun build_aux lthy tm =
- case tm of
- Abs (a as (_, vty, _)) =>
- let
- val (vs, t) = Term.dest_abs a;
- val v = Free(vs, vty);
- val t' = lambda v (build_aux lthy t)
- in
- if (not (needs_lift rty (fastype_of tm))) then t'
- else mk_rep (mk_abs (
- if not (needs_lift rty vty) then t'
- else
- let
- val v' = mk_rep (mk_abs v);
- val t1 = Envir.beta_norm (t' $ v')
- in
- lambda v t1
- end
- ))
- end
- | x =>
- let
- val _ = tracing (">>" ^ Syntax.string_of_term @{context} tm)
- val (opp, tms0) = Term.strip_comb tm
- val tms = map (build_aux lthy) tms0
- val ty = fastype_of tm
- in
- 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)))
- else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
- mk_rep(mk_abs(list_comb(opp,tms)))
- else if tms = [] then opp
- else list_comb(opp, tms)
- end
- in
- build_aux lthy (Thm.prop_of thm)
- end
-*}
-
-ML {*
-fun build_goal_term_old ctxt thm constructors rty qty mk_rep mk_abs =
- let
- fun mk_rep_abs x = mk_rep (mk_abs x);
-
- fun is_constructor (Const (x, _)) = member (op =) constructors x
- | is_constructor _ = false;
-
- fun maybe_mk_rep_abs t =
- let
- val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t)
- in
- if fastype_of t = rty then mk_rep_abs t else t
- end;
-
- fun is_all (Const ("all", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty
- | is_all _ = false;
-
- fun is_ex (Const ("Ex", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty
- | is_ex _ = false;
-
- fun build_aux ctxt1 tm =
- let
- val (head, args) = Term.strip_comb tm;
- val args' = map (build_aux ctxt1) args;
- in
- (case head of
- Abs (x, T, t) =>
- if T = rty then let
- val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;
- val v = Free (x', qty);
- val t' = subst_bound (mk_rep v, t);
- val rec_term = build_aux ctxt2 t';
- val _ = tracing (Syntax.string_of_term ctxt2 t')
- val _ = tracing (Syntax.string_of_term ctxt2 (Term.lambda_name (x, v) rec_term))
- in
- Term.lambda_name (x, v) rec_term
- end else let
- val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;
- val v = Free (x', T);
- val t' = subst_bound (v, t);
- val rec_term = build_aux ctxt2 t';
- in Term.lambda_name (x, v) rec_term end
- | _ => (* I assume that we never lift 'prop' since it is not of sort type *)
- if is_all head then
- list_comb (Const(@{const_name all}, dummyT), args') |> Syntax.check_term ctxt1
- else if is_ex head then
- list_comb (Const(@{const_name Ex}, dummyT), args') |> Syntax.check_term ctxt1
- else if is_constructor head then
- maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args'))
- else
- maybe_mk_rep_abs (list_comb (head, args'))
- )
- end;
- in
- build_aux ctxt (Thm.prop_of thm)
- end
-*}
-
-ML {*
-fun build_goal ctxt thm cons rty qty =
- Logic.mk_equals ((Thm.prop_of thm), (build_goal_term ctxt thm cons rty qty))
-*}
ML {*
val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
@@ -825,66 +1059,8 @@
ML {*
cterm_of @{theory} (prop_of m1_novars);
cterm_of @{theory} (build_goal_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"});
-cterm_of @{theory} (build_goal_term_old @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs)
-*}
-
-
-text {*
- Unabs_def converts a definition given as
-
- c \<equiv> %x. %y. f x y
-
- to a theorem of the form
-
- c x y \<equiv> f x y
-
- This function is needed to rewrite the right-hand
- side to the left-hand side.
*}
-ML {*
-fun unabs_def ctxt def =
-let
- val (lhs, rhs) = Thm.dest_equals (cprop_of def)
- val xs = strip_abs_vars (term_of rhs)
- val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
-
- val thy = ProofContext.theory_of ctxt'
- val cxs = map (cterm_of thy o Free) xs
- val new_lhs = Drule.list_comb (lhs, cxs)
-
- fun get_conv [] = Conv.rewr_conv def
- | get_conv (x::xs) = Conv.fun_conv (get_conv xs)
-in
- get_conv xs new_lhs |>
- singleton (ProofContext.export ctxt' ctxt)
-end
-*}
-
-ML {* (* Test: *) @{thm IN_def}; unabs_def @{context} @{thm IN_def} *}
-
-ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
-ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}
-
-lemma atomize_eqv[atomize]:
- shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
-proof
- assume "A \<equiv> B"
- then show "Trueprop A \<equiv> Trueprop B" by unfold
-next
- assume *: "Trueprop A \<equiv> Trueprop B"
- have "A = B"
- proof (cases A)
- case True
- have "A" by fact
- then show "A = B" using * by simp
- next
- case False
- have "\<not>A" by fact
- then show "A = B" using * by auto
- qed
- then show "A \<equiv> B" by (rule eq_reflection)
-qed
(* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
ML {*
@@ -973,229 +1149,6 @@
apply (tactic {* transconv_fset_tac' @{context} *})
done
-section {* handling quantifiers - regularize *}
-
-text {* tyRel takes a type and builds a relation that a quantifier over this
- type needs to respect. *}
-ML {*
-fun tyRel ty rty rel lthy =
- if ty = rty
- then rel
- else (case ty of
- Type (s, tys) =>
- let
- val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
- val ty_out = ty --> ty --> @{typ bool};
- val tys_out = tys_rel ---> ty_out;
- in
- (case (maps_lookup (ProofContext.theory_of lthy) s) of
- SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
- | NONE => HOLogic.eq_const ty
- )
- end
- | _ => HOLogic.eq_const ty)
-*}
-
-ML {*
- cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context})
-*}
-
-definition
- Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-where
- "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
-(* TODO: Consider defining it with an "if"; sth like:
- Babs p m = \<lambda>x. if x \<in> p then m x else undefined
-*)
-
-ML {*
-(* trm \<Rightarrow> new_trm *)
-fun regularise trm rty rel lthy =
- case trm of
- Abs (x, T, t) =>
- if (needs_lift rty T) then let
- val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
- val v = Free (x', T);
- val t' = subst_bound (v, t);
- val rec_term = regularise t' rty rel lthy2;
- val lam_term = Term.lambda_name (x, v) rec_term;
- val sub_res_term = tyRel T rty rel lthy;
- val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
- val res_term = respects $ sub_res_term;
- val ty = fastype_of trm;
- val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty);
- val rabs_term = (rabs $ res_term) $ lam_term;
- in
- rabs_term
- end else let
- val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
- val v = Free (x', T);
- val t' = subst_bound (v, t);
- val rec_term = regularise t' rty rel lthy2;
- in
- Term.lambda_name (x, v) rec_term
- end
- | ((Const (@{const_name "All"}, at)) $ (Abs (x, T, t))) =>
- if (needs_lift rty T) then let
- val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
- val v = Free (x', T);
- val t' = subst_bound (v, t);
- val rec_term = regularise t' rty rel lthy2;
- val lam_term = Term.lambda_name (x, v) rec_term;
- val sub_res_term = tyRel T rty rel lthy;
- val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
- val res_term = respects $ sub_res_term;
- val ty = fastype_of lam_term;
- val rall = Const (@{const_name Ball}, (fastype_of res_term) --> ty --> @{typ bool});
- val rall_term = (rall $ res_term) $ lam_term;
- in
- rall_term
- end else let
- val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
- val v = Free (x', T);
- val t' = subst_bound (v, t);
- val rec_term = regularise t' rty rel lthy2;
- val lam_term = Term.lambda_name (x, v) rec_term
- in
- Const(@{const_name "All"}, at) $ lam_term
- end
- | ((Const (@{const_name "All"}, at)) $ P) =>
- let
- val (_, [al, _]) = dest_Type (fastype_of P);
- val ([x], lthy2) = Variable.variant_fixes [""] lthy;
- val v = (Free (x, al));
- val abs = Term.lambda_name (x, v) (P $ v);
- in regularise ((Const (@{const_name "All"}, at)) $ abs) rty rel lthy2 end
- | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) =>
- if (needs_lift rty T) then let
- val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
- val v = Free (x', T);
- val t' = subst_bound (v, t);
- val rec_term = regularise t' rty rel lthy2;
- val lam_term = Term.lambda_name (x, v) rec_term;
- val sub_res_term = tyRel T rty rel lthy;
- val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
- val res_term = respects $ sub_res_term;
- val ty = fastype_of lam_term;
- val rall = Const (@{const_name Bex}, (fastype_of res_term) --> ty --> @{typ bool});
- val rall_term = (rall $ res_term) $ lam_term;
- in
- rall_term
- end else let
- val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
- val v = Free (x', T);
- val t' = subst_bound (v, t);
- val rec_term = regularise t' rty rel lthy2;
- val lam_term = Term.lambda_name (x, v) rec_term
- in
- Const(@{const_name "Ex"}, at) $ lam_term
- end
- | ((Const (@{const_name "Ex"}, at)) $ P) =>
- let
- val (_, [al, _]) = dest_Type (fastype_of P);
- val ([x], lthy2) = Variable.variant_fixes [""] lthy;
- val v = (Free (x, al));
- val abs = Term.lambda_name (x, v) (P $ v);
- in regularise ((Const (@{const_name "Ex"}, at)) $ abs) rty rel lthy2 end
- | a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy)
- | _ => trm
-
-*}
-
-ML {*
- cterm_of @{theory} (regularise @{term "\<lambda>x :: int. x"} @{typ "trm"} @{term "RR"} @{context});
- cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
- cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
- cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
- cterm_of @{theory} (regularise @{term "All (P :: trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
-*}
-
-(* my version of regularise *)
-(****************************)
-
-(* some helper functions *)
-
-
-ML {*
-fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)
-fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
-fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
-fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})
-*}
-
-(* applies f to the subterm of an abstractions, otherwise to the given term *)
-ML {*
-fun apply_subt f trm =
- case trm of
- Abs (x, T, t) => Abs (x, T, f t)
- | _ => f trm
-*}
-
-
-(* FIXME: assumes always the typ is qty! *)
-(* FIXME: if there are more than one quotient, then you have to look up the relation *)
-ML {*
-fun my_reg rel trm =
- case trm of
- Abs (x, T, t) =>
- let
- val ty1 = fastype_of trm
- in
- (mk_babs ty1 T) $ (mk_resp T $ rel) $ (Abs (x, T, my_reg rel t))
- end
- | Const (@{const_name "All"}, ty) $ t =>
- let
- val ty1 = domain_type ty
- val ty2 = domain_type ty1
- in
- (mk_ball ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)
- end
- | Const (@{const_name "Ex"}, ty) $ t =>
- let
- val ty1 = domain_type ty
- val ty2 = domain_type ty1
- in
- (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)
- end
- | t1 $ t2 => (my_reg rel t1) $ (my_reg rel t2)
- | _ => trm
-*}
-
-ML {*
- cterm_of @{theory} (regularise @{term "\<lambda>x::trm. x"} @{typ "trm"} @{term "RR"} @{context});
- cterm_of @{theory} (my_reg @{term "RR"} @{term "\<lambda>x::trm. x"})
-*}
-
-ML {*
- cterm_of @{theory} (regularise @{term "\<forall>(x::trm) (y::trm). P x y"} @{typ "trm"} @{term "RR"} @{context});
- cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>(x::trm) (y::trm). P x y"})
-*}
-
-ML {*
- cterm_of @{theory} (regularise @{term "\<forall>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
- cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>x::trm. P x"})
-*}
-
-ML {*
- cterm_of @{theory} (regularise @{term "\<exists>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
- cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>x::trm. P x"})
-*}
-
-(* my version is not eta-expanded, but that should be OK *)
-ML {*
- cterm_of @{theory} (regularise @{term "All (P::trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
- cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm \<Rightarrow> bool)"})
-*}
-
-ML {*
-fun atomize_thm thm =
-let
- val thm' = forall_intr_vars thm
- val thm'' = ObjectLogic.atomize (cprop_of thm')
-in
- Simplifier.rewrite_rule [thm''] thm'
-end
-*}
thm list.induct
lemma list_induct_hol4:
@@ -1206,9 +1159,6 @@
ML {* atomize_thm @{thm list_induct_hol4} *}
-(*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
- trm == new_trm
-*)
ML {* val li = Thm.freezeT (atomize_thm @{thm list_induct_hol4}) *}
@@ -1366,7 +1316,6 @@
ML_prf {* val t = Thm.lift_rule (hd (cprems_of (Isar.goal ()))) @{thm "APPLY_RSP_II" } *}
ML_prf {* Toplevel.program (fn () => cterm_instantiate insts t) *}
-ML_prf {* Toplevel.program (fn () => Drule.instantiate' [] [SOME f_abs_c, SOME f_abs_c] t) *}