equal
deleted
inserted
replaced
35 "height_trm (Var x) = 1" |
35 "height_trm (Var x) = 1" |
36 | "height_trm (App l r) = max (height_trm l) (height_trm r)" |
36 | "height_trm (App l r) = max (height_trm l) (height_trm r)" |
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 add: eqvt_def height_trm_height_bp_graph_aux_def) |
41 apply (rule, perm_simp, rule, rule TrueI) |
41 apply(rule TrueI) |
42 using [[simproc del: alpha_set]] |
42 using [[simproc del: alpha_set]] |
43 apply auto |
43 apply auto |
44 apply (case_tac x) |
44 apply (case_tac x) |
45 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]] |
46 using [[simproc del: alpha_set]] |