author  wenzelm 
Wed, 31 Dec 2008 18:53:18 +0100  
changeset 29273  285c00993bc2 
parent 29269  5c25a2012975 
permissions  rwrr 
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
24630
diff
changeset

1 
(* Author: Amine Chaieb, TU Muenchen 
20319  2 

3 
A trial for automatical reification. 

4 
*) 

5 

29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
24630
diff
changeset

6 
signature REFLECTION = 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
24630
diff
changeset

7 
sig 
20319  8 
val genreify_tac: Proof.context > thm list > term option > int > tactic 
23648
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

9 
val reflection_tac: Proof.context > thm list > thm list > term option > int > tactic 
21878  10 
val gen_reflection_tac: Proof.context > (cterm > thm) 
23648
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

11 
> thm list > thm list > term option > int > tactic 
20319  12 
end; 
13 

29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
24630
diff
changeset

14 
structure Reflection : REFLECTION = 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
24630
diff
changeset

15 
struct 
20319  16 

20374  17 
val ext2 = thm "ext2"; 
21669  18 
val nth_Cons_0 = thm "nth_Cons_0"; 
19 
val nth_Cons_Suc = thm "nth_Cons_Suc"; 

20 

20374  21 
(* Make a congruence rule out of a defining equation for the interpretation *) 
22 
(* th is one defining equation of f, i.e. 

23 
th is "f (Cp ?t1 ... ?tn) = P(f ?t1, .., f ?tn)" *) 

24 
(* Cp is a constructor pattern and P is a pattern *) 

25 

26 
(* The result is: 

27 
[?A1 = f ?t1 ; .. ; ?An= f ?tn ] ==> P (?A1, .., ?An) = f (Cp ?t1 .. ?tn) *) 

28 
(* + the a list of names of the A1 .. An, Those are fresh in the ctxt*) 

29 

30 

31 
fun mk_congeq ctxt fs th = 

32 
let 

20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

33 
val (f as Const(fN,fT)) = th > prop_of > HOLogic.dest_Trueprop > HOLogic.dest_eq 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

34 
> fst > strip_comb > fst 
20374  35 
val thy = ProofContext.theory_of ctxt 
36 
val cert = Thm.cterm_of thy 

22568
ed7aa5a350ef
renamed Variable.import to import_thms (avoid clash with Alice keywords);
wenzelm
parents:
22199
diff
changeset

37 
val (((_,_),[th']), ctxt') = Variable.import_thms true [th] ctxt 
20374  38 
val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th')) 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

39 
fun add_fterms (t as t1 $ t2) = 
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
24630
diff
changeset

40 
if exists (fn f => Term.could_unify (t > strip_comb > fst, f)) fs then insert (op aconv) t 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

41 
else add_fterms t1 #> add_fterms t2 
20374  42 
 add_fterms (t as Abs(xn,xT,t')) = 
29273  43 
if exists_Const (fn (c, _) => c = fN) t then (fn _ => [t]) else (fn _ => []) 
20374  44 
 add_fterms _ = I 
45 
val fterms = add_fterms rhs [] 

20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20595
diff
changeset

46 
val (xs, ctxt'') = Variable.variant_fixes (replicate (length fterms) "x") ctxt' 
20374  47 
val tys = map fastype_of fterms 
48 
val vs = map Free (xs ~~ tys) 

49 
val env = fterms ~~ vs 

20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

50 
(* FIXME!!!!*) 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

51 
fun replace_fterms (t as t1 $ t2) = 
20374  52 
(case AList.lookup (op aconv) env t of 
53 
SOME v => v 

20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

54 
 NONE => replace_fterms t1 $ replace_fterms t2) 
20374  55 
 replace_fterms t = (case AList.lookup (op aconv) env t of 
56 
SOME v => v 

57 
 NONE => t) 

58 

59 
fun mk_def (Abs(x,xT,t),v) = HOLogic.mk_Trueprop ((HOLogic.all_const xT)$ Abs(x,xT,HOLogic.mk_eq(v$(Bound 0), t))) 

60 
 mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t)) 

23605  61 
fun tryext x = (x RS ext2 handle THM _ => x) 
20374  62 
val cong = (Goal.prove ctxt'' [] (map mk_def env) 
63 
(HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs))) 

64 
(fn x => LocalDefs.unfold_tac (#context x) (map tryext (#prems x)) 

65 
THEN rtac th' 1)) RS sym 

66 

67 
val (cong' :: vars') = 

68 
Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs) 

69 
val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars' 

70 

71 
in (vs', cong') end; 

20319  72 
(* congs is a list of pairs (P,th) where th is a theorem for *) 
73 
(* [ f p1 = A1; ...; f pn = An] ==> f (C p1 .. pn) = P *) 

74 
val FWD = curry (op OF); 

75 

76 
(* da is the decomposition for atoms, ie. it returns ([],g) where g 

77 
returns the right instance f (AtC n) = t , where AtC is the Atoms 

78 
constructor and n is the number of the atom corresponding to t *) 

79 

80 
(* Generic decomp for reification : matches the actual term with the 

81 
rhs of one cong rule. The result of the matching guides the 

82 
proof synthesis: The matches of the introduced Variables A1 .. An are 

83 
processed recursively 

84 
The rest is instantiated in the cong rule,i.e. no reification is needed *) 

85 

20374  86 
exception REIF of string; 
87 

20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

88 
val bds = ref ([]: (typ * ((term list) * (term list))) list); 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

89 

6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

90 
fun index_of t = 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

91 
let 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

92 
val tt = HOLogic.listT (fastype_of t) 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

93 
in 
22199
b617ddd200eb
Now deals with simples cases where the input equations contain type variables
chaieb
parents:
21878
diff
changeset

94 
(case AList.lookup Type.could_unify (!bds) tt of 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

95 
NONE => error "index_of : type not found in environements!" 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

96 
 SOME (tbs,tats) => 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

97 
let 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

98 
val i = find_index_eq t tats 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

99 
val j = find_index_eq t tbs 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

100 
in (if j= ~1 then 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

101 
if i= ~1 
23605  102 
then (bds := AList.update Type.could_unify (tt,(tbs,tats@[t])) (!bds) ; 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

103 
length tbs + length tats) 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

104 
else i else j) 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

105 
end) 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

106 
end; 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

107 

6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

108 
fun dest_listT (Type ("List.list", [T])) = T; 
20374  109 

110 
fun decomp_genreif da cgns (t,ctxt) = 

20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

111 
let 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

112 
val thy = ProofContext.theory_of ctxt 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

113 
val cert = cterm_of thy 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

114 
fun tryabsdecomp (s,ctxt) = 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

115 
(case s of 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

116 
Abs(xn,xT,ta) => 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

117 
(let 
20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20595
diff
changeset

118 
val ([xn],ctxt') = Variable.variant_fixes ["x"] ctxt 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

119 
val (xn,ta) = variant_abs (xn,xT,ta) 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

120 
val x = Free(xn,xT) 
23605  121 
val _ = (case AList.lookup Type.could_unify (!bds) (HOLogic.listT xT) 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

122 
of NONE => error "tryabsdecomp: Type not found in the Environement" 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

123 
 SOME (bsT,atsT) => 
23605  124 
(bds := AList.update Type.could_unify (HOLogic.listT xT, ((x::bsT), atsT)) (!bds))) 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

125 
in ([(ta, ctxt')] , 
23605  126 
fn [th] => ((let val (bsT,asT) = the(AList.lookup Type.could_unify (!bds) (HOLogic.listT xT)) 
127 
in (bds := AList.update Type.could_unify (HOLogic.listT xT,(tl bsT,asT)) (!bds)) 

20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

128 
end) ; 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

129 
hd (Variable.export ctxt' ctxt [(forall_intr (cert x) th) COMP allI]))) 
20374  130 
end) 
131 
 _ => da (s,ctxt)) 

132 
in 

133 
(case cgns of 

134 
[] => tryabsdecomp (t,ctxt) 

135 
 ((vns,cong)::congs) => ((let 

136 
val cert = cterm_of thy 

20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

137 
val certy = ctyp_of thy 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

138 
val (tyenv, tmenv) = 
20319  139 
Pattern.match thy 
140 
((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t) 

29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
24630
diff
changeset

141 
(Envir.type_env (Envir.empty 0), Vartab.empty) 
20319  142 
val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv) 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

143 
val (fts,its) = 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

144 
(map (snd o snd) fnvs, 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

145 
map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs) 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

146 
val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv) 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

147 
in (fts ~~ (replicate (length fts) ctxt), FWD (instantiate (ctyenv, its) cong)) 
20319  148 
end) 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

149 
handle MATCH => decomp_genreif da congs (t,ctxt))) 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

150 
end; 
23648
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

151 

bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

152 
(* looks for the atoms equation and instantiates it with the right number *) 
20374  153 

23548
e25991f126ce
Generalized case for atoms. Selection of environment lists is allowed more than once.
chaieb
parents:
22568
diff
changeset

154 

20374  155 
fun mk_decompatom eqs (t,ctxt) = 
23605  156 
let 
157 
val tT = fastype_of t 

158 
fun isat eq = 

159 
let 

160 
val rhs = eq > prop_of > HOLogic.dest_Trueprop > HOLogic.dest_eq > snd 

20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

161 
in exists_Const 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

162 
(fn (n,ty) => n="List.nth" 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

163 
andalso 
22199
b617ddd200eb
Now deals with simples cases where the input equations contain type variables
chaieb
parents:
21878
diff
changeset

164 
AList.defined Type.could_unify (!bds) (domain_type ty)) rhs 
b617ddd200eb
Now deals with simples cases where the input equations contain type variables
chaieb
parents:
21878
diff
changeset

165 
andalso Type.could_unify (fastype_of rhs, tT) 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

166 
end 
23605  167 
fun get_nths t acc = 
168 
case t of 

169 
Const("List.nth",_)$vs$n => insert (fn ((a,_),(b,_)) => a aconv b) (t,(vs,n)) acc 

170 
 t1$t2 => get_nths t1 (get_nths t2 acc) 

171 
 Abs(_,_,t') => get_nths t' acc 

172 
 _ => acc 

23548
e25991f126ce
Generalized case for atoms. Selection of environment lists is allowed more than once.
chaieb
parents:
22568
diff
changeset

173 

23605  174 
fun 
175 
tryeqs [] = error "Can not find the atoms equation" 

176 
 tryeqs (eq::eqs) = (( 

177 
let 

178 
val rhs = eq > prop_of > HOLogic.dest_Trueprop > HOLogic.dest_eq > snd 

179 
val nths = get_nths rhs [] 

180 
val (vss,ns) = fold_rev (fn (_,(vs,n)) => fn (vss,ns) => 

181 
(insert (op aconv) vs vss, insert (op aconv) n ns)) nths ([],[]) 

182 
val (vsns, ctxt') = Variable.variant_fixes (replicate (length vss) "vs") ctxt 

183 
val (xns, ctxt'') = Variable.variant_fixes (replicate (length nths) "x") ctxt' 

184 
val thy = ProofContext.theory_of ctxt'' 

185 
val cert = cterm_of thy 

186 
val certT = ctyp_of thy 

187 
val vsns_map = vss ~~ vsns 

188 
val xns_map = (fst (split_list nths)) ~~ xns 

189 
val subst = map (fn (nt, xn) => (nt, Var ((xn,0), fastype_of nt))) xns_map 

190 
val rhs_P = subst_free subst rhs 

191 
val (tyenv, tmenv) = Pattern.match 

192 
thy (rhs_P, t) 

29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
24630
diff
changeset

193 
(Envir.type_env (Envir.empty 0), Vartab.empty) 
23605  194 
val sbst = Envir.subst_vars (tyenv, tmenv) 
195 
val sbsT = Envir.typ_subst_TVars tyenv 

196 
val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t)) 

197 
(Vartab.dest tyenv) 

198 
val tml = Vartab.dest tmenv 

199 
val t's = map (fn xn => snd (valOf (AList.lookup (op =) tml (xn,0)))) xns (* FIXME : Express with sbst*) 

200 
val subst_ns = map (fn (Const _ $ vs $ n, Var (xn0,T)) => 

201 
(cert n, snd (valOf (AList.lookup (op =) tml xn0)) 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24044
diff
changeset

202 
> (index_of #> HOLogic.mk_nat #> cert))) 
23605  203 
subst 
204 
val subst_vs = 

205 
let 

206 
fun ty (Const _ $ (vs as Var (vsn,lT)) $ n, Var (xn0,T)) = (certT T, certT (sbsT T)) 

207 
fun h (Const _ $ (vs as Var (vsn,lT)) $ n, Var (xn0,T)) = 

20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

208 
let 
23605  209 
val cns = sbst (Const("List.list.Cons", T > lT > lT)) 
210 
val lT' = sbsT lT 

211 
val (bsT,asT) = the (AList.lookup Type.could_unify (!bds) lT) 

212 
val vsn = valOf (AList.lookup (op =) vsns_map vs) 

213 
val cvs = cert (fold_rev (fn x => fn xs => cns$x$xs) bsT (Free (vsn, lT'))) 

214 
in (cert vs, cvs) end 

215 
in map h subst end 

216 
val cts = map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) 

217 
(fold (AList.delete (fn (((a: string),_),(b,_)) => a = b)) 

218 
(map (fn n => (n,0)) xns) tml) 

219 
val substt = 

220 
let val ih = Drule.cterm_rule (Thm.instantiate (subst_ty,[])) 

221 
in map (fn (v,t) => (ih v, ih t)) (subst_ns@subst_vs@cts) end 

222 
val th = (instantiate (subst_ty, substt) eq) RS sym 

223 
in hd (Variable.export ctxt'' ctxt [th]) end) 

224 
handle MATCH => tryeqs eqs) 

225 
in ([], fn _ => tryeqs (filter isat eqs)) 

226 
end; 

20374  227 

20319  228 
(* Generic reification procedure: *) 
229 
(* creates all needed cong rules and then just uses the theorem synthesis *) 

20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

230 

23624
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

231 
fun mk_congs ctxt raw_eqs = 
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

232 
let 
21078  233 
val fs = fold_rev (fn eq => 
20853  234 
insert (op =) (eq > prop_of > HOLogic.dest_Trueprop 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

235 
> HOLogic.dest_eq > fst > strip_comb 
21078  236 
> fst)) raw_eqs [] 
23624
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

237 
val tys = fold_rev (fn f => fn ts => (f > fastype_of > binder_types > tl) 
21078  238 
union ts) fs [] 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

239 
val _ = bds := AList.make (fn _ => ([],[])) tys 
20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20595
diff
changeset

240 
val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

241 
val thy = ProofContext.theory_of ctxt' 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

242 
val cert = cterm_of thy 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

243 
val vstys = map (fn (t,v) => (t,SOME (cert (Free(v,t))))) 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

244 
(tys ~~ vs) 
23624
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

245 
val is_Var = can dest_Var 
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

246 
fun insteq eq vs = 
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

247 
let 
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

248 
val subst = map (fn (v as Var(n,t)) => (cert v, (valOf o valOf) (AList.lookup (op =) vstys t))) 
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

249 
(filter is_Var vs) 
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

250 
in Thm.instantiate ([],subst) eq 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

251 
end 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

252 
val eqs = map (fn eq => eq > prop_of > HOLogic.dest_Trueprop 
23624
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

253 
> HOLogic.dest_eq > fst > strip_comb > snd > tl 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

254 
> (insteq eq)) raw_eqs 
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

255 
val (ps,congs) = split_list (map (mk_congeq ctxt' fs) eqs) 
23624
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

256 
in ps ~~ (Variable.export ctxt' ctxt congs) 
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

257 
end 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

258 

23648
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

259 
fun partition P [] = ([],[]) 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

260 
 partition P (x::xs) = 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

261 
let val (yes,no) = partition P xs 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

262 
in if P x then (x::yes,no) else (yes, x::no) end 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

263 

bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

264 
fun rearrange congs = 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

265 
let 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

266 
fun P (_, th) = 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

267 
let val @{term "Trueprop"}$(Const ("op =",_) $l$_) = concl_of th 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

268 
in can dest_Var l end 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

269 
val (yes,no) = partition P congs 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

270 
in no @ yes end 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

271 

bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

272 

bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

273 

20319  274 
fun genreif ctxt raw_eqs t = 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

275 
let 
23648
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

276 
val congs = rearrange (mk_congs ctxt raw_eqs) 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

277 
val th = divide_and_conquer (decomp_genreif (mk_decompatom raw_eqs) congs) (t,ctxt) 
23624
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

278 
fun is_listVar (Var (_,t)) = can dest_listT t 
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

279 
 is_listVar _ = false 
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

280 
val vars = th > prop_of > HOLogic.dest_Trueprop > HOLogic.dest_eq > snd 
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

281 
> strip_comb > snd > filter is_listVar 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

282 
val cert = cterm_of (ProofContext.theory_of ctxt) 
23624
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

283 
val cvs = map (fn (v as Var(n,t)) => (cert v, the (AList.lookup Type.could_unify (!bds) t) > snd > HOLogic.mk_list (dest_listT t) > cert)) vars 
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

284 
val th' = instantiate ([], cvs) th 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

285 
val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th' 
23643
32ee4111d1bc
Corrected erronus use of compiletime context to the runtime context
chaieb
parents:
23624
diff
changeset

286 
val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) 
24044  287 
(fn _ => simp_tac (local_simpset_of ctxt) 1) 
20564
6857bd9f1a79
Reifiaction now deals with Interpretations with an arbtrary number of parameters. It deals with binding. The Atomic cases can be I ... = f (xs!n)
chaieb
parents:
20374
diff
changeset

288 
val _ = bds := [] 
23624
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

289 
in FWD trans [th'',th'] 
82091387f6d7
The order for parameter for interpretation is now inversted:
chaieb
parents:
23605
diff
changeset

290 
end 
20319  291 

23648
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

292 

bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

293 
fun genreflect ctxt conv corr_thms raw_eqs t = 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

294 
let 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

295 
val reifth = genreif ctxt raw_eqs t 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

296 
fun trytrans [] = error "No suitable correctness theorem found" 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

297 
 trytrans (th::ths) = 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

298 
(FWD trans [reifth, th RS sym] handle THM _ => trytrans ths) 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

299 
val th = trytrans corr_thms 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

300 
val ft = (Thm.dest_arg1 o Thm.dest_arg o Thm.dest_arg o cprop_of) th 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

301 
val rth = conv ft 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

302 
in simplify (HOL_basic_ss addsimps raw_eqs addsimps [nth_Cons_0, nth_Cons_Suc]) 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

303 
(simplify (HOL_basic_ss addsimps [rth]) th) 
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

304 
end 
20319  305 

306 
fun genreify_tac ctxt eqs to i = (fn st => 

307 
let 

308 
val P = HOLogic.dest_Trueprop (List.nth (prems_of st, i  1)) 

309 
val t = (case to of NONE => P  SOME x => x) 

310 
val th = (genreif ctxt eqs t) RS ssubst 

311 
in rtac th i st 

312 
end); 

313 

314 
(* Reflection calls reification and uses the correctness *) 

315 
(* theorem assumed to be the dead of the list *) 

23648
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

316 
fun gen_reflection_tac ctxt conv corr_thms raw_eqs to i = (fn st => 
21878  317 
let 
318 
val P = HOLogic.dest_Trueprop (nth (prems_of st) (i  1)); 

319 
val t = the_default P to; 

23648
bccbf6138c30
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
chaieb
parents:
23643
diff
changeset

320 
val th = genreflect ctxt conv corr_thms raw_eqs t 
21878  321 
RS ssubst; 
23791  322 
in (rtac th i THEN TRY(rtac TrueI i)) st end); 
21878  323 

23791  324 
fun reflection_tac ctxt = gen_reflection_tac ctxt Codegen.evaluation_conv; 
20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20595
diff
changeset

325 
end 