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"

24825

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

0

20 
NatPR :: "i set"


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


22 

24825

23 
defs

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

24825

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

20140

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

24825

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

20140

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

24034

509 
structure Data = NamedThmsFun(val name = "eval" val description = "evaluation rules");

20140

510 
in


511 


512 
fun eval_tac ctxt ths =


513 
METAHYPS (fn prems =>

24034

514 
DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get ctxt) 1)) 1;

20140

515 


516 
val eval_setup =

24034

517 
Data.setup #>

20140

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


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


520 


521 
end;


522 


523 
*}


524 


525 
setup eval_setup


526 


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


528 


529 
lemma applyV [eval]:


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


531 
and "b(a) > c"


532 
shows "f ` a > c"


533 
unfolding apply_def by (eval prems)


534 


535 
lemma letV:


536 
assumes 1: "t > a"


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


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


539 
apply (unfold let_def)


540 
apply (rule 1 [THEN canonical])


541 
apply (tactic {*


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


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


544 
done


545 


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


547 
apply (unfold fix_def)


548 
apply (rule applyV)


549 
apply (rule lamV)


550 
apply assumption


551 
done


552 


553 
lemma letrecV:


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


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


556 
apply (unfold letrec_def)


557 
apply (assumption  rule fixV applyV lamV)+


558 
done


559 


560 
lemmas [eval] = letV letrecV fixV


561 


562 
lemma V_rls [eval]:


563 
"true > true"


564 
"false > false"


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


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


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


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


569 
"zero > zero"


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


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


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


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


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


575 
"[] > []"


576 
"!!h t. h$t > h$t"


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


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


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


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


581 
unfolding data_defs by eval+


582 


583 


584 
subsection {* Factorial *}


585 


586 
lemma


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


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


589 
by eval


590 


591 
lemma


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


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


594 
by eval


595 


596 
subsection {* Less Than Or Equal *}


597 


598 
lemma


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


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


601 
by eval


602 


603 
lemma


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


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


606 
by eval


607 


608 
lemma


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


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


611 
by eval


612 


613 


614 
subsection {* Reverse *}


615 


616 
lemma


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


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


619 
by eval


620 


621 
lemma


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


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


624 
by eval


625 


626 
end
