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;
wenzelm@58889
     1
section {* Addition with fixpoint of successor *}
wenzelm@4905
     2
wenzelm@17248
     3
theory Ex3
wenzelm@58974
     4
imports "../LCF"
wenzelm@17248
     5
begin
wenzelm@4905
     6
wenzelm@47025
     7
axiomatization
wenzelm@58977
     8
  s     :: "'a \<Rightarrow> 'a" and
wenzelm@58977
     9
  p     :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
wenzelm@47025
    10
where
wenzelm@47025
    11
  p_strict:     "p(UU) = UU" and
wenzelm@17248
    12
  p_s:          "p(s(x),y) = s(p(x,y))"
wenzelm@17248
    13
wenzelm@19755
    14
declare p_strict [simp] p_s [simp]
wenzelm@19755
    15
wenzelm@19755
    16
lemma example: "p(FIX(s),y) = FIX(s)"
wenzelm@58973
    17
  apply (induct s)
wenzelm@47025
    18
  apply simp
wenzelm@47025
    19
  apply simp
wenzelm@19755
    20
  done
wenzelm@4905
    21
wenzelm@4905
    22
end