28 end |
28 end |
29 |
29 |
30 structure FundefInductiveWrap = |
30 structure FundefInductiveWrap = |
31 struct |
31 struct |
32 |
32 |
|
33 open FundefLib |
33 |
34 |
34 fun inst_forall (Free (n,_)) (_ $ Abs (_, T, b)) = subst_bound (Free (n, T), b) |
35 fun requantify ctxt lfix (qs, t) thm = |
35 | inst_forall t1 t2 = sys_error ((Sign.string_of_term (the_context ()) t1)) |
|
36 |
|
37 fun permute_bounds_in_premises thy [] impl = impl |
|
38 | permute_bounds_in_premises thy ((oldvs, newvs) :: perms) impl = |
|
39 let |
36 let |
40 val (prem, concl) = dest_implies (cprop_of impl) |
37 val thy = theory_of_thm (print thm) |
41 |
38 val frees = frees_in_term ctxt t |
42 val newprem = term_of prem |
39 |> remove (op =) lfix |
43 |> fold inst_forall oldvs |
40 val vars = Term.add_vars (prop_of thm) [] |> rev |
44 |> fold_rev mk_forall newvs |
41 |
45 |> cterm_of thy |
42 val varmap = frees ~~ vars |
46 in |
43 in |
47 assume newprem |
44 fold_rev (fn Free (n, T) => |
48 |> fold (forall_elim o cterm_of thy) newvs |
45 forall_intr_rename (n, cterm_of thy (Var (the_default (("",0), T) (AList.lookup (op =) varmap (n, T)))))) |
49 |> fold_rev (forall_intr o cterm_of thy) oldvs |
46 qs |
50 |> implies_elim impl |
47 thm |
51 |> permute_bounds_in_premises thy perms |
48 end |
52 |> implies_intr newprem |
49 |
53 end |
50 |
54 |
|
55 |
51 |
56 fun inductive_def defs (((R, T), mixfix), lthy) = |
52 fun inductive_def defs (((R, T), mixfix), lthy) = |
57 let |
53 let |
58 fun wrap1 thy = |
54 val qdefs = map dest_all_all defs |
59 let |
55 |
60 val thy = Sign.add_consts_i [(R, T, mixfix)] thy |
56 val (lthy, {intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], ...}) = |
61 val RC = Const (Sign.full_name thy R, T) |
57 InductivePackage.add_inductive_i true (*verbose*) |
|
58 "" (* no altname *) |
|
59 false (* no coind *) |
|
60 false (* elims, please *) |
|
61 false (* induction thm please *) |
|
62 [(R, SOME T, NoSyn)] (* the relation *) |
|
63 [] (* no parameters *) |
|
64 (map (fn t => (("", []), t)) defs) (* the intros *) |
|
65 [] (* no special monos *) |
|
66 lthy |
62 |
67 |
63 val cdefs = map (Pattern.rewrite_term thy [(Free (R, T), RC)] []) defs |
68 val thy = ProofContext.theory_of lthy |
64 val qdefs = map dest_all_all cdefs |
69 |
|
70 fun inst qdef intr_gen = |
|
71 intr_gen |
|
72 |> Thm.freezeT |
|
73 |> requantify lthy (R, T) qdef |
|
74 |
|
75 val intrs = map2 inst qdefs intrs_gen |
|
76 |
|
77 val elim = elim_gen |
|
78 |> Thm.freezeT |
|
79 |> forall_intr_vars (* FIXME... *) |
65 |
80 |
66 val (thy, {intrs = intrs_gen, elims = [elim_gen], ...}) = |
81 val Rdef_real = prop_of (Thm.freezeT elim_gen) |
67 OldInductivePackage.add_inductive_i true (*verbose*) |
82 |> Logic.dest_implies |> fst |
68 false (* dont add_consts *) |
83 |> Term.strip_comb |> snd |> hd (* Trueprop *) |
69 "" (* no altname *) |
84 |> Term.strip_comb |> fst |
70 false (* no coind *) |
|
71 false (* elims, please *) |
|
72 false (* induction thm please *) |
|
73 [RC] (* the constant *) |
|
74 (map (fn (_,t) => (("", t),[])) qdefs) (* the intros *) |
|
75 [] (* no special monos *) |
|
76 thy |
|
77 |
|
78 val perms = map (fn (qs, t) => ((term_frees t) inter qs, qs)) qdefs |
|
79 |
|
80 fun inst (qs, _) intr_gen = |
|
81 intr_gen |
|
82 |> Thm.freezeT |
|
83 |> fold_rev (forall_intr o (fn Free (n, T) => cterm_of thy (Var ((n,0), T)))) qs |
|
84 |
|
85 |
|
86 val a = cterm_of thy (Free ("a0123", HOLogic.dest_setT T)) (* Let's just hope there are no clashes :-} *) |
|
87 val P = cterm_of thy (Free ("P0123", HOLogic.boolT)) |
|
88 |
|
89 val intrs = map2 inst qdefs intrs_gen |
|
90 |
|
91 val elim = elim_gen |
|
92 |> Thm.freezeT |
|
93 |> forall_intr_vars (* FIXME... *) |
|
94 |> forall_elim a |
|
95 |> forall_elim P |
|
96 |> permute_bounds_in_premises thy (([],[]) :: perms) |
|
97 |> forall_intr P |
|
98 |> forall_intr a |
|
99 in |
|
100 ((RC, (intrs, elim)), thy) |
|
101 end |
|
102 |
|
103 val ((RC, (intrs, elim)), lthy) = LocalTheory.theory_result wrap1 lthy |
|
104 in |
85 in |
105 (intrs, (RC, elim, lthy)) |
86 (intrs, (Rdef_real, elim, lthy)) |
106 end |
87 end |
107 |
88 |
108 |
|
109 end |
89 end |
110 |
90 |