author | Thomas Sewell <tsewell@nicta.com.au> |
Thu, 10 Sep 2009 16:38:18 +1000 | |
changeset 32745 | 192d58483fdf |
parent 32744 | 50406c4951d9 |
permissions | -rw-r--r-- |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/ntuple_support.ML |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
2 |
Author: Thomas Sewell, NICTA |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
3 |
|
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
4 |
Support for defining instances of tuple-like types and supplying |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
5 |
introduction rules needed by the record package. |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
6 |
*) |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
7 |
|
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
8 |
|
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
9 |
signature ISTUPLE_SUPPORT = |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
10 |
sig |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
11 |
val add_istuple_type: bstring * string list -> (typ * typ) -> theory -> |
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
12 |
(term * term * theory); |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
13 |
|
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
14 |
val mk_cons_tuple: term * term -> term; |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
15 |
val dest_cons_tuple: term -> term * term; |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
16 |
|
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
17 |
val istuple_intros_tac: theory -> int -> tactic; |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
18 |
|
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
19 |
val named_cterm_instantiate: (string * cterm) list -> thm -> thm; |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
20 |
end; |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
21 |
|
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
22 |
structure IsTupleSupport : ISTUPLE_SUPPORT = |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
23 |
struct |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
24 |
|
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
25 |
val isomN = "_TupleIsom"; |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
26 |
val defN = "_def"; |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
27 |
|
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
28 |
val istuple_UNIV_I = @{thm "istuple_UNIV_I"}; |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
29 |
val istuple_True_simp = @{thm "istuple_True_simp"}; |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
30 |
|
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
31 |
val istuple_intro = @{thm "isomorphic_tuple_intro"}; |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
32 |
val istuple_intros = build_net (@{thms "isomorphic_tuple.intros"}); |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
33 |
|
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
34 |
val constname = fst o dest_Const; |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
35 |
val tuple_istuple = (constname @{term tuple_istuple}, @{thm tuple_istuple}); |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
36 |
|
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
37 |
val istuple_constN = constname @{term isomorphic_tuple}; |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
38 |
val istuple_consN = constname @{term istuple_cons}; |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
39 |
|
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
40 |
val tup_isom_typeN = fst (dest_Type @{typ "('a, 'b, 'c) tuple_isomorphism"}); |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
41 |
|
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
42 |
fun named_cterm_instantiate values thm = let |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
43 |
fun match name (Var ((name', _), _)) = name = name' |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
44 |
| match name _ = false; |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
45 |
fun getvar name = case (find_first (match name) |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
46 |
(OldTerm.term_vars (prop_of thm))) |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
47 |
of SOME var => cterm_of (theory_of_thm thm) var |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
48 |
| NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm]) |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
49 |
in |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
50 |
cterm_instantiate (map (apfst getvar) values) thm |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
51 |
end; |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
52 |
|
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
53 |
structure IsTupleThms = TheoryDataFun |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
54 |
( |
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
55 |
type T = thm Symtab.table; |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
56 |
val empty = Symtab.make [tuple_istuple]; |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
57 |
val copy = I; |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
58 |
val extend = I; |
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
59 |
val merge = K (Symtab.merge Thm.eq_thm_prop); |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
60 |
); |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
61 |
|
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
62 |
fun do_typedef name repT alphas thy = |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
63 |
let |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
64 |
fun get_thms thy name = |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
65 |
let |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
66 |
val SOME { Rep_inject=rep_inject, Abs_name=absN, abs_type=absT, |
32744
50406c4951d9
Record patch imported and working.
Thomas Sewell <tsewell@nicta.com.au>
parents:
32743
diff
changeset
|
67 |
Abs_inverse=abs_inverse, ...} = Typedef.get_info thy name; |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
68 |
val rewrite_rule = MetaSimplifier.rewrite_rule [istuple_UNIV_I, istuple_True_simp]; |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
69 |
in (map rewrite_rule [rep_inject, abs_inverse], |
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
70 |
Const (absN, repT --> absT), absT) end; |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
71 |
in |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
72 |
thy |
32744
50406c4951d9
Record patch imported and working.
Thomas Sewell <tsewell@nicta.com.au>
parents:
32743
diff
changeset
|
73 |
|> Typecopy.typecopy (Binding.name name, alphas) repT NONE |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
74 |
|-> (fn (name, _) => `(fn thy => get_thms thy name)) |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
75 |
end; |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
76 |
|
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
77 |
fun mk_cons_tuple (left, right) = let |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
78 |
val (leftT, rightT) = (fastype_of left, fastype_of right); |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
79 |
val prodT = HOLogic.mk_prodT (leftT, rightT); |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
80 |
val isomT = Type (tup_isom_typeN, [prodT, leftT, rightT]); |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
81 |
in |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
82 |
Const (istuple_consN, isomT --> leftT --> rightT --> prodT) |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
83 |
$ Const (fst tuple_istuple, isomT) $ left $ right |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
84 |
end; |
32744
50406c4951d9
Record patch imported and working.
Thomas Sewell <tsewell@nicta.com.au>
parents:
32743
diff
changeset
|
85 |
|
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
86 |
fun dest_cons_tuple (v as Const (ic, _) $ Const _ $ left $ right) |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
87 |
= if ic = istuple_consN then (left, right) |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
88 |
else raise TERM ("dest_cons_tuple", [v]) |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
89 |
| dest_cons_tuple v = raise TERM ("dest_cons_tuple", [v]); |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
90 |
|
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
91 |
fun add_istuple_type (name, alphas) (leftT, rightT) thy = |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
92 |
let |
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
93 |
val repT = HOLogic.mk_prodT (leftT, rightT); |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
94 |
|
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
95 |
val (([rep_inject, abs_inverse], absC, absT), typ_thy) = |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
96 |
thy |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
97 |
|> do_typedef name repT alphas |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
98 |
||> Sign.add_path name; |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
99 |
|
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
100 |
(* construct a type and body for the isomorphism constant by |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
101 |
instantiating the theorem to which the definition will be applied *) |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
102 |
val intro_inst = rep_inject RS |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
103 |
(named_cterm_instantiate [("abst", cterm_of typ_thy absC)] |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
104 |
istuple_intro); |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
105 |
val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst)); |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
106 |
val isomT = fastype_of body; |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
107 |
val isomBind = Binding.name (name ^ isomN); |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
108 |
val isom = Const (Sign.full_name typ_thy isomBind, isomT); |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
109 |
val isom_spec = (name ^ isomN ^ defN, Logic.mk_equals (isom, body)); |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
110 |
|
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
111 |
val ([isom_def], cdef_thy) = |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
112 |
typ_thy |
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
113 |
|> Sign.add_consts_i [Syntax.no_syn (isomBind, isomT)] |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
114 |
|> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)]; |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
115 |
|
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
116 |
val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro)); |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
117 |
val cons = Const (istuple_consN, isomT --> leftT --> rightT --> absT) |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
118 |
|
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
119 |
val thm_thy = |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
120 |
cdef_thy |
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
121 |
|> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
122 |
(constname isom, istuple)) |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
123 |
|> Sign.parent_path; |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
124 |
in |
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
125 |
(isom, cons $ isom, thm_thy) |
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
126 |
end; |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
127 |
|
32745
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
128 |
fun istuple_intros_tac thy = let |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
129 |
val isthms = IsTupleThms.get thy; |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
130 |
fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]); |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
131 |
val use_istuple_thm_tac = SUBGOAL (fn (goal, n) => let |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
132 |
val goal' = Envir.beta_eta_contract goal; |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
133 |
val isom = case goal' of (Const tp $ (Const pr $ Const is)) |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
134 |
=> if fst tp = "Trueprop" andalso fst pr = istuple_constN |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
135 |
then Const is |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
136 |
else err "unexpected goal predicate" goal' |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
137 |
| _ => err "unexpected goal format" goal'; |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
138 |
val isthm = case Symtab.lookup isthms (constname isom) of |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
139 |
SOME isthm => isthm |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
140 |
| NONE => err "no thm found for constant" isom; |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
141 |
in rtac isthm n end); |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
142 |
in |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
143 |
fn n => resolve_from_net_tac istuple_intros n |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
144 |
THEN use_istuple_thm_tac n |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
145 |
end; |
192d58483fdf
Simplification of various aspects of the IsTuple component
Thomas Sewell <tsewell@nicta.com.au>
parents:
32744
diff
changeset
|
146 |
|
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
147 |
end; |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
148 |
|
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
diff
changeset
|
149 |