Up to index of Isabelle/HOL/sHowe
theory BiAbstr = Abstr(*
File: Abstr.thy
Author: Simon Ambler (sja4@mcs.le.ac.uk)
Copyright: Leicester University, 2001.
Time-stamp: <2002-01-09 11:24:41 sja4>
Abstraction of two variables
*)
BiAbstr = Abstr +
consts
biAbstSet :: "(bnd * ('a expr => 'a expr => 'a expr)) set"
syntax
biAbst :: "[bnd, 'a expr => 'a expr => 'a expr] => bool"
translations
"biAbst i e" == "(i, e) : biAbstSet"
constdefs
biAbstr :: "('a expr => 'a expr => 'a expr) => bool"
"biAbstr == % e. biAbst 0 e"
biOrdinary :: "('a expr => 'a expr => 'a expr) => bool"
"biOrdinary == % e. (? a. e = (% x y. CON a)) \
\ | ( e = (% x y. x)) \
\ | ( e = (% x y. y)) \
\ | (? n. e = (% x y. VAR n)) \
\ | (? j. e = (% x y. BND j)) \
\ | (? f g. e = (% x y. f x y $$ g x y)) \
\ | (? f. e = (% x y. ABS (f x y)))"
biRank :: "('a expr => 'a expr => 'a expr) => nat"
"biRank == % e. size (e (VAR 0) (VAR 0))"
biSubst :: "['a expr => 'a expr, var, 'a expr] => ('a expr => 'a expr)"
"biSubst == % e n. @ f. biAbstr f & newFor n (f dflt dflt) \
\ & f (VAR n) = e"
inductive biAbstSet
intrs
biAbst_CON "biAbst i (% x y. CON a)"
biAbst_pr1 "biAbst i (% x y. x)"
biAbst_pr2 "biAbst i (% x y. y)"
biAbst_VAR "biAbst i (% x y. VAR n)"
biAbst_BND "j < i ==> biAbst i (% x y. BND j)"
biAbst_APP "[| biAbst i e; biAbst i f |] \
\ ==> biAbst i (% x y. e x y $$ f x y)"
biAbst_ABS "biAbst (Suc i) e ==> biAbst i (% x y. ABS (e x y))"
end
theorem abstr_APP_E:
[| abstr (%x. e x $$ f x); [| abstr e; abstr f |] ==> P |] ==> P
theorem abstr_BND_E:
abstr (%x. BND j) ==> P
theorem abst_ordinary:
abst i e ==> ordinary e
theorem abstr_ordinary:
abstr e ==> ordinary e
theorem insts_inst:
insts i [s] t = inst i s t
theorem ABS_LAM_insts:
abst 1 f ==> (%x. ABS (f x)) = (%x. LAM y. insts 0 [y, x] (lbind 1 f))
theorem rank_inst:
abst i e ==> rank (%x. inst j (VAR n) (e x)) = rank e
theorem rank_insts1:
level i s ==> rank (%x. insts j [VAR n, x] s) = size s
theorem rank_insts2:
level i s ==> rank (%x. insts j [x, VAR n] s) = size s
theorem level_abst_insts1:
level (Suc (Suc j)) s ==> abst j (%x. insts j [VAR n, x] s)
theorem level_abst_insts2:
level (Suc (Suc j)) s ==> abst j (%x. insts j [x, VAR n] s)
theorem size_lbind:
abst i e ==> size (lbind j e) = rank e
theorem biAbst_swap:
biAbst j e ==> biAbst j (%x y. e y x)
theorem biAbstr_swap:
biAbstr f ==> biAbstr (%x y. f y x)
theorem biAbst_proper_abst:
[| biAbst i e; proper s |] ==> abst i (e s)
theorem biAbstr_proper_abstr1:
[| biAbstr e; proper s |] ==> abstr (e s)
theorem biAbstr_proper_abstr2:
[| biAbstr e; proper s |] ==> abstr (%x. e x s)
theorem biAbstr_abstr_LAM1:
biAbstr f ==> abstr (%x. LAM y. f x y)
theorem biAbstr_abstr_LAM2:
biAbstr f ==> abstr (%y. LAM x. f x y)
theorem level_biAbst_insts:
level (Suc (Suc j)) s ==> biAbst j (%x y. insts j [x, y] s)
theorem abstr_VAR_induct:
[| abstr e; !!a. P (%x. CON a); !!j. P (%x. VAR j); P (%x. x);
!!f g. [| abstr f; P f; abstr g; P g |] ==> P (%x. f x $$ g x);
!!f. [| biAbstr f; ALL n. P (%x. f x (VAR n)); ALL n. P (f (VAR n)) |]
==> P (%x. LAM y. f x y) |]
==> P e
theorem abstrE:
[| abstr e; !!a. e = (%x. CON a) ==> P; e = (%x. x) ==> P;
!!n. e = (%x. VAR n) ==> P;
!!f g. [| e = (%x. f x $$ g x); abstr f; abstr g |] ==> P;
!!f. [| e = (%x. LAM y. f x y); biAbstr f |] ==> P |]
==> P
theorem biRank_APP1:
biRank f < biRank (%x y. f x y $$ g x y)
theorem biRank_APP2:
biRank g < biRank (%x y. f x y $$ g x y)
theorem biRank_ABS:
biRank e < biRank (%x y. ABS (e x y))
theorem biAbstraction_induct:
[| !!a. P (%x y. CON a); !!j. P (%x y. VAR j); P (%x y. x); P (%x y. y);
!!j. P (%x y. BND j); !!f g. [| P f; P g |] ==> P (%x y. f x y $$ g x y);
!!f. P f ==> P (%x y. ABS (f x y)); !!f. ¬ biOrdinary f ==> P f |]
==> P e
theorem proj1_neq_const:
(%x y. x) ~= (%x y. s)
theorem proj2_neq_const:
(%x y. y) ~= (%x y. s)
theorem proj1_neq_proj2:
(%x y. x) ~= (%x y. y)
theorem proj1_neq_APP:
(%x y. x) ~= (%x y. f x y $$ g x y)
theorem proj2_neq_APP:
(%x y. y) ~= (%x y. f x y $$ g x y)
theorem proj1_neq_ABS:
(%x y. x) ~= (%x y. ABS (e x y))
theorem proj2_neq_ABS:
(%x y. y) ~= (%x y. ABS (e x y))
theorem biAbstr_extensionality:
[| biAbstr f; biAbstr g; newFor n (f dflt dflt); newFor n (g dflt dflt);
f (VAR n) = g (VAR n) |]
==> f = g
theorem biAbstr_biSubst:
[| f (VAR n) = e; biAbstr f; newFor n (f dflt dflt) |] ==> biSubst e n = f
theorem abstr_biSubst_lemma:
abstr e ==> EX f. biAbstr f & newFor n (f dflt dflt) & f (VAR n) = e
theorem abstr_biAbstr_biSubst:
abstr e ==> biAbstr (biSubst e n)
theorem abstr_biSubst_id:
abstr e ==> biSubst e n (VAR n) = e
theorem abstr_newFor_biSubst:
abstr e ==> newFor n (biSubst e n dflt dflt)
theorem subst_LAM:
abstr e ==> subst (LAM y. e y) n = (%x. LAM y. biSubst e n x y)
theorem biAbst_abst_compose:
[| biAbst i f; abst i e |] ==> abst i (%x. f x (e x))
theorem biAbstr_abstr_compose:
[| biAbstr f; abstr e |] ==> abstr (%x. f x (e x))
theorem biAbstr_newFor_apply:
[| biAbstr f; proper s; proper t; newFor n s; newFor n t;
newFor n (f dflt dflt) |]
==> newFor n (f s t)
theorem biSubst_subst_simp:
[| abstr e; proper u; proper t |] ==> biSubst e n u (subst t n u) = subst (e t) n u