7 pt-class. |
7 pt-class. |
8 *) |
8 *) |
9 |
9 |
10 signature NOMINAL_DT_RAWPERM = |
10 signature NOMINAL_DT_RAWPERM = |
11 sig |
11 sig |
12 val define_raw_perms: string list -> typ list -> term list -> thm -> theory -> |
12 val define_raw_perms: string list -> typ list -> term list -> thm -> local_theory -> |
13 (term list * thm list * thm list) * theory |
13 (term list * thm list * thm list) * local_theory |
14 end |
14 end |
15 |
15 |
16 |
16 |
17 structure Nominal_Dt_RawPerm: NOMINAL_DT_RAWPERM = |
17 structure Nominal_Dt_RawPerm: NOMINAL_DT_RAWPERM = |
18 struct |
18 struct |
19 |
19 |
20 |
20 |
21 (** proves the two pt-type class properties **) |
21 (** proves the two pt-type class properties **) |
22 |
22 |
23 fun prove_permute_zero lthy induct perm_defs perm_fns = |
23 fun prove_permute_zero induct perm_defs perm_fns lthy = |
24 let |
24 let |
25 val perm_types = map (body_type o fastype_of) perm_fns |
25 val perm_types = map (body_type o fastype_of) perm_fns |
26 val perm_indnames = Datatype_Prop.make_tnames perm_types |
26 val perm_indnames = Datatype_Prop.make_tnames perm_types |
27 |
27 |
28 fun single_goal ((perm_fn, T), x) = |
28 fun single_goal ((perm_fn, T), x) = |
40 Goal.prove lthy perm_indnames [] goals (K tac) |
40 Goal.prove lthy perm_indnames [] goals (K tac) |
41 |> Datatype_Aux.split_conj_thm |
41 |> Datatype_Aux.split_conj_thm |
42 end |
42 end |
43 |
43 |
44 |
44 |
45 fun prove_permute_plus lthy induct perm_defs perm_fns = |
45 fun prove_permute_plus induct perm_defs perm_fns lthy = |
46 let |
46 let |
47 val p = Free ("p", @{typ perm}) |
47 val p = Free ("p", @{typ perm}) |
48 val q = Free ("q", @{typ perm}) |
48 val q = Free ("q", @{typ perm}) |
49 val perm_types = map (body_type o fastype_of) perm_fns |
49 val perm_types = map (body_type o fastype_of) perm_fns |
50 val perm_indnames = Datatype_Prop.make_tnames perm_types |
50 val perm_indnames = Datatype_Prop.make_tnames perm_types |
88 in |
88 in |
89 (Attrib.empty_binding, eq) |
89 (Attrib.empty_binding, eq) |
90 end |
90 end |
91 |
91 |
92 |
92 |
93 fun define_raw_perms full_ty_names tys constrs induct_thm thy = |
93 fun define_raw_perms full_ty_names tys constrs induct_thm lthy = |
94 let |
94 let |
95 val perm_fn_names = full_ty_names |
95 val perm_fn_names = full_ty_names |
96 |> map Long_Name.base_name |
96 |> map Long_Name.base_name |
97 |> map (prefix "permute_") |
97 |> map (prefix "permute_") |
98 |
98 |
100 val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) |
100 val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) |
101 val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names |
101 val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names |
102 |
102 |
103 val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs |
103 val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs |
104 |
104 |
105 val lthy = |
|
106 Class.instantiation (full_ty_names, [], @{sort pt}) thy |
|
107 |
|
108 val ((perm_funs, perm_eq_thms), lthy') = |
|
109 Primrec.add_primrec perm_fn_binds perm_eqs lthy; |
|
110 |
|
111 val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs |
|
112 val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs |
|
113 |
|
114 fun tac _ (_, _, simps) = |
105 fun tac _ (_, _, simps) = |
115 Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) |
106 Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) |
116 |
107 |
117 fun morphism phi (fvs, dfs, simps) = |
108 fun morphism phi (fvs, dfs, simps) = |
118 (map (Morphism.term phi) fvs, |
109 (map (Morphism.term phi) fvs, |
119 map (Morphism.thm phi) dfs, |
110 map (Morphism.thm phi) dfs, |
120 map (Morphism.thm phi) simps); |
111 map (Morphism.thm phi) simps); |
|
112 |
|
113 val ((perm_funs, perm_eq_thms), lthy') = |
|
114 lthy |
|
115 |> Local_Theory.exit_global |
|
116 |> Class.instantiation (full_ty_names, [], @{sort pt}) |
|
117 |> Primrec.add_primrec perm_fn_binds perm_eqs |
|
118 |
|
119 val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy' |
|
120 val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy' |
121 in |
121 in |
122 lthy' |
122 lthy' |
123 |> Class.prove_instantiation_exit_result morphism tac |
123 |> Class.prove_instantiation_exit_result morphism tac |
124 (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms) |
124 (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms) |
|
125 ||> Named_Target.theory_init |
125 end |
126 end |
126 |
127 |
127 |
128 |
128 end (* structure *) |
129 end (* structure *) |
129 |
130 |