diff -r e6b6e5ba0cc5 -r 553bef083318 FSet.thy --- 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 \ 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 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 *})