src/HOL/Product_Type.thy
 changeset 14359 3d9948163018 parent 14337 e13731554e50 child 14565 c6dc17aab88a
equal inserted replaced
14358:233c5bd5b539 14359:3d9948163018
`   125   (* The last rule accommodates tuples in `case C ... (x,y) ... => ...'`
`   125   (* The last rule accommodates tuples in `case C ... (x,y) ... => ...'`
`   126      The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)`
`   126      The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)`
`   127 `
`   127 `
`   128   "SIGMA x:A. B" => "Sigma A (%x. B)"`
`   128   "SIGMA x:A. B" => "Sigma A (%x. B)"`
`   129   "A <*> B"      => "Sigma A (_K B)"`
`   129   "A <*> B"      => "Sigma A (_K B)"`
`       `
`   130 `
`       `
`   131 (* reconstructs pattern from (nested) splits, avoiding eta-contraction of body*)`
`       `
`   132 (* works best with enclosing "let", if "let" does not avoid eta-contraction   *)`
`       `
`   133 print_translation {*`
`       `
`   134 let fun split_tr' [Abs (x,T,t as (Abs abs))] =`
`       `
`   135       (* split (%x y. t) => %(x,y) t *)`
`       `
`   136       let val (y,t') = atomic_abs_tr' abs;`
`       `
`   137           val (x',t'') = atomic_abs_tr' (x,T,t');`
`       `
`   138     `
`       `
`   139       in Syntax.const "_abs" \$ (Syntax.const "_pattern" \$x'\$y) \$ t'' end`
`       `
`   140     | split_tr' [Abs (x,T,(s as Const ("split",_)\$t))] =`
`       `
`   141        (* split (%x. (split (%y z. t))) => %(x,y,z). t *)`
`       `
`   142        let val (Const ("_abs",_)\$(Const ("_pattern",_)\$y\$z)\$t') = split_tr' [t];`
`       `
`   143            val (x',t'') = atomic_abs_tr' (x,T,t');`
`       `
`   144        in Syntax.const "_abs"\$ `
`       `
`   145            (Syntax.const "_pattern"\$x'\$(Syntax.const "_patterns"\$y\$z))\$t'' end`
`       `
`   146     | split_tr' [Const ("split",_)\$t] =`
`       `
`   147        (* split (split (%x y z. t)) => %((x,y),z). t *)   `
`       `
`   148        split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)`
`       `
`   149     | split_tr' [Const ("_abs",_)\$x_y\$(Abs abs)] =`
`       `
`   150        (* split (%pttrn z. t) => %(pttrn,z). t *)`
`       `
`   151        let val (z,t) = atomic_abs_tr' abs;`
`       `
`   152        in Syntax.const "_abs" \$ (Syntax.const "_pattern" \$x_y\$z) \$ t end`
`       `
`   153     | split_tr' _ =  raise Match;`
`       `
`   154 in [("split", split_tr')]`
`       `
`   155 end`
`       `
`   156 *}`
`   130 `
`   157 `
`   131 syntax (xsymbols)`
`   158 syntax (xsymbols)`
`   132   "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)`
`   159   "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)`
`   133   "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)`
`   160   "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)`
`   134 `
`   161 `