<commit_before>(*  Title:      Cube/cube.thy
    ID:         $Id$
    Author:     <NAME>
    Copyright   1993  University of Cambridge

Barendregt's Lambda-Cube
*)

Cube = Pure +

types
  term, context, typing 0

arities
  term :: logic

consts
  Abs, Prod     :: "[term, term => term] => term"
  Trueprop      :: "[context, typing] => prop"          ("(_/ |- _)")
  Trueprop1     :: "typing => prop"                     ("(_)")
  MT_context    :: "context"                            ("")
  ""            :: "id => context"                      ("_ ")
  ""            :: "var => context"                     ("_ ")
  Context       :: "[typing, context] => context"       ("_ _")
  star          :: "term"                               ("*")
  box           :: "term"                               ("[]")
  "^"           :: "[term, term] => term"               (infixl 20)
  Lam           :: "[id, term, term] => term"           ("(3Lam _:_./ _)" [0, 0, 0] 10)
  Pi            :: "[id, term, term] => term"           ("(3Pi _:_./ _)" [0, 0] 10)
  "->"          :: "[term, term] => term"               (infixr 10)
  Has_type      :: "[term, term] => typing"             ("(_:/ _)" [0, 0] 5)

translations
  (prop) "x:X"  == (prop) "|- x:X"
  "Lam x:A. B"  == "Abs(A, %x. B)"
  "Pi x:A. B"   => "Prod(A, %x. B)"

rules
  s_b           "*: []"

  strip_s       "[| A:*;  a:A ==> G |- x:X |] ==> a:A G |- x:X"
  strip_b       "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X"

  app           "[| F:Prod(A, B); C:A |] ==> F^C: B(C)"

  pi_ss         "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*"

  lam_ss        "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \
\                   ==> Abs(A, f) : Prod(A, B)"

  beta          "Abs(A, f)^a == f(a)"

end


ML

val parse_translation = [("op ->", ndependent_tr "Prod")];<commit_msg>replaced id by idt; added parse rule for ->; removed ndependent_tr;<commit_after>(*  Title:      Cube/cube.thy
    ID:         $Id$
    Author:     <NAME>
    Copyright   1993  University of Cambridge

Barendregt's Lambda-Cube
*)

Cube = Pure +

types
  term, context, typing 0

arities
  term :: logic

consts
  Abs, Prod     :: "[term, term => term] => term"
  Trueprop      :: "[context, typing] => prop"          ("(_/ |- _)")
  Trueprop1     :: "typing => prop"                     ("(_)")
  MT_context    :: "context"                            ("")
  ""            :: "id => context"                      ("_ ")
  ""            :: "var => context"                     ("_ ")
  Context       :: "[typing, context] => context"       ("_ _")
  star          :: "term"                               ("*")
  box           :: "term"                               ("[]")
  "^"           :: "[term, term] => term"               (infixl 20)
  Lam           :: "[idt, term, term] => term"          ("(3Lam _:_./ _)" [0, 0, 0] 10)
  Pi            :: "[idt, term, term] => term"          ("(3Pi _:_./ _)" [0, 0] 10)
  "->"          :: "[term, term] => term"               (infixr 10)
  Has_type      :: "[term, term] => typing"             ("(_:/ _)" [0, 0] 5)

translations
  (prop) "x:X"  == (prop) "|- x:X"
  "Lam x:A. B"  == "Abs(A, %x. B)"
  "Pi x:A. B"   => "Prod(A, %x. B)"
  "A -> B"      => "Prod(A, _K(B))"

rules
  s_b           "*: []"

  strip_s       "[| A:*;  a:A ==> G |- x:X |] ==> a:A G |- x:X"
  strip_b       "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X"

  app           "[| F:Prod(A, B); C:A |] ==> F^C: B(C)"

  pi_ss         "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*"

  lam_ss        "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \
\                   ==> Abs(A, f) : Prod(A, B)"

  beta          "Abs(A, f)^a == f(a)"

end


ML

{'fraction_non_alphanumeric': 0.23454790823211877, 'fraction_numerical': 0.012955465587044534, 'mean_word_length': 1.3396464646464648, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 57, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6768817', 'n_tokens_mistral': 1483, 'n_tokens_neox': 1428, 'n_words': 325}