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)


343 
apply assumption+


344 
done


345 


346 
lemma hyprcall3T:


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


348 
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)"


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


350 
and 4: "a:A"


351 
and 5: "b:B"


352 
and 6: "c:C"


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


354 
shows P


355 
apply (rule 3)


356 
apply (rule 1 [symmetric])


357 
apply (rule rcall3T)


358 
apply assumption+


359 
done


360 


361 
lemmas hyprcallTs = hyprcallT hyprcall2T hyprcall3T


362 


363 


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


365 


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


367 


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


369 


370 
lemma rmIH3:


371 
"[ 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);


372 
P ] ==>


373 
P" .


374 


375 
lemmas rmIHs = rmIH1 rmIH2 rmIH3


376 


377 


378 
subsection {* Lemmas for constructors and subtypes *}


379 


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


381 
(* correctly by applying SubtypeI *)


382 


383 
lemma Subtype_canTs:


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


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


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


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


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


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


390 


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


392 
apply (erule letB [THEN ssubst])


393 
apply assumption


394 
done


395 


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


397 
apply (erule applyT)


398 
apply assumption


399 
done


400 


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


402 
by blast


403 


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


405 
by blast


406 


407 
lemmas rcall_lemmas = asm_rl rcall_lemma1 SubtypeD1 rcall_lemma2


408 


409 


410 
subsection {* Typechecking *}


411 


412 
ML {*


413 


414 
local


415 


416 
val type_rls =


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


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


419 


420 
val rcallT = thm "rcallT";


421 
val rcall2T = thm "rcall2T";


422 
val rcall3T = thm "rcall3T";


423 
val rcallTs = thms "rcallTs";


424 
val rcall_lemmas = thms "rcall_lemmas";


425 
val SubtypeE = thm "SubtypeE";


426 
val SubtypeI = thm "SubtypeI";


427 
val rmIHs = thms "rmIHs";


428 
val hyprcallTs = thms "hyprcallTs";


429 


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


431 
 bvars _ l = l


432 


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


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


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


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


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


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


439 


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


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


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


443 
could_unify(x,hd (prems_of rcall3T))


444 


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


446 
let val bvs = bvars Bi []


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


448 
val rnames = map (fn x=>


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


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


451 
fun try_IHs [] = no_tac


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


453 
in try_IHs rnames end)


454 


455 
fun is_rigid_prog t =


456 
case (Logic.strip_assums_concl t) of


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


458 
 _ => false


459 
in


460 


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


462 
in IHinst tac rcallTs i end THEN


463 
eresolve_tac rcall_lemmas i


464 


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


466 
rcall_tac i ORELSE


467 
ematch_tac [SubtypeE] i ORELSE


468 
match_tac [SubtypeI] i


469 


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


471 
if is_rigid_prog Bi then raw_step_tac prems i else no_tac)


472 


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


474 


475 
val tac = typechk_tac [] 1


476 


477 
(*** Clean up Correctness Condictions ***)


478 


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


480 
hyp_subst_tac)


481 


482 
val clean_ccs_tac =


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


484 
in TRY (REPEAT_FIRST (IHinst tac hyprcallTs ORELSE'


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


486 
hyp_subst_tac)) end


487 


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


489 
clean_ccs_tac) i

17456

490 

0

491 
end

20140

492 
*}


493 


494 


495 
subsection {* Evaluation *}


496 


497 
ML {*


498 


499 
local


500 


501 
structure Data = GenericDataFun


502 
(


503 
val name = "CCL/eval";


504 
type T = thm list;


505 
val empty = [];


506 
val extend = I;


507 
fun merge _ (rules1, rules2) = gen_union Drule.eq_thm_prop (rules1, rules2);


508 
fun print _ _ = ();


509 
);


510 


511 
in


512 


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


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


515 


516 
fun eval_tac ctxt ths =


517 
METAHYPS (fn prems =>


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


519 


520 
val eval_setup =


521 
Data.init #>


522 
Attrib.add_attributes


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


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


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


526 


527 
end;


528 


529 
*}


530 


531 
setup eval_setup


532 


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


534 


535 
lemma applyV [eval]:


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


537 
and "b(a) > c"


538 
shows "f ` a > c"


539 
unfolding apply_def by (eval prems)


540 


541 
lemma letV:


542 
assumes 1: "t > a"


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


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


545 
apply (unfold let_def)


546 
apply (rule 1 [THEN canonical])


547 
apply (tactic {*


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


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


550 
done


551 


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


553 
apply (unfold fix_def)


554 
apply (rule applyV)


555 
apply (rule lamV)


556 
apply assumption


557 
done


558 


559 
lemma letrecV:


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


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


562 
apply (unfold letrec_def)


563 
apply (assumption  rule fixV applyV lamV)+


564 
done


565 


566 
lemmas [eval] = letV letrecV fixV


567 


568 
lemma V_rls [eval]:


569 
"true > true"


570 
"false > false"


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


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


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


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


575 
"zero > zero"


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


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


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


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


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


581 
"[] > []"


582 
"!!h t. h$t > h$t"


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


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


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


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


587 
unfolding data_defs by eval+


588 


589 


590 
subsection {* Factorial *}


591 


592 
lemma


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


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


595 
by eval


596 


597 
lemma


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


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


600 
by eval


601 


602 
subsection {* Less Than Or Equal *}


603 


604 
lemma


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


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


607 
by eval


608 


609 
lemma


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


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


612 
by eval


613 


614 
lemma


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


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


617 
by eval


618 


619 


620 
subsection {* Reverse *}


621 


622 
lemma


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


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


625 
by eval


626 


627 
lemma


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


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


630 
by eval


631 


632 
end
