src/CCL/Wfd.thy
author wenzelm
Thu Jul 02 17:34:14 2009 +0200 (2009-07-02)
changeset 31902 862ae16a799d
parent 30515 bca05b17b618
child 32211 752dbe71cc89
permissions -rw-r--r--
renamed NamedThmsFun to Named_Thms;
simplified/unified names of instances of Named_Thms;
     1 (*  Title:      CCL/Wfd.thy
     2     Author:     Martin Coen, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 *)
     5 
     6 header {* Well-founded relations in CCL *}
     7 
     8 theory Wfd
     9 imports Trancl Type Hered
    10 begin
    11 
    12 consts
    13       (*** Predicates ***)
    14   Wfd        ::       "[i set] => o"
    15       (*** Relations ***)
    16   wf         ::       "[i set] => i set"
    17   wmap       ::       "[i=>i,i set] => i set"
    18   lex        ::       "[i set,i set] => i set"      (infixl "**" 70)
    19   NatPR      ::       "i set"
    20   ListPR     ::       "i set => i set"
    21 
    22 defs
    23 
    24   Wfd_def:
    25   "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a. a:P)"
    26 
    27   wf_def:         "wf(R) == {x. x:R & Wfd(R)}"
    28 
    29   wmap_def:       "wmap(f,R) == {p. EX x y. p=<x,y>  &  <f(x),f(y)> : R}"
    30   lex_def:
    31   "ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
    32 
    33   NatPR_def:      "NatPR == {p. EX x:Nat. p=<x,succ(x)>}"
    34   ListPR_def:     "ListPR(A) == {p. EX h:A. EX t:List(A). p=<t,h$t>}"
    35 
    36 
    37 lemma wfd_induct:
    38   assumes 1: "Wfd(R)"
    39     and 2: "!!x.[| ALL y. <y,x>: R --> P(y) |] ==> P(x)"
    40   shows "P(a)"
    41   apply (rule 1 [unfolded Wfd_def, rule_format, THEN CollectD])
    42   using 2 apply blast
    43   done
    44 
    45 lemma wfd_strengthen_lemma:
    46   assumes 1: "!!x y.<x,y> : R ==> Q(x)"
    47     and 2: "ALL x. (ALL y. <y,x> : R --> y : P) --> x : P"
    48     and 3: "!!x. Q(x) ==> x:P"
    49   shows "a:P"
    50   apply (rule 2 [rule_format])
    51   using 1 3
    52   apply blast
    53   done
    54 
    55 ML {*
    56   fun wfd_strengthen_tac ctxt s i =
    57     res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
    58 *}
    59 
    60 lemma wf_anti_sym: "[| Wfd(r);  <a,x>:r;  <x,a>:r |] ==> P"
    61   apply (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P")
    62    apply blast
    63   apply (erule wfd_induct)
    64   apply blast
    65   done
    66 
    67 lemma wf_anti_refl: "[| Wfd(r);  <a,a>: r |] ==> P"
    68   apply (rule wf_anti_sym)
    69   apply assumption+
    70   done
    71 
    72 
    73 subsection {* Irreflexive transitive closure *}
    74 
    75 lemma trancl_wf:
    76   assumes 1: "Wfd(R)"
    77   shows "Wfd(R^+)"
    78   apply (unfold Wfd_def)
    79   apply (rule allI ballI impI)+
    80 (*must retain the universal formula for later use!*)
    81   apply (rule allE, assumption)
    82   apply (erule mp)
    83   apply (rule 1 [THEN wfd_induct])
    84   apply (rule impI [THEN allI])
    85   apply (erule tranclE)
    86    apply blast
    87   apply (erule spec [THEN mp, THEN spec, THEN mp])
    88    apply assumption+
    89   done
    90 
    91 
    92 subsection {* Lexicographic Ordering *}
    93 
    94 lemma lexXH:
    95   "p : ra**rb <-> (EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))"
    96   unfolding lex_def by blast
    97 
    98 lemma lexI1: "<a,a'> : ra ==> <<a,b>,<a',b'>> : ra**rb"
    99   by (blast intro!: lexXH [THEN iffD2])
   100 
   101 lemma lexI2: "<b,b'> : rb ==> <<a,b>,<a,b'>> : ra**rb"
   102   by (blast intro!: lexXH [THEN iffD2])
   103 
   104 lemma lexE:
   105   assumes 1: "p : ra**rb"
   106     and 2: "!!a a' b b'.[| <a,a'> : ra; p=<<a,b>,<a',b'>> |] ==> R"
   107     and 3: "!!a b b'.[| <b,b'> : rb;  p = <<a,b>,<a,b'>> |] ==> R"
   108   shows R
   109   apply (rule 1 [THEN lexXH [THEN iffD1], THEN exE])
   110   using 2 3
   111   apply blast
   112   done
   113 
   114 lemma lex_pair: "[| p : r**s;  !!a a' b b'. p = <<a,b>,<a',b'>> ==> P |] ==>P"
   115   apply (erule lexE)
   116    apply blast+
   117   done
   118 
   119 lemma lex_wf:
   120   assumes 1: "Wfd(R)"
   121     and 2: "Wfd(S)"
   122   shows "Wfd(R**S)"
   123   apply (unfold Wfd_def)
   124   apply safe
   125   apply (tactic {* wfd_strengthen_tac @{context} "%x. EX a b. x=<a,b>" 1 *})
   126    apply (blast elim!: lex_pair)
   127   apply (subgoal_tac "ALL a b.<a,b>:P")
   128    apply blast
   129   apply (rule 1 [THEN wfd_induct, THEN allI])
   130   apply (rule 2 [THEN wfd_induct, THEN allI]) back
   131   apply (fast elim!: lexE)
   132   done
   133 
   134 
   135 subsection {* Mapping *}
   136 
   137 lemma wmapXH: "p : wmap(f,r) <-> (EX x y. p=<x,y>  &  <f(x),f(y)> : r)"
   138   unfolding wmap_def by blast
   139 
   140 lemma wmapI: "<f(a),f(b)> : r ==> <a,b> : wmap(f,r)"
   141   by (blast intro!: wmapXH [THEN iffD2])
   142 
   143 lemma wmapE: "[| p : wmap(f,r);  !!a b.[| <f(a),f(b)> : r;  p=<a,b> |] ==> R |] ==> R"
   144   by (blast dest!: wmapXH [THEN iffD1])
   145 
   146 lemma wmap_wf:
   147   assumes 1: "Wfd(r)"
   148   shows "Wfd(wmap(f,r))"
   149   apply (unfold Wfd_def)
   150   apply clarify
   151   apply (subgoal_tac "ALL b. ALL a. f (a) =b-->a:P")
   152    apply blast
   153   apply (rule 1 [THEN wfd_induct, THEN allI])
   154   apply clarify
   155   apply (erule spec [THEN mp])
   156   apply (safe elim!: wmapE)
   157   apply (erule spec [THEN mp, THEN spec, THEN mp])
   158    apply assumption
   159    apply (rule refl)
   160   done
   161 
   162 
   163 subsection {* Projections *}
   164 
   165 lemma wfstI: "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)"
   166   apply (rule wmapI)
   167   apply simp
   168   done
   169 
   170 lemma wsndI: "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)"
   171   apply (rule wmapI)
   172   apply simp
   173   done
   174 
   175 lemma wthdI: "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)"
   176   apply (rule wmapI)
   177   apply simp
   178   done
   179 
   180 
   181 subsection {* Ground well-founded relations *}
   182 
   183 lemma wfI: "[| Wfd(r);  a : r |] ==> a : wf(r)"
   184   unfolding wf_def by blast
   185 
   186 lemma Empty_wf: "Wfd({})"
   187   unfolding Wfd_def by (blast elim: EmptyXH [THEN iffD1, THEN FalseE])
   188 
   189 lemma wf_wf: "Wfd(wf(R))"
   190   unfolding wf_def
   191   apply (rule_tac Q = "Wfd(R)" in excluded_middle [THEN disjE])
   192    apply simp_all
   193   apply (rule Empty_wf)
   194   done
   195 
   196 lemma NatPRXH: "p : NatPR <-> (EX x:Nat. p=<x,succ(x)>)"
   197   unfolding NatPR_def by blast
   198 
   199 lemma ListPRXH: "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=<t,h$t>)"
   200   unfolding ListPR_def by blast
   201 
   202 lemma NatPRI: "x : Nat ==> <x,succ(x)> : NatPR"
   203   by (auto simp: NatPRXH)
   204 
   205 lemma ListPRI: "[| t : List(A); h : A |] ==> <t,h $ t> : ListPR(A)"
   206   by (auto simp: ListPRXH)
   207 
   208 lemma NatPR_wf: "Wfd(NatPR)"
   209   apply (unfold Wfd_def)
   210   apply clarify
   211   apply (tactic {* wfd_strengthen_tac @{context} "%x. x:Nat" 1 *})
   212    apply (fastsimp iff: NatPRXH)
   213   apply (erule Nat_ind)
   214    apply (fastsimp iff: NatPRXH)+
   215   done
   216 
   217 lemma ListPR_wf: "Wfd(ListPR(A))"
   218   apply (unfold Wfd_def)
   219   apply clarify
   220   apply (tactic {* wfd_strengthen_tac @{context} "%x. x:List (A)" 1 *})
   221    apply (fastsimp iff: ListPRXH)
   222   apply (erule List_ind)
   223    apply (fastsimp iff: ListPRXH)+
   224   done
   225 
   226 
   227 subsection {* General Recursive Functions *}
   228 
   229 lemma letrecT:
   230   assumes 1: "a : A"
   231     and 2: "!!p g.[| p:A; ALL x:{x: A. <x,p>:wf(R)}. g(x) : D(x) |] ==> h(p,g) : D(p)"
   232   shows "letrec g x be h(x,g) in g(a) : D(a)"
   233   apply (rule 1 [THEN rev_mp])
   234   apply (rule wf_wf [THEN wfd_induct])
   235   apply (subst letrecB)
   236   apply (rule impI)
   237   apply (erule 2)
   238   apply blast
   239   done
   240 
   241 lemma SPLITB: "SPLIT(<a,b>,B) = B(a,b)"
   242   unfolding SPLIT_def
   243   apply (rule set_ext)
   244   apply blast
   245   done
   246 
   247 lemma letrec2T:
   248   assumes "a : A"
   249     and "b : B"
   250     and "!!p q g.[| p:A; q:B;
   251               ALL x:A. ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==> 
   252                 h(p,q,g) : D(p,q)"
   253   shows "letrec g x y be h(x,y,g) in g(a,b) : D(a,b)"
   254   apply (unfold letrec2_def)
   255   apply (rule SPLITB [THEN subst])
   256   apply (assumption | rule letrecT pairT splitT prems)+
   257   apply (subst SPLITB)
   258   apply (assumption | rule ballI SubtypeI prems)+
   259   apply (rule SPLITB [THEN subst])
   260   apply (assumption | rule letrecT SubtypeI pairT splitT prems |
   261     erule bspec SubtypeE sym [THEN subst])+
   262   done
   263 
   264 lemma lem: "SPLIT(<a,<b,c>>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)"
   265   by (simp add: SPLITB)
   266 
   267 lemma letrec3T:
   268   assumes "a : A"
   269     and "b : B"
   270     and "c : C"
   271     and "!!p q r g.[| p:A; q:B; r:C;
   272        ALL x:A. ALL y:B. ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}.  
   273                                                         g(x,y,z) : D(x,y,z) |] ==> 
   274                 h(p,q,r,g) : D(p,q,r)"
   275   shows "letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)"
   276   apply (unfold letrec3_def)
   277   apply (rule lem [THEN subst])
   278   apply (assumption | rule letrecT pairT splitT prems)+
   279   apply (simp add: SPLITB)
   280   apply (assumption | rule ballI SubtypeI prems)+
   281   apply (rule lem [THEN subst])
   282   apply (assumption | rule letrecT SubtypeI pairT splitT prems |
   283     erule bspec SubtypeE sym [THEN subst])+
   284   done
   285 
   286 lemmas letrecTs = letrecT letrec2T letrec3T
   287 
   288 
   289 subsection {* Type Checking for Recursive Calls *}
   290 
   291 lemma rcallT:
   292   "[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x);  
   293       g(a) : D(a) ==> g(a) : E;  a:A;  <a,p>:wf(R) |] ==>  
   294   g(a) : E"
   295   by blast
   296 
   297 lemma rcall2T:
   298   "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y);  
   299       g(a,b) : D(a,b) ==> g(a,b) : E;  a:A;  b:B;  <<a,b>,<p,q>>:wf(R) |] ==>  
   300   g(a,b) : E"
   301   by blast
   302 
   303 lemma rcall3T:
   304   "[| 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);  
   305       g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E;   
   306       a:A;  b:B;  c:C;  <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==>  
   307   g(a,b,c) : E"
   308   by blast
   309 
   310 lemmas rcallTs = rcallT rcall2T rcall3T
   311 
   312 
   313 subsection {* Instantiating an induction hypothesis with an equality assumption *}
   314 
   315 lemma hyprcallT:
   316   assumes 1: "g(a) = b"
   317     and 2: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x)"
   318     and 3: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> b=g(a) ==> g(a) : D(a) ==> P"
   319     and 4: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> a:A"
   320     and 5: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> <a,p>:wf(R)"
   321   shows P
   322   apply (rule 3 [OF 2, OF 1 [symmetric]])
   323   apply (rule rcallT [OF 2])
   324     apply assumption
   325    apply (rule 4 [OF 2])
   326   apply (rule 5 [OF 2])
   327   done
   328 
   329 lemma hyprcall2T:
   330   assumes 1: "g(a,b) = c"
   331     and 2: "ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y)"
   332     and 3: "[| c=g(a,b);  g(a,b) : D(a,b) |] ==> P"
   333     and 4: "a:A"
   334     and 5: "b:B"
   335     and 6: "<<a,b>,<p,q>>:wf(R)"
   336   shows P
   337   apply (rule 3)
   338     apply (rule 1 [symmetric])
   339   apply (rule rcall2T)
   340       apply (rule 2)
   341      apply assumption
   342     apply (rule 4)
   343    apply (rule 5)
   344   apply (rule 6)
   345   done
   346 
   347 lemma hyprcall3T:
   348   assumes 1: "g(a,b,c) = d"
   349     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)"
   350     and 3: "[| d=g(a,b,c);  g(a,b,c) : D(a,b,c) |] ==> P"
   351     and 4: "a:A"
   352     and 5: "b:B"
   353     and 6: "c:C"
   354     and 7: "<<a,<b,c>>,<p,<q,r>>> : wf(R)"
   355   shows P
   356   apply (rule 3)
   357    apply (rule 1 [symmetric])
   358   apply (rule rcall3T)
   359        apply (rule 2)
   360       apply assumption
   361      apply (rule 4)
   362     apply (rule 5)
   363    apply (rule 6)
   364   apply (rule 7)
   365   done
   366 
   367 lemmas hyprcallTs = hyprcallT hyprcall2T hyprcall3T
   368 
   369 
   370 subsection {* Rules to Remove Induction Hypotheses after Type Checking *}
   371 
   372 lemma rmIH1: "[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); P |] ==> P" .
   373 
   374 lemma rmIH2: "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> P" .
   375   
   376 lemma rmIH3:
   377  "[| 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);  
   378      P |] ==>  
   379      P" .
   380 
   381 lemmas rmIHs = rmIH1 rmIH2 rmIH3
   382 
   383 
   384 subsection {* Lemmas for constructors and subtypes *}
   385 
   386 (* 0-ary constructors do not need additional rules as they are handled *)
   387 (*                                      correctly by applying SubtypeI *)
   388 
   389 lemma Subtype_canTs:
   390   "!!a b A B P. a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}"
   391   "!!a A B P. a : {x:A. P(inl(x))} ==> inl(a) : {x:A+B. P(x)}"
   392   "!!b A B P. b : {x:B. P(inr(x))} ==> inr(b) : {x:A+B. P(x)}"
   393   "!!a P. a : {x:Nat. P(succ(x))} ==> succ(a) : {x:Nat. P(x)}"
   394   "!!h t A P. h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"
   395   by (assumption | rule SubtypeI canTs icanTs | erule SubtypeE)+
   396 
   397 lemma letT: "[| f(t):B;  ~t=bot  |] ==> let x be t in f(x) : B"
   398   apply (erule letB [THEN ssubst])
   399   apply assumption
   400   done
   401 
   402 lemma applyT2: "[| a:A;  f : Pi(A,B)  |] ==> f ` a  : B(a)"
   403   apply (erule applyT)
   404   apply assumption
   405   done
   406 
   407 lemma rcall_lemma1: "[| a:A;  a:A ==> P(a) |] ==> a : {x:A. P(x)}"
   408   by blast
   409 
   410 lemma rcall_lemma2: "[| a:{x:A. Q(x)};  [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A. P(x)}"
   411   by blast
   412 
   413 lemmas rcall_lemmas = asm_rl rcall_lemma1 SubtypeD1 rcall_lemma2
   414 
   415 
   416 subsection {* Typechecking *}
   417 
   418 ML {*
   419 
   420 local
   421 
   422 val type_rls =
   423   @{thms canTs} @ @{thms icanTs} @ @{thms applyT2} @ @{thms ncanTs} @ @{thms incanTs} @
   424   @{thms precTs} @ @{thms letrecTs} @ @{thms letT} @ @{thms Subtype_canTs};
   425 
   426 fun bvars (Const("all",_) $ Abs(s,_,t)) l = bvars t (s::l)
   427   | bvars _ l = l
   428 
   429 fun get_bno l n (Const("all",_) $ Abs(s,_,t)) = get_bno (s::l) n t
   430   | get_bno l n (Const("Trueprop",_) $ t) = get_bno l n t
   431   | get_bno l n (Const("Ball",_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t
   432   | get_bno l n (Const("mem",_) $ t $ _) = get_bno l n t
   433   | get_bno l n (t $ s) = get_bno l n t
   434   | get_bno l n (Bound m) = (m-length(l),n)
   435 
   436 (* Not a great way of identifying induction hypothesis! *)
   437 fun could_IH x = Term.could_unify(x,hd (prems_of @{thm rcallT})) orelse
   438                  Term.could_unify(x,hd (prems_of @{thm rcall2T})) orelse
   439                  Term.could_unify(x,hd (prems_of @{thm rcall3T}))
   440 
   441 fun IHinst tac rls = SUBGOAL (fn (Bi,i) =>
   442   let val bvs = bvars Bi []
   443       val ihs = List.filter could_IH (Logic.strip_assums_hyp Bi)
   444       val rnames = map (fn x=>
   445                     let val (a,b) = get_bno [] 0 x
   446                     in (List.nth(bvs,a),b) end) ihs
   447       fun try_IHs [] = no_tac
   448         | try_IHs ((x,y)::xs) = tac [(("g", 0), x)] (List.nth(rls,y-1)) i ORELSE (try_IHs xs)
   449   in try_IHs rnames end)
   450 
   451 fun is_rigid_prog t =
   452      case (Logic.strip_assums_concl t) of
   453         (Const("Trueprop",_) $ (Const("mem",_) $ a $ _)) => null (Term.add_vars a [])
   454        | _ => false
   455 in
   456 
   457 fun rcall_tac ctxt i =
   458   let fun tac ps rl i = res_inst_tac ctxt ps rl i THEN atac i
   459   in IHinst tac @{thms rcallTs} i end
   460   THEN eresolve_tac @{thms rcall_lemmas} i
   461 
   462 fun raw_step_tac ctxt prems i = ares_tac (prems@type_rls) i ORELSE
   463                            rcall_tac ctxt i ORELSE
   464                            ematch_tac [@{thm SubtypeE}] i ORELSE
   465                            match_tac [@{thm SubtypeI}] i
   466 
   467 fun tc_step_tac ctxt prems = SUBGOAL (fn (Bi,i) =>
   468           if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac)
   469 
   470 fun typechk_tac ctxt rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls)) i
   471 
   472 fun tac ctxt = typechk_tac ctxt [] 1
   473 
   474 (*** Clean up Correctness Condictions ***)
   475 
   476 val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([@{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
   477                                  hyp_subst_tac)
   478 
   479 fun clean_ccs_tac ctxt =
   480   let fun tac ps rl i = eres_inst_tac ctxt ps rl i THEN atac i in
   481     TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE'
   482     eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
   483     hyp_subst_tac))
   484   end
   485 
   486 fun gen_ccs_tac ctxt rls i =
   487   SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls) THEN clean_ccs_tac ctxt) i
   488 
   489 end
   490 *}
   491 
   492 
   493 subsection {* Evaluation *}
   494 
   495 ML {*
   496 
   497 local
   498   structure Data = Named_Thms(val name = "eval" val description = "evaluation rules");
   499 in
   500 
   501 fun eval_tac ctxt ths =
   502   METAHYPS (fn prems =>
   503     DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get ctxt) 1)) 1;
   504 
   505 val eval_setup =
   506   Data.setup #>
   507   Method.setup @{binding eval}
   508     (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (CHANGED (eval_tac ctxt ths))))
   509     "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