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