--- a/QuotMain.thy Mon Sep 21 10:53:01 2009 +0200
+++ b/QuotMain.thy Mon Sep 21 18:18:01 2009 +0200
@@ -152,31 +152,26 @@
end
*}
-(*
ML {*
- typedef_term @{term R} @{typ "nat"} @{context}
- |> Syntax.string_of_term @{context}
- |> writeln
-*}*)
-
-ML {*
-val typedef_tac =
- EVERY1 [rewrite_goal_tac @{thms mem_def},
- rtac @{thm exI}, rtac @{thm exI}, rtac @{thm refl}]
+(* makes the new type definitions and proves non-emptyness*)
+fun typedef_make (qty_name, rel, ty) lthy =
+let
+ val typedef_tac =
+ EVERY1 [rewrite_goal_tac @{thms mem_def},
+ rtac @{thm exI},
+ rtac @{thm exI},
+ rtac @{thm refl}]
+in
+ LocalTheory.theory_result
+ (Typedef.add_typedef false NONE
+ (qty_name, map fst (Term.add_tfreesT ty []), NoSyn)
+ (typedef_term rel ty lthy)
+ NONE typedef_tac) lthy
+end
*}
ML {*
-(* makes the new type definitions *)
-fun typedef_make (qty_name, rel, ty) lthy =
- LocalTheory.theory_result
- (Typedef.add_typedef false NONE
- (qty_name, map fst (Term.add_tfreesT ty []), NoSyn)
- (typedef_term rel ty lthy)
- NONE typedef_tac) lthy
-*}
-
-text {* proves the QUOT_TYPE theorem for the new type *}
-ML {*
+(* proves the QUOT_TYPE theorem for the new type *)
fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
let
val rep_thm = #Rep typedef_info
@@ -195,14 +190,7 @@
rtac abs_inv_simpd, rtac @{thm exI}, rtac @{thm refl},
rtac rep_inj]
end
-*}
-term QUOT_TYPE
-ML {* HOLogic.mk_Trueprop *}
-ML {* Goal.prove *}
-ML {* Syntax.check_term *}
-
-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)
@@ -210,26 +198,24 @@
|> Syntax.check_term lthy
in
Goal.prove lthy [] [] goal
- (fn _ => typedef_quot_type_tac equiv_thm typedef_info)
+ (K (typedef_quot_type_tac equiv_thm typedef_info))
end
*}
ML {*
-fun typedef_quotient_thm_tac defs quot_type_thm =
- EVERY1 [K (rewrite_goals_tac defs),
- rtac @{thm QUOT_TYPE.QUOTIENT},
- rtac quot_type_thm]
-*}
-
-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)
val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep)
|> Syntax.check_term lthy
+
+ val typedef_quotient_thm_tac =
+ EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]),
+ rtac @{thm QUOT_TYPE.QUOTIENT},
+ rtac quot_type_thm]
in
- Goal.prove lthy [] [] goal
- (fn _ => typedef_quotient_thm_tac [abs_def, rep_def] quot_type_thm)
+ Goal.prove lthy [] [] goal
+ (K typedef_quotient_thm_tac)
end
*}
@@ -245,7 +231,7 @@
*}
ML {*
-fun reg_thm (name, thm) lthy =
+fun note_thm (name, thm) lthy =
let
val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy
in
@@ -265,7 +251,7 @@
fun typedef_main (qty_name, rel, ty, equiv_thm) lthy =
let
(* generates typedef *)
- val ((_, typedef_info), lthy') = typedef_make (qty_name, rel, ty) lthy
+ val ((_, typedef_info), lthy1) = typedef_make (qty_name, rel, ty) lthy
(* abs and rep functions *)
val abs_ty = #abs_type typedef_info
@@ -278,30 +264,30 @@
(* 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 lthy1 (ABS_const $ rel $ abs)
+ val REP_trm = Syntax.check_term lthy1 (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'') =
- lthy' |> make_def (ABS_name, NoSyn, ABS_trm)
+ val (((ABS, ABS_def), (REP, REP_def)), lthy2) =
+ lthy1 |> make_def (ABS_name, NoSyn, ABS_trm)
||>> make_def (REP_name, NoSyn, REP_trm)
(* quot_type theorem *)
- val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy''
+ val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy2
val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name
(* quotient theorem *)
- val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy''
+ val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2
val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
(* interpretation *)
val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
- val ((_, [eqn1pre]), lthy''') = Variable.import true [ABS_def] lthy'';
+ val ((_, [eqn1pre]), lthy3) = Variable.import true [ABS_def] lthy2;
val eqn1i = Thm.prop_of (symmetric eqn1pre)
- val ((_, [eqn2pre]), lthy'''') = Variable.import true [REP_def] lthy''';
+ val ((_, [eqn2pre]), lthy4) = Variable.import true [REP_def] lthy3;
val eqn2i = Thm.prop_of (symmetric eqn2pre)
- val exp_morphism = ProofContext.export_morphism lthy'''' (ProofContext.init (ProofContext.theory_of lthy''''));
+ val exp_morphism = ProofContext.export_morphism lthy4 (ProofContext.init (ProofContext.theory_of lthy4));
val exp_term = Morphism.term exp_morphism;
val exp = Morphism.thm exp_morphism;
@@ -316,14 +302,14 @@
("Rep", rep)
]))]
in
- lthy''''
- |> reg_thm (quot_thm_name, quot_thm)
- ||>> reg_thm (quotient_thm_name, quotient_thm)
+ lthy4
+ |> note_thm (quot_thm_name, quot_thm)
+ ||>> note_thm (quotient_thm_name, quotient_thm)
||> LocalTheory.theory (fn thy =>
let
val global_eqns = map exp_term [eqn2i, eqn1i];
(* Not sure if the following context should not be used *)
- val (global_eqns2, lthy''''') = Variable.import_terms true global_eqns lthy'''';
+ val (global_eqns2, lthy5) = Variable.import_terms true global_eqns lthy4;
val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;
in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
end
@@ -335,13 +321,11 @@
| app "trm" "trm"
| lam "nat" "trm"
-axiomatization RR :: "trm \<Rightarrow> trm \<Rightarrow> bool" where
+axiomatization
+ RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"
+where
r_eq: "EQUIV RR"
-ML {*
- typedef_main
-*}
-
local_setup {*
typedef_main (@{binding "qtrm"}, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd
*}
@@ -355,6 +339,7 @@
(* Test interpretation *)
thm QUOT_TYPE_I_qtrm.thm11
+thm QUOT_TYPE.thm11
print_theorems