Got rid of listsp
authornipkow
Sun May 13 07:11:21 2007 +0200 (2007-05-13)
changeset 229441d471b8dec4e
parent 22943 0b928312ab94
child 22945 2863582c61b5
Got rid of listsp
src/HOL/ex/Primrec.thy
     1.1 --- a/src/HOL/ex/Primrec.thy	Sun May 13 04:38:24 2007 +0200
     1.2 +++ b/src/HOL/ex/Primrec.thy	Sun May 13 07:11:21 2007 +0200
     1.3 @@ -71,7 +71,7 @@
     1.4      SC: "PRIMREC SC"
     1.5    | CONSTANT: "PRIMREC (CONSTANT k)"
     1.6    | PROJ: "PRIMREC (PROJ i)"
     1.7 -  | COMP: "PRIMREC g ==> listsp PRIMREC fs ==> PRIMREC (COMP g fs)"
     1.8 +  | COMP: "PRIMREC g ==> \<forall>f \<in> set fs. PRIMREC f ==> PRIMREC (COMP g fs)"
     1.9    | PREC: "PRIMREC f ==> PRIMREC g ==> PRIMREC (PREC f g)"
    1.10  
    1.11  
    1.12 @@ -272,23 +272,20 @@
    1.13  
    1.14  text {* @{term COMP} case *}
    1.15  
    1.16 -lemma COMP_map_aux: "listsp (\<lambda>f. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack (kf, list_add l))) fs
    1.17 +lemma COMP_map_aux: "\<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack (kf, list_add l))
    1.18    ==> \<exists>k. \<forall>l. list_add (map (\<lambda>f. f l) fs) < ack (k, list_add l)"
    1.19 -  apply (erule listsp.induct)
    1.20 +  apply (induct fs)
    1.21    apply (rule_tac x = 0 in exI)
    1.22     apply simp
    1.23 -  apply safe
    1.24    apply simp
    1.25 -  apply (rule exI)
    1.26    apply (blast intro: add_less_mono ack_add_bound less_trans)
    1.27    done
    1.28  
    1.29  lemma COMP_case:
    1.30    "\<forall>l. g l < ack (kg, list_add l) ==>
    1.31 -  listsp (\<lambda>f. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack(kf, list_add l))) fs
    1.32 +  \<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack(kf, list_add l))
    1.33    ==> \<exists>k. \<forall>l. COMP g fs  l < ack(k, list_add l)"
    1.34    apply (unfold COMP_def)
    1.35 -  apply (subgoal_tac "listsp PRIMREC fs")
    1.36      --{*Now, if meson tolerated map, we could finish with
    1.37    @{text "(drule COMP_map_aux, meson ack_less_mono2 ack_nest_bound less_trans)"} *}
    1.38    apply (erule COMP_map_aux [THEN exE])
    1.39 @@ -297,7 +294,6 @@
    1.40    apply (drule spec)+
    1.41    apply (erule less_trans)
    1.42    apply (blast intro: ack_less_mono2 ack_nest_bound less_trans)
    1.43 -  apply simp
    1.44    done
    1.45  
    1.46