nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:6885fa184e89
+:68d64432623e
 (HOLogic.mk_exists
 ("x", ty, HOLogic.mk_eq (c, (rel $ x))))
 end
 *}
-(*
+ML {*
-ML {*
+(* makes the new type definitions and proves non-emptyness*)
-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}]
-*}
-ML {*
-(* makes the new type definitions *)
 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
+*}
-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
 val rep_inv = #Rep_inverse typedef_info
 val abs_inv = #Abs_inverse typedef_info
 rtac rep_thm_simpd,
 rtac rep_inv,
 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)
 val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
 |> 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
-in
-Goal.prove lthy [] [] goal
+val typedef_quotient_thm_tac =
-(fn _ => typedef_quotient_thm_tac [abs_def, rep_def] quot_type_thm)
+EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]),
+rtac @{thm QUOT_TYPE.QUOTIENT},
+rtac quot_type_thm]
+in
+Goal.prove lthy [] [] goal
+(K typedef_quotient_thm_tac)
 end
 *}
 text {* two wrappers for define and note *}
 ML {*
 ((rhs, thm), lthy')
 end
 *}
 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
 (thm', lthy')
 end
 ML {*
 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
 val rep_ty = #rep_type typedef_info
 val abs_name = #Abs_name typedef_info
 val rep = Const (rep_name, abs_ty --> rep_ty)
 (* 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 ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs)
-val REP_trm = Syntax.check_term lthy' (REP_const $ rep)
+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'') =
+val (((ABS, ABS_def), (REP, REP_def)), lthy2) =
-lthy' |> make_def (ABS_name, NoSyn, ABS_trm)
+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;
 val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN
 ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))])))
 ("R", rel),
 ("Abs", abs),
 ("Rep", rep)
 ]))]
 in
-lthy''''
+lthy4
-|> reg_thm (quot_thm_name, quot_thm)
+|> note_thm (quot_thm_name, quot_thm)
-||>> reg_thm (quotient_thm_name, quotient_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
 *}
 datatype trm =
 var  "nat"
 | 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
 *}
 thm QUOT_TYPE_qtrm
 thm QUOTIENT_qtrm
 (* Test interpretation *)
 thm QUOT_TYPE_I_qtrm.thm11
+thm QUOT_TYPE.thm11
 print_theorems
 thm Rep_qtrm

changeset 26	68d64432623e
parent 24	6885fa184e89
child 27	160f287ebb75