equal
deleted
inserted
replaced
7 |
7 |
8 signature NOMINAL_DT_SUPP = |
8 signature NOMINAL_DT_SUPP = |
9 sig |
9 sig |
10 val prove_supports: Proof.context -> thm list -> term list -> thm list |
10 val prove_supports: Proof.context -> thm list -> term list -> thm list |
11 val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list |
11 val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list |
|
12 |
|
13 val fs_instance: typ list -> string list -> (string * sort) list -> thm list -> |
|
14 local_theory -> local_theory |
12 end |
15 end |
13 |
16 |
14 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = |
17 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = |
15 struct |
18 struct |
16 |
19 |
73 |> singleton (ProofContext.export ctxt' ctxt) |
76 |> singleton (ProofContext.export ctxt' ctxt) |
74 |> Datatype_Aux.split_conj_thm |
77 |> Datatype_Aux.split_conj_thm |
75 |> map zero_var_indexes |
78 |> map zero_var_indexes |
76 end |
79 end |
77 |
80 |
|
81 |
|
82 (* finite supp instances *) |
|
83 |
|
84 fun fs_instance qtys qfull_ty_names tvs qfsupp_thms lthy = |
|
85 let |
|
86 val lthy1 = |
|
87 lthy |
|
88 |> Local_Theory.exit_global |
|
89 |> Class.instantiation (qfull_ty_names, tvs, @{sort fs}) |
|
90 |
|
91 fun tac _ = |
|
92 Class.intro_classes_tac [] THEN |
|
93 (ALLGOALS (resolve_tac qfsupp_thms)) |
|
94 in |
|
95 lthy1 |
|
96 |> Class.prove_instantiation_exit tac |
|
97 |> Named_Target.theory_init |
|
98 end |
|
99 |
|
100 |
78 end (* structure *) |
101 end (* structure *) |
79 |
102 |