# HG changeset patch # User Christian Urban # Date 1260578696 -3600 # Node ID 0d98a4c7f8dc138a11b6f7e8634a9f28a22e6ea0 # Parent d705d7ae2410cec135ed0790da817e637c6fd628 renamed quotient.ML to quotient_typ.ML diff -r d705d7ae2410 -r 0d98a4c7f8dc Quot/QuotMain.thy --- a/Quot/QuotMain.thy Fri Dec 11 19:22:30 2009 +0100 +++ b/Quot/QuotMain.thy Sat Dec 12 01:44:56 2009 +0100 @@ -1,7 +1,7 @@ theory QuotMain imports QuotScript Prove uses ("quotient_info.ML") - ("quotient.ML") + ("quotient_typ.ML") ("quotient_def.ML") begin @@ -102,8 +102,7 @@ lemmas [quot_equiv] = identity_equivp (* definition of the quotient types *) -(* FIXME: should be called quotient_typ.ML *) -use "quotient.ML" +use "quotient_typ.ML" (* lifting of constants *) use "quotient_def.ML" diff -r d705d7ae2410 -r 0d98a4c7f8dc Quot/quotient.ML --- a/Quot/quotient.ML Fri Dec 11 19:22:30 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,226 +0,0 @@ -signature QUOTIENT = -sig - exception LIFT_MATCH of string - - val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state - val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state - -end; - -structure Quotient: QUOTIENT = -struct - -exception LIFT_MATCH of string - -(* wrappers for define, note and theorem_i *) -fun define (name, mx, rhs) lthy = -let - val ((rhs, (_ , thm)), lthy') = - Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy -in - ((rhs, thm), lthy') -end - -fun note (name, thm, attrs) lthy = -let - val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy -in - (thm', lthy') -end - -fun internal_attr at = Attrib.internal (K at) - -fun theorem after_qed goals ctxt = -let - val goals' = map (rpair []) goals - fun after_qed' thms = after_qed (the_single thms) -in - Proof.theorem_i NONE after_qed' [goals'] ctxt -end - - -(* definition of quotient types *) -(********************************) - -(* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) -fun typedef_term rel rty lthy = -let - val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)] - |> Variable.variant_frees lthy [rel] - |> map Free -in - lambda c - (HOLogic.exists_const rty $ - lambda x (HOLogic.mk_eq (c, (rel $ x)))) -end - -(* 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 - Local_Theory.theory_result - (Typedef.add_typedef false NONE - (qty_name, tfrees, mx) - (typedef_term rel rty lthy) - NONE typedef_tac) lthy -end - -(* 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 [@{thm 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 - -(* proves the QUOT_TYPE theorem *) -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 - -(* 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 - -(* main function for constructing the quotient type *) -fun mk_typedef_main (((qty_name, mx), (rty, rel)), 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 |> define (ABS_name, NoSyn, ABS_trm) - ||>> define (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 - - (* storing the quot-info *) - val qty_str = fst (Term.dest_Type abs_ty) - val lthy3 = quotdata_update qty_str - (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 - (* FIXME: varifyT should not be used *) - (* FIXME: the relation needs to be a string, since its type needs *) - (* FIXME: to recalculated in for example REGULARIZE *) - -in - lthy3 - |> note (quot_thm_name, quot_thm, []) - ||>> note (quotient_thm_name, quotient_thm, [internal_attr quotient_rules_add]) - ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [internal_attr equiv_rules_add]) -end - - - - -(* interface and syntax setup *) - -(* the ML-interface takes a list of 4-tuples consisting of *) -(* *) -(* - the name of the quotient type *) -(* - its mixfix annotation *) -(* - the type to be quotient *) -(* - the relation according to which the type is quotient *) - -fun quotient_type quot_list lthy = -let - fun mk_goal (rty, rel) = - let - val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} - in - HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel) - end - - val goals = map (mk_goal o snd) quot_list - - fun after_qed thms lthy = - fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd -in - theorem after_qed goals lthy -end - -fun quotient_type_cmd spec lthy = -let - fun parse_spec (((qty_str, mx), rty_str), rel_str) = - let - val qty_name = Binding.name qty_str - val rty = Syntax.read_typ lthy rty_str - val rel = Syntax.read_term lthy rel_str - in - ((qty_name, mx), (rty, rel)) - end -in - quotient_type (map parse_spec spec) lthy -end - -val quotspec_parser = - OuterParse.and_list1 - (OuterParse.short_ident -- OuterParse.opt_infix -- - (OuterParse.$$$ "=" |-- OuterParse.typ) -- - (OuterParse.$$$ "/" |-- OuterParse.term)) - -val _ = OuterKeyword.keyword "/" - -val _ = - OuterSyntax.local_theory_to_proof "quotient" - "quotient type definitions (requires equivalence proofs)" - OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd) - -end; (* structure *) - -open Quotient diff -r d705d7ae2410 -r 0d98a4c7f8dc Quot/quotient_typ.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/quotient_typ.ML Sat Dec 12 01:44:56 2009 +0100 @@ -0,0 +1,226 @@ +signature QUOTIENT = +sig + exception LIFT_MATCH of string + + val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state + val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state + +end; + +structure Quotient: QUOTIENT = +struct + +exception LIFT_MATCH of string + +(* wrappers for define, note and theorem_i *) +fun define (name, mx, rhs) lthy = +let + val ((rhs, (_ , thm)), lthy') = + Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy +in + ((rhs, thm), lthy') +end + +fun note (name, thm, attrs) lthy = +let + val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy +in + (thm', lthy') +end + +fun internal_attr at = Attrib.internal (K at) + +fun theorem after_qed goals ctxt = +let + val goals' = map (rpair []) goals + fun after_qed' thms = after_qed (the_single thms) +in + Proof.theorem_i NONE after_qed' [goals'] ctxt +end + + +(* definition of quotient types *) +(********************************) + +(* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) +fun typedef_term rel rty lthy = +let + val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)] + |> Variable.variant_frees lthy [rel] + |> map Free +in + lambda c + (HOLogic.exists_const rty $ + lambda x (HOLogic.mk_eq (c, (rel $ x)))) +end + +(* 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 + Local_Theory.theory_result + (Typedef.add_typedef false NONE + (qty_name, tfrees, mx) + (typedef_term rel rty lthy) + NONE typedef_tac) lthy +end + +(* 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 [@{thm 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 + +(* proves the QUOT_TYPE theorem *) +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 + +(* 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 + +(* main function for constructing the quotient type *) +fun mk_typedef_main (((qty_name, mx), (rty, rel)), 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 |> define (ABS_name, NoSyn, ABS_trm) + ||>> define (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 + + (* storing the quot-info *) + val qty_str = fst (Term.dest_Type abs_ty) + val lthy3 = quotdata_update qty_str + (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 + (* FIXME: varifyT should not be used *) + (* FIXME: the relation needs to be a string, since its type needs *) + (* FIXME: to recalculated in for example REGULARIZE *) + +in + lthy3 + |> note (quot_thm_name, quot_thm, []) + ||>> note (quotient_thm_name, quotient_thm, [internal_attr quotient_rules_add]) + ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [internal_attr equiv_rules_add]) +end + + + + +(* interface and syntax setup *) + +(* the ML-interface takes a list of 4-tuples consisting of *) +(* *) +(* - the name of the quotient type *) +(* - its mixfix annotation *) +(* - the type to be quotient *) +(* - the relation according to which the type is quotient *) + +fun quotient_type quot_list lthy = +let + fun mk_goal (rty, rel) = + let + val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} + in + HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel) + end + + val goals = map (mk_goal o snd) quot_list + + fun after_qed thms lthy = + fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd +in + theorem after_qed goals lthy +end + +fun quotient_type_cmd spec lthy = +let + fun parse_spec (((qty_str, mx), rty_str), rel_str) = + let + val qty_name = Binding.name qty_str + val rty = Syntax.read_typ lthy rty_str + val rel = Syntax.read_term lthy rel_str + in + ((qty_name, mx), (rty, rel)) + end +in + quotient_type (map parse_spec spec) lthy +end + +val quotspec_parser = + OuterParse.and_list1 + (OuterParse.short_ident -- OuterParse.opt_infix -- + (OuterParse.$$$ "=" |-- OuterParse.typ) -- + (OuterParse.$$$ "/" |-- OuterParse.term)) + +val _ = OuterKeyword.keyword "/" + +val _ = + OuterSyntax.local_theory_to_proof "quotient" + "quotient type definitions (requires equivalence proofs)" + OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd) + +end; (* structure *) + +open Quotient