nominal2: comparison Quot/quotient

equal deleted inserted replaced

-:243a5ceaa088
+:17ca92ab4660
 *)
 signature QUOTIENT_TYPE =
 sig
 val quotient_type: ((string list * binding * mixfix) * (typ * term)) list
 -> Proof.context -> Proof.state
 val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list
 -> Proof.context -> Proof.state
 end;
 structure Quotient_Type: QUOTIENT_TYPE =
 struct
 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
 val ((rep, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2
 (* quot_type theorem *)
 val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, equiv_thm, typedef_info) lthy3
 (* quotient theorem *)
 val quotient_thm = typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_thm) lthy3
 val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
 (* name equivalence theorem *)
 val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
 val illegal_rel_vars =
 if null rel_vars andalso null rel_tvars then []
 else [qty_str ^ "illegal schematic variable(s) in the relation."]
 val dup_vs =
 (case duplicates (op =) vs of
 [] => []
 | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups])
 val extra_rty_tfrees =
 (case subtract (op =) vs rty_tfreesT of
 [] => []
 | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras])
 val extra_rel_tfrees =
 (case subtract (op =) vs rel_tfrees of
 [] => []
 | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras])
 val illegal_rel_frees =
 (case rel_frees of
 [] => []
 | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs])
 val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees
 in
 it opens a proof-state in which one has to show that the
 relations are equivalence relations
 *)
 fun quotient_type quot_list lthy =
 let
 (* sanity check *)
 val _ = List.app sanity_check quot_list
 val _ = List.app (map_check lthy) quot_list
 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_quotient_type (quot_list ~~ thms) lthy |> snd
 in
 theorem after_qed goals lthy
 end
 fun quotient_type_cmd specs lthy =
 let
 fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy =
 let
 (* new parsing with proper declaration *)
 val rty = Syntax.read_typ lthy rty_str
 val lthy1 = Variable.declare_typ rty lthy
 val pre_rel = Syntax.parse_term lthy1 rel_str
 val pre_rel' = Syntax.type_constraint (rty --> rty --> @{typ bool}) pre_rel
 val rel = Syntax.check_term lthy1 pre_rel'
 val lthy2 = Variable.declare_term rel lthy1
 (* old parsing *)
 (* val rty = Syntax.read_typ lthy rty_str
 val rel = Syntax.read_term lthy rel_str *)
 in
 (((vs, qty_name, mx), (rty, rel)), lthy2)
 end
 val (spec', lthy') = fold_map parse_spec specs lthy
 in
 quotient_type spec' lthy'
 end
 val quotspec_parser =
 OuterParse.and_list1
 ((OuterParse.type_args -- OuterParse.binding) --
 OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) --
 (OuterParse.$$$ "/" |-- OuterParse.term))
 val _ = OuterKeyword.keyword "/"
 val _ =
 OuterSyntax.local_theory_to_proof "quotient_type"
 "quotient type definitions (require equivalence proofs)"
 OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
 end; (* structure *)

changeset 1128	17ca92ab4660
parent 1124	4a4c714ff795
child 1152	fbaebf08c1bd