diff -r 7d3d86beacd6 -r f46dc0ca08c3 QuotMain.thy --- a/QuotMain.thy Fri Nov 20 13:03:01 2009 +0100 +++ b/QuotMain.thy Sat Nov 21 02:49:39 2009 +0100 @@ -557,7 +557,62 @@ *} ML {* -fun get_fun_new flag (rty, qty) lthy ty = +fun negF absF = repF + | negF repF = absF + +fun get_fun flag qenv lthy ty = +let + + fun get_fun_aux s fs = + (case (maps_lookup (ProofContext.theory_of lthy) s) of + SOME info => list_comb (Const (#mapfun info, dummyT), fs) + | NONE => error ("no map association for type " ^ s)) + + fun get_const flag qty = + let + val thy = ProofContext.theory_of lthy + val qty_name = Long_Name.base_name (fst (dest_Type qty)) + in + case flag of + absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT) + | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT) + end + + fun mk_identity ty = Abs ("", ty, Bound 0) + +in + if (AList.defined (op=) qenv ty) + then (get_const flag ty) + else (case ty of + TFree _ => mk_identity ty + | Type (_, []) => mk_identity ty + | Type ("fun" , [ty1, ty2]) => + let + val fs_ty1 = get_fun (negF flag) qenv lthy ty1 + val fs_ty2 = get_fun flag qenv lthy ty2 + in + get_fun_aux "fun" [fs_ty1, fs_ty2] + end + | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys) + | _ => error ("no type variables allowed")) +end + +(* returns all subterms where two types differ *) +fun diff (T, S) Ds = + case (T, S) of + (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds + | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds + | (Type (a, Ts), Type (b, Us)) => + if a = b then diffs (Ts, Us) Ds else (T, S)::Ds + | _ => (T, S)::Ds +and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds) + | diffs ([], []) Ds = Ds + | diffs _ _ = error "Unequal length of type arguments" + +*} + +ML {* +fun get_fun_OLD flag (rty, qty) lthy ty = let val tys = find_matching_types rty ty; val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys; @@ -657,11 +712,11 @@ fun mk_abs tm = let val ty = fastype_of tm - in Syntax.check_term lthy ((get_fun_new absF (rty, qty) lthy ty) $ tm) end + in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end fun mk_repabs tm = let val ty = fastype_of tm - in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ (mk_abs tm)) end + in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end fun is_lifted_const (Const (x, _)) = member (op =) consts x | is_lifted_const _ = false; @@ -1008,11 +1063,11 @@ fun mk_rep tm = let val ty = exchange_ty lthy qty rty (fastype_of tm) - in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ tm) end; + in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ tm) end; fun mk_abs tm = let val ty = fastype_of tm - in Syntax.check_term lthy ((get_fun_new absF (rty, qty) lthy ty) $ tm) end + in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end val (l, ltl) = Term.strip_type ty; val nl = map absty l; val vs = map (fn _ => "x") l; @@ -1149,7 +1204,6 @@ (******************************************) (* exception for when qtrm and rtrm do not match *) -ML {* exception LIFT_MATCH of string *} ML {* fun mk_resp_arg lthy (rty, qty) = @@ -1161,7 +1215,7 @@ if s = s' then let val SOME map_info = maps_lookup thy s - val args = map (mk_resp_arg lthy) (tys ~~tys') + val args = map (mk_resp_arg lthy) (tys ~~ tys') in list_comb (Const (#relfun map_info, dummyT), args) end @@ -1192,12 +1246,28 @@ fun qnt_typ ty = domain_type (domain_type ty) *} +(* +Regularizing an rterm means: + - Quantifiers over a type that needs lifting are replaced by + bounded quantifiers, for example: + \x. P \ \x\(Respects R). P + - Abstractions over a type that needs lifting are replaced + by bounded abstractions: + \x. P \ Ball (Respects R) (\x. P) + + - Equalities over the type being lifted are replaced by + appropriate relations: + A = B \ A \ B + Example with more complicated types of A, B: + A = B \ (op = \ op \) A B +*) + ML {* -fun REGULARIZE_aux lthy rtrm qtrm = +fun REGULARIZE_trm lthy rtrm qtrm = case (rtrm, qtrm) of (Abs (x, T, t), Abs (x', T', t')) => let - val subtrm = REGULARIZE_aux lthy t t' + val subtrm = REGULARIZE_trm lthy t t' in if T = T' then Abs (x, T, subtrm) @@ -1205,7 +1275,7 @@ end | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => let - val subtrm = apply_subt (REGULARIZE_aux lthy) t t' + val subtrm = apply_subt (REGULARIZE_trm lthy) t t' in if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm @@ -1213,7 +1283,7 @@ end | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => let - val subtrm = apply_subt (REGULARIZE_aux lthy) t t' + val subtrm = apply_subt (REGULARIZE_trm lthy) t t' in if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm @@ -1222,14 +1292,14 @@ (* FIXME: why is there a case for equality? is it correct? *) | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') => let - val subtrm = REGULARIZE_aux lthy t t' + val subtrm = REGULARIZE_trm lthy t t' in if ty = ty' then Const (@{const_name "op ="}, ty) $ subtrm else mk_resp_arg lthy (ty, ty') $ subtrm end | (t1 $ t2, t1' $ t2') => - (REGULARIZE_aux lthy t1 t1') $ (REGULARIZE_aux lthy t2 t2') + (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2') | (Free (x, ty), Free (x', ty')) => if x = x' then rtrm @@ -1246,11 +1316,98 @@ *} ML {* -fun REGULARIZE_trm lthy rtrm qtrm = - REGULARIZE_aux lthy rtrm qtrm - |> Syntax.check_term lthy - +fun mk_REGULARIZE_goal lthy rtrm qtrm = + Logic.mk_implies (rtrm, REGULARIZE_trm lthy rtrm qtrm |> Syntax.check_term lthy) *} +(* +To prove that the old theorem implies the new one, we first +atomize it and then try: + - Reflexivity of the relation + - Assumption + - Elimnating quantifiers on both sides of toplevel implication + - Simplifying implications on both sides of toplevel implication + - Ball (Respects ?E) ?P = All ?P + - (\x. ?R x \ ?P x \ ?Q x) \ All ?P \ Ball ?R ?Q + +*) + +lemma my_equiv_res_forall2: + fixes P::"'a \ bool" + fixes Q::"'b \ bool" + assumes a: "(All Q) \ (All P)" + shows "(All Q) \ Ball (Respects E) P" +using a by auto + +lemma my_equiv_res_exists: + fixes P::"'a \ bool" + fixes Q::"'b \ bool" + assumes a: "EQUIV E" + and b: "(Ex Q) \ (Ex P)" + shows "(Ex Q) \ Bex (Respects E) P" +apply(subst equiv_res_exists) +apply(rule a) +apply(rule b) +done + +ML {* +fun REGULARIZE_tac lthy rel_refl rel_eqv = + ObjectLogic.full_atomize_tac THEN' + REPEAT_ALL_NEW (FIRST' + [rtac rel_refl, + atac, + rtac @{thm universal_twice}, + rtac @{thm impI} THEN' atac, + rtac @{thm implication_twice}, + rtac @{thm my_equiv_res_forall2}, + rtac (rel_eqv RS @{thm my_equiv_res_exists}), + (* For a = b \ a \ b *) + rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl, + rtac @{thm RIGHT_RES_FORALL_REGULAR}]) +*} + +(* same version including debugging information *) +ML {* +fun my_print_tac ctxt s thm = +let + val prems_str = prems_of thm + |> map (Syntax.string_of_term ctxt) + |> cat_lines + val _ = tracing (s ^ "\n" ^ prems_str) +in + Seq.single thm +end + +fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))] +*} + +ML {* +fun REGULARIZE_tac' lthy rel_refl rel_eqv = + (REPEAT1 o FIRST1) + [(K (print_tac "start")) THEN' (K no_tac), + DT lthy "1" (rtac rel_refl), + DT lthy "2" atac, + DT lthy "3" (rtac @{thm universal_twice}), + DT lthy "4" (rtac @{thm impI} THEN' atac), + DT lthy "5" (rtac @{thm implication_twice}), + DT lthy "6" (rtac @{thm my_equiv_res_forall2}), + DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_exists})), + (* For a = b \ a \ b *) + DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), + DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})] +*} + +ML {* +fun REGULARIZE_prove rtrm qtrm rel_eqv rel_refl lthy = + let + val goal = mk_REGULARIZE_goal lthy rtrm qtrm + val cthm = Goal.prove lthy [] [] goal + (fn {context, ...} => REGULARIZE_tac context rel_refl rel_eqv 1) + in + cthm + end +*} + + end