equal
deleted
inserted
replaced
35 (* Config *) |
35 (* Config *) |
36 |
36 |
37 type config = { notes: bool }; |
37 type config = { notes: bool }; |
38 val default_config = { notes = true }; |
38 val default_config = { notes = true }; |
39 |
39 |
40 fun define_crel config rep_fun lthy = |
40 fun define_crel (config: config) rep_fun lthy = |
41 let |
41 let |
42 val (qty, rty) = (dest_funT o fastype_of) rep_fun |
42 val (qty, rty) = (dest_funT o fastype_of) rep_fun |
43 val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0) |
43 val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0) |
44 val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph)) |
44 val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph)) |
45 val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty |
45 val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty |
61 [Pretty.str "Reason:", Pretty.brk 2, msg]))] |
61 [Pretty.str "Reason:", Pretty.brk 2, msg]))] |
62 in |
62 in |
63 warning warning_msg |
63 warning warning_msg |
64 end |
64 end |
65 |
65 |
66 fun define_pcrel config crel lthy = |
66 fun define_pcrel (config: config) crel lthy = |
67 let |
67 let |
68 val (fixed_crel, lthy) = yield_singleton Variable.importT_terms crel lthy |
68 val (fixed_crel, lthy) = yield_singleton Variable.importT_terms crel lthy |
69 val [rty', qty] = (binder_types o fastype_of) fixed_crel |
69 val [rty', qty] = (binder_types o fastype_of) fixed_crel |
70 val (param_rel, args) = Lifting_Term.generate_parametrized_relator lthy rty' |
70 val (param_rel, args) = Lifting_Term.generate_parametrized_relator lthy rty' |
71 val rty_raw = (domain_type o range_type o fastype_of) param_rel |
71 val rty_raw = (domain_type o range_type o fastype_of) param_rel |
120 "Most probably a relator_eq rule for one of the involved types is missing."] |
120 "Most probably a relator_eq rule for one of the involved types is missing."] |
121 in |
121 in |
122 error error_msg |
122 error error_msg |
123 end |
123 end |
124 in |
124 in |
125 fun define_pcr_cr_eq config lthy pcr_rel_def = |
125 fun define_pcr_cr_eq (config: config) lthy pcr_rel_def = |
126 let |
126 let |
127 val lhs = (Thm.term_of o Thm.lhs_of) pcr_rel_def |
127 val lhs = (Thm.term_of o Thm.lhs_of) pcr_rel_def |
128 val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type o List.last o binder_types o fastype_of) lhs |
128 val qty_name = |
|
129 (Binding.name o Long_Name.base_name o fst o dest_Type o |
|
130 List.last o binder_types o fastype_of) lhs |
129 val args = (snd o strip_comb) lhs |
131 val args = (snd o strip_comb) lhs |
130 |
132 |
131 fun make_inst var ctxt = |
133 fun make_inst var ctxt = |
132 let |
134 let |
133 val typ = (snd o relation_types o snd o dest_Var) var |
135 val typ = (snd o relation_types o snd o dest_Var) var |
517 opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive |
519 opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive |
518 (in the form "reflp R") |
520 (in the form "reflp R") |
519 opt_par_thm - a parametricity theorem for R |
521 opt_par_thm - a parametricity theorem for R |
520 *) |
522 *) |
521 |
523 |
522 fun setup_by_quotient config quot_thm opt_reflp_thm opt_par_thm lthy = |
524 fun setup_by_quotient (config: config) quot_thm opt_reflp_thm opt_par_thm lthy = |
523 let |
525 let |
524 (**) |
526 (**) |
525 val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy) quot_thm |
527 val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy) quot_thm |
526 (**) |
528 (**) |
527 val (rty, qty) = quot_thm_rty_qty quot_thm |
529 val (rty, qty) = quot_thm_rty_qty quot_thm |