author | wenzelm |
Sat, 21 Jan 2006 23:02:14 +0100 | |
changeset 18728 | 6790126ab5f6 |
parent 18669 | cd6d6baf0411 |
child 18894 | 9c8c60853966 |
permissions | -rw-r--r-- |
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/element.ML |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
4 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
5 |
Explicit data structures for some Isar language elements. |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
6 |
*) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
7 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
8 |
signature ELEMENT = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
9 |
sig |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
10 |
datatype ('typ, 'term, 'fact) ctxt = |
18669 | 11 |
Fixes of (string * 'typ option * mixfix) list | |
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
12 |
Constrains of (string * 'typ) list | |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
13 |
Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list | |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
14 |
Defines of ((string * Attrib.src list) * ('term * 'term list)) list | |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
15 |
Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
16 |
type context (*= (string, string, thmref) ctxt*) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
17 |
type context_i (*= (typ, term, thm list) ctxt*) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
18 |
val map_ctxt: {name: string -> string, |
18669 | 19 |
var: string * mixfix -> string * mixfix, |
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
20 |
typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c, |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
21 |
attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
22 |
val map_ctxt_values: (typ -> typ) -> (term -> term) -> (thm -> thm) -> context_i -> context_i |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
23 |
val pretty_ctxt: ProofContext.context -> context_i -> Pretty.T list |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
24 |
val rename: (string * (string * mixfix option)) list -> string -> string |
18669 | 25 |
val rename_var: (string * (string * mixfix option)) list -> string * mixfix -> string * mixfix |
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
26 |
val rename_term: (string * (string * mixfix option)) list -> term -> term |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
27 |
val rename_thm: (string * (string * mixfix option)) list -> thm -> thm |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
28 |
val rename_ctxt: (string * (string * mixfix option)) list -> context_i -> context_i |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
29 |
val instT_type: typ Symtab.table -> typ -> typ |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
30 |
val instT_term: typ Symtab.table -> term -> term |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
31 |
val instT_thm: theory -> typ Symtab.table -> thm -> thm |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
32 |
val instT_ctxt: theory -> typ Symtab.table -> context_i -> context_i |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
33 |
val inst_term: typ Symtab.table * term Symtab.table -> term -> term |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
34 |
val inst_thm: theory -> typ Symtab.table * term Symtab.table -> thm -> thm |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
35 |
val inst_ctxt: theory -> typ Symtab.table * term Symtab.table -> context_i -> context_i |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
36 |
end; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
37 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
38 |
structure Element: ELEMENT = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
39 |
struct |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
40 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
41 |
(** context elements **) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
42 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
43 |
(* datatype ctxt *) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
44 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
45 |
datatype ('typ, 'term, 'fact) ctxt = |
18669 | 46 |
Fixes of (string * 'typ option * mixfix) list | |
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
47 |
Constrains of (string * 'typ) list | |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
48 |
Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list | |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
49 |
Defines of ((string * Attrib.src list) * ('term * 'term list)) list | |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
50 |
Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
51 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
52 |
type context = (string, string, thmref) ctxt; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
53 |
type context_i = (typ, term, thm list) ctxt; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
54 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
55 |
fun map_ctxt {name, var, typ, term, fact, attrib} = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
56 |
fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
57 |
let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end)) |
18669 | 58 |
| Constrains xs => Constrains (xs |> map (fn (x, T) => (#1 (var (x, NoSyn)), typ T))) |
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
59 |
| Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) => |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
60 |
((name a, map attrib atts), propps |> map (fn (t, (ps, qs)) => |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
61 |
(term t, (map term ps, map term qs)))))) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
62 |
| Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
63 |
((name a, map attrib atts), (term t, map term ps)))) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
64 |
| Notes facts => Notes (facts |> map (fn ((a, atts), bs) => |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
65 |
((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts))))); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
66 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
67 |
fun map_ctxt_values typ term thm = map_ctxt |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
68 |
{name = I, var = I, typ = typ, term = term, fact = map thm, |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
69 |
attrib = Args.map_values I typ term thm}; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
70 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
71 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
72 |
(* pretty_ctxt *) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
73 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
74 |
fun pretty_ctxt ctxt = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
75 |
let |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
76 |
val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
77 |
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; |
18606 | 78 |
val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt; |
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
79 |
val prt_atts = Args.pretty_attribs ctxt; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
80 |
|
18669 | 81 |
fun prt_mixfix mx = |
82 |
let val s = Syntax.string_of_mixfix mx |
|
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
83 |
in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end; |
18669 | 84 |
fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 :: |
85 |
prt_typ T :: Pretty.brk 1 :: prt_mixfix mx) |
|
86 |
| prt_fix (x, NONE, mx) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_mixfix mx); |
|
87 |
fun prt_constrain (x, T) = prt_fix (x, SOME T, NoSyn); |
|
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
88 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
89 |
fun prt_name name = Pretty.str (ProofContext.extern_thm ctxt name); |
18606 | 90 |
fun prt_name_atts (name, atts) sep = |
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
91 |
if name = "" andalso null atts then [] |
18606 | 92 |
else [Pretty.block (Pretty.breaks (prt_name name :: prt_atts atts @ [Pretty.str sep]))]; |
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
93 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
94 |
fun prt_asm (a, ts) = |
18606 | 95 |
Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts)); |
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
96 |
fun prt_def (a, (t, _)) = |
18606 | 97 |
Pretty.block (Pretty.breaks (prt_name_atts a ":" @ [prt_term t])); |
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
98 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
99 |
fun prt_fact (ths, []) = map prt_thm ths |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
100 |
| prt_fact (ths, atts) = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
101 |
Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) :: prt_atts atts; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
102 |
fun prt_note (a, ths) = |
18606 | 103 |
Pretty.block (Pretty.breaks (List.concat (prt_name_atts a "=" :: map prt_fact ths))); |
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
104 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
105 |
fun items _ [] = [] |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
106 |
| items prfx (x :: xs) = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
107 |
Pretty.block [Pretty.str prfx, Pretty.brk 1, x] :: items " and" xs; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
108 |
in |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
109 |
fn Fixes fixes => items "fixes" (map prt_fix fixes) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
110 |
| Constrains xs => items "constrains" (map prt_constrain xs) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
111 |
| Assumes asms => items "assumes" (map prt_asm asms) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
112 |
| Defines defs => items "defines" (map prt_def defs) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
113 |
| Notes facts => items "notes" (map prt_note facts) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
114 |
end; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
115 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
116 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
117 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
118 |
(** logical operations **) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
119 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
120 |
(* derived rules *) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
121 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
122 |
fun instantiate_tfrees thy subst = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
123 |
let |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
124 |
val certT = Thm.ctyp_of thy; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
125 |
fun inst vs (a, T) = AList.lookup (op =) vs a |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
126 |
|> Option.map (fn v => (certT (TVar v), certT T)); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
127 |
in |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
128 |
Drule.tvars_intr_list (map fst subst) #-> |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
129 |
(fn vs => Thm.instantiate (List.mapPartial (inst vs) subst, [])) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
130 |
end; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
131 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
132 |
fun instantiate_frees thy subst = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
133 |
let val cert = Thm.cterm_of thy in |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
134 |
Drule.forall_intr_list (map (cert o Free o fst) subst) #> |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
135 |
Drule.forall_elim_list (map (cert o snd) subst) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
136 |
end; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
137 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
138 |
fun hyps_rule rule th = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
139 |
let |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
140 |
val cterm_rule = Thm.reflexive #> rule #> Thm.cprop_of #> Drule.dest_equals #> #1; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
141 |
val {hyps, ...} = Thm.crep_thm th; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
142 |
in |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
143 |
Drule.implies_elim_list |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
144 |
(rule (Drule.implies_intr_list hyps th)) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
145 |
(map (Thm.assume o cterm_rule) hyps) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
146 |
end; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
147 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
148 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
149 |
(* renaming *) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
150 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
151 |
fun rename ren x = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
152 |
(case AList.lookup (op =) ren (x: string) of |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
153 |
NONE => x |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
154 |
| SOME (x', _) => x'); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
155 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
156 |
fun rename_var ren (x, mx) = |
18669 | 157 |
(case (AList.lookup (op =) ren (x: string), mx) of |
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
158 |
(NONE, _) => (x, mx) |
18669 | 159 |
| (SOME (x', NONE), Structure) => (x', mx) |
160 |
| (SOME (x', SOME _), Structure) => |
|
161 |
error ("Attempt to change syntax of structure parameter " ^ quote x) |
|
162 |
| (SOME (x', NONE), _) => (x', NoSyn) |
|
163 |
| (SOME (x', SOME mx'), _) => (x', mx')); |
|
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
164 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
165 |
fun rename_term ren (Free (x, T)) = Free (rename ren x, T) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
166 |
| rename_term ren (t $ u) = rename_term ren t $ rename_term ren u |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
167 |
| rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
168 |
| rename_term _ a = a; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
169 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
170 |
fun rename_thm ren th = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
171 |
let |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
172 |
val subst = Drule.frees_of th |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
173 |
|> List.mapPartial (fn (x, T) => |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
174 |
let val x' = rename ren x |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
175 |
in if x = x' then NONE else SOME ((x, T), (Free (x', T))) end); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
176 |
in |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
177 |
if null subst then th |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
178 |
else th |> hyps_rule (instantiate_frees (Thm.theory_of_thm th) subst) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
179 |
end; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
180 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
181 |
fun rename_ctxt ren = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
182 |
map_ctxt_values I (rename_term ren) (rename_thm ren) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
183 |
#> map_ctxt {name = I, typ = I, term = I, fact = I, attrib = I, var = rename_var ren}; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
184 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
185 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
186 |
(* type instantiation *) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
187 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
188 |
fun instT_type env = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
189 |
if Symtab.is_empty env then I |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
190 |
else Term.map_type_tfree (fn (x, S) => the_default (TFree (x, S)) (Symtab.lookup env x)); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
191 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
192 |
fun instT_term env = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
193 |
if Symtab.is_empty env then I |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
194 |
else Term.map_term_types (instT_type env); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
195 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
196 |
fun instT_subst env th = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
197 |
Drule.tfrees_of th |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
198 |
|> List.mapPartial (fn (a, S) => |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
199 |
let |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
200 |
val T = TFree (a, S); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
201 |
val T' = the_default T (Symtab.lookup env a); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
202 |
in if T = T' then NONE else SOME (a, T') end); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
203 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
204 |
fun instT_thm thy env th = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
205 |
if Symtab.is_empty env then th |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
206 |
else |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
207 |
let val subst = instT_subst env th |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
208 |
in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
209 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
210 |
fun instT_ctxt thy env = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
211 |
map_ctxt_values (instT_type env) (instT_term env) (instT_thm thy env); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
212 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
213 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
214 |
(* type and term instantiation *) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
215 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
216 |
fun inst_term (envT, env) = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
217 |
if Symtab.is_empty env then instT_term envT |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
218 |
else |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
219 |
let |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
220 |
val instT = instT_type envT; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
221 |
fun inst (Const (x, T)) = Const (x, instT T) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
222 |
| inst (Free (x, T)) = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
223 |
(case Symtab.lookup env x of |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
224 |
NONE => Free (x, instT T) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
225 |
| SOME t => t) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
226 |
| inst (Var (xi, T)) = Var (xi, instT T) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
227 |
| inst (b as Bound _) = b |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
228 |
| inst (Abs (x, T, t)) = Abs (x, instT T, inst t) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
229 |
| inst (t $ u) = inst t $ inst u; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
230 |
in Envir.beta_norm o inst end; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
231 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
232 |
fun inst_thm thy (envT, env) th = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
233 |
if Symtab.is_empty env then instT_thm thy envT th |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
234 |
else |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
235 |
let |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
236 |
val substT = instT_subst envT th; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
237 |
val subst = Drule.frees_of th |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
238 |
|> List.mapPartial (fn (x, T) => |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
239 |
let |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
240 |
val T' = instT_type envT T; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
241 |
val t = Free (x, T'); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
242 |
val t' = the_default t (Symtab.lookup env x); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
243 |
in if t aconv t' then NONE else SOME ((x, T'), t') end); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
244 |
in |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
245 |
if null substT andalso null subst then th |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
246 |
else th |> hyps_rule |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
247 |
(instantiate_tfrees thy substT #> |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
248 |
instantiate_frees thy subst #> |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
249 |
Drule.fconv_rule (Thm.beta_conversion true)) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
250 |
end; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
251 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
252 |
fun inst_ctxt thy envs = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
253 |
map_ctxt_values (instT_type (#1 envs)) (inst_term envs) (inst_thm thy envs); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
254 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
255 |
end; |