author | wenzelm |
Tue, 25 Apr 2006 22:23:41 +0200 | |
changeset 19466 | 29bc35832a77 |
parent 19305 | 5c16895d548b |
child 19482 | 9f11af8f7ef9 |
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 |
19259 | 10 |
datatype ('typ, 'term) stmt = |
11 |
Shows of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list | |
|
12 |
Obtains of (string * ((string * 'typ option) list * 'term list)) list |
|
13 |
type statement (*= (string, string) stmt*) |
|
14 |
type statement_i (*= (typ, term) stmt*) |
|
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
15 |
datatype ('typ, 'term, 'fact) ctxt = |
18669 | 16 |
Fixes of (string * 'typ option * mixfix) list | |
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
17 |
Constrains of (string * 'typ) list | |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
18 |
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
|
19 |
Defines of ((string * Attrib.src list) * ('term * 'term list)) list | |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
20 |
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
|
21 |
type context (*= (string, string, thmref) ctxt*) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
22 |
type context_i (*= (typ, term, thm list) ctxt*) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
23 |
val map_ctxt: {name: string -> string, |
18669 | 24 |
var: string * mixfix -> string * mixfix, |
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
25 |
typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c, |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
26 |
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
|
27 |
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
|
28 |
val rename: (string * (string * mixfix option)) list -> string -> string |
18669 | 29 |
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
|
30 |
val rename_term: (string * (string * mixfix option)) list -> term -> term |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
31 |
val rename_thm: (string * (string * mixfix option)) list -> thm -> thm |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
32 |
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
|
33 |
val instT_type: typ Symtab.table -> typ -> typ |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
34 |
val instT_term: typ Symtab.table -> term -> term |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
35 |
val instT_thm: theory -> typ Symtab.table -> thm -> thm |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
36 |
val instT_ctxt: theory -> typ Symtab.table -> context_i -> context_i |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
37 |
val inst_term: typ Symtab.table * term Symtab.table -> term -> term |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
38 |
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
|
39 |
val inst_ctxt: theory -> typ Symtab.table * term Symtab.table -> context_i -> context_i |
19259 | 40 |
val pretty_stmt: ProofContext.context -> statement_i -> Pretty.T list |
41 |
val pretty_ctxt: ProofContext.context -> context_i -> Pretty.T list |
|
19267 | 42 |
val pretty_statement: ProofContext.context -> string -> thm -> Pretty.T |
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
43 |
end; |
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 |
structure Element: ELEMENT = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
46 |
struct |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
47 |
|
19259 | 48 |
|
49 |
(** conclusions **) |
|
50 |
||
51 |
datatype ('typ, 'term) stmt = |
|
52 |
Shows of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list | |
|
53 |
Obtains of (string * ((string * 'typ option) list * 'term list)) list; |
|
54 |
||
55 |
type statement = (string, string) stmt; |
|
56 |
type statement_i = (typ, term) stmt; |
|
57 |
||
58 |
||
59 |
||
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
60 |
(** context elements **) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
61 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
62 |
(* datatype ctxt *) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
63 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
64 |
datatype ('typ, 'term, 'fact) ctxt = |
18669 | 65 |
Fixes of (string * 'typ option * mixfix) list | |
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
66 |
Constrains of (string * 'typ) list | |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
67 |
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
|
68 |
Defines of ((string * Attrib.src list) * ('term * 'term list)) list | |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
69 |
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
|
70 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
71 |
type context = (string, string, thmref) ctxt; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
72 |
type context_i = (typ, term, thm list) 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 map_ctxt {name, var, typ, term, fact, attrib} = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
75 |
fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
76 |
let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end)) |
18669 | 77 |
| 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
|
78 |
| Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) => |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
79 |
((name a, map attrib atts), propps |> map (fn (t, (ps, qs)) => |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
80 |
(term t, (map term ps, map term qs)))))) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
81 |
| Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
82 |
((name a, map attrib atts), (term t, map term ps)))) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
83 |
| Notes facts => Notes (facts |> map (fn ((a, atts), bs) => |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
84 |
((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
|
85 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
86 |
fun map_ctxt_values typ term thm = map_ctxt |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
87 |
{name = I, var = I, typ = typ, term = term, fact = map thm, |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
88 |
attrib = Args.map_values I typ term thm}; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
89 |
|
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 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
92 |
(** logical operations **) |
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 |
(* derived rules *) |
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 instantiate_tfrees thy subst = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
97 |
let |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
98 |
val certT = Thm.ctyp_of thy; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
99 |
fun inst vs (a, T) = AList.lookup (op =) vs a |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
100 |
|> Option.map (fn v => (certT (TVar v), certT T)); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
101 |
in |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
102 |
Drule.tvars_intr_list (map fst subst) #-> |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
103 |
(fn vs => Thm.instantiate (List.mapPartial (inst vs) subst, [])) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
104 |
end; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
105 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
106 |
fun instantiate_frees thy subst = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
107 |
let val cert = Thm.cterm_of thy in |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
108 |
Drule.forall_intr_list (map (cert o Free o fst) subst) #> |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
109 |
Drule.forall_elim_list (map (cert o snd) subst) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
110 |
end; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
111 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
112 |
fun hyps_rule rule th = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
113 |
let |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
114 |
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
|
115 |
val {hyps, ...} = Thm.crep_thm th; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
116 |
in |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
117 |
Drule.implies_elim_list |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
118 |
(rule (Drule.implies_intr_list hyps th)) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
119 |
(map (Thm.assume o cterm_rule) hyps) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
120 |
end; |
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 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
123 |
(* renaming *) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
124 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
125 |
fun rename ren x = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
126 |
(case AList.lookup (op =) ren (x: string) of |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
127 |
NONE => x |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
128 |
| SOME (x', _) => x'); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
129 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
130 |
fun rename_var ren (x, mx) = |
18669 | 131 |
(case (AList.lookup (op =) ren (x: string), mx) of |
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
132 |
(NONE, _) => (x, mx) |
18669 | 133 |
| (SOME (x', NONE), Structure) => (x', mx) |
134 |
| (SOME (x', SOME _), Structure) => |
|
135 |
error ("Attempt to change syntax of structure parameter " ^ quote x) |
|
136 |
| (SOME (x', NONE), _) => (x', NoSyn) |
|
137 |
| (SOME (x', SOME mx'), _) => (x', mx')); |
|
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
138 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
139 |
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
|
140 |
| 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
|
141 |
| 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
|
142 |
| rename_term _ a = a; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
143 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
144 |
fun rename_thm ren th = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
145 |
let |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
146 |
val subst = Drule.frees_of th |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
147 |
|> List.mapPartial (fn (x, T) => |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
148 |
let val x' = rename ren x |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
149 |
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
|
150 |
in |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
151 |
if null subst then th |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
152 |
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
|
153 |
end; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
154 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
155 |
fun rename_ctxt ren = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
156 |
map_ctxt_values I (rename_term ren) (rename_thm ren) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
157 |
#> 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
|
158 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
159 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
160 |
(* type instantiation *) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
161 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
162 |
fun instT_type env = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
163 |
if Symtab.is_empty env then I |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
164 |
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
|
165 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
166 |
fun instT_term env = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
167 |
if Symtab.is_empty env then I |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
168 |
else Term.map_term_types (instT_type env); |
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 instT_subst env th = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
171 |
Drule.tfrees_of th |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
172 |
|> List.mapPartial (fn (a, S) => |
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 T = TFree (a, S); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
175 |
val T' = the_default T (Symtab.lookup env a); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
176 |
in if T = T' then NONE else SOME (a, T') end); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
177 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
178 |
fun instT_thm thy env th = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
179 |
if Symtab.is_empty env then th |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
180 |
else |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
181 |
let val subst = instT_subst env th |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
182 |
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
|
183 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
184 |
fun instT_ctxt thy env = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
185 |
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
|
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 and term 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 inst_term (envT, env) = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
191 |
if Symtab.is_empty env then instT_term envT |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
192 |
else |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
193 |
let |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
194 |
val instT = instT_type envT; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
195 |
fun inst (Const (x, T)) = Const (x, instT T) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
196 |
| inst (Free (x, T)) = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
197 |
(case Symtab.lookup env x of |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
198 |
NONE => Free (x, instT T) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
199 |
| SOME t => t) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
200 |
| inst (Var (xi, T)) = Var (xi, instT T) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
201 |
| inst (b as Bound _) = b |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
202 |
| inst (Abs (x, T, t)) = Abs (x, instT T, inst t) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
203 |
| inst (t $ u) = inst t $ inst u; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
204 |
in Envir.beta_norm o inst 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 inst_thm thy (envT, env) th = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
207 |
if Symtab.is_empty env then instT_thm thy envT 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 |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
210 |
val substT = instT_subst envT th; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
211 |
val subst = Drule.frees_of th |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
212 |
|> List.mapPartial (fn (x, T) => |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
213 |
let |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
214 |
val T' = instT_type envT T; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
215 |
val t = Free (x, T'); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
216 |
val t' = the_default t (Symtab.lookup env x); |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
217 |
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
|
218 |
in |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
219 |
if null substT andalso null subst then th |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
220 |
else th |> hyps_rule |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
221 |
(instantiate_tfrees thy substT #> |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
222 |
instantiate_frees thy subst #> |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
223 |
Drule.fconv_rule (Thm.beta_conversion true)) |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
224 |
end; |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
225 |
|
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
226 |
fun inst_ctxt thy envs = |
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
227 |
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
|
228 |
|
18894 | 229 |
|
230 |
||
19259 | 231 |
(** pretty printing **) |
232 |
||
19267 | 233 |
fun pretty_items _ _ [] = [] |
234 |
| pretty_items keyword sep (x :: ys) = |
|
235 |
Pretty.block [Pretty.keyword keyword, Pretty.brk 1, x] :: |
|
236 |
map (fn y => Pretty.block [Pretty.str " ", Pretty.keyword sep, Pretty.brk 1, y]) ys; |
|
19259 | 237 |
|
238 |
fun pretty_name_atts ctxt (name, atts) sep = |
|
239 |
if name = "" andalso null atts then [] |
|
240 |
else [Pretty.block (Pretty.breaks (Pretty.str (ProofContext.extern_thm ctxt name) :: |
|
241 |
Args.pretty_attribs ctxt atts @ [Pretty.str sep]))]; |
|
242 |
||
243 |
||
244 |
(* pretty_stmt *) |
|
245 |
||
246 |
fun pretty_stmt ctxt = |
|
247 |
let |
|
248 |
val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; |
|
249 |
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; |
|
19267 | 250 |
val prt_terms = separate (Pretty.keyword "and") o map prt_term; |
19259 | 251 |
val prt_name_atts = pretty_name_atts ctxt; |
252 |
||
253 |
fun prt_show (a, ts) = |
|
19267 | 254 |
Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts))); |
19259 | 255 |
|
256 |
fun prt_var (x, SOME T) = Pretty.block [Pretty.str (x ^ " ::"), Pretty.brk 1, prt_typ T] |
|
257 |
| prt_var (x, NONE) = Pretty.str x; |
|
258 |
||
19267 | 259 |
fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts)) |
19259 | 260 |
| prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks |
19267 | 261 |
(map prt_var xs @ [Pretty.keyword "where"] @ prt_terms ts)); |
19259 | 262 |
in |
19267 | 263 |
fn Shows shows => pretty_items "shows" "and" (map prt_show shows) |
264 |
| Obtains obtains => pretty_items "obtains" "|" (map prt_obtain obtains) |
|
19259 | 265 |
end; |
266 |
||
18894 | 267 |
|
19259 | 268 |
(* pretty_ctxt *) |
269 |
||
270 |
fun pretty_ctxt ctxt = |
|
271 |
let |
|
272 |
val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; |
|
273 |
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; |
|
274 |
val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt; |
|
275 |
val prt_name_atts = pretty_name_atts ctxt; |
|
276 |
||
19267 | 277 |
fun prt_mixfix NoSyn = [] |
278 |
| prt_mixfix mx = [Pretty.brk 2, Syntax.pretty_mixfix mx]; |
|
279 |
||
19259 | 280 |
fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 :: |
281 |
prt_typ T :: Pretty.brk 1 :: prt_mixfix mx) |
|
282 |
| prt_fix (x, NONE, mx) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_mixfix mx); |
|
283 |
fun prt_constrain (x, T) = prt_fix (x, SOME T, NoSyn); |
|
18894 | 284 |
|
19259 | 285 |
fun prt_asm (a, ts) = |
286 |
Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts)); |
|
287 |
fun prt_def (a, (t, _)) = |
|
288 |
Pretty.block (Pretty.breaks (prt_name_atts a ":" @ [prt_term t])); |
|
289 |
||
290 |
fun prt_fact (ths, []) = map prt_thm ths |
|
291 |
| prt_fact (ths, atts) = Pretty.enclose "(" ")" |
|
292 |
(Pretty.breaks (map prt_thm ths)) :: Args.pretty_attribs ctxt atts; |
|
293 |
fun prt_note (a, ths) = |
|
294 |
Pretty.block (Pretty.breaks (List.concat (prt_name_atts a "=" :: map prt_fact ths))); |
|
295 |
in |
|
19267 | 296 |
fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes) |
297 |
| Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs) |
|
298 |
| Assumes asms => pretty_items "assumes" "and" (map prt_asm asms) |
|
299 |
| Defines defs => pretty_items "defines" "and" (map prt_def defs) |
|
300 |
| Notes facts => pretty_items "notes" "and" (map prt_note facts) |
|
19259 | 301 |
end; |
18894 | 302 |
|
19267 | 303 |
|
304 |
(* pretty_statement *) |
|
305 |
||
306 |
local |
|
307 |
||
308 |
fun thm_name kind th prts = |
|
309 |
let val head = |
|
310 |
(case #1 (Thm.get_name_tags th) of |
|
311 |
"" => Pretty.command kind |
|
312 |
| a => Pretty.block [Pretty.command kind, Pretty.brk 1, Pretty.str (Sign.base_name a ^ ":")]) |
|
313 |
in Pretty.block (Pretty.fbreaks (head :: prts)) end; |
|
314 |
||
315 |
fun obtain prop ctxt = |
|
316 |
let |
|
317 |
val xs = ProofContext.rename_frees ctxt [] (Logic.strip_params prop); |
|
318 |
val args = rev (map Free xs); |
|
319 |
val As = Logic.strip_assums_hyp prop |> map (fn t => Term.subst_bounds (args, t)); |
|
320 |
val ctxt' = ctxt |> fold ProofContext.declare_term args; |
|
321 |
in (("", (map (apsnd SOME) xs, As)), ctxt') end; |
|
322 |
||
323 |
in |
|
324 |
||
325 |
fun pretty_statement ctxt kind raw_th = |
|
326 |
let |
|
327 |
val thy = ProofContext.theory_of ctxt; |
|
328 |
val th = Goal.norm_hhf raw_th; |
|
329 |
||
330 |
fun standard_thesis t = |
|
331 |
let |
|
332 |
val C = ObjectLogic.drop_judgment thy (Thm.concl_of th); |
|
19466 | 333 |
val C' = Var ((AutoBind.thesisN, Thm.maxidx_of th + 1), Term.fastype_of C); |
19267 | 334 |
in Term.subst_atomic [(C, C')] t end; |
335 |
||
336 |
val raw_prop = |
|
337 |
Thm.prop_of th |
|
338 |
|> singleton (ProofContext.monomorphic ctxt) |
|
339 |
|> K (ObjectLogic.is_elim th) ? standard_thesis |
|
340 |
|> Term.zero_var_indexes; |
|
341 |
||
342 |
val vars = Term.add_vars raw_prop []; |
|
343 |
val frees = ProofContext.rename_frees ctxt [raw_prop] (map (apfst fst) vars); |
|
19305 | 344 |
val fixes = rev (filter_out (fn (x, _) => x = AutoBind.thesisN) frees); |
19267 | 345 |
|
346 |
val prop = Term.instantiate ([], vars ~~ map Free frees) raw_prop; |
|
347 |
val (prems, concl) = Logic.strip_horn prop; |
|
348 |
val thesis = ObjectLogic.fixed_judgment thy AutoBind.thesisN; |
|
349 |
val (asms, cases) = take_suffix (fn prem => thesis aconv Logic.strip_assums_concl prem) prems; |
|
350 |
in |
|
351 |
pretty_ctxt ctxt (Fixes (map (fn (x, T) => (x, SOME T, NoSyn)) fixes)) @ |
|
352 |
pretty_ctxt ctxt (Assumes (map (fn t => (("", []), [(t, ([], []))])) asms)) @ |
|
353 |
pretty_stmt ctxt |
|
354 |
(if null cases then Shows [(("", []), [(concl, ([], []))])] |
|
355 |
else Obtains (#1 (fold_map obtain cases (ctxt |> ProofContext.declare_term prop)))) |
|
356 |
end |> thm_name kind raw_th; |
|
357 |
||
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset
|
358 |
end; |
19267 | 359 |
|
360 |
end; |