src/LCF/ex/Ex3.thy
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 58977 9576b510f6a2
child 60770 240563fbf41d
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
     1 section {* Addition with fixpoint of successor *}
     2 
     3 theory Ex3
     4 imports "../LCF"
     5 begin
     6 
     7 axiomatization
     8   s     :: "'a \<Rightarrow> 'a" and
     9   p     :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    10 where
    11   p_strict:     "p(UU) = UU" and
    12   p_s:          "p(s(x),y) = s(p(x,y))"
    13 
    14 declare p_strict [simp] p_s [simp]
    15 
    16 lemma example: "p(FIX(s),y) = FIX(s)"
    17   apply (induct s)
    18   apply simp
    19   apply simp
    20   done
    21 
    22 end