--- 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: "\<And>x. Abs (Rep x) = x"
and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
-begin
+begin
definition
"ABS x \<equiv> 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 "\<dots> = 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 \<lambda>(c::ty \<Rightarrow> bool). \<exists>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 "\<lambda>(c::'a my\<Rightarrow>bool). \<exists>x. c = Rmy x"
datatype 'a trm' =
- var' "'a"
+ var' "'a"
| app' "'a trm'" "'a trm'"
| lam' "'a" "'a trm'"
-
+
consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> 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