equal
deleted
inserted
replaced
40 term APP_raw |
40 term APP_raw |
41 term LET_raw |
41 term LET_raw |
42 term Test.BP_raw |
42 term Test.BP_raw |
43 thm bi_raw.simps |
43 thm bi_raw.simps |
44 thm permute_lam_raw_permute_bp_raw.simps |
44 thm permute_lam_raw_permute_bp_raw.simps |
45 thm alpha_lam_raw_alpha_bp_raw.intros[no_vars] |
45 thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros[no_vars] |
46 thm fv_lam_raw_fv_bp_raw.simps[no_vars] |
46 thm fv_lam_raw_fv_bp_raw.simps[no_vars] |
47 (*thm lam_bp_induct |
47 (*thm lam_bp_induct |
48 thm lam_bp_perm |
48 thm lam_bp_perm |
49 thm lam_bp_fv |
49 thm lam_bp_fv |
50 thm lam_bp_bn |
50 thm lam_bp_bn |
75 compat (PS x) pi (PS x') == pi o x = x' |
75 compat (PS x) pi (PS x') == pi o x = x' |
76 compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2' |
76 compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2' |
77 *) |
77 *) |
78 |
78 |
79 |
79 |
80 thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars] |
80 thm alpha_trm'_raw_alpha_pat'_raw_alpha_f_raw.intros[no_vars] |
81 thm fv_trm'_raw_fv_pat'_raw.simps[no_vars] |
81 thm fv_trm'_raw_fv_pat'_raw.simps[no_vars] |
82 thm f_raw.simps |
82 thm f_raw.simps |
83 (*thm trm'_pat'_induct |
83 (*thm trm'_pat'_induct |
84 thm trm'_pat'_perm |
84 thm trm'_pat'_perm |
85 thm trm'_pat'_fv |
85 thm trm'_pat'_fv |
165 compat (As x t) pi (As x' t') == pi o x = x' & alpha t t' |
165 compat (As x t) pi (As x' t') == pi o x = x' & alpha t t' |
166 *) |
166 *) |
167 |
167 |
168 |
168 |
169 thm fv_trm2_raw_fv_assign_raw.simps[no_vars] |
169 thm fv_trm2_raw_fv_assign_raw.simps[no_vars] |
170 thm alpha_trm2_raw_alpha_assign_raw.intros[no_vars] |
170 thm alpha_trm2_raw_alpha_assign_raw_alpha_bv2_raw.intros[no_vars] |
171 |
171 |
172 |
172 |
173 |
173 |
174 text {* example 3 from Terms.thy *} |
174 text {* example 3 from Terms.thy *} |
175 |
175 |
337 and Cbinders :: "spec \<Rightarrow> atom set" |
337 and Cbinders :: "spec \<Rightarrow> atom set" |
338 where |
338 where |
339 "cbinders (Type t T) = {atom t}" |
339 "cbinders (Type t T) = {atom t}" |
340 | "cbinders (Dty t) = {atom t}" |
340 | "cbinders (Dty t) = {atom t}" |
341 | "cbinders (DStru x s) = {atom x}" |
341 | "cbinders (DStru x s) = {atom x}" |
342 | "cbinders (Val v M) = {atom v}"*) |
342 | "cbinders (Val v M) = {atom v}" |
343 | "Cbinders (Type1 t) = {atom t}" |
343 | "Cbinders (Type1 t) = {atom t}" |
344 | "Cbinders (Type2 t T) = {atom t}" |
344 | "Cbinders (Type2 t T) = {atom t}" |
345 | "Cbinders (SStru x S) = {atom x}" |
345 | "Cbinders (SStru x S) = {atom x}" |
346 | "Cbinders (SVal v T) = {atom v}" |
346 | "Cbinders (SVal v T) = {atom v}" |
347 |
347 |
348 |
348 |
349 (* core haskell *) |
349 (* core haskell *) |
350 print_theorems |
350 print_theorems |
351 |
351 |
422 (* example 3 from Peter Sewell's bestiary *) |
422 (* example 3 from Peter Sewell's bestiary *) |
423 nominal_datatype exp = |
423 nominal_datatype exp = |
424 VarP "name" |
424 VarP "name" |
425 | AppP "exp" "exp" |
425 | AppP "exp" "exp" |
426 | LamP x::"name" e::"exp" bind x in e |
426 | LamP x::"name" e::"exp" bind x in e |
427 | LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1 |
427 | LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp' p" in e1 |
428 and pat3 = |
428 and pat3 = |
429 PVar "name" |
429 PVar "name" |
430 | PUnit |
430 | PUnit |
431 | PPair "pat3" "pat3" |
431 | PPair "pat3" "pat3" |
432 binder |
432 binder |
433 bp :: "pat3 \<Rightarrow> atom set" |
433 bp' :: "pat3 \<Rightarrow> atom set" |
434 where |
434 where |
435 "bp (PVar x) = {atom x}" |
435 "bp' (PVar x) = {atom x}" |
436 | "bp (PUnit) = {}" |
436 | "bp' (PUnit) = {}" |
437 | "bp (PPair p1 p2) = bp p1 \<union> bp p2" |
437 | "bp' (PPair p1 p2) = bp' p1 \<union> bp' p2" |
438 thm alpha_exp_raw_alpha_pat3_raw.intros |
438 thm alpha_exp_raw_alpha_pat3_raw_alpha_bp'_raw.intros |
439 |
439 |
440 (* example 6 from Peter Sewell's bestiary *) |
440 (* example 6 from Peter Sewell's bestiary *) |
441 nominal_datatype exp6 = |
441 nominal_datatype exp6 = |
442 EVar name |
442 EVar name |
443 | EPair exp6 exp6 |
443 | EPair exp6 exp6 |
450 bp6 :: "pat6 \<Rightarrow> atom set" |
450 bp6 :: "pat6 \<Rightarrow> atom set" |
451 where |
451 where |
452 "bp6 (PVar' x) = {atom x}" |
452 "bp6 (PVar' x) = {atom x}" |
453 | "bp6 (PUnit') = {}" |
453 | "bp6 (PUnit') = {}" |
454 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2" |
454 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2" |
455 thm alpha_exp6_raw_alpha_pat6_raw.intros |
455 thm alpha_exp6_raw_alpha_pat6_raw_alpha_bp6_raw.intros |
456 |
456 |
457 (* example 7 from Peter Sewell's bestiary *) |
457 (* example 7 from Peter Sewell's bestiary *) |
458 nominal_datatype exp7 = |
458 nominal_datatype exp7 = |
459 EVar name |
459 EVar name |
460 | EUnit |
460 | EUnit |