--- a/FSet.thy Wed Nov 11 18:51:59 2009 +0100
+++ b/FSet.thy Wed Nov 11 22:30:43 2009 +0100
@@ -101,8 +101,8 @@
lemma not_mem_card1:
fixes x :: "'a"
fixes xs :: "'a list"
- shows "~(x memb xs) \<Longrightarrow> card1 (x # xs) = Suc (card1 xs)"
- by simp
+ shows "(~(x memb xs)) = (card1 (x # xs) = Suc (card1 xs))"
+ by auto
lemma mem_cons:
fixes x :: "'a"
@@ -315,6 +315,7 @@
ML {* lift_thm_fset @{context} @{thm append_assoc} *}
ML {* lift_thm_fset @{context} @{thm list.induct} *}
ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *}
+ML {* lift_thm_fset @{context} @{thm not_mem_card1} *}
quotient_def
fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
@@ -392,10 +393,19 @@
val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
*}
prove {* Syntax.check_term @{context} rg *}
+ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
apply(atomize(full))
-ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
+apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
+apply (rule FUN_QUOTIENT)
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
+apply (rule IDENTITY_QUOTIENT)
+apply (rule IDENTITY_QUOTIENT)
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-
done
ML {*
val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms
@@ -419,8 +429,8 @@
ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_id *}
ML allthms
thm FORALL_PRS
-ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_d *}
-ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_a *}
+ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *}
+ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *}
ML {* ObjectLogic.rulify t_s *}
ML {* Type.freeze *}
@@ -431,8 +441,322 @@
ML {* val gla = fold lambda_all vars gl *}
ML {* val glf = Type.freeze gla *}
ML {* val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of @{theory} glf)) *}
-ML {* val allsym = map symmetric allthms *}
-ML {* val t_a = (snd o Thm.dest_equals o cprop_of) (MetaSimplifier.rewrite true allsym glac) *}
+
+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 {*
+fun tyRel2 lthy ty gty =
+ if ty = gty then HOLogic.eq_const ty else
+
+ case find_first (fn x => Sign.typ_instance (ProofContext.theory_of lthy) (gty, (#qtyp x))) (quotdata_lookup lthy) 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 {*
+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)) *}
+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,
+ rtac @{thm universal_twice},
+ (rtac @{thm impI} THEN' atac),
+ rtac @{thm implication_twice},
+ (*rtac @{thm equality_twice},*)
+ EqSubst.eqsubst_tac ctxt [0]
+ [(@{thm equiv_res_forall} OF [rel_eqv]),
+ (@{thm equiv_res_exists} OF [rel_eqv])],
+ (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
+ (rtac @{thm RIGHT_RES_FORALL_REGULAR})
+ ]; *}
+
+ apply (atomize(full))
+ apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *})
+ done
+
+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 si = simp_ids_trm (cterm_of @{theory} ttt) *}
+prove t_t: {* Logic.mk_equals ((Thm.prop_of t_r), 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 *})
+apply (rule FUN_QUOTIENT)
+apply (rule FUN_QUOTIENT)
+apply (rule IDENTITY_QUOTIENT)
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
+apply (rule IDENTITY_QUOTIENT)
+apply (rule IDENTITY_QUOTIENT)
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
+apply (rule IDENTITY_QUOTIENT)
+apply (rule IDENTITY_QUOTIENT)
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
+apply (rule IDENTITY_QUOTIENT)
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
+apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
+apply (rule IDENTITY_QUOTIENT)
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
+
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
+apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
+apply (rule IDENTITY_QUOTIENT)
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
+
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
+apply (rule IDENTITY_QUOTIENT)
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+done
+
+thm t_t
+ML {* val t_t = @{thm Pure.equal_elim_rule1} OF [@{thm t_t}, t_r] *}
+ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_t *}
+ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *}
+ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *}
+ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *}
+
ML {*
fun lift_thm_fset_note name thm lthy =