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