17456

1 
(* Title: CCL/Wfd.thy

0

2 
ID: $Id$

1474

3 
Author: Martin Coen, Cambridge University Computer Laboratory

0

4 
Copyright 1993 University of Cambridge


5 
*)


6 

17456

7 
header {* Wellfounded relations in CCL *}


8 


9 
theory Wfd


10 
imports Trancl Type Hered


11 
begin

0

12 


13 
consts


14 
(*** Predicates ***)


15 
Wfd :: "[i set] => o"


16 
(*** Relations ***)


17 
wf :: "[i set] => i set"


18 
wmap :: "[i=>i,i set] => i set"


19 
"**" :: "[i set,i set] => i set" (infixl 70)


20 
NatPR :: "i set"


21 
ListPR :: "i set => i set"


22 

17456

23 
axioms

0

24 

17456

25 
Wfd_def:

3837

26 
"Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R > y:P) > x:P) > (ALL a. a:P)"

0

27 

17456

28 
wf_def: "wf(R) == {x. x:R & Wfd(R)}"

0

29 

17456

30 
wmap_def: "wmap(f,R) == {p. EX x y. p=<x,y> & <f(x),f(y)> : R}"


31 
lex_def:

3837

32 
"ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra  (a=a' & <b,b'> : rb))}"

0

33 

17456

34 
NatPR_def: "NatPR == {p. EX x:Nat. p=<x,succ(x)>}"


35 
ListPR_def: "ListPR(A) == {p. EX h:A. EX t:List(A). p=<t,h$t>}"


36 

20140

37 


38 
lemma wfd_induct:


39 
assumes 1: "Wfd(R)"


40 
and 2: "!!x.[ ALL y. <y,x>: R > P(y) ] ==> P(x)"


41 
shows "P(a)"


42 
apply (rule 1 [unfolded Wfd_def, rule_format, THEN CollectD])


43 
using 2 apply blast


44 
done


45 


46 
lemma wfd_strengthen_lemma:


47 
assumes 1: "!!x y.<x,y> : R ==> Q(x)"


48 
and 2: "ALL x. (ALL y. <y,x> : R > y : P) > x : P"


49 
and 3: "!!x. Q(x) ==> x:P"


50 
shows "a:P"


51 
apply (rule 2 [rule_format])


52 
using 1 3


53 
apply blast


54 
done


55 


56 
ML {*


57 
local val wfd_strengthen_lemma = thm "wfd_strengthen_lemma" in


58 
fun wfd_strengthen_tac s i =


59 
res_inst_tac [("Q",s)] wfd_strengthen_lemma i THEN assume_tac (i+1)


60 
end


61 
*}


62 


63 
lemma wf_anti_sym: "[ Wfd(r); <a,x>:r; <x,a>:r ] ==> P"


64 
apply (subgoal_tac "ALL x. <a,x>:r > <x,a>:r > P")


65 
apply blast


66 
apply (erule wfd_induct)


67 
apply blast


68 
done


69 


70 
lemma wf_anti_refl: "[ Wfd(r); <a,a>: r ] ==> P"


71 
apply (rule wf_anti_sym)


72 
apply assumption+


73 
done


74 


75 


76 
subsection {* Irreflexive transitive closure *}


77 


78 
lemma trancl_wf:


79 
assumes 1: "Wfd(R)"


80 
shows "Wfd(R^+)"


81 
apply (unfold Wfd_def)


82 
apply (rule allI ballI impI)+


83 
(*must retain the universal formula for later use!*)


84 
apply (rule allE, assumption)


85 
apply (erule mp)


86 
apply (rule 1 [THEN wfd_induct])


87 
apply (rule impI [THEN allI])


88 
apply (erule tranclE)


89 
apply blast


90 
apply (erule spec [THEN mp, THEN spec, THEN mp])


91 
apply assumption+


92 
done


93 


94 


95 
subsection {* Lexicographic Ordering *}


96 


97 
lemma lexXH:


98 
"p : ra**rb <> (EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra  a=a' & <b,b'> : rb))"


99 
unfolding lex_def by blast


100 


101 
lemma lexI1: "<a,a'> : ra ==> <<a,b>,<a',b'>> : ra**rb"


102 
by (blast intro!: lexXH [THEN iffD2])


103 


104 
lemma lexI2: "<b,b'> : rb ==> <<a,b>,<a,b'>> : ra**rb"


105 
by (blast intro!: lexXH [THEN iffD2])


106 


107 
lemma lexE:


108 
assumes 1: "p : ra**rb"


109 
and 2: "!!a a' b b'.[ <a,a'> : ra; p=<<a,b>,<a',b'>> ] ==> R"


110 
and 3: "!!a b b'.[ <b,b'> : rb; p = <<a,b>,<a,b'>> ] ==> R"


111 
shows R


112 
apply (rule 1 [THEN lexXH [THEN iffD1], THEN exE])


113 
using 2 3


114 
apply blast


115 
done


116 


117 
lemma lex_pair: "[ p : r**s; !!a a' b b'. p = <<a,b>,<a',b'>> ==> P ] ==>P"


118 
apply (erule lexE)


119 
apply blast+


120 
done


121 


122 
lemma lex_wf:


123 
assumes 1: "Wfd(R)"


124 
and 2: "Wfd(S)"


125 
shows "Wfd(R**S)"


126 
apply (unfold Wfd_def)


127 
apply safe


128 
apply (tactic {* wfd_strengthen_tac "%x. EX a b. x=<a,b>" 1 *})


129 
apply (blast elim!: lex_pair)


130 
apply (subgoal_tac "ALL a b.<a,b>:P")


131 
apply blast


132 
apply (rule 1 [THEN wfd_induct, THEN allI])


133 
apply (rule 2 [THEN wfd_induct, THEN allI]) back


134 
apply (fast elim!: lexE)


135 
done


136 


137 


138 
subsection {* Mapping *}


139 


140 
lemma wmapXH: "p : wmap(f,r) <> (EX x y. p=<x,y> & <f(x),f(y)> : r)"


141 
unfolding wmap_def by blast


142 


143 
lemma wmapI: "<f(a),f(b)> : r ==> <a,b> : wmap(f,r)"


144 
by (blast intro!: wmapXH [THEN iffD2])


145 


146 
lemma wmapE: "[ p : wmap(f,r); !!a b.[ <f(a),f(b)> : r; p=<a,b> ] ==> R ] ==> R"


147 
by (blast dest!: wmapXH [THEN iffD1])


148 


149 
lemma wmap_wf:


150 
assumes 1: "Wfd(r)"


151 
shows "Wfd(wmap(f,r))"


152 
apply (unfold Wfd_def)


153 
apply clarify


154 
apply (subgoal_tac "ALL b. ALL a. f (a) =b>a:P")


155 
apply blast


156 
apply (rule 1 [THEN wfd_induct, THEN allI])


157 
apply clarify


158 
apply (erule spec [THEN mp])


159 
apply (safe elim!: wmapE)


160 
apply (erule spec [THEN mp, THEN spec, THEN mp])


161 
apply assumption


162 
apply (rule refl)


163 
done


164 


165 


166 
subsection {* Projections *}


167 


168 
lemma wfstI: "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)"


169 
apply (rule wmapI)


170 
apply simp


171 
done


172 


173 
lemma wsndI: "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)"


174 
apply (rule wmapI)


175 
apply simp


176 
done


177 


178 
lemma wthdI: "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)"


179 
apply (rule wmapI)


180 
apply simp


181 
done


182 


183 


184 
subsection {* Ground wellfounded relations *}


185 


186 
lemma wfI: "[ Wfd(r); a : r ] ==> a : wf(r)"


187 
unfolding wf_def by blast


188 


189 
lemma Empty_wf: "Wfd({})"


190 
unfolding Wfd_def by (blast elim: EmptyXH [THEN iffD1, THEN FalseE])


191 


192 
lemma wf_wf: "Wfd(wf(R))"


193 
unfolding wf_def


194 
apply (rule_tac Q = "Wfd(R)" in excluded_middle [THEN disjE])


195 
apply simp_all


196 
apply (rule Empty_wf)


197 
done


198 


199 
lemma NatPRXH: "p : NatPR <> (EX x:Nat. p=<x,succ(x)>)"


200 
unfolding NatPR_def by blast


201 


202 
lemma ListPRXH: "p : ListPR(A) <> (EX h:A. EX t:List(A).p=<t,h$t>)"


203 
unfolding ListPR_def by blast


204 


205 
lemma NatPRI: "x : Nat ==> <x,succ(x)> : NatPR"


206 
by (auto simp: NatPRXH)


207 


208 
lemma ListPRI: "[ t : List(A); h : A ] ==> <t,h $ t> : ListPR(A)"


209 
by (auto simp: ListPRXH)


210 


211 
lemma NatPR_wf: "Wfd(NatPR)"


212 
apply (unfold Wfd_def)


213 
apply clarify


214 
apply (tactic {* wfd_strengthen_tac "%x. x:Nat" 1 *})


215 
apply (fastsimp iff: NatPRXH)


216 
apply (erule Nat_ind)


217 
apply (fastsimp iff: NatPRXH)+


218 
done


219 


220 
lemma ListPR_wf: "Wfd(ListPR(A))"


221 
apply (unfold Wfd_def)


222 
apply clarify


223 
apply (tactic {* wfd_strengthen_tac "%x. x:List (A)" 1 *})


224 
apply (fastsimp iff: ListPRXH)


225 
apply (erule List_ind)


226 
apply (fastsimp iff: ListPRXH)+


227 
done


228 


229 


230 
subsection {* General Recursive Functions *}


231 


232 
lemma letrecT:


233 
assumes 1: "a : A"


234 
and 2: "!!p g.[ p:A; ALL x:{x: A. <x,p>:wf(R)}. g(x) : D(x) ] ==> h(p,g) : D(p)"


235 
shows "letrec g x be h(x,g) in g(a) : D(a)"


236 
apply (rule 1 [THEN rev_mp])


237 
apply (rule wf_wf [THEN wfd_induct])


238 
apply (subst letrecB)


239 
apply (rule impI)


240 
apply (erule 2)


241 
apply blast


242 
done


243 


244 
lemma SPLITB: "SPLIT(<a,b>,B) = B(a,b)"


245 
unfolding SPLIT_def


246 
apply (rule set_ext)


247 
apply blast


248 
done

17456

249 

20140

250 
lemma letrec2T:


251 
assumes "a : A"


252 
and "b : B"


253 
and "!!p q g.[ p:A; q:B;


254 
ALL x:A. ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) ] ==>


255 
h(p,q,g) : D(p,q)"


256 
shows "letrec g x y be h(x,y,g) in g(a,b) : D(a,b)"


257 
apply (unfold letrec2_def)


258 
apply (rule SPLITB [THEN subst])


259 
apply (assumption  rule letrecT pairT splitT prems)+


260 
apply (subst SPLITB)


261 
apply (assumption  rule ballI SubtypeI prems)+


262 
apply (rule SPLITB [THEN subst])


263 
apply (assumption  rule letrecT SubtypeI pairT splitT prems 


264 
erule bspec SubtypeE sym [THEN subst])+


265 
done


266 


267 
lemma lem: "SPLIT(<a,<b,c>>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)"


268 
by (simp add: SPLITB)


269 


270 
lemma letrec3T:


271 
assumes "a : A"


272 
and "b : B"


273 
and "c : C"


274 
and "!!p q r g.[ p:A; q:B; r:C;


275 
ALL x:A. ALL y:B. ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}.


276 
g(x,y,z) : D(x,y,z) ] ==>


277 
h(p,q,r,g) : D(p,q,r)"


278 
shows "letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)"


279 
apply (unfold letrec3_def)


280 
apply (rule lem [THEN subst])


281 
apply (assumption  rule letrecT pairT splitT prems)+


282 
apply (simp add: SPLITB)


283 
apply (assumption  rule ballI SubtypeI prems)+


284 
apply (rule lem [THEN subst])


285 
apply (assumption  rule letrecT SubtypeI pairT splitT prems 


286 
erule bspec SubtypeE sym [THEN subst])+


287 
done


288 


289 
lemmas letrecTs = letrecT letrec2T letrec3T


290 


291 


292 
subsection {* Type Checking for Recursive Calls *}


293 


294 
lemma rcallT:


295 
"[ ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x);


296 
g(a) : D(a) ==> g(a) : E; a:A; <a,p>:wf(R) ] ==>


297 
g(a) : E"


298 
by blast


299 


300 
lemma rcall2T:


301 
"[ ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y);


302 
g(a,b) : D(a,b) ==> g(a,b) : E; a:A; b:B; <<a,b>,<p,q>>:wf(R) ] ==>


303 
g(a,b) : E"


304 
by blast


305 


306 
lemma rcall3T:


307 
"[ ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z);


308 
g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E;


309 
a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R) ] ==>


310 
g(a,b,c) : E"


311 
by blast


312 


313 
lemmas rcallTs = rcallT rcall2T rcall3T


314 


315 


316 
subsection {* Instantiating an induction hypothesis with an equality assumption *}


317 


318 
lemma hyprcallT:


319 
assumes 1: "g(a) = b"


320 
and 2: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x)"


321 
and 3: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> b=g(a) ==> g(a) : D(a) ==> P"


322 
and 4: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> a:A"


323 
and 5: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> <a,p>:wf(R)"


324 
shows P


325 
apply (rule 3 [OF 2, OF 1 [symmetric]])


326 
apply (rule rcallT [OF 2])


327 
apply assumption


328 
apply (rule 4 [OF 2])


329 
apply (rule 5 [OF 2])


330 
done


331 


332 
lemma hyprcall2T:


333 
assumes 1: "g(a,b) = c"


334 
and 2: "ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y)"


335 
and 3: "[ c=g(a,b); g(a,b) : D(a,b) ] ==> P"


336 
and 4: "a:A"


337 
and 5: "b:B"


338 
and 6: "<<a,b>,<p,q>>:wf(R)"


339 
shows P


340 
apply (rule 3)


341 
apply (rule 1 [symmetric])


342 
apply (rule rcall2T)

23467

343 
apply (rule 2)


344 
apply assumption


345 
apply (rule 4)


346 
apply (rule 5)


347 
apply (rule 6)

20140

348 
done


349 


350 
lemma hyprcall3T:


351 
assumes 1: "g(a,b,c) = d"


352 
and 2: "ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z)"


353 
and 3: "[ d=g(a,b,c); g(a,b,c) : D(a,b,c) ] ==> P"


354 
and 4: "a:A"


355 
and 5: "b:B"


356 
and 6: "c:C"


357 
and 7: "<<a,<b,c>>,<p,<q,r>>> : wf(R)"


358 
shows P


359 
apply (rule 3)


360 
apply (rule 1 [symmetric])


361 
apply (rule rcall3T)

23467

362 
apply (rule 2)


363 
apply assumption


364 
apply (rule 4)


365 
apply (rule 5)


366 
apply (rule 6)


367 
apply (rule 7)

20140

368 
done


369 


370 
lemmas hyprcallTs = hyprcallT hyprcall2T hyprcall3T


371 


372 


373 
subsection {* Rules to Remove Induction Hypotheses after Type Checking *}


374 


375 
lemma rmIH1: "[ ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); P ] ==> P" .


376 


377 
lemma rmIH2: "[ ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P ] ==> P" .


378 


379 
lemma rmIH3:


380 
"[ ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z);


381 
P ] ==>


382 
P" .


383 


384 
lemmas rmIHs = rmIH1 rmIH2 rmIH3


385 


386 


387 
subsection {* Lemmas for constructors and subtypes *}


388 


389 
(* 0ary constructors do not need additional rules as they are handled *)


390 
(* correctly by applying SubtypeI *)


391 


392 
lemma Subtype_canTs:


393 
"!!a b A B P. a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}"


394 
"!!a A B P. a : {x:A. P(inl(x))} ==> inl(a) : {x:A+B. P(x)}"


395 
"!!b A B P. b : {x:B. P(inr(x))} ==> inr(b) : {x:A+B. P(x)}"


396 
"!!a P. a : {x:Nat. P(succ(x))} ==> succ(a) : {x:Nat. P(x)}"


397 
"!!h t A P. h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"


398 
by (assumption  rule SubtypeI canTs icanTs  erule SubtypeE)+


399 


400 
lemma letT: "[ f(t):B; ~t=bot ] ==> let x be t in f(x) : B"


401 
apply (erule letB [THEN ssubst])


402 
apply assumption


403 
done


404 


405 
lemma applyT2: "[ a:A; f : Pi(A,B) ] ==> f ` a : B(a)"


406 
apply (erule applyT)


407 
apply assumption


408 
done


409 


410 
lemma rcall_lemma1: "[ a:A; a:A ==> P(a) ] ==> a : {x:A. P(x)}"


411 
by blast


412 


413 
lemma rcall_lemma2: "[ a:{x:A. Q(x)}; [ a:A; Q(a) ] ==> P(a) ] ==> a : {x:A. P(x)}"


414 
by blast


415 


416 
lemmas rcall_lemmas = asm_rl rcall_lemma1 SubtypeD1 rcall_lemma2


417 


418 


419 
subsection {* Typechecking *}


420 


421 
ML {*


422 


423 
local


424 


425 
val type_rls =


426 
thms "canTs" @ thms "icanTs" @ thms "applyT2" @ thms "ncanTs" @ thms "incanTs" @


427 
thms "precTs" @ thms "letrecTs" @ thms "letT" @ thms "Subtype_canTs";


428 


429 
val rcallT = thm "rcallT";


430 
val rcall2T = thm "rcall2T";


431 
val rcall3T = thm "rcall3T";


432 
val rcallTs = thms "rcallTs";


433 
val rcall_lemmas = thms "rcall_lemmas";


434 
val SubtypeE = thm "SubtypeE";


435 
val SubtypeI = thm "SubtypeI";


436 
val rmIHs = thms "rmIHs";


437 
val hyprcallTs = thms "hyprcallTs";


438 


439 
fun bvars (Const("all",_) $ Abs(s,_,t)) l = bvars t (s::l)


440 
 bvars _ l = l


441 


442 
fun get_bno l n (Const("all",_) $ Abs(s,_,t)) = get_bno (s::l) n t


443 
 get_bno l n (Const("Trueprop",_) $ t) = get_bno l n t


444 
 get_bno l n (Const("Ball",_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t


445 
 get_bno l n (Const("op :",_) $ t $ _) = get_bno l n t


446 
 get_bno l n (t $ s) = get_bno l n t


447 
 get_bno l n (Bound m) = (mlength(l),n)


448 


449 
(* Not a great way of identifying induction hypothesis! *)


450 
fun could_IH x = could_unify(x,hd (prems_of rcallT)) orelse


451 
could_unify(x,hd (prems_of rcall2T)) orelse


452 
could_unify(x,hd (prems_of rcall3T))


453 


454 
fun IHinst tac rls = SUBGOAL (fn (Bi,i) =>


455 
let val bvs = bvars Bi []


456 
val ihs = List.filter could_IH (Logic.strip_assums_hyp Bi)


457 
val rnames = map (fn x=>


458 
let val (a,b) = get_bno [] 0 x


459 
in (List.nth(bvs,a),b) end) ihs


460 
fun try_IHs [] = no_tac


461 
 try_IHs ((x,y)::xs) = tac [("g",x)] (List.nth(rls,y1)) i ORELSE (try_IHs xs)


462 
in try_IHs rnames end)


463 


464 
fun is_rigid_prog t =


465 
case (Logic.strip_assums_concl t) of


466 
(Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) => (term_vars a = [])


467 
 _ => false


468 
in


469 


470 
fun rcall_tac i = let fun tac ps rl i = res_inst_tac ps rl i THEN atac i


471 
in IHinst tac rcallTs i end THEN


472 
eresolve_tac rcall_lemmas i


473 


474 
fun raw_step_tac prems i = ares_tac (prems@type_rls) i ORELSE


475 
rcall_tac i ORELSE


476 
ematch_tac [SubtypeE] i ORELSE


477 
match_tac [SubtypeI] i


478 


479 
fun tc_step_tac prems = SUBGOAL (fn (Bi,i) =>


480 
if is_rigid_prog Bi then raw_step_tac prems i else no_tac)


481 


482 
fun typechk_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls)) i


483 


484 
val tac = typechk_tac [] 1


485 


486 
(*** Clean up Correctness Condictions ***)


487 


488 
val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([SubtypeE]@rmIHs) ORELSE'


489 
hyp_subst_tac)


490 


491 
val clean_ccs_tac =


492 
let fun tac ps rl i = eres_inst_tac ps rl i THEN atac i


493 
in TRY (REPEAT_FIRST (IHinst tac hyprcallTs ORELSE'


494 
eresolve_tac ([asm_rl,SubtypeE]@rmIHs) ORELSE'


495 
hyp_subst_tac)) end


496 


497 
fun gen_ccs_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls) THEN


498 
clean_ccs_tac) i

17456

499 

0

500 
end

20140

501 
*}


502 


503 


504 
subsection {* Evaluation *}


505 


506 
ML {*


507 


508 
local


509 


510 
structure Data = GenericDataFun


511 
(


512 
type T = thm list;


513 
val empty = [];


514 
val extend = I;

20193

515 
fun merge _ = Drule.merge_rules;

20140

516 
);


517 


518 
in


519 


520 
val eval_add = Thm.declaration_attribute (Data.map o Drule.add_rule);


521 
val eval_del = Thm.declaration_attribute (Data.map o Drule.del_rule);


522 


523 
fun eval_tac ctxt ths =


524 
METAHYPS (fn prems =>


525 
DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get (Context.Proof ctxt)) 1)) 1;


526 


527 
val eval_setup =


528 
Attrib.add_attributes


529 
[("eval", Attrib.add_del_args eval_add eval_del, "declaration of evaluation rule")] #>


530 
Method.add_methods [("eval", Method.thms_ctxt_args (fn ths => fn ctxt =>


531 
Method.SIMPLE_METHOD (CHANGED (eval_tac ctxt ths))), "evaluation")];


532 


533 
end;


534 


535 
*}


536 


537 
setup eval_setup


538 


539 
lemmas eval_rls [eval] = trueV falseV pairV lamV caseVtrue caseVfalse caseVpair caseVlam


540 


541 
lemma applyV [eval]:


542 
assumes "f > lam x. b(x)"


543 
and "b(a) > c"


544 
shows "f ` a > c"


545 
unfolding apply_def by (eval prems)


546 


547 
lemma letV:


548 
assumes 1: "t > a"


549 
and 2: "f(a) > c"


550 
shows "let x be t in f(x) > c"


551 
apply (unfold let_def)


552 
apply (rule 1 [THEN canonical])


553 
apply (tactic {*


554 
REPEAT (DEPTH_SOLVE_1 (resolve_tac (thms "prems" @ thms "eval_rls") 1 ORELSE


555 
etac (thm "substitute") 1)) *})


556 
done


557 


558 
lemma fixV: "f(fix(f)) > c ==> fix(f) > c"


559 
apply (unfold fix_def)


560 
apply (rule applyV)


561 
apply (rule lamV)


562 
apply assumption


563 
done


564 


565 
lemma letrecV:


566 
"h(t,%y. letrec g x be h(x,g) in g(y)) > c ==>


567 
letrec g x be h(x,g) in g(t) > c"


568 
apply (unfold letrec_def)


569 
apply (assumption  rule fixV applyV lamV)+


570 
done


571 


572 
lemmas [eval] = letV letrecV fixV


573 


574 
lemma V_rls [eval]:


575 
"true > true"


576 
"false > false"


577 
"!!b c t u. [ b>true; t>c ] ==> if b then t else u > c"


578 
"!!b c t u. [ b>false; u>c ] ==> if b then t else u > c"


579 
"!!a b. <a,b> > <a,b>"


580 
"!!a b c t h. [ t > <a,b>; h(a,b) > c ] ==> split(t,h) > c"


581 
"zero > zero"


582 
"!!n. succ(n) > succ(n)"


583 
"!!c n t u. [ n > zero; t > c ] ==> ncase(n,t,u) > c"


584 
"!!c n t u x. [ n > succ(x); u(x) > c ] ==> ncase(n,t,u) > c"


585 
"!!c n t u. [ n > zero; t > c ] ==> nrec(n,t,u) > c"


586 
"!!c n t u x. [ n>succ(x); u(x,nrec(x,t,u))>c ] ==> nrec(n,t,u)>c"


587 
"[] > []"


588 
"!!h t. h$t > h$t"


589 
"!!c l t u. [ l > []; t > c ] ==> lcase(l,t,u) > c"


590 
"!!c l t u x xs. [ l > x$xs; u(x,xs) > c ] ==> lcase(l,t,u) > c"


591 
"!!c l t u. [ l > []; t > c ] ==> lrec(l,t,u) > c"


592 
"!!c l t u x xs. [ l>x$xs; u(x,xs,lrec(xs,t,u))>c ] ==> lrec(l,t,u)>c"


593 
unfolding data_defs by eval+


594 


595 


596 
subsection {* Factorial *}


597 


598 
lemma


599 
"letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h))))


600 
in f(succ(succ(zero))) > ?a"


601 
by eval


602 


603 
lemma


604 
"letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h))))


605 
in f(succ(succ(succ(zero)))) > ?a"


606 
by eval


607 


608 
subsection {* Less Than Or Equal *}


609 


610 
lemma


611 
"letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))


612 
in f(<succ(zero), succ(zero)>) > ?a"


613 
by eval


614 


615 
lemma


616 
"letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))


617 
in f(<succ(zero), succ(succ(succ(succ(zero))))>) > ?a"


618 
by eval


619 


620 
lemma


621 
"letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))


622 
in f(<succ(succ(succ(succ(succ(zero))))), succ(succ(succ(succ(zero))))>) > ?a"


623 
by eval


624 


625 


626 
subsection {* Reverse *}


627 


628 
lemma


629 
"letrec id l be lcase(l,[],%x xs. x$id(xs))


630 
in id(zero$succ(zero)$[]) > ?a"


631 
by eval


632 


633 
lemma


634 
"letrec rev l be lcase(l,[],%x xs. lrec(rev(xs),x$[],%y ys g. y$g))


635 
in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) > ?a"


636 
by eval


637 


638 
end
