# HG changeset patch # User berghofe # Date 1170868287 -3600 # Node ID 26140713540b69e9f05b096815caef12791fdbbf # Parent 71b4aefad2274c58e9af903da0848fc484cd13a8 Adapted to new inductive definition package. diff -r 71b4aefad227 -r 26140713540b src/HOL/ex/Primrec.thy --- a/src/HOL/ex/Primrec.thy Wed Feb 07 18:10:21 2007 +0100 +++ b/src/HOL/ex/Primrec.thy Wed Feb 07 18:11:27 2007 +0100 @@ -66,14 +66,13 @@ | x # l' => nat_rec (f l') (\y r. g (r # y # l')) x)" -- {* Note that @{term g} is applied first to @{term "PREC f g y"} and then to @{term y}! *} -consts PRIMREC :: "(nat list => nat) set" -inductive PRIMREC - intros - SC: "SC \ PRIMREC" - CONSTANT: "CONSTANT k \ PRIMREC" - PROJ: "PROJ i \ PRIMREC" - COMP: "g \ PRIMREC ==> fs \ lists PRIMREC ==> COMP g fs \ PRIMREC" - PREC: "f \ PRIMREC ==> g \ PRIMREC ==> PREC f g \ PRIMREC" +inductive2 PRIMREC :: "(nat list => nat) => bool" + where + SC: "PRIMREC SC" + | CONSTANT: "PRIMREC (CONSTANT k)" + | PROJ: "PRIMREC (PROJ i)" + | COMP: "PRIMREC g ==> listsp PRIMREC fs ==> PRIMREC (COMP g fs)" + | PREC: "PRIMREC f ==> PRIMREC g ==> PRIMREC (PREC f g)" text {* Useful special cases of evaluation *} @@ -273,9 +272,9 @@ text {* @{term COMP} case *} -lemma COMP_map_aux: "fs \ lists (PRIMREC \ {f. \kf. \l. f l < ack (kf, list_add l)}) +lemma COMP_map_aux: "listsp (\f. PRIMREC f \ (\kf. \l. f l < ack (kf, list_add l))) fs ==> \k. \l. list_add (map (\f. f l) fs) < ack (k, list_add l)" - apply (erule lists.induct) + apply (erule listsp.induct) apply (rule_tac x = 0 in exI) apply simp apply safe @@ -286,10 +285,10 @@ lemma COMP_case: "\l. g l < ack (kg, list_add l) ==> - fs \ lists(PRIMREC Int {f. \kf. \l. f l < ack(kf, list_add l)}) + listsp (\f. PRIMREC f \ (\kf. \l. f l < ack(kf, list_add l))) fs ==> \k. \l. COMP g fs l < ack(k, list_add l)" apply (unfold COMP_def) - apply (frule Int_lower1 [THEN lists_mono, THEN subsetD]) + apply (subgoal_tac "listsp PRIMREC fs") --{*Now, if meson tolerated map, we could finish with @{text "(drule COMP_map_aux, meson ack_less_mono2 ack_nest_bound less_trans)"} *} apply (erule COMP_map_aux [THEN exE]) @@ -298,6 +297,7 @@ apply (drule spec)+ apply (erule less_trans) apply (blast intro: ack_less_mono2 ack_nest_bound less_trans) + apply simp done @@ -338,12 +338,12 @@ apply (blast intro: ack_add_bound2)+ done -lemma ack_bounds_PRIMREC: "f \ PRIMREC ==> \k. \l. f l < ack (k, list_add l)" +lemma ack_bounds_PRIMREC: "PRIMREC f ==> \k. \l. f l < ack (k, list_add l)" apply (erule PRIMREC.induct) apply (blast intro: SC_case CONSTANT_case PROJ_case COMP_case PREC_case)+ done -lemma ack_not_PRIMREC: "(\l. case l of [] => 0 | x # l' => ack (x, x)) \ PRIMREC" +lemma ack_not_PRIMREC: "\ PRIMREC (\l. case l of [] => 0 | x # l' => ack (x, x))" apply (rule notI) apply (erule ack_bounds_PRIMREC [THEN exE]) apply (rule less_irrefl)