src/CCL/Wfd.thy
author wenzelm
Sat Jun 14 23:52:51 2008 +0200 (2008-06-14)
changeset 27221 31328dc30196
parent 27208 5fe899199f85
child 27239 f2f42f9fa09d
permissions -rw-r--r--
proper context for tactics derived from res_inst_tac;
     1 (*  Title:      CCL/Wfd.thy
     2     ID:         $Id$
     3     Author:     Martin Coen, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 *)
     6 
     7 header {* Well-founded relations in CCL *}
     8 
     9 theory Wfd
    10 imports Trancl Type Hered
    11 begin
    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   lex        ::       "[i set,i set] => i set"      (infixl "**" 70)
    20   NatPR      ::       "i set"
    21   ListPR     ::       "i set => i set"
    22 
    23 defs
    24 
    25   Wfd_def:
    26   "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a. a:P)"
    27 
    28   wf_def:         "wf(R) == {x. x:R & Wfd(R)}"
    29 
    30   wmap_def:       "wmap(f,R) == {p. EX x y. p=<x,y>  &  <f(x),f(y)> : R}"
    31   lex_def:
    32   "ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
    33 
    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 
    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   fun wfd_strengthen_tac ctxt s i =
    58     RuleInsts.res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
    59 *}
    60 
    61 lemma wf_anti_sym: "[| Wfd(r);  <a,x>:r;  <x,a>:r |] ==> P"
    62   apply (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P")
    63    apply blast
    64   apply (erule wfd_induct)
    65   apply blast
    66   done
    67 
    68 lemma wf_anti_refl: "[| Wfd(r);  <a,a>: r |] ==> P"
    69   apply (rule wf_anti_sym)
    70   apply assumption+
    71   done
    72 
    73 
    74 subsection {* Irreflexive transitive closure *}
    75 
    76 lemma trancl_wf:
    77   assumes 1: "Wfd(R)"
    78   shows "Wfd(R^+)"
    79   apply (unfold Wfd_def)
    80   apply (rule allI ballI impI)+
    81 (*must retain the universal formula for later use!*)
    82   apply (rule allE, assumption)
    83   apply (erule mp)
    84   apply (rule 1 [THEN wfd_induct])
    85   apply (rule impI [THEN allI])
    86   apply (erule tranclE)
    87    apply blast
    88   apply (erule spec [THEN mp, THEN spec, THEN mp])
    89    apply assumption+
    90   done
    91 
    92 
    93 subsection {* Lexicographic Ordering *}
    94 
    95 lemma lexXH:
    96   "p : ra**rb <-> (EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))"
    97   unfolding lex_def by blast
    98 
    99 lemma lexI1: "<a,a'> : ra ==> <<a,b>,<a',b'>> : ra**rb"
   100   by (blast intro!: lexXH [THEN iffD2])
   101 
   102 lemma lexI2: "<b,b'> : rb ==> <<a,b>,<a,b'>> : ra**rb"
   103   by (blast intro!: lexXH [THEN iffD2])
   104 
   105 lemma lexE:
   106   assumes 1: "p : ra**rb"
   107     and 2: "!!a a' b b'.[| <a,a'> : ra; p=<<a,b>,<a',b'>> |] ==> R"
   108     and 3: "!!a b b'.[| <b,b'> : rb;  p = <<a,b>,<a,b'>> |] ==> R"
   109   shows R
   110   apply (rule 1 [THEN lexXH [THEN iffD1], THEN exE])
   111   using 2 3
   112   apply blast
   113   done
   114 
   115 lemma lex_pair: "[| p : r**s;  !!a a' b b'. p = <<a,b>,<a',b'>> ==> P |] ==>P"
   116   apply (erule lexE)
   117    apply blast+
   118   done
   119 
   120 lemma lex_wf:
   121   assumes 1: "Wfd(R)"
   122     and 2: "Wfd(S)"
   123   shows "Wfd(R**S)"
   124   apply (unfold Wfd_def)
   125   apply safe
   126   apply (tactic {* wfd_strengthen_tac @{context} "%x. EX a b. x=<a,b>" 1 *})
   127    apply (blast elim!: lex_pair)
   128   apply (subgoal_tac "ALL a b.<a,b>:P")
   129    apply blast
   130   apply (rule 1 [THEN wfd_induct, THEN allI])
   131   apply (rule 2 [THEN wfd_induct, THEN allI]) back
   132   apply (fast elim!: lexE)
   133   done
   134 
   135 
   136 subsection {* Mapping *}
   137 
   138 lemma wmapXH: "p : wmap(f,r) <-> (EX x y. p=<x,y>  &  <f(x),f(y)> : r)"
   139   unfolding wmap_def by blast
   140 
   141 lemma wmapI: "<f(a),f(b)> : r ==> <a,b> : wmap(f,r)"
   142   by (blast intro!: wmapXH [THEN iffD2])
   143 
   144 lemma wmapE: "[| p : wmap(f,r);  !!a b.[| <f(a),f(b)> : r;  p=<a,b> |] ==> R |] ==> R"
   145   by (blast dest!: wmapXH [THEN iffD1])
   146 
   147 lemma wmap_wf:
   148   assumes 1: "Wfd(r)"
   149   shows "Wfd(wmap(f,r))"
   150   apply (unfold Wfd_def)
   151   apply clarify
   152   apply (subgoal_tac "ALL b. ALL a. f (a) =b-->a:P")
   153    apply blast
   154   apply (rule 1 [THEN wfd_induct, THEN allI])
   155   apply clarify
   156   apply (erule spec [THEN mp])
   157   apply (safe elim!: wmapE)
   158   apply (erule spec [THEN mp, THEN spec, THEN mp])
   159    apply assumption
   160    apply (rule refl)
   161   done
   162 
   163 
   164 subsection {* Projections *}
   165 
   166 lemma wfstI: "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)"
   167   apply (rule wmapI)
   168   apply simp
   169   done
   170 
   171 lemma wsndI: "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)"
   172   apply (rule wmapI)
   173   apply simp
   174   done
   175 
   176 lemma wthdI: "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)"
   177   apply (rule wmapI)
   178   apply simp
   179   done
   180 
   181 
   182 subsection {* Ground well-founded relations *}
   183 
   184 lemma wfI: "[| Wfd(r);  a : r |] ==> a : wf(r)"
   185   unfolding wf_def by blast
   186 
   187 lemma Empty_wf: "Wfd({})"
   188   unfolding Wfd_def by (blast elim: EmptyXH [THEN iffD1, THEN FalseE])
   189 
   190 lemma wf_wf: "Wfd(wf(R))"
   191   unfolding wf_def
   192   apply (rule_tac Q = "Wfd(R)" in excluded_middle [THEN disjE])
   193    apply simp_all
   194   apply (rule Empty_wf)
   195   done
   196 
   197 lemma NatPRXH: "p : NatPR <-> (EX x:Nat. p=<x,succ(x)>)"
   198   unfolding NatPR_def by blast
   199 
   200 lemma ListPRXH: "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=<t,h$t>)"
   201   unfolding ListPR_def by blast
   202 
   203 lemma NatPRI: "x : Nat ==> <x,succ(x)> : NatPR"
   204   by (auto simp: NatPRXH)
   205 
   206 lemma ListPRI: "[| t : List(A); h : A |] ==> <t,h $ t> : ListPR(A)"
   207   by (auto simp: ListPRXH)
   208 
   209 lemma NatPR_wf: "Wfd(NatPR)"
   210   apply (unfold Wfd_def)
   211   apply clarify
   212   apply (tactic {* wfd_strengthen_tac @{context} "%x. x:Nat" 1 *})
   213    apply (fastsimp iff: NatPRXH)
   214   apply (erule Nat_ind)
   215    apply (fastsimp iff: NatPRXH)+
   216   done
   217 
   218 lemma ListPR_wf: "Wfd(ListPR(A))"
   219   apply (unfold Wfd_def)
   220   apply clarify
   221   apply (tactic {* wfd_strengthen_tac @{context} "%x. x:List (A)" 1 *})
   222    apply (fastsimp iff: ListPRXH)
   223   apply (erule List_ind)
   224    apply (fastsimp iff: ListPRXH)+
   225   done
   226 
   227 
   228 subsection {* General Recursive Functions *}
   229 
   230 lemma letrecT:
   231   assumes 1: "a : A"
   232     and 2: "!!p g.[| p:A; ALL x:{x: A. <x,p>:wf(R)}. g(x) : D(x) |] ==> h(p,g) : D(p)"
   233   shows "letrec g x be h(x,g) in g(a) : D(a)"
   234   apply (rule 1 [THEN rev_mp])
   235   apply (rule wf_wf [THEN wfd_induct])
   236   apply (subst letrecB)
   237   apply (rule impI)
   238   apply (erule 2)
   239   apply blast
   240   done
   241 
   242 lemma SPLITB: "SPLIT(<a,b>,B) = B(a,b)"
   243   unfolding SPLIT_def
   244   apply (rule set_ext)
   245   apply blast
   246   done
   247 
   248 lemma letrec2T:
   249   assumes "a : A"
   250     and "b : B"
   251     and "!!p q g.[| p:A; q:B;
   252               ALL x:A. ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==> 
   253                 h(p,q,g) : D(p,q)"
   254   shows "letrec g x y be h(x,y,g) in g(a,b) : D(a,b)"
   255   apply (unfold letrec2_def)
   256   apply (rule SPLITB [THEN subst])
   257   apply (assumption | rule letrecT pairT splitT prems)+
   258   apply (subst SPLITB)
   259   apply (assumption | rule ballI SubtypeI prems)+
   260   apply (rule SPLITB [THEN subst])
   261   apply (assumption | rule letrecT SubtypeI pairT splitT prems |
   262     erule bspec SubtypeE sym [THEN subst])+
   263   done
   264 
   265 lemma lem: "SPLIT(<a,<b,c>>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)"
   266   by (simp add: SPLITB)
   267 
   268 lemma letrec3T:
   269   assumes "a : A"
   270     and "b : B"
   271     and "c : C"
   272     and "!!p q r g.[| p:A; q:B; r:C;
   273        ALL x:A. ALL y:B. ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}.  
   274                                                         g(x,y,z) : D(x,y,z) |] ==> 
   275                 h(p,q,r,g) : D(p,q,r)"
   276   shows "letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)"
   277   apply (unfold letrec3_def)
   278   apply (rule lem [THEN subst])
   279   apply (assumption | rule letrecT pairT splitT prems)+
   280   apply (simp add: SPLITB)
   281   apply (assumption | rule ballI SubtypeI prems)+
   282   apply (rule lem [THEN subst])
   283   apply (assumption | rule letrecT SubtypeI pairT splitT prems |
   284     erule bspec SubtypeE sym [THEN subst])+
   285   done
   286 
   287 lemmas letrecTs = letrecT letrec2T letrec3T
   288 
   289 
   290 subsection {* Type Checking for Recursive Calls *}
   291 
   292 lemma rcallT:
   293   "[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x);  
   294       g(a) : D(a) ==> g(a) : E;  a:A;  <a,p>:wf(R) |] ==>  
   295   g(a) : E"
   296   by blast
   297 
   298 lemma rcall2T:
   299   "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y);  
   300       g(a,b) : D(a,b) ==> g(a,b) : E;  a:A;  b:B;  <<a,b>,<p,q>>:wf(R) |] ==>  
   301   g(a,b) : E"
   302   by blast
   303 
   304 lemma rcall3T:
   305   "[| 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);  
   306       g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E;   
   307       a:A;  b:B;  c:C;  <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==>  
   308   g(a,b,c) : E"
   309   by blast
   310 
   311 lemmas rcallTs = rcallT rcall2T rcall3T
   312 
   313 
   314 subsection {* Instantiating an induction hypothesis with an equality assumption *}
   315 
   316 lemma hyprcallT:
   317   assumes 1: "g(a) = b"
   318     and 2: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x)"
   319     and 3: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> b=g(a) ==> g(a) : D(a) ==> P"
   320     and 4: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> a:A"
   321     and 5: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> <a,p>:wf(R)"
   322   shows P
   323   apply (rule 3 [OF 2, OF 1 [symmetric]])
   324   apply (rule rcallT [OF 2])
   325     apply assumption
   326    apply (rule 4 [OF 2])
   327   apply (rule 5 [OF 2])
   328   done
   329 
   330 lemma hyprcall2T:
   331   assumes 1: "g(a,b) = c"
   332     and 2: "ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y)"
   333     and 3: "[| c=g(a,b);  g(a,b) : D(a,b) |] ==> P"
   334     and 4: "a:A"
   335     and 5: "b:B"
   336     and 6: "<<a,b>,<p,q>>:wf(R)"
   337   shows P
   338   apply (rule 3)
   339     apply (rule 1 [symmetric])
   340   apply (rule rcall2T)
   341       apply (rule 2)
   342      apply assumption
   343     apply (rule 4)
   344    apply (rule 5)
   345   apply (rule 6)
   346   done
   347 
   348 lemma hyprcall3T:
   349   assumes 1: "g(a,b,c) = d"
   350     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)"
   351     and 3: "[| d=g(a,b,c);  g(a,b,c) : D(a,b,c) |] ==> P"
   352     and 4: "a:A"
   353     and 5: "b:B"
   354     and 6: "c:C"
   355     and 7: "<<a,<b,c>>,<p,<q,r>>> : wf(R)"
   356   shows P
   357   apply (rule 3)
   358    apply (rule 1 [symmetric])
   359   apply (rule rcall3T)
   360        apply (rule 2)
   361       apply assumption
   362      apply (rule 4)
   363     apply (rule 5)
   364    apply (rule 6)
   365   apply (rule 7)
   366   done
   367 
   368 lemmas hyprcallTs = hyprcallT hyprcall2T hyprcall3T
   369 
   370 
   371 subsection {* Rules to Remove Induction Hypotheses after Type Checking *}
   372 
   373 lemma rmIH1: "[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); P |] ==> P" .
   374 
   375 lemma rmIH2: "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> P" .
   376   
   377 lemma rmIH3:
   378  "[| 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);  
   379      P |] ==>  
   380      P" .
   381 
   382 lemmas rmIHs = rmIH1 rmIH2 rmIH3
   383 
   384 
   385 subsection {* Lemmas for constructors and subtypes *}
   386 
   387 (* 0-ary constructors do not need additional rules as they are handled *)
   388 (*                                      correctly by applying SubtypeI *)
   389 
   390 lemma Subtype_canTs:
   391   "!!a b A B P. a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}"
   392   "!!a A B P. a : {x:A. P(inl(x))} ==> inl(a) : {x:A+B. P(x)}"
   393   "!!b A B P. b : {x:B. P(inr(x))} ==> inr(b) : {x:A+B. P(x)}"
   394   "!!a P. a : {x:Nat. P(succ(x))} ==> succ(a) : {x:Nat. P(x)}"
   395   "!!h t A P. h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"
   396   by (assumption | rule SubtypeI canTs icanTs | erule SubtypeE)+
   397 
   398 lemma letT: "[| f(t):B;  ~t=bot  |] ==> let x be t in f(x) : B"
   399   apply (erule letB [THEN ssubst])
   400   apply assumption
   401   done
   402 
   403 lemma applyT2: "[| a:A;  f : Pi(A,B)  |] ==> f ` a  : B(a)"
   404   apply (erule applyT)
   405   apply assumption
   406   done
   407 
   408 lemma rcall_lemma1: "[| a:A;  a:A ==> P(a) |] ==> a : {x:A. P(x)}"
   409   by blast
   410 
   411 lemma rcall_lemma2: "[| a:{x:A. Q(x)};  [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A. P(x)}"
   412   by blast
   413 
   414 lemmas rcall_lemmas = asm_rl rcall_lemma1 SubtypeD1 rcall_lemma2
   415 
   416 
   417 subsection {* Typechecking *}
   418 
   419 ML {*
   420 
   421 local
   422 
   423 val type_rls =
   424   @{thms canTs} @ @{thms icanTs} @ @{thms applyT2} @ @{thms ncanTs} @ @{thms incanTs} @
   425   @{thms precTs} @ @{thms letrecTs} @ @{thms letT} @ @{thms Subtype_canTs};
   426 
   427 fun bvars (Const("all",_) $ Abs(s,_,t)) l = bvars t (s::l)
   428   | bvars _ l = l
   429 
   430 fun get_bno l n (Const("all",_) $ Abs(s,_,t)) = get_bno (s::l) n t
   431   | get_bno l n (Const("Trueprop",_) $ t) = get_bno l n t
   432   | get_bno l n (Const("Ball",_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t
   433   | get_bno l n (Const("mem",_) $ t $ _) = get_bno l n t
   434   | get_bno l n (t $ s) = get_bno l n t
   435   | get_bno l n (Bound m) = (m-length(l),n)
   436 
   437 (* Not a great way of identifying induction hypothesis! *)
   438 fun could_IH x = could_unify(x,hd (prems_of @{thm rcallT})) orelse
   439                  could_unify(x,hd (prems_of @{thm rcall2T})) orelse
   440                  could_unify(x,hd (prems_of @{thm rcall3T}))
   441 
   442 fun IHinst tac rls = SUBGOAL (fn (Bi,i) =>
   443   let val bvs = bvars Bi []
   444       val ihs = List.filter could_IH (Logic.strip_assums_hyp Bi)
   445       val rnames = map (fn x=>
   446                     let val (a,b) = get_bno [] 0 x
   447                     in (List.nth(bvs,a),b) end) ihs
   448       fun try_IHs [] = no_tac
   449         | try_IHs ((x,y)::xs) = tac [(("g", 0), x)] (List.nth(rls,y-1)) i ORELSE (try_IHs xs)
   450   in try_IHs rnames end)
   451 
   452 fun is_rigid_prog t =
   453      case (Logic.strip_assums_concl t) of
   454         (Const("Trueprop",_) $ (Const("mem",_) $ a $ _)) => (term_vars a = [])
   455        | _ => false
   456 in
   457 
   458 fun rcall_tac ctxt i =
   459   let fun tac ps rl i = RuleInsts.res_inst_tac ctxt ps rl i THEN atac i
   460   in IHinst tac @{thms rcallTs} i end
   461   THEN eresolve_tac @{thms rcall_lemmas} i
   462 
   463 fun raw_step_tac ctxt prems i = ares_tac (prems@type_rls) i ORELSE
   464                            rcall_tac ctxt i ORELSE
   465                            ematch_tac [@{thm SubtypeE}] i ORELSE
   466                            match_tac [@{thm SubtypeI}] i
   467 
   468 fun tc_step_tac ctxt prems = SUBGOAL (fn (Bi,i) =>
   469           if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac)
   470 
   471 fun typechk_tac ctxt rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls)) i
   472 
   473 fun tac ctxt = typechk_tac ctxt [] 1
   474 
   475 (*** Clean up Correctness Condictions ***)
   476 
   477 val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([@{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
   478                                  hyp_subst_tac)
   479 
   480 fun clean_ccs_tac ctxt =
   481   let fun tac ps rl i = RuleInsts.eres_inst_tac ctxt ps rl i THEN atac i in
   482     TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE'
   483     eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
   484     hyp_subst_tac))
   485   end
   486 
   487 fun gen_ccs_tac ctxt rls i =
   488   SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls) THEN clean_ccs_tac ctxt) i
   489 
   490 end
   491 *}
   492 
   493 
   494 subsection {* Evaluation *}
   495 
   496 ML {*
   497 
   498 local
   499   structure Data = NamedThmsFun(val name = "eval" val description = "evaluation rules");
   500 in
   501 
   502 fun eval_tac ctxt ths =
   503   METAHYPS (fn prems =>
   504     DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get ctxt) 1)) 1;
   505 
   506 val eval_setup =
   507   Data.setup #>
   508   Method.add_methods [("eval", Method.thms_ctxt_args (fn ths => fn ctxt =>
   509     Method.SIMPLE_METHOD (CHANGED (eval_tac ctxt ths))), "evaluation")];
   510 
   511 end;
   512 
   513 *}
   514 
   515 setup eval_setup
   516 
   517 lemmas eval_rls [eval] = trueV falseV pairV lamV caseVtrue caseVfalse caseVpair caseVlam
   518 
   519 lemma applyV [eval]:
   520   assumes "f ---> lam x. b(x)"
   521     and "b(a) ---> c"
   522   shows "f ` a ---> c"
   523   unfolding apply_def by (eval prems)
   524 
   525 lemma letV:
   526   assumes 1: "t ---> a"
   527     and 2: "f(a) ---> c"
   528   shows "let x be t in f(x) ---> c"
   529   apply (unfold let_def)
   530   apply (rule 1 [THEN canonical])
   531   apply (tactic {*
   532     REPEAT (DEPTH_SOLVE_1 (resolve_tac (@{thms assms} @ @{thms eval_rls}) 1 ORELSE
   533       etac @{thm substitute} 1)) *})
   534   done
   535 
   536 lemma fixV: "f(fix(f)) ---> c ==> fix(f) ---> c"
   537   apply (unfold fix_def)
   538   apply (rule applyV)
   539    apply (rule lamV)
   540   apply assumption
   541   done
   542 
   543 lemma letrecV:
   544   "h(t,%y. letrec g x be h(x,g) in g(y)) ---> c ==>  
   545                  letrec g x be h(x,g) in g(t) ---> c"
   546   apply (unfold letrec_def)
   547   apply (assumption | rule fixV applyV  lamV)+
   548   done
   549 
   550 lemmas [eval] = letV letrecV fixV
   551 
   552 lemma V_rls [eval]:
   553   "true ---> true"
   554   "false ---> false"
   555   "!!b c t u. [| b--->true;  t--->c |] ==> if b then t else u ---> c"
   556   "!!b c t u. [| b--->false;  u--->c |] ==> if b then t else u ---> c"
   557   "!!a b. <a,b> ---> <a,b>"
   558   "!!a b c t h. [| t ---> <a,b>;  h(a,b) ---> c |] ==> split(t,h) ---> c"
   559   "zero ---> zero"
   560   "!!n. succ(n) ---> succ(n)"
   561   "!!c n t u. [| n ---> zero; t ---> c |] ==> ncase(n,t,u) ---> c"
   562   "!!c n t u x. [| n ---> succ(x); u(x) ---> c |] ==> ncase(n,t,u) ---> c"
   563   "!!c n t u. [| n ---> zero; t ---> c |] ==> nrec(n,t,u) ---> c"
   564   "!!c n t u x. [| n--->succ(x); u(x,nrec(x,t,u))--->c |] ==> nrec(n,t,u)--->c"
   565   "[] ---> []"
   566   "!!h t. h$t ---> h$t"
   567   "!!c l t u. [| l ---> []; t ---> c |] ==> lcase(l,t,u) ---> c"
   568   "!!c l t u x xs. [| l ---> x$xs; u(x,xs) ---> c |] ==> lcase(l,t,u) ---> c"
   569   "!!c l t u. [| l ---> []; t ---> c |] ==> lrec(l,t,u) ---> c"
   570   "!!c l t u x xs. [| l--->x$xs; u(x,xs,lrec(xs,t,u))--->c |] ==> lrec(l,t,u)--->c"
   571   unfolding data_defs by eval+
   572 
   573 
   574 subsection {* Factorial *}
   575 
   576 lemma
   577   "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h))))  
   578    in f(succ(succ(zero))) ---> ?a"
   579   by eval
   580 
   581 lemma
   582   "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h))))  
   583    in f(succ(succ(succ(zero)))) ---> ?a"
   584   by eval
   585 
   586 subsection {* Less Than Or Equal *}
   587 
   588 lemma
   589   "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
   590    in f(<succ(zero), succ(zero)>) ---> ?a"
   591   by eval
   592 
   593 lemma
   594   "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
   595    in f(<succ(zero), succ(succ(succ(succ(zero))))>) ---> ?a"
   596   by eval
   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(succ(succ(succ(succ(zero))))), succ(succ(succ(succ(zero))))>) ---> ?a"
   601   by eval
   602 
   603 
   604 subsection {* Reverse *}
   605 
   606 lemma
   607   "letrec id l be lcase(l,[],%x xs. x$id(xs))  
   608    in id(zero$succ(zero)$[]) ---> ?a"
   609   by eval
   610 
   611 lemma
   612   "letrec rev l be lcase(l,[],%x xs. lrec(rev(xs),x$[],%y ys g. y$g))  
   613    in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a"
   614   by eval
   615 
   616 end