--- a/FSet.thy Mon Nov 23 13:55:31 2009 +0100
+++ b/FSet.thy Mon Nov 23 14:05:02 2009 +0100
@@ -439,178 +439,8 @@
ML {* val glf = Type.legacy_freeze gla *}
ML {* val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of @{theory} glf)) *}
-ML {*
-fun apply_subt2 f trm trm2 =
- case (trm, trm2) of
- (Abs (x, T, t), Abs (x2, T2, t2)) =>
- let
- val (x', t') = Term.dest_abs (x, T, t);
- val (x2', t2') = Term.dest_abs (x2, T2, t2)
- val (s1, s2) = f t' t2';
- in
- (Term.absfree (x', T, s1),
- Term.absfree (x2', T2, s2))
- end
- | _ => f trm trm2
-*}
-
-(*ML_prf {*
-val concl = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ()))))
-val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP2})
-val insts = Thm.first_order_match (pat, concl)
-val t = Drule.instantiate insts @{thm APPLY_RSP2}
-*}*)
-
-ML {*
-fun tyRel2 lthy ty gty =
- if ty = gty then HOLogic.eq_const ty else
-
- case quotdata_lookup lthy (fst (dest_Type gty)) of
- SOME quotdata =>
- if Sign.typ_instance (ProofContext.theory_of lthy) (ty, #rtyp quotdata) then
- case #rel quotdata of
- Const(s, _) => Const(s, dummyT)
- | _ => error "tyRel2 fail: relation is not a constant"
- else error "tyRel2 fail: a non-lifted type lifted to a lifted type"
- | NONE => (case (ty, gty) of
- (Type (s, tys), Type (s2, tys2)) =>
- if s = s2 andalso length tys = length tys2 then
- 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),
- map2 (tyRel2 lthy) tys tys2)
- | NONE => HOLogic.eq_const ty
- )
- end
- else error "tyRel2 fail: different type structures"
- | _ => HOLogic.eq_const ty)
-*}
-
-ML mk_babs
-
-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})
-*}
-
+prove t_r: {* mk_REGULARIZE_goal @{context} (prop_of t_a) (term_of glac) *}
-ML {*
-fun my_reg2 lthy trm gtrm =
- case (trm, gtrm) of
- (Abs (x, T, t), Abs (x2, T2, t2)) =>
- if not (T = T2) then
- let
- val rrel = tyRel2 lthy T T2;
- val (s1, s2) = apply_subt2 (my_reg2 lthy) trm gtrm
- in
- (((mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ s1),
- ((mk_babs (fastype_of gtrm) T2) $ (mk_resp T2 $ (HOLogic.eq_const dummyT)) $ s2))
- end
- else
- let
- val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
- in
- (Abs(x, T, s1), Abs(x2, T2, s2))
- end
- | (Const (@{const_name "All"}, ty) $ (t as Abs (_, T, _)),
- Const (@{const_name "All"}, ty') $ (t2 as Abs (_, T2, _))) =>
- if not (T = T2) then
- let
- val ty1 = domain_type ty;
- val ty2 = domain_type ty1;
- val ty'1 = domain_type ty';
- val ty'2 = domain_type ty'1;
- val rrel = tyRel2 lthy T T2;
- val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2;
- in
- (((mk_ball ty1) $ (mk_resp ty2 $ rrel) $ s1),
- ((mk_ball ty'1) $ (mk_resp ty'2 $ (HOLogic.eq_const dummyT)) $ s2))
- end
- else
- let
- val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
- in
- ((Const (@{const_name "All"}, ty) $ s1),
- (Const (@{const_name "All"}, ty') $ s2))
- end
- | (Const (@{const_name "Ex"}, ty) $ (t as Abs (_, T, _)),
- Const (@{const_name "Ex"}, ty') $ (t2 as Abs (_, T2, _))) =>
- if not (T = T2) then
- let
- val ty1 = domain_type ty
- val ty2 = domain_type ty1
- val ty'1 = domain_type ty'
- val ty'2 = domain_type ty'1
- val rrel = tyRel2 lthy T T2
- val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
- in
- (((mk_bex ty1) $ (mk_resp ty2 $ rrel) $ s1),
- ((mk_bex ty'1) $ (mk_resp ty'2 $ (HOLogic.eq_const dummyT)) $ s2))
- end
- else
- let
- val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
- in
- ((Const (@{const_name "Ex"}, ty) $ s1),
- (Const (@{const_name "Ex"}, ty') $ s2))
- end
- | (Const (@{const_name "op ="}, T) $ t, (Const (@{const_name "op ="}, T2) $ t2)) =>
- let
- val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
- val rhs = Const (@{const_name "op ="}, T2) $ s2
- in
- if not (T = T2) then
- ((tyRel2 lthy T T2) $ s1, rhs)
- else
- (Const (@{const_name "op ="}, T) $ s1, rhs)
- end
- | (t $ t', t2 $ t2') =>
- let
- val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
- val (s1', s2') = apply_subt2 (my_reg2 lthy) t' t2'
- in
- (s1 $ s1', s2 $ s2')
- end
- | (Const c1, Const c2) => (Const c1, Const c2) (* c2 may be lifted *)
- | (Bound i, Bound j) => (* Bounds are replaced, so should never happen? *)
- if i = j then (Bound i, Bound j) else error "my_reg2: different Bounds"
- | (Free (n, T), Free(n2, T2)) => if n = n2 then (Free (n, T), Free (n2, T2))
- else error ("my_ref2: different variables: " ^ n ^ ", " ^ n2)
- | _ => error "my_reg2: terms don't agree"
-*}
-
-
-ML {* prop_of t_a *}
-ML {* term_of glac *}
-ML {* val (tta, ttb) = (my_reg2 @{context} (prop_of t_a) (term_of glac)) *}
-
-(* Does not work. *)
-ML {*
- prop_of t_a
- |> Syntax.string_of_term @{context}
- |> writeln
-*}
-
-ML {*
- (term_of glac)
- |> Syntax.string_of_term @{context}
- |> writeln
-*}
-
-ML {* val tta = REGULARIZE_trm @{context} (prop_of t_a) (term_of glac) *}
-
-ML {* val tt = Syntax.check_term @{context} tta *}
-
-
-
-prove t_r: {* Logic.mk_implies
- ((prop_of t_a), tt) *}
ML_prf {* fun tac ctxt = FIRST' [
rtac rel_refl,
atac,
@@ -631,66 +461,9 @@
ML {* val t_r = @{thm t_r} OF [t_a] *}
-ML {* val ttg = Syntax.check_term @{context} ttb *}
-
-ML {*
-fun is_lifted_const h gh = is_Const h andalso is_Const gh andalso not (h = gh)
-
-fun mkrepabs lthy ty gty t =
- let
- val qenv = distinct (op=) (diff (gty, ty) [])
-(* val _ = sanity_chk qenv lthy *)
- val ty = fastype_of t
- val abs = get_fun absF qenv lthy gty $ t
- val rep = get_fun repF qenv lthy gty $ abs
- in
- Syntax.check_term lthy rep
- end
-*}
-
-ML {*
- cterm_of @{theory} (mkrepabs @{context} @{typ "'a list \<Rightarrow> bool"} @{typ "'a fset \<Rightarrow> bool"} @{term "f :: ('a list \<Rightarrow> bool)"})
-*}
-
-
-
-ML {*
-fun build_repabs_term lthy trm gtrm =
- case (trm, gtrm) of
- (Abs (a as (_, T, _)), Abs (a2 as (_, T2, _))) =>
- let
- val (vs, t) = Term.dest_abs a;
- val (_, g) = Term.dest_abs a2;
- val v = Free(vs, T);
- val t' = lambda v (build_repabs_term lthy t g);
- val ty = fastype_of trm;
- val gty = fastype_of gtrm;
- in
- if (ty = gty) then t' else
- mkrepabs lthy ty gty (
- if (T = T2) then t' else
- lambda v (t' $ (mkrepabs lthy T T2 v))
- )
- end
- | _ =>
- case (Term.strip_comb trm, Term.strip_comb gtrm) of
- ((Const(@{const_name Respects}, _), _), _) => trm
- | ((h, tms), (gh, gtms)) =>
- let
- val ty = fastype_of trm;
- val gty = fastype_of gtrm;
- val tms' = map2 (build_repabs_term lthy) tms gtms
- val t' = list_comb(h, tms')
- in
- if ty = gty then t' else
- if is_lifted_const h gh then mkrepabs lthy ty gty t' else
- if (Term.is_Free h) andalso (length tms > 0) then mkrepabs lthy ty gty t' else t'
- end
-*}
-
-ML {* val ttt = build_repabs_term @{context} tt ttg *}
+ML {* val ttt = mk_inj_REPABS_goal @{context} (prop_of t_r, term_of glac) *}
ML {* val si = simp_ids_trm (cterm_of @{theory} ttt) *}
-prove t_t: {* Logic.mk_equals ((Thm.prop_of t_r), term_of si) *}
+prove t_t: {* term_of si *}
ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
apply(atomize(full))
apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})