diff -r e39c8793a233 -r 20fa8dd8fb93 FSet.thy --- 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) \ 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 \ ('b \ 'b fset \ 'a \ 'a) \ 'b fset \ '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 \ bool"} @{typ "'a fset \ bool"} @{term "f :: ('a list \ 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 =