Adapted to new inductive definition package.
authorberghofe
Wed Feb 07 18:11:27 2007 +0100 (2007-02-07)
changeset 2228326140713540b
parent 22282 71b4aefad227
child 22284 8d6d489f6ab3
Adapted to new inductive definition package.
src/HOL/ex/Primrec.thy
     1.1 --- a/src/HOL/ex/Primrec.thy	Wed Feb 07 18:10:21 2007 +0100
     1.2 +++ b/src/HOL/ex/Primrec.thy	Wed Feb 07 18:11:27 2007 +0100
     1.3 @@ -66,14 +66,13 @@
     1.4      | x # l' => nat_rec (f l') (\<lambda>y r. g (r # y # l')) x)"
     1.5    -- {* Note that @{term g} is applied first to @{term "PREC f g y"} and then to @{term y}! *}
     1.6  
     1.7 -consts PRIMREC :: "(nat list => nat) set"
     1.8 -inductive PRIMREC
     1.9 -  intros
    1.10 -    SC: "SC \<in> PRIMREC"
    1.11 -    CONSTANT: "CONSTANT k \<in> PRIMREC"
    1.12 -    PROJ: "PROJ i \<in> PRIMREC"
    1.13 -    COMP: "g \<in> PRIMREC ==> fs \<in> lists PRIMREC ==> COMP g fs \<in> PRIMREC"
    1.14 -    PREC: "f \<in> PRIMREC ==> g \<in> PRIMREC ==> PREC f g \<in> PRIMREC"
    1.15 +inductive2 PRIMREC :: "(nat list => nat) => bool"
    1.16 +  where
    1.17 +    SC: "PRIMREC SC"
    1.18 +  | CONSTANT: "PRIMREC (CONSTANT k)"
    1.19 +  | PROJ: "PRIMREC (PROJ i)"
    1.20 +  | COMP: "PRIMREC g ==> listsp PRIMREC fs ==> PRIMREC (COMP g fs)"
    1.21 +  | PREC: "PRIMREC f ==> PRIMREC g ==> PRIMREC (PREC f g)"
    1.22  
    1.23  
    1.24  text {* Useful special cases of evaluation *}
    1.25 @@ -273,9 +272,9 @@
    1.26  
    1.27  text {* @{term COMP} case *}
    1.28  
    1.29 -lemma COMP_map_aux: "fs \<in> lists (PRIMREC \<inter> {f. \<exists>kf. \<forall>l. f l < ack (kf, list_add l)})
    1.30 +lemma COMP_map_aux: "listsp (\<lambda>f. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack (kf, list_add l))) fs
    1.31    ==> \<exists>k. \<forall>l. list_add (map (\<lambda>f. f l) fs) < ack (k, list_add l)"
    1.32 -  apply (erule lists.induct)
    1.33 +  apply (erule listsp.induct)
    1.34    apply (rule_tac x = 0 in exI)
    1.35     apply simp
    1.36    apply safe
    1.37 @@ -286,10 +285,10 @@
    1.38  
    1.39  lemma COMP_case:
    1.40    "\<forall>l. g l < ack (kg, list_add l) ==>
    1.41 -  fs \<in> lists(PRIMREC Int {f. \<exists>kf. \<forall>l. f l < ack(kf, list_add l)})
    1.42 +  listsp (\<lambda>f. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack(kf, list_add l))) fs
    1.43    ==> \<exists>k. \<forall>l. COMP g fs  l < ack(k, list_add l)"
    1.44    apply (unfold COMP_def)
    1.45 -  apply (frule Int_lower1 [THEN lists_mono, THEN subsetD])
    1.46 +  apply (subgoal_tac "listsp PRIMREC fs")
    1.47      --{*Now, if meson tolerated map, we could finish with
    1.48    @{text "(drule COMP_map_aux, meson ack_less_mono2 ack_nest_bound less_trans)"} *}
    1.49    apply (erule COMP_map_aux [THEN exE])
    1.50 @@ -298,6 +297,7 @@
    1.51    apply (drule spec)+
    1.52    apply (erule less_trans)
    1.53    apply (blast intro: ack_less_mono2 ack_nest_bound less_trans)
    1.54 +  apply simp
    1.55    done
    1.56  
    1.57  
    1.58 @@ -338,12 +338,12 @@
    1.59     apply (blast intro: ack_add_bound2)+
    1.60    done
    1.61  
    1.62 -lemma ack_bounds_PRIMREC: "f \<in> PRIMREC ==> \<exists>k. \<forall>l. f l < ack (k, list_add l)"
    1.63 +lemma ack_bounds_PRIMREC: "PRIMREC f ==> \<exists>k. \<forall>l. f l < ack (k, list_add l)"
    1.64    apply (erule PRIMREC.induct)
    1.65        apply (blast intro: SC_case CONSTANT_case PROJ_case COMP_case PREC_case)+
    1.66    done
    1.67  
    1.68 -lemma ack_not_PRIMREC: "(\<lambda>l. case l of [] => 0 | x # l' => ack (x, x)) \<notin> PRIMREC"
    1.69 +lemma ack_not_PRIMREC: "\<not> PRIMREC (\<lambda>l. case l of [] => 0 | x # l' => ack (x, x))"
    1.70    apply (rule notI)
    1.71    apply (erule ack_bounds_PRIMREC [THEN exE])
    1.72    apply (rule less_irrefl)