equal
deleted
inserted
replaced
37 | "height_trm (Lam v b) = 1 + (height_trm b)" |
37 | "height_trm (Lam v b) = 1 + (height_trm b)" |
38 | "height_trm (Let_Rec bp b) = max (height_bp bp) (height_trm b)" |
38 | "height_trm (Let_Rec bp b) = max (height_bp bp) (height_trm b)" |
39 | "height_bp (Bp v t) = height_trm t" |
39 | "height_bp (Bp v t) = height_trm t" |
40 apply (simp only: eqvt_def height_trm_height_bp_graph_def) |
40 apply (simp only: eqvt_def height_trm_height_bp_graph_def) |
41 apply (rule, perm_simp, rule, rule TrueI) |
41 apply (rule, perm_simp, rule, rule TrueI) |
|
42 using [[simproc del: alpha_set]] |
42 apply auto |
43 apply auto |
43 apply (case_tac x) |
44 apply (case_tac x) |
44 apply (case_tac a rule: let_rec.exhaust(1)) |
45 apply (case_tac a rule: let_rec.exhaust(1)) |
|
46 using [[simproc del: alpha_set]] |
45 apply auto |
47 apply auto |
46 apply (case_tac b rule: let_rec.exhaust(2)) |
48 apply (case_tac b rule: let_rec.exhaust(2)) |
47 apply blast |
49 apply blast |
48 apply (erule Abs_set_fcb) |
50 apply (erule Abs_set_fcb) |
49 apply (simp_all add: pure_fresh)[2] |
51 apply (simp_all add: pure_fresh)[2] |