diff -r f3cbda066c3a -r 35be65791f1d QuotMain.thy --- a/QuotMain.thy Tue Oct 06 15:11:30 2009 +0200 +++ b/QuotMain.thy Thu Oct 08 14:27:50 2009 +0200 @@ -1,5 +1,6 @@ theory QuotMain imports QuotScript QuotList Prove +uses ("quotient.ML") begin locale QUOT_TYPE = @@ -142,109 +143,7 @@ section {* type definition for the quotient type *} -ML {* -(* constructs the term \(c::rty \ bool). \x. c = rel x *) -fun typedef_term rel rty lthy = -let - val [x, c] = [("x", rty), ("c", rty --> @{typ bool})] - |> Variable.variant_frees lthy [rel] - |> map Free -in - lambda c - (HOLogic.exists_const rty $ - lambda x (HOLogic.mk_eq (c, (rel $ x)))) -end -*} - -ML {* -(* makes the new type definitions and proves non-emptyness*) -fun typedef_make (qty_name, mx, rel, rty) lthy = -let - val typedef_tac = - EVERY1 [rewrite_goal_tac @{thms mem_def}, - rtac @{thm exI}, - rtac @{thm exI}, - rtac @{thm refl}] - val tfrees = map fst (Term.add_tfreesT rty []) -in - LocalTheory.theory_result - (Typedef.add_typedef false NONE - (qty_name, tfrees, mx) - (typedef_term rel rty lthy) - NONE typedef_tac) lthy -end -*} - -ML {* -(* tactic to prove the QUOT_TYPE theorem for the new type *) -fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = -let - val unfold_mem = MetaSimplifier.rewrite_rule @{thms mem_def} - val rep_thm = #Rep typedef_info |> unfold_mem - val rep_inv = #Rep_inverse typedef_info - val abs_inv = #Abs_inverse typedef_info |> unfold_mem - val rep_inj = #Rep_inject typedef_info -in - EVERY1 [rtac @{thm QUOT_TYPE.intro}, - rtac equiv_thm, - rtac rep_thm, - rtac rep_inv, - rtac abs_inv, - rtac @{thm exI}, - rtac @{thm refl}, - rtac rep_inj] -end -*} - -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 - (K (typedef_quot_type_tac equiv_thm typedef_info)) -end -*} - -ML {* -(* proves the quotient theorem *) -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 - (K typedef_quotient_thm_tac) -end -*} - -text {* two wrappers for define and note *} -ML {* -fun make_def (name, mx, rhs) lthy = -let - val ((rhs, (_ , thm)), lthy') = - LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy -in - ((rhs, thm), lthy') -end -*} - -ML {* -fun note_thm (name, thm) lthy = -let - val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy -in - (thm', lthy') -end -*} +use "quotient.ML" ML {* val no_vars = Thm.rule_attribute (fn context => fn th => @@ -254,75 +153,6 @@ in th' end); *} -ML {* -fun typedef_main (qty_name, mx, rel, rty, equiv_thm) lthy = -let - (* generates typedef *) - val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) 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_name = #Rep_name typedef_info - val abs = Const (abs_name, rep_ty --> abs_ty) - 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 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)), 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) 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) lthy2 - val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name - - (* interpretation *) - val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) - val ((_, [eqn1pre]), lthy3) = Variable.import true [ABS_def] lthy2; - val eqn1i = Thm.prop_of (symmetric eqn1pre) - val ((_, [eqn2pre]), lthy4) = Variable.import true [REP_def] lthy3; - val eqn2i = Thm.prop_of (symmetric eqn2pre) - - 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))]))) - val mthdt = Method.Basic (fn _ => mthd) - val bymt = Proof.global_terminal_proof (mthdt, NONE) - val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), - Expression.Named [ - ("R", rel), - ("Abs", abs), - ("Rep", rep) - ]))] -in - 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, 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 -*} - - section {* various tests for quotient types*} datatype trm = var "nat"