src/HOL/HOLCF/ex/Letrec.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45788 9049b24959de
child 58880 0baae4311a9f
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 41479
diff changeset
     1
(*  Title:      HOL/HOLCF/ex/Letrec.thy
35932
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
     3
*)
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
     4
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
     5
header {* Recursive let bindings *}
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
     6
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
     7
theory Letrec
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
     8
imports HOLCF
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
     9
begin
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    10
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    11
definition
45788
9049b24959de HOLCF/ex/Letrec.thy: keep class 'domain' as default sort
huffman
parents: 42151
diff changeset
    12
  CLetrec :: "('a::pcpo \<rightarrow> 'a \<times> 'b::pcpo) \<rightarrow> 'b" where
35932
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    13
  "CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))"
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    14
41229
d797baa3d57c replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents: 40774
diff changeset
    15
nonterminal recbinds and recbindt and recbind
35932
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    16
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    17
syntax
41479
655f583840d0 use proper syntactic types for 'syntax' commands
huffman
parents: 41229
diff changeset
    18
  "_recbind"  :: "[logic, logic] \<Rightarrow> recbind"         ("(2_ =/ _)" 10)
35932
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    19
  ""          :: "recbind \<Rightarrow> recbindt"               ("_")
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    20
  "_recbindt" :: "[recbind, recbindt] \<Rightarrow> recbindt"   ("_,/ _")
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    21
  ""          :: "recbindt \<Rightarrow> recbinds"              ("_")
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    22
  "_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds"  ("_;/ _")
41479
655f583840d0 use proper syntactic types for 'syntax' commands
huffman
parents: 41229
diff changeset
    23
  "_Letrec"   :: "[recbinds, logic] \<Rightarrow> logic"        ("(Letrec (_)/ in (_))" 10)
35932
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    24
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    25
translations
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    26
  (recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)"
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    27
  (recbindt) "x = a, y = b"          == (recbindt) "(x,y) = (a,b)"
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    28
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    29
translations
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    30
  "_Letrec (_recbinds b bs) e" == "_Letrec b (_Letrec bs e)"
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    31
  "Letrec xs = a in (e,es)"    == "CONST CLetrec\<cdot>(\<Lambda> xs. (a,e,es))"
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    32
  "Letrec xs = a in e"         == "CONST CLetrec\<cdot>(\<Lambda> xs. (a,e))"
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    33
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
diff changeset
    34
end