summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Tue, 05 Aug 1997 16:22:17 +0200 | |

changeset 3590 | 4d307341d0af |

parent 3589 | 244daa75f890 |

child 3591 | 412c62dd43de |

Added example mapf which requires a special congruence rule.

src/HOL/ex/Recdef.ML | file | annotate | diff | comparison | revisions | |

src/HOL/ex/Recdef.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/ex/Recdef.ML Tue Aug 05 16:21:45 1997 +0200 +++ b/src/HOL/ex/Recdef.ML Tue Aug 05 16:22:17 1997 +0200 @@ -33,3 +33,18 @@ by (ALLGOALS (asm_simp_tac (!simpset addsimps [g_terminates]))); qed "g_zero"; +(*** the contrived `mapf' ***) + +(* proving the termination condition: *) +val [tc] = mapf.tcs; +goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc)); +br allI 1; +by(case_tac "n=0" 1); +by(ALLGOALS Asm_simp_tac); +val lemma = result(); + +(* removing the termination condition from the generated thms: *) +val [mapf_0,mapf_Suc] = mapf.rules; +val mapf_Suc = lemma RS mapf_Suc; + +val mapf_induct = lemma RS mapf.induct;

--- a/src/HOL/ex/Recdef.thy Tue Aug 05 16:21:45 1997 +0200 +++ b/src/HOL/ex/Recdef.thy Tue Aug 05 16:22:17 1997 +0200 @@ -87,4 +87,16 @@ in fqsort(ord,less)@[x]@fqsort(ord,more))" +(* silly example which demonstrates the occasional need for additional + congruence rules (here: map_cong from List). If the congruence rule is + removed, an unprovable termination condition is generated! + Termination not proved automatically; see the ML file. + TFL requires (%x.mapf x) instead of mapf. +*) +consts mapf :: nat => nat list +recdef mapf "measure(%m.m)" +congs "[map_cong]" +"mapf 0 = []" +"mapf (Suc n) = concat(map (%x.mapf x) (replicate n n))" + end