# HG changeset patch # User Christian Urban # Date 1253549881 -7200 # Node ID 68d64432623e83e50906df67286e4d88ffbfc654 # Parent 6885fa184e894bccd8c1360e897225ff461430f2 slight tuning diff -r 6885fa184e89 -r 68d64432623e QuotMain.thy --- 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 \ trm \ bool" where +axiomatization + RR :: "trm \ trm \ 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