diff -r 5f6ee943c697 -r f46eddb570a3 QuotMain.thy --- a/QuotMain.thy Tue Sep 15 09:59:56 2009 +0200 +++ b/QuotMain.thy Tue Sep 15 10:00:34 2009 +0200 @@ -17,7 +17,7 @@ and rep_inverse: "\x. Abs (Rep x) = x" and abs_inverse: "\x. (Rep (Abs (R x))) = (R x)" and rep_inject: "\x y. (Rep x = Rep y) = (x = y)" -begin +begin definition "ABS x \ Abs (R x)" @@ -25,12 +25,12 @@ definition "REP a = Eps (Rep a)" -lemma lem9: +lemma lem9: shows "R (Eps (R x)) = R x" proof - have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def) then have "R x (Eps (R x))" by (rule someI) - then show "R (Eps (R x)) = R x" + then show "R (Eps (R x)) = R x" using equiv unfolding EQUIV_def by simp qed @@ -38,7 +38,7 @@ shows "ABS (REP a) = a" unfolding ABS_def REP_def proof - - from rep_prop + from rep_prop obtain x where eq: "Rep a = R x" by auto have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp also have "\ = Abs (R x)" using lem9 by simp @@ -48,7 +48,7 @@ show "Abs (R (Eps (Rep a))) = a" by simp qed -lemma REP_refl: +lemma REP_refl: shows "R (REP a) (REP a)" unfolding REP_def by (simp add: equiv[simplified EQUIV_def]) @@ -60,7 +60,7 @@ apply(drule rep_inject[THEN iffD2]) apply(simp add: abs_inverse) done - + theorem thm11: shows "R r r' = (ABS r = ABS r')" unfolding ABS_def @@ -97,13 +97,13 @@ ML {* (* constructs the term \(c::ty \ bool). \x. c = rel x *) fun typedef_term rel ty lthy = -let - val [x, c] = [("x", ty), ("c", ty --> @{typ bool})] +let + val [x, c] = [("x", ty), ("c", ty --> @{typ bool})] |> Variable.variant_frees lthy [rel] |> map Free in - lambda c - (HOLogic.mk_exists + lambda c + (HOLogic.mk_exists ("x", ty, HOLogic.mk_eq (c, (rel $ x)))) end *} @@ -116,7 +116,7 @@ *}*) ML {* -val typedef_tac = +val typedef_tac = EVERY1 [rewrite_goal_tac @{thms mem_def}, rtac @{thm exI}, rtac @{thm exI}, rtac @{thm refl}] *} @@ -125,7 +125,7 @@ (* makes the new type definitions *) fun typedef_make (qty_name, rel, ty) lthy = LocalTheory.theory_result - (Typedef.add_typedef false NONE + (Typedef.add_typedef false NONE (qty_name, map fst (Term.add_tfreesT ty []), NoSyn) (typedef_term rel ty lthy) NONE typedef_tac) lthy @@ -133,7 +133,7 @@ text {* proves the QUOT_TYPE theorem for the new type *} ML {* -fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = +fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = let val rep_thm = #Rep typedef_info val rep_inv = #Rep_inverse typedef_info @@ -145,9 +145,9 @@ val abs_inv_simpd = Simplifier.asm_full_simplify ss abs_inv in EVERY1 [rtac @{thm QUOT_TYPE.intro}, - rtac equiv_thm, - rtac rep_thm_simpd, - rtac rep_inv, + rtac equiv_thm, + rtac rep_thm_simpd, + rtac rep_inv, rtac abs_inv_simpd, rtac @{thm exI}, rtac @{thm refl}, rtac rep_inj] end @@ -158,7 +158,7 @@ ML {* Goal.prove *} ML {* Syntax.check_term *} -ML {* +ML {* fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = let val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT) @@ -172,12 +172,12 @@ ML {* fun typedef_quotient_thm_tac defs quot_type_thm = - EVERY1 [K (rewrite_goals_tac defs), - rtac @{thm QUOT_TYPE.QUOTIENT}, + EVERY1 [K (rewrite_goals_tac defs), + rtac @{thm QUOT_TYPE.QUOTIENT}, rtac quot_type_thm] *} -ML {* +ML {* fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = let val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT) @@ -190,10 +190,10 @@ *} text {* two wrappers for define and note *} -ML {* +ML {* fun make_def (name, mx, trm) lthy = -let - val ((trm, (_ , thm)), lthy') = +let + val ((trm, (_ , thm)), lthy') = LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, trm)) lthy in ((trm, thm), lthy') @@ -208,9 +208,9 @@ *) ML {* -fun reg_thm (name, thm) lthy = +fun reg_thm (name, thm) lthy = let - val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy + val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy in (thm',lthy') end @@ -243,7 +243,7 @@ ML {* fun typedef_main (qty_name, rel, ty, equiv_thm) lthy = -let +let (* generates typedef *) val ((_,typedef_info), lthy') = typedef_make (qty_name, rel, ty) lthy @@ -258,11 +258,11 @@ (* ABS and REP definitions *) val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT ) val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT ) - val ABS_trm = Syntax.check_term lthy' (ABS_const $ rel $ abs) - val REP_trm = Syntax.check_term lthy' (REP_const $ rep) + val ABS_trm = Syntax.check_term lthy' (ABS_const $ rel $ abs) + val REP_trm = Syntax.check_term lthy' (REP_const $ rep) val ABS_name = Binding.prefix_name "ABS_" qty_name - val REP_name = Binding.prefix_name "REP_" qty_name - val (((ABS, ABS_def), (REP, REP_def)), lthy'') = + val REP_name = Binding.prefix_name "REP_" qty_name + val (((ABS, ABS_def), (REP, REP_def)), lthy'') = lthy' |> make_def (ABS_name, NoSyn, ABS_trm) ||>> make_def (REP_name, NoSyn, REP_trm) @@ -318,7 +318,7 @@ section {* various tests for quotient types*} datatype trm = - var "nat" + var "nat" | app "trm" "trm" | lam "nat" "trm" @@ -326,7 +326,7 @@ r_eq: "EQUIV RR" ML {* - typedef_main + typedef_main *} (*ML {* @@ -367,10 +367,10 @@ term "\(c::'a my\bool). \x. c = Rmy x" datatype 'a trm' = - var' "'a" + var' "'a" | app' "'a trm'" "'a trm'" | lam' "'a" "'a trm'" - + consts R' :: "'a trm' \ 'a trm' \ bool" axioms r_eq': "EQUIV R'" @@ -417,7 +417,7 @@ fun merge _ = Symtab.merge (K true)) in val lookup = Symtab.lookup o Data.get - fun update k v = Data.map (Symtab.update (k, v)) + fun update k v = Data.map (Symtab.update (k, v)) end *} @@ -434,19 +434,19 @@ ML {* datatype abs_or_rep = abs | rep -fun get_fun abs_or_rep rty qty lthy ty = +fun get_fun abs_or_rep rty qty lthy ty = let val qty_name = Long_Name.base_name (fst (dest_Type qty)) - + fun get_fun_aux s fs_tys = let val (fs, tys) = split_list fs_tys - val (otys, ntys) = split_list tys + val (otys, ntys) = split_list tys val oty = Type (s, otys) val nty = Type (s, ntys) val ftys = map (op -->) tys in - (case (lookup (Context.Proof lthy) s) of + (case (lookup (Context.Proof lthy) s) of SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty)) | NONE => raise ERROR ("no map association for type " ^ s)) end @@ -459,7 +459,7 @@ else (case ty of TFree _ => (Abs ("x", ty, Bound 0), (ty, ty)) | Type (_, []) => (Abs ("x", ty, Bound 0), (ty, ty)) - | Type (s, tys) => get_fun_aux s (map (get_fun abs_or_rep rty qty lthy) tys) + | Type (s, tys) => get_fun_aux s (map (get_fun abs_or_rep rty qty lthy) tys) | _ => raise ERROR ("no variables") ) end @@ -480,7 +480,7 @@ val (arg_tys, res_ty) = strip_type ty val fresh_args = arg_tys |> map (pair "x") - |> Variable.variant_frees lthy [nconst, oconst] + |> Variable.variant_frees lthy [nconst, oconst] |> map Free val rep_fns = map (fst o get_fun rep rty qty lthy) arg_tys @@ -495,16 +495,16 @@ *} ML {* -fun exchange_ty rty qty ty = +fun exchange_ty rty qty ty = if ty = rty then qty - else + else (case ty of Type (s, tys) => Type (s, map (exchange_ty rty qty) tys) | _ => ty) *} ML {* -fun make_const_def nconst_name oconst mx rty qty lthy = +fun make_const_def nconst_name oconst mx rty qty lthy = let val oconst_ty = fastype_of oconst val nconst_ty = exchange_ty rty qty oconst_ty @@ -512,7 +512,7 @@ val def_trm = get_const_def nconst oconst rty qty lthy in make_def (Binding.name nconst_name, mx, def_trm) lthy -end +end *} local_setup {* @@ -625,7 +625,7 @@ make_const_def "UNION" @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd *} -term append +term append term UNION thm UNION_def